{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,23]],"date-time":"2026-09-23T17:13:18Z","timestamp":1790183598628,"version":"4.1.0"},"publisher-location":"Cham","reference-count":60,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031711619","type":"print"},{"value":"9783031711626","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T00:00:00Z","timestamp":1726012800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We study the problem of certifying the robustness of Bayesian neural networks (BNNs) to adversarial input perturbations. Specifically, we define two notions of robustness for BNNs in an adversarial setting: probabilistic robustness and decision robustness. The former deals with the probabilistic behaviour of the network, that is, it ensures robustness across different stochastic realisations of the network, while the latter provides guarantees for the overall (output) decision of the BNN. Although these robustness properties cannot be computed analytically, we present a unified computational framework for efficiently and formally bounding them. Our approach is based on weight interval sampling, integration and bound propagation techniques, and can be applied to BNNs with a large number of parameters independently of the (approximate) inference method employed to train the BNN. We evaluate the effectiveness of our method on tasks including airborne collision avoidance, medical imaging and autonomous driving, demonstrating that it can compute non-trivial guarantees on medium size images (i.e., over 16 thousand input parameters).<\/jats:p>","DOI":"10.1007\/978-3-031-71162-6_1","type":"book-chapter","created":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:02:27Z","timestamp":1725933747000},"page":"3-28","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Adversarial Robustness Certification for\u00a0Bayesian Neural Networks"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0779-3114","authenticated-orcid":false,"given":"Matthew","family":"Wicker","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0492-4860","authenticated-orcid":false,"given":"Andrea","family":"Patane","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1190-6097","authenticated-orcid":false,"given":"Luca","family":"Laurenti","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9022-7599","authenticated-orcid":false,"given":"Marta","family":"Kwiatkowska","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,9,11]]},"reference":[{"key":"1_CR1","unstructured":"Adams, S., Patane, A., Lahijanian, M., Laurenti, L.: BNN-DP: robustness certification of Bayesian neural networks via dynamic programming. In: ICML, pp. 133\u2013151. PMLR (2023)"},{"issue":"1","key":"1_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1038\/s41746-021-00438-z","volume":"4","author":"R Aggarwal","year":"2021","unstructured":"Aggarwal, R., et al.: Diagnostic accuracy of deep learning in medical imaging: a systematic review and meta-analysis. NPJ Digit. Med. 4(1), 1\u201323 (2021)","journal-title":"NPJ Digit. Med."},{"key":"1_CR3","unstructured":"Batten, B., Hosseini, M., Lomuscio, A.: Tight verification of probabilistic robustness in Bayesian neural networks. In: AISTATS (2024)"},{"key":"1_CR4","unstructured":"Bekasov, A., Murray, I.: Bayesian adversarial spheres: Bayesian inference and adversarial examples in a noiseless setting. arXiv preprint arXiv:1811.12335 (2018)"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Benussi, E., Patane, A., Wicker, M., Laurenti, L., Kwiatkowska, M.: Individual fairness guarantees for neural networks. In: IJCAI (2022)","DOI":"10.24963\/ijcai.2022\/92"},{"key":"1_CR6","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-4286-2","volume-title":"Statistical Decision Theory and Bayesian Analysis","author":"JO Berger","year":"2013","unstructured":"Berger, J.O.: Statistical Decision Theory and Bayesian Analysis. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-1-4757-4286-2"},{"key":"1_CR7","unstructured":"Berrada, L., et al.: Make sure you\u2019re unsure: a framework for verifying probabilistic specifications. In: NeurIPS, vol.\u00a034 (2021)"},{"key":"1_CR8","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1016\/j.patcog.2018.07.023","volume":"84","author":"B Biggio","year":"2018","unstructured":"Biggio, B., Roli, F.: Wild patterns: ten years after the rise of adversarial machine learning. Pattern Recogn. 84, 317\u2013331 (2018)","journal-title":"Pattern Recogn."},{"key":"1_CR9","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780198538493.001.0001","volume-title":"Neural Networks for Pattern Recognition","author":"C Bishop","year":"1995","unstructured":"Bishop, C.: Neural Networks for Pattern Recognition. Oxford University Press, Oxford (1995)"},{"key":"1_CR10","unstructured":"Blundell, C., Cornebise, J., Kavukcuoglu, K., Wierstra, D.: Weight uncertainty in neural networks. In: ICML (2015)"},{"key":"1_CR11","unstructured":"Carbone, G., Wicker, M., Laurenti, L., Patane, A., Bortolussi, L., Sanguinetti, G.: Robustness of Bayesian neural networks to gradient-based attacks. In: NeurIPS, vol.\u00a033, pp. 15602\u201315613 (2020)"},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"Cardelli, L., Kwiatkowska, M., Laurenti, L., Paoletti, N., Patane, A., Wicker, M.: Statistical guarantees for the robustness of Bayesian neural networks. In: IJCAI (2019)","DOI":"10.24963\/ijcai.2019\/789"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Cardelli, L., Kwiatkowska, M., Laurenti, L., Patane, A.: Robustness guarantees for Bayesian inference with Gaussian processes. In: AAAI (2018)","DOI":"10.1609\/aaai.v33i01.33017759"},{"issue":"11","key":"1_CR14","doi-asserted-by":"publisher","first-page":"2939","DOI":"10.1109\/TCOMM.2011.072011.100049","volume":"59","author":"SH Chang","year":"2011","unstructured":"Chang, S.H., Cosman, P.C., Milstein, L.B.: Chernoff-type bounds for the Gaussian error function. IEEE Trans. Commun. 59(11), 2939\u20132944 (2011)","journal-title":"IEEE Trans. Commun."},{"issue":"6","key":"1_CR15","doi-asserted-by":"publisher","first-page":"3234","DOI":"10.1109\/TITS.2020.2993926","volume":"22","author":"L Chen","year":"2021","unstructured":"Chen, L., et al.: Deep neural network based vehicle and pedestrian detection for autonomous driving: a survey. IEEE Trans. Intell. Transp. Syst. 22(6), 3234\u20133246 (2021)","journal-title":"IEEE Trans. Intell. Transp. Syst."},{"key":"1_CR16","unstructured":"De\u00a0Palma, G., Kiani, B., Lloyd, S.: Adversarial robustness guarantees for random deep neural networks. In: ICML, pp. 2522\u20132534. PMLR (2021)"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Deng, J., Dong, W., Socher, R., Li, L.J., Li, K., Fei-Fei, L.: Imagenet: a large-scale hierarchical image database. In: CVPR, pp. 248\u2013255 (2009)","DOI":"10.1109\/CVPR.2009.5206848"},{"key":"1_CR18","unstructured":"Doherty, A., Wicker, M., Laurenti, L., Patane, A.: Individual fairness in Bayesian neural networks. arXiv preprint arXiv:2304.10828 (2023)"},{"key":"1_CR19","unstructured":"Dvijotham, K., Garnelo, M., Fawzi, A., Kohli, P.: Verification of deep probabilistic models. arXiv preprint arXiv:1812.02795 (2018)"},{"key":"1_CR20","doi-asserted-by":"crossref","unstructured":"Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, P., Chaudhuri, S., Vechev, M.: Ai2: safety and robustness certification of neural networks with abstract interpretation. In: 2018 IEEE S &P, pp. 3\u201318. IEEE (2018)","DOI":"10.1109\/SP.2018.00058"},{"key":"1_CR21","unstructured":"Goodfellow, I., Bengio, Y., Courville, A.: Deep Learning. MIT Press, Cambridge (2016)"},{"key":"1_CR22","unstructured":"Goodfellow, I.J., Shlens, J., Szegedy, C.: Explaining and harnessing adversarial examples. arXiv preprint arXiv:1412.6572 (2014)"},{"key":"1_CR23","unstructured":"Gowal, S., et al.: On the effectiveness of interval bound propagation for training verifiably robust models. In: SecML 2018 (2018)"},{"key":"1_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-63387-9_1","volume-title":"Computer Aided Verification","author":"X Huang","year":"2017","unstructured":"Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 3\u201329. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_1"},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"Julian, K.D., Kochenderfer, M.J.: Guaranteeing safety for neural network-based aircraft collision avoidance systems. In: DASC (2019)","DOI":"10.1109\/DASC43569.2019.9081748"},{"key":"1_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-319-63387-9_5","volume-title":"Computer Aided Verification","author":"G Katz","year":"2017","unstructured":"Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: an efficient SMT solver for verifying deep neural networks. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 97\u2013117. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_5"},{"key":"1_CR27","unstructured":"Kendall, A., Gal, Y.: What uncertainties do we need in Bayesian deep learning for computer vision? In: NeurIPS (2017)"},{"key":"1_CR28","unstructured":"Khan, M., Nielsen, D., Tangkaratt, V., Lin, W., Gal, Y., Srivastava, A.: Fast and scalable Bayesian deep learning by weight-perturbation in Adam. In: ICML, pp. 2611\u20132620. PMLR (2018)"},{"key":"1_CR29","unstructured":"Lechner, M., \u017dikeli\u0107, D., Chatterjee, K., Henzinger, T.: Infinite time horizon safety of Bayesian neural networks. In: NeurIPS, vol.\u00a034, pp. 10171\u201310185 (2021)"},{"key":"1_CR30","unstructured":"LeCun, Y.: The MNIST database of handwritten digits (1998)"},{"key":"1_CR31","unstructured":"Liu, X., Li, Y., Wu, C., Hsieh, C.J.: Adv-BNN: improved adversarial defense through robust Bayesian neural network. In: ICLR (2019)"},{"key":"1_CR32","doi-asserted-by":"crossref","unstructured":"Michelmore, R., Wicker, M., Laurenti, L., Cardelli, L., Gal, Y., Kwiatkowska, M.: Uncertainty quantification with statistical guarantees in end-to-end autonomous driving control. In: ICRA (2019)","DOI":"10.1109\/ICRA40945.2020.9196844"},{"key":"1_CR33","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0745-0","volume-title":"Bayesian Learning for Neural Networks","author":"RM Neal","year":"2012","unstructured":"Neal, R.M.: Bayesian Learning for Neural Networks. Springer, New York (2012). https:\/\/doi.org\/10.1007\/978-1-4612-0745-0"},{"key":"1_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-642-28145-7_18","volume-title":"Applied Parallel and Scientific Computing","author":"NH Diep","year":"2012","unstructured":"Diep, N.H.: Efficient implementation of interval matrix multiplication. In: J\u00f3nasson, K. (ed.) PARA 2010. LNCS, vol. 7134, pp. 179\u2013188. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28145-7_18"},{"key":"1_CR35","unstructured":"Patane, A., Blaas, A., Laurenti, L., Cardelli, L., Roberts, S., Kwiatkowska, M.: Adversarial robustness guarantees for Gaussian processes. J. Mach. Learn. Res. 23 (2022)"},{"key":"1_CR36","unstructured":"Raghunathan, A., Steinhardt, J., Liang, P.S.: Semidefinite relaxations for certifying robustness to adversarial examples. In: NeurIPS, vol.\u00a031 (2018)"},{"key":"1_CR37","doi-asserted-by":"publisher","first-page":"534","DOI":"10.1023\/A:1022374804152","volume":"39","author":"SM Rump","year":"1999","unstructured":"Rump, S.M.: Fast and parallel interval arithmetic. BIT Numer. Math. 39, 534\u2013554 (1999)","journal-title":"BIT Numer. Math."},{"key":"1_CR38","unstructured":"Smith, M.T., Grosse, K., Backes, M., Alvarez, M.A.: Adversarial vulnerability bounds for Gaussian process classification. arXiv preprint arXiv:1909.08864 (2019)"},{"key":"1_CR39","unstructured":"Sosnin, P., M\u00fcller, M., Baader, M., Tsay, C., Wicker, M.: Certified robustness to data poisoning in gradient-based training. arXiv preprint arXiv:2406.05670 (2024)"},{"key":"1_CR40","doi-asserted-by":"crossref","unstructured":"Stallkamp, J., Schlipsing, M., Salmen, J., Igel, C.: Man vs. computer: benchmarking machine learning algorithms for traffic sign recognition. Neural Netw. 32, 323\u2013332 (2012)","DOI":"10.1016\/j.neunet.2012.02.016"},{"key":"1_CR41","unstructured":"Stanforth, R., Gowal, S., Mann, T., Kohli, P., et\u00a0al.: A dual approach to scalable verification of deep networks. arXiv preprint arXiv:1803.06567 (2018)"},{"key":"1_CR42","unstructured":"Szegedy, C., et al.: Intriguing properties of neural networks. In: ICLR (2014)"},{"key":"1_CR43","unstructured":"Tjeng, V., Xiao, K., Tedrake, R.: Evaluating robustness of neural networks with mixed integer programming. arXiv preprint arXiv:1711.07356 (2017)"},{"key":"1_CR44","unstructured":"Wei, T., Liu, C.: Safe control with neural network dynamic models. In: Learning for Dynamics and Control Conference, pp. 739\u2013750. PMLR (2022)"},{"key":"1_CR45","unstructured":"Weng, T.W., et al.: Towards fast computation of certified robustness for ReLU networks. In: ICML (2018)"},{"key":"1_CR46","unstructured":"Wicker, M.: Adversarial robustness of Bayesian neural networks. Ph.D. thesis, University of Oxford (2021)"},{"key":"1_CR47","unstructured":"Wicker, M., Heo, J., Costabello, L., Weller, A.: Robust explanation constraints for neural networks. arXiv preprint arXiv:2212.08507 (2022)"},{"key":"1_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1007\/978-3-319-89960-2_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Wicker","year":"2018","unstructured":"Wicker, M., Huang, X., Kwiatkowska, M.: Feature-guided black-box safety testing of deep neural networks. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 408\u2013426. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_22"},{"key":"1_CR49","unstructured":"Wicker, M., Laurenti, L., Patane, A., Chen, Z., Zhang, Z., Kwiatkowska, M.: Bayesian inference with certifiable adversarial robustness. In: AISTATS, pp. 2431\u20132439. PMLR (2021)"},{"key":"1_CR50","unstructured":"Wicker, M., Laurenti, L., Patane, A., Kwiatkowska, M.: Probabilistic safety for Bayesian neural networks. In: UAI, pp. 1198\u20131207. PMLR (2020)"},{"key":"1_CR51","unstructured":"Wicker, M., Laurenti, L., Patane, A., Paoletti, N., Abate, A., Kwiatkowska, M.: Certification of iterative predictions in Bayesian neural networks. In: UAI, pp. 1713\u20131723. PMLR (2021)"},{"key":"1_CR52","doi-asserted-by":"crossref","unstructured":"Wicker, M., Laurenti, L., Patane, A., Paoletti, N., Abate, A., Kwiatkowska, M.: Probabilistic reach-avoid for Bayesian neural networks. Artif. Intell. (2024)","DOI":"10.1016\/j.artint.2024.104132"},{"key":"1_CR53","unstructured":"Wicker, M., et al.: Certificates of differential privacy and unlearning for gradient-based training. arXiv preprint arXiv:2406.13433 (2024)"},{"key":"1_CR54","unstructured":"Wong, E., Kolter, Z.: Provable defenses against adversarial examples via the convex outer adversarial polytope. In: ICML, pp. 5286\u20135295. PMLR (2018)"},{"key":"1_CR55","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1016\/j.tcs.2019.05.046","volume":"807","author":"M Wu","year":"2020","unstructured":"Wu, M., Wicker, M., Ruan, W., Huang, X., Kwiatkowska, M.: A game-based approximate verification of deep neural networks with provable guarantees. Theoret. Comput. Sci. 807, 298\u2013329 (2020)","journal-title":"Theoret. Comput. Sci."},{"issue":"1","key":"1_CR56","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1038\/s41597-022-01721-8","volume":"10","author":"J Yang","year":"2023","unstructured":"Yang, J., et al.: MedMNIST v2-a large-scale lightweight benchmark for 2D and 3D biomedical image classification. Sci. Data 10(1), 41 (2023)","journal-title":"Sci. Data"},{"key":"1_CR57","unstructured":"Yuan, M., Wicker, M., Laurenti, L.: Gradient-free adversarial attacks for Bayesian neural networks. In: AABI (2020)"},{"key":"1_CR58","unstructured":"Zhang, G., Sun, S., Duvenaud, D., Grosse, R.: Noisy natural gradient as variational inference. In: ICML, pp. 5852\u20135861. PMLR (2018)"},{"key":"1_CR59","unstructured":"Zhang, H., Weng, T.W., Chen, P.Y., Hsieh, C.J., Daniel, L.: Efficient neural network robustness certification with general activation functions. In: NeurIPS, pp. 4939\u20134948 (2018)"},{"key":"1_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-031-57256-2_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems - TACAS 2024","author":"X Zhang","year":"2024","unstructured":"Zhang, X., Wang, B., Kwiatkowska, M.: Provable preimage under-approximation for neural networks. In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) TACAS 2024. LNCS, vol. 14572, pp. 3\u201323. Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-57256-2_1"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71162-6_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:03:27Z","timestamp":1725933807000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71162-6_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,11]]},"ISBN":["9783031711619","9783031711626"],"references-count":60,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71162-6_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,9,11]]},"assertion":[{"value":"11 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that\u00a0are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}