{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,14]],"date-time":"2026-06-14T23:26:01Z","timestamp":1781479561596,"version":"3.54.1"},"publisher-location":"Cham","reference-count":36,"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>The reliability and usefulness of verification depend on the ability to represent appropriately the uncertainty. Most existing work on neural network verification relies on the hypothesis of either set-based or probabilistic information on the inputs. In this work, we rely on the framework of imprecise probabilities, specifically p-boxes, to propose a quantitative verification of ReLU neural networks, which can account for both probabilistic information and epistemic uncertainty on inputs. On classical benchmarks, including the ACAS Xu examples, we demonstrate that our approach improves the tradeoff between tightness and efficiency compared to related work on probabilistic network verification, while handling much more general classes of uncertainties on the inputs and providing fully guaranteed results.<\/jats:p>","DOI":"10.1007\/978-3-031-71162-6_17","type":"book-chapter","created":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:02:27Z","timestamp":1725933747000},"page":"324-342","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["A Zonotopic Dempster-Shafer Approach to\u00a0the\u00a0Quantitative Verification of\u00a0Neural Networks"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3198-1863","authenticated-orcid":false,"given":"Eric","family":"Goubault","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5624-3755","authenticated-orcid":false,"given":"Sylvie","family":"Putot","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,9,11]]},"reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/978-3-319-63387-9_20","volume-title":"Computer Aided Verification","author":"S Bak","year":"2017","unstructured":"Bak, S., Duggirala, P.S.: Simulation-equivalent reachability of large linear systems with inputs. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 401\u2013420. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_20"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"Baluta, T., Chua, Z.L., Meel, K.S., Saxena, P.: Scalable quantitative verification for deep neural networks (2021)","DOI":"10.1109\/ICSE43902.2021.00039"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"Baluta, T., Shen, S., S., S., Meel, K.S., Saxena, P.: Quantitative verification of neural networks and its security applications. In: Computer and Communications Security (2019)","DOI":"10.1145\/3319535.3354245"},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Beer, M., S.F., Kreinovich, V.: Imprecise probabilities in engineering analyses. Mech. Syst. Signal Process. 37(1), 4\u201329 (2013)","DOI":"10.1016\/j.ymssp.2013.01.024"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"Boopathy, A., Weng, T.W., Chen, P.Y., Liu, S., Daniel, L.: CNN-cert: an efficient framework for certifying robustness of convolutional neural networks. In: AAAI (2019)","DOI":"10.1609\/aaai.v33i01.33013240"},{"issue":"2\u20134","key":"17_CR6","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/s00607-011-0182-8","volume":"94","author":"O Bouissou","year":"2012","unstructured":"Bouissou, O., Goubault, E., Goubault-Larrecq, J., Putot, S.: A generalization of p-boxes to affine arithmetic. Computing 94(2\u20134), 189\u2013201 (2012)","journal-title":"Computing"},{"key":"17_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1007\/978-3-662-49674-9_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"O Bouissou","year":"2016","unstructured":"Bouissou, O., Goubault, E., Putot, S., Chakarov, A., Sankaranarayanan, S.: Uncertainty propagation using probabilistic affine forms and concentration of measure inequalities. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 225\u2013243. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_13"},{"key":"17_CR8","doi-asserted-by":"publisher","unstructured":"Fazlyab, M., Morari, M., Pappas, G.J.: Probabilistic verification and reachability analysis of neural networks via semidefinite programming. In: 2019 IEEE 58th Conference on Decision and Control (CDC), pp. 2726\u20132731 (2019). https:\/\/doi.org\/10.1109\/CDC40024.2019.9029310","DOI":"10.1109\/CDC40024.2019.9029310"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"Ferson, S., Kreinovich, V., Ginzburg, L., Myers, D.: Constructing probability boxes and dempster-shafer structures. Tech. rep., Sandia National Laboratories, SAND2002-4015, Albuquerque, New Mexico (2003)","DOI":"10.2172\/809606"},{"key":"17_CR10","unstructured":"Goubault, E., Putot, S.: A Zonotopic Dempster-Shafer Approach to the Quantitative Verification of Neural Networks (2024). https:\/\/hal.science\/hal-04546350. Working paper or preprint"},{"key":"17_CR11","unstructured":"Gray, A., Ferson, S., Patelli, E.: ProbabilityBoundsAnalysis.jl: arithmetic with sets of distributions. In: Proceedings of JuliaCon (2021)"},{"key":"17_CR12","doi-asserted-by":"publisher","unstructured":"Gray, A., Forets, M., Schilling, C., Ferson, S., Benet, L.: Verified propagation of imprecise probabilities in non-linear ODEs. Int. J. Approx. Reason. 164, 109044 (2024). https:\/\/doi.org\/10.1016\/j.ijar.2023.109044","DOI":"10.1016\/j.ijar.2023.109044"},{"key":"17_CR13","unstructured":"Henriksen, P., Lomuscio, A.R.: Efficient neural network verification via adaptive refinement and adversarial search. In: Giacomo, G.D., et al. (eds.) ECAI 2020 - 24th European Conference on Artificial Intelligence, 2020 - Including 10th Conference on Prestigious Applications of Artificial Intelligence (PAIS 2020). Frontiers in Artificial Intelligence and Applications, vol.\u00a0325, pp. 2513\u20132520. IOS Press (2020)"},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-030-86362-3_7","volume-title":"Artificial Neural Networks and Machine Learning \u2013 ICANN 2021","author":"C Huang","year":"2021","unstructured":"Huang, C., Hu, Z., Huang, X., Pei, K.: Statistical certification of acceptable robustness for neural networks. In: Farka\u0161, I., Masulli, P., Otte, S., Wermter, S. (eds.) ICANN 2021. LNCS, vol. 12891, pp. 79\u201390. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-86362-3_7"},{"key":"17_CR15","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"},{"issue":"04","key":"17_CR16","first-page":"5037","volume":"34","author":"Z Lyu","year":"2020","unstructured":"Lyu, Z., Ko, C.Y., Kong, Z., Wong, N., Lin, D., Daniel, L.: Fastened crown: tightened neural network robustness certificates. Proc. AAAI Conf. Artif. Intell. 34(04), 5037\u20135044 (2020)","journal-title":"Proc. AAAI Conf. Artif. Intell."},{"key":"17_CR17","doi-asserted-by":"publisher","unstructured":"Montes, I., Miranda, E., Pelessoni, R., Vicig, P.: Sklar\u2019s theorem in an imprecise setting. Fuzzy Sets and Systems 278, 48\u201366 (2015). https:\/\/doi.org\/10.1016\/j.fss.2014.10.007, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0165011414004539, special Issue on uncertainty and imprecision modelling in decision making (EUROFUSE 2013)","DOI":"10.1016\/j.fss.2014.10.007"},{"key":"17_CR18","unstructured":"Nelsen, R.B.: An Introduction to Copulas, 2nd edn. Springer, New York (2006)"},{"key":"17_CR19","doi-asserted-by":"publisher","unstructured":"Omladi\u010d, M., Stopar, N.: A full scale sklar\u2019s theorem in the imprecise setting. Fuzzy Sets and Systems 393, 113\u2013125 (2020). https:\/\/doi.org\/10.1016\/j.fss.2020.02.001, https:\/\/www.sciencedirect.com\/science\/article\/pii\/S0165011420300348, copulas and Related Topics","DOI":"10.1016\/j.fss.2020.02.001"},{"key":"17_CR20","doi-asserted-by":"publisher","unstructured":"Pautov, M., Tursynbek, N., Munkhoeva, M., Muravev, N., Petiushko, A., Oseledets, I.: Cc-cert: A probabilistic approach to certify general robustness of neural networks. Proceedings of the AAAI Conference on Artificial Intelligence 36, 7975\u20137983 (06 2022). https:\/\/doi.org\/10.1609\/aaai.v36i7.20768","DOI":"10.1609\/aaai.v36i7.20768"},{"key":"17_CR21","unstructured":"Pilipovsky, J., Sivaramakrishnan, V., Oishi, M., Tsiotras, P.: Probabilistic verification of Relu neural networks via characteristic functions. In: Matni, N., Morari, M., Pappas, G.J. (eds.) Proceedings of The 5th Annual Learning for Dynamics and Control Conference. Proceedings of Machine Learning Research, vol.\u00a0211, pp. 966\u2013979. PMLR (2023)"},{"key":"17_CR22","doi-asserted-by":"publisher","unstructured":"P\u0103s\u0103reanu, C., Converse, H., Filieri, A., Gopinath, D.: On the probabilistic analysis of neural networks. In: 2020 IEEE\/ACM 15th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS), pp. 5\u20138 (2020). https:\/\/doi.org\/10.1145\/3387939.3391594","DOI":"10.1145\/3387939.3391594"},{"key":"17_CR23","doi-asserted-by":"publisher","unstructured":"Regan, H., Ferson, S., Berleant, D.: Equivalence of methods for uncertainty propagation of real-valued random variables. Int. J. Approx. Reason. 36, 1\u201330 (2004). https:\/\/doi.org\/10.1016\/j.ijar.2003.07.013","DOI":"10.1016\/j.ijar.2003.07.013"},{"key":"17_CR24","doi-asserted-by":"publisher","unstructured":"Schmelzer, B.: Random sets, copulas and related sets of probability measures. Int. J. Approx. Reason. 160, 108952 (2023). https:\/\/doi.org\/10.1016\/j.ijar.2023.108952","DOI":"10.1016\/j.ijar.2023.108952"},{"key":"17_CR25","doi-asserted-by":"crossref","unstructured":"Shafer, G.: A Mathematical Theory of Evidence. Princeton University Press (1976)","DOI":"10.1515\/9780691214696"},{"key":"17_CR26","unstructured":"Singh, G., Gehr, T., Mirman, M., P\u00fcschel, M., Vechev, M.: Fast and effective robustness certification. In: Bengio, S., Wallach, H., Larochelle, H., Grauman, K., Cesa-Bianchi, N., Garnett, R. (eds.) Advances in Neural Information Processing Systems. vol.\u00a031. Curran Associates, Inc. (2018). https:\/\/proceedings.neurips.cc\/paper_files\/paper\/2018\/file\/f2f446980d8e971ef3da97af089481c3-Paper.pdf"},{"key":"17_CR27","unstructured":"Singh, G., Gehr, T., Mirman, M., P\u00fcschel, M., Vechev, M.T.: Fast and effective robustness certification. In: Advances in Neural Information Processing Systems, NeurIPS, pp. 10825\u201310836 (2018)"},{"key":"17_CR28","doi-asserted-by":"crossref","unstructured":"Singh, G., Gehr, T., P\u00fcschel, M., Vechev, M.: An abstract domain for certifying neural networks. Proc. ACM Program. Lang. (POPL) (2019)","DOI":"10.1145\/3290354"},{"key":"17_CR29","doi-asserted-by":"publisher","unstructured":"Tran, H.D., Choi, S., Okamoto, H., Hoxha, B., Fainekos, G., Prokhorov, D.: Quantitative verification for neural networks using probstars. In: Proceedings of the 26th ACM International Conference on Hybrid Systems: Computation and Control (HSCC 2023). Association for Computing Machinery, New York (2023). https:\/\/doi.org\/10.1145\/3575870.3587112","DOI":"10.1145\/3575870.3587112"},{"key":"17_CR30","doi-asserted-by":"crossref","unstructured":"Walley, P.: Statistical Reasoning with Imprecise Probabilities. Chapman & Hall (1991)","DOI":"10.1007\/978-1-4899-3472-7"},{"key":"17_CR31","unstructured":"Webb, S., Rainforth, T., Teh, Y.W., Kumar, M.P.: A statistical approach to assessing neural network robustness. ICLR. arXiv preprint arXiv:1811.07209 (2019)"},{"key":"17_CR32","unstructured":"Weng, L., et al.: PROVEN: Verifying robustness of neural networks with a probabilistic approach. In: Chaudhuri, K., Salakhutdinov, R. (eds.) Proceedings of the 36th International Conference on Machine Learning. Proceedings of Machine Learning Research, vol.\u00a097, pp. 6727\u20136736. PMLR (2019). https:\/\/proceedings.mlr.press\/v97\/weng19a.html"},{"key":"17_CR33","doi-asserted-by":"crossref","unstructured":"Williamson, R.C., Downs, T.: Probabilistic arithmetic: numerical methods for calculating convolutions and dependency bounds. Journ. Approx. Reas. (1990)","DOI":"10.1016\/0888-613X(90)90022-T"},{"key":"17_CR34","unstructured":"Zhang, D., Ye, M., Gong, C., Zhu, Z., Liu, Q.: Black-box certification with randomized smoothing: a functional optimization based framework. In: Proceedings of the 34th International Conference on Neural Information Processing Systems (NIPS 2020). Curran Associates Inc., Red Hook (2020)"},{"key":"17_CR35","unstructured":"Zhang, H., Weng, T.W., Chen, P.Y., Hsieh, C.J., Daniel, L.: Efficient neural network robustness certification with general activation functions. In: Bengio, S., Wallach, H., Larochelle, H., Grauman, K., Cesa-Bianchi, N., Garnett, R. (eds.) Advances in Neural Information Processing Systems, vol.\u00a031, pp. 4939\u20134948. Curran Associates, Inc. (2018). https:\/\/proceedings.neurips.cc\/paper\/2018\/file\/d04863f100d59b3eb688a11f95b0ae60-Paper.pdf"},{"key":"17_CR36","doi-asserted-by":"publisher","unstructured":"Zhang, T., Ruan, W., Fieldsend, J.E.: Proa: a probabilistic robustness assessment against functional perturbations. In: ECML PKDD 2022, Part III. LNCS, pp. 154\u2013170. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-26409-2_10","DOI":"10.1007\/978-3-031-26409-2_10"}],"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_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T02:05:41Z","timestamp":1725933941000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71162-6_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,11]]},"ISBN":["9783031711619","9783031711626"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71162-6_17","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 Julia implementation of our approach and the examples to reproduce results of this paper are available from .","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Data Availability Statement"}},{"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"}}]}}