{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,11]],"date-time":"2025-09-11T19:34:36Z","timestamp":1757619276323,"version":"3.44.0"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031986789"},{"type":"electronic","value":"9783031986796"}],"license":[{"start":{"date-parts":[[2025,1,1]],"date-time":"2025-01-01T00:00:00Z","timestamp":1735689600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,7,22]],"date-time":"2025-07-22T00:00:00Z","timestamp":1753142400000},"content-version":"vor","delay-in-days":202,"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>\n          <jats:p>Neural networks are often susceptible to minor perturbations in input that cause them to misclassify. A recent solution to this problem is the use of globally-robust neural networks, which employ a function to certify that the classification of an input cannot be altered by such a perturbation. Outputs that pass this test are called <jats:italic>certified robust<\/jats:italic>. However, to the authors\u2019 knowledge, these certification functions have not yet been verified at the implementation level. We demonstrate how previous unverified implementations are exploitably unsound in certain circumstances. Moreover, they often rely on approximation-based algorithms, such as power iteration, that (perhaps surprisingly) do not guarantee soundness. To provide assurance that a given output is robust, we implemented and formally verified a certification function for globally-robust neural networks in Dafny. We describe the program, its specifications, and the important design decisions taken for its implementation and verification, as well as our experience applying it in practice.<\/jats:p>","DOI":"10.1007\/978-3-031-98679-6_15","type":"book-chapter","created":{"date-parts":[[2025,7,21]],"date-time":"2025-07-21T09:20:19Z","timestamp":1753089619000},"page":"327-348","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Formally Verified Robustness Certifier for\u00a0Neural Networks"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1205-3455","authenticated-orcid":false,"given":"James","family":"Tobler","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4923-3783","authenticated-orcid":false,"given":"Hira Taqdees","family":"Syeda","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8271-0289","authenticated-orcid":false,"given":"Toby","family":"Murray","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,22]]},"reference":[{"key":"15_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-642-22110-1_7","volume-title":"Computer Aided Verification","author":"E Alkassar","year":"2011","unstructured":"Alkassar, E., B\u00f6hme, S., Mehlhorn, K., Rizkallah, C.: Verification of certifying computations. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 67\u201382. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_7"},{"key":"15_CR2","unstructured":"Anil, C., Lucas, J., Grosse, R.: Sorting out Lipschitz function approximation. In: International Conference on Machine Learning (ICML), pp. 291\u2013301. PMLR (2019)"},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"Brucker, A.D., Cameron-Burke, T., Stell, A.: Formally verified interval arithmetic and its application to program verification. In: Proceedings of the 2024 IEEE\/ACM 12th International Conference on Formal Methods in Software Engineering (FormaliSE), pp. 111\u2013121 (2024)","DOI":"10.1145\/3644033.3644370"},{"key":"15_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/978-3-319-96142-2_26","volume-title":"Computer Aided Verification","author":"A Chudnov","year":"2018","unstructured":"Chudnov, A., et al.: Continuous formal verification of amazon s2n. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 430\u2013446. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_26"},{"key":"15_CR5","unstructured":"Cohen, J., Rosenfeld, E., Kolter, Z.: Certified adversarial robustness via randomized smoothing. In: International Conference on Machine Learning (ICML), pp. 1310\u20131320. PMLR (2019)"},{"key":"15_CR6","unstructured":"Delattre, B., Barth\u00e9lemy, Q., Araujo, A., Allauzen, A.: Efficient bound of Lipschitz constant for convolutional layers by Gram iteration. In: International Conference on Machine Learning (ICML), pp. 7513\u20137532. PMLR (2023)"},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"Dong, Y., Liao, F., Pang, T., Su, H., Zhu, J., Hu, X., Li, J.: Boosting adversarial attacks with momentum. In: Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition (CVPR), pp. 9185\u20139193 (2018)","DOI":"10.1109\/CVPR.2018.00957"},{"key":"15_CR8","doi-asserted-by":"publisher","unstructured":"Dross, C., Kanig, J.: Making proofs of floating-point programs accessible to regular developers. In: International Workshop on Numerical Software Verification, pp. 7\u201324. Springer, Heidelberg (2021). https:\/\/doi.org\/10.1007\/978-3-030-95561-8_2","DOI":"10.1007\/978-3-030-95561-8_2"},{"key":"15_CR9","unstructured":"Fromherz, A., Leino, K., Fredrikson, M., Parno, B., Pasareanu, C.S.: Fast geometric projections for local robustness certification. In: International Conference on Learning Representations (ICLR). OpenReview.net (2021). https:\/\/openreview.net\/forum?id=zWy1uxjDdZJ"},{"key":"15_CR10","unstructured":"GitHub user vanajac: Hyperas on fashion-mnist - hyperparameter tuning for dense networks (2021). https:\/\/github.com\/vanajac\/fashion_mnist\/blob\/main\/fashionMNIST.ipynb"},{"key":"15_CR11","unstructured":"Goodfellow, I.J., Shlens, J., Szegedy, C.: Explaining and harnessing adversarial examples. In: International Conference on Learning Representations (ICLR) (2015)"},{"key":"15_CR12","doi-asserted-by":"publisher","unstructured":"Gouk, H., Frank, E., Pfahringer, B., Cree, M.J.: Regularisation of neural networks by enforcing Lipschitz continuity. Mach. Learn. 110(2), 393\u2013416 (2021). https:\/\/doi.org\/10.1007\/S10994-020-05929-W","DOI":"10.1007\/S10994-020-05929-W"},{"key":"15_CR13","unstructured":"Hu, K., Leino, K., Wang, Z., Fredrikson, M.: A recipe for improved certifiable robustness. In: International Conference on Learning Representations (ICLR) (2024)"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"Jin, J., Ohrimenko, O., Rubinstein, B.I.: Getting a-round guarantees: floating-point attacks on certified robustness. In: Proceedings of the 2024 Workshop on Artificial Intelligence and Security, pp. 53\u201364 (2024)","DOI":"10.1145\/3689932.3694761"},{"issue":"OOPSLA1","key":"15_CR15","doi-asserted-by":"publisher","first-page":"1010","DOI":"10.1145\/3649847","volume":"8","author":"A Kabaha","year":"2024","unstructured":"Kabaha, A., Cohen, D.D.: Verification of neural networks\u2019 global robustness. Proc. ACM Program. Lang. 8(OOPSLA1), 1010\u20131039 (2024)","journal-title":"Proc. ACM Program. Lang."},{"key":"15_CR16","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":"1","key":"15_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2560537","volume":"32","author":"G Klein","year":"2014","unstructured":"Klein, G., et al.: Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst. (TOCS) 32(1), 1\u201370 (2014)","journal-title":"ACM Trans. Comput. Syst. (TOCS)"},{"key":"15_CR18","unstructured":"Krizhevsky, A.: Learning multiple layers of features from tiny images. University of Toronto, Technical report (2009)"},{"issue":"11","key":"15_CR19","doi-asserted-by":"publisher","first-page":"2278","DOI":"10.1109\/5.726791","volume":"86","author":"Y LeCun","year":"1998","unstructured":"LeCun, Y., Bottou, L., Bengio, Y., Haffner, P.: Gradient-based learning applied to document recognition. Proc. IEEE 86(11), 2278\u20132324 (1998)","journal-title":"Proc. IEEE"},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"Lecuyer, M., Atlidakis, V., Geambasu, R., Hsu, D., Jana, S.: Certified robustness to adversarial examples with differential privacy. In: IEEE Symposium on Security and Privacy, pp. 656\u2013672. IEEE (2019)","DOI":"10.1109\/SP.2019.00044"},{"key":"15_CR21","first-page":"16891","volume":"33","author":"S Lee","year":"2020","unstructured":"Lee, S., Lee, J., Park, S.: Lipschitz-certifiable training with a tight outer bound. Adv. Neural Inf. Process. Syst. (NeurIPS) 33, 16891\u201316902 (2020)","journal-title":"Adv. Neural Inf. Process. Syst. (NeurIPS)"},{"key":"15_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"K Leino","year":"2010","unstructured":"Leino, K.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"key":"15_CR23","unstructured":"Leino, K., Wang, Z., Fredrikson, M.: Globally-robust neural networks. In: International Conference on Machine Learning (ICML). Proceedings of Machine Learning Research, vol.\u00a0139, pp. 6212\u20136222. PMLR (2021). http:\/\/proceedings.mlr.press\/v139\/leino21a.html"},{"key":"15_CR24","unstructured":"Madry, A., Makelov, A., Schmidt, L., Tsipras, D., Vladu, A.: Towards deep learning models resistant to adversarial attacks. In: International Conference on Learning Representations (ICLR) (2018)"},{"key":"15_CR25","unstructured":"Mangal, R., et al.: Is certifying $$\\ell _p$$\u00a0robustness still worthwhile? arXiv preprint arXiv:2310.09361 (2023)"},{"key":"15_CR26","unstructured":"Meng, M.H., et al.: Adversarial robustness of deep neural networks: a survey from a formal verification perspective. IEEE Trans. Depend. Secure Comput. (2022)"},{"key":"15_CR27","doi-asserted-by":"crossref","unstructured":"Murray, T., et al.: seL4: from general purpose to a proof of information flow enforcement. In: IEEE Symposium on Security and Privacy, pp. 415\u2013429. IEEE (2013)","DOI":"10.1109\/SP.2013.35"},{"key":"15_CR28","unstructured":"Nicolae, M.I., et\u00a0al.: Adversarial Robustness Toolbox v1.0.0. arXiv preprint arXiv:1807.01069 (2018)"},{"key":"15_CR29","unstructured":"Rizkallah, C.: Verification of Program Computations. Ph.D. thesis, Saarland University (2015)"},{"key":"15_CR30","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. 3(POPL), 1\u201330 (2019)","DOI":"10.1145\/3290354"},{"key":"15_CR31","unstructured":"Szegedy, C.: Intriguing properties of neural networks. arXiv preprint arXiv:1312.6199 (2013)"},{"key":"15_CR32","doi-asserted-by":"crossref","unstructured":"Tobler, J., Syeda, H.T., Murray, T.: A formally verified robustness certifier for neural networks (extended version) (2025). https:\/\/arxiv.org\/abs\/2505.06958","DOI":"10.1007\/978-3-031-98679-6_15"},{"key":"15_CR33","unstructured":"Xiao, H., Rasul, K., Vollgraf, R.: Fashion-MNIST: a novel image dataset for benchmarking machine learning algorithms. arXiv preprint arXiv:1708.07747 (2017)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-98679-6_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,7]],"date-time":"2025-09-07T16:18:15Z","timestamp":1757261895000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98679-6_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986789","9783031986796"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98679-6_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"22 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Zagreb","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Croatia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"37","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conferences.i-cav.org\/2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}