{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,5]],"date-time":"2026-01-05T21:48:05Z","timestamp":1767649685793,"version":"3.40.5"},"reference-count":90,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2023,5,23]],"date-time":"2023-05-23T00:00:00Z","timestamp":1684800000000},"content-version":"unspecified","delay-in-days":111,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2023,2]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>A domain-theoretic framework is presented for validated robustness analysis of neural networks. First, global robustness of a general class of networks is analyzed. Then, using the fact that Edalat\u2019s domain-theoretic<jats:italic>L<\/jats:italic>-derivative coincides with Clarke\u2019s generalized gradient, the framework is extended for attack-agnostic local robustness analysis. The proposed framework is ideal for designing algorithms which are correct by construction. This claim is exemplified by developing a validated algorithm for estimation of Lipschitz constant of feedforward regressors. The completeness of the algorithm is proved over differentiable networks and also over general position<jats:inline-formula><jats:alternatives><jats:inline-graphic xmlns:xlink=\"http:\/\/www.w3.org\/1999\/xlink\" mime-subtype=\"png\" xlink:href=\"S0960129523000142_inline1.png\"\/><jats:tex-math>${\\mathrm{ReLU}}$<\/jats:tex-math><\/jats:alternatives><\/jats:inline-formula>networks. Computability results are obtained within the framework of effectively given domains. Using the proposed domain model, differentiable and non-differentiable networks can be analyzed uniformly. The validated algorithm is implemented using arbitrary-precision interval arithmetic, and the results of some experiments are presented. The software implementation is truly validated, as it handles floating-point errors as well.<\/jats:p>","DOI":"10.1017\/s0960129523000142","type":"journal-article","created":{"date-parts":[[2023,5,23]],"date-time":"2023-05-23T07:26:32Z","timestamp":1684826792000},"page":"68-105","update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":3,"title":["A domain-theoretic framework for robustness analysis of neural networks"],"prefix":"10.1017","volume":"33","author":[{"given":"Can","family":"Zhou","sequence":"first","affiliation":[]},{"given":"Razin A.","family":"Shaikh","sequence":"additional","affiliation":[]},{"given":"Yiran","family":"Li","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1879-0763","authenticated-orcid":false,"given":"Amin","family":"Farjudian","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2023,5,23]]},"reference":[{"key":"S0960129523000142_ref20","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80007-0"},{"key":"S0960129523000142_ref31","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2007.01.002"},{"key":"S0960129523000142_ref58","doi-asserted-by":"publisher","DOI":"10.1145\/3498718"},{"key":"S0960129523000142_ref14","unstructured":"Clarke, F. H. (1990). Optimization and Nonsmooth Analysis, Philadelphia, Classics in Applied Mathematics, Society for Industrial and Applied Mathematics."},{"key":"S0960129523000142_ref88","unstructured":"Wong, E. and Kolter, J. Z. (2018). Provable defenses against adversarial examples via the convex outer adversarial polytope. In: Dy, J. G. and Krause, A. (eds.) Proceedings of the 35th International Conference on Machine Learning, ICML 2018, Stockholmsm\u00e4ssan, Stockholm, Sweden, July 10\u201315, 2018, Proceedings of Machine Learning Research, vol. 80, PMLR, 5283\u20135292."},{"key":"S0960129523000142_ref57","unstructured":"Latorre, F. , Rolland, P. and Cevher, V. (2020). Lipschitz constant estimation of Neural Networks via sparse polynomial optimization. In: International Conference on Learning Representations."},{"key":"S0960129523000142_ref49","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-88806-0_9"},{"key":"S0960129523000142_ref56","first-page":"2597","article-title":"Semantics of query-driven communication of exact values","volume":"16","author":"Kone\u010dn\u00fd","year":"2010","journal-title":"Journal of Universal Computer Science"},{"key":"S0960129523000142_ref46","unstructured":"Hein, M. and Andriushchenko, M. (2017). Formal guarantees on the robustness of a classifier against adversarial manipulation. In: Proceedings of the 31st International Conference on Neural Information Processing Systems. NIPS\u201917, Long Beach, California, USA, 2263\u20132273."},{"key":"S0960129523000142_ref11","doi-asserted-by":"publisher","DOI":"10.1145\/2025113.2025131"},{"key":"S0960129523000142_ref52","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2017.08.002"},{"key":"S0960129523000142_ref42","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139524438"},{"key":"S0960129523000142_ref61","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2018.06.020"},{"key":"S0960129523000142_ref5","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.1907378117"},{"key":"S0960129523000142_ref33","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00250-2"},{"key":"S0960129523000142_ref34","doi-asserted-by":"publisher","DOI":"10.1016\/S0166-8641(97)00225-3"},{"key":"S0960129523000142_ref66","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-7091-6918-6_14"},{"key":"S0960129523000142_ref78","unstructured":"Stanley, R. P. (2006). An Introduction to Hyperplane Arrangements, IAS\/Park City Mathematics Series."},{"key":"S0960129523000142_ref62","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-22348-9_4"},{"key":"S0960129523000142_ref79","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00296-5"},{"key":"S0960129523000142_ref83","unstructured":"Virmaux, A. and Scaman, K. (2018). Lipschitz regularity of deep neural networks: Analysis and efficient estimation. In: Bengio, S. , Wallach, H. M. , Larochelle, H. , Grauman, K. , Bianchi, N. C. and Garnett, R. (eds.) Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3\u20138, 2018, Montr\u00e9al, Canada, 3839\u20133848."},{"volume-title":"Functional Analysis","year":"1991","author":"Rudin","key":"S0960129523000142_ref71"},{"key":"S0960129523000142_ref87","unstructured":"Weng, T.-W. , Zhang, H. , Chen, H. , Song, Z. , Hsieh, C.-J. , Boning, D. , Dhillon, I.S. and Daniel, L. (2018b). Towards fast computation of certified robustness for ReLU networks. In: International Conference on Machine Learning (ICML)."},{"volume-title":"Nonsmooth Analysis and Control Theory","year":"1998","author":"Clarke","key":"S0960129523000142_ref13"},{"year":"2018","author":"Tankimanova","key":"S0960129523000142_ref82"},{"volume-title":"Berlin Heidelberg","year":"2000","author":"Weihrauch","key":"S0960129523000142_ref85"},{"key":"S0960129523000142_ref89","unstructured":"Wong, E. , Schmidt, F. R. and Kolter, J. Z. (2019). Wasserstein Adversarial Examples via Projected Sinkhorn Iterations. arXiv: 1902.07906 [cs.LG]."},{"year":"2021","author":"Bhowmick","key":"S0960129523000142_ref7"},{"key":"S0960129523000142_ref27","doi-asserted-by":"publisher","DOI":"10.2307\/421098"},{"key":"S0960129523000142_ref44","unstructured":"Hashemi, N. , Ruths, J. and Fazlyab, M. (2021). Certifying incremental quadratic constraints for neural networks via convex optimization. In: Jadbabaie, A. , Lygeros, J. , Pappas, G. J. , Parrilo, A. , , P. , Recht, B. , Tomlin, C. J. and Zeilinger, M. N. (eds.) Proceedings of the 3rd Annual Conference on Learning for Dynamics and Control, L4DC 2021, 7\u20138 June 2021, Virtual Event, Switzerland, Proceedings of Machine Learning Research, vol. 144, 842\u2013853."},{"key":"S0960129523000142_ref64","doi-asserted-by":"publisher","DOI":"10.1137\/1.9780898717716"},{"key":"S0960129523000142_ref28","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2844"},{"key":"S0960129523000142_ref18","doi-asserted-by":"publisher","DOI":"10.1609\/aimag.v38i3.2756"},{"key":"S0960129523000142_ref32","doi-asserted-by":"publisher","DOI":"10.1016\/S0166-8641(97)00226-5"},{"key":"S0960129523000142_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(86)90010-9"},{"key":"S0960129523000142_ref41","unstructured":"Goodfellow, I. J. , Shlens, J. and Szegedy, C. (2015). Explaining and harnessing adversarial examples. CoRR abs\/1412.6572. http:\/\/arxiv.org\/abs\/1412.6572."},{"volume-title":"Handbook of Logic in Computer Science","year":"1994","author":"Abramsky","key":"S0960129523000142_ref1"},{"key":"S0960129523000142_ref45","doi-asserted-by":"publisher","DOI":"10.1038\/d41586-019-03013-5"},{"key":"S0960129523000142_ref29","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2020.09.006"},{"key":"S0960129523000142_ref9","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.49"},{"key":"S0960129523000142_ref77","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-65474-0_4"},{"key":"S0960129523000142_ref67","doi-asserted-by":"publisher","DOI":"10.1109\/LCSYS.2021.3050444"},{"key":"S0960129523000142_ref60","unstructured":"Mirman, M. , Gehr, T. and Vechev, M. T. (2018). Differentiable abstract interpretation for provably robust neural networks. In: Dy, J. G. and Krause, A. (eds.) Proceedings of the 35th International Conference on Machine Learning, ICML 2018, Stockholmsm\u00e4ssan, Stockholm, Sweden, July 10\u201315, 2018, Proceedings of Machine Learning Research, vol. 80, PMLR, 3575\u20133583."},{"key":"S0960129523000142_ref65","doi-asserted-by":"publisher","DOI":"10.1109\/JSAIT.2020.2984716"},{"key":"S0960129523000142_ref69","doi-asserted-by":"publisher","DOI":"10.1007\/s11155-005-6891-y"},{"key":"S0960129523000142_ref37","unstructured":"Fazlyab, M. , Robey, A. , Hassani, H. , Morari, M. and Pappas, G. J. (2019). Efficient and accurate estimation of Lipschitz constants for deep neural networks. In: Wallach, H. M. , Larochelle, H. , Beygelzimer, A. , d\u2019Alch\u00e9-Buc, F. , Fox, E.B. and Garnett, R. (eds.) Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurIPS 2019, December 8\u201314, 2019, Vancouver, BC, Canada, 11423\u201311434."},{"key":"S0960129523000142_ref80","doi-asserted-by":"crossref","unstructured":"Stoltenberg-Hansen, V. and Tucker, J. V. (1995). Effective algebras. In: Abramsky, S. , Gabbay, D. M. , and Maibaum, T. S. E. (eds.) Handbook of Logic in Computer Science, Semantic Modelling, vol. IV, Oxford University Press, 357\u2013526.","DOI":"10.1093\/oso\/9780198537809.003.0004"},{"key":"S0960129523000142_ref90","unstructured":"Zombori, D. , B\u00e1nhelyi, B. , Csendes, T. , Megyeri, I. and Jelasity, M. (2021). Fooling a complete neural network verifier. In: International Conference on Learning Representations."},{"key":"S0960129523000142_ref55","first-page":"2629","article-title":"Compositional semantics of dataflow networks with query-driven communication of exact values","volume":"16","author":"Kone\u010dn\u00fd","year":"2010","journal-title":"Journal of Universal Computer Science"},{"key":"S0960129523000142_ref54","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-6802-1"},{"key":"S0960129523000142_ref4","doi-asserted-by":"crossref","unstructured":"Araujo, A. , N\u00e9grevergne, B. , Chevaleyre, Y. and Atif, J. (2021). On Lipschitz regularization of convolutional layers using Toeplitz matrix theory. In: AAAI.","DOI":"10.1609\/aaai.v35i8.16824"},{"key":"S0960129523000142_ref19","doi-asserted-by":"publisher","DOI":"10.1109\/TPEL.2018.2883947"},{"key":"S0960129523000142_ref81","unstructured":"Szegedy, C. , Zaremba, W. , Sutskever, I. , Bruna, J. , Erhan, D. , Goodfellow, I and Fergus, R. (2014). Intriguing Properties of Neural Networks. arXiv: 1312.6199 [cs.CV]."},{"key":"S0960129523000142_ref39","volume-title":"Encycloedia of Mathematics and its Applications","volume":"93","author":"Gierz","year":"2003"},{"key":"S0960129523000142_ref10","doi-asserted-by":"publisher","DOI":"10.1145\/2240236.2240262"},{"key":"S0960129523000142_ref43","doi-asserted-by":"publisher","DOI":"10.1007\/0-387-34471-3"},{"key":"S0960129523000142_ref76","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(77)90045-7"},{"key":"S0960129523000142_ref47","first-page":"1","article-title":"Clarke\u2019s generalized gradient and Edalat\u2019s L-derivative","volume":"9","author":"Hertling","year":"2017","journal-title":"Journal of Logic and Analysis"},{"key":"S0960129523000142_ref75","doi-asserted-by":"publisher","DOI":"10.1145\/3290354"},{"key":"S0960129523000142_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37075-5_22"},{"key":"S0960129523000142_ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-68546-5_19"},{"key":"S0960129523000142_ref63","unstructured":"Moggi, E. , Farjudian, A. and Taha, W. (2019b). System analysis and robustness. In: Proceedings of the 20th Italian Conference on Theoretical Computer Science, ICTCS 2019, Como, Italy, September 9\u201311, 2019, pp. 1\u20137. http:\/\/ceur-ws.org\/Vol-2504\/paper1.pdf."},{"key":"S0960129523000142_ref36","unstructured":"Farjudian, A. and Moggi, E. (2022). Robustness, Scott Continuity, and Computability. arXiv:2208.12347 [cs.LO]."},{"key":"S0960129523000142_ref74","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055795"},{"key":"S0960129523000142_ref12","unstructured":"Chen, T. , Lasserre, J. B. , Magron, V. and Pauwels, E. (2020). Semialgebraic optimization for Lipschitz constants of ReLU networks. In: Larochelle, H. , Ranzato, M. , Hadsell, R. , Balcan, M. and Lin, H. (eds.) Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020, NeurIPS 2020, December 6\u201312, 2020, virtual."},{"key":"S0960129523000142_ref35","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-006-1339-2"},{"key":"S0960129523000142_ref38","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2018.00058"},{"key":"S0960129523000142_ref23","doi-asserted-by":"publisher","DOI":"10.1112\/S1461157000001315"},{"key":"S0960129523000142_ref50","unstructured":"Jordan, M. and Dimakis, A. G. (2020). Exactly computing the local Lipschitz constant of ReLU networks. In: 34th Conference on Neural Information Processing Systems (NeurIPS 2020), Vancouver, Canada."},{"key":"S0960129523000142_ref73","doi-asserted-by":"publisher","DOI":"10.1145\/3398394"},{"key":"S0960129523000142_ref15","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"volume-title":"Berlin Heidelberg","year":"2002","author":"Jech","key":"S0960129523000142_ref48"},{"key":"S0960129523000142_ref24","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.22"},{"key":"S0960129523000142_ref72","unstructured":"Scott, D. (1970). Outline of a mathematical theory of computation. In: Proceedings of the Fourth Annual Princeton Conference on Information Sciences and Systems, 169\u2013176."},{"key":"S0960129523000142_ref6","doi-asserted-by":"publisher","DOI":"10.1017\/S0962492921000039"},{"key":"S0960129523000142_ref2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/1.1.5"},{"volume-title":"Topics in Banach Space Theory","year":"2006","author":"Albiac","key":"S0960129523000142_ref3"},{"key":"S0960129523000142_ref53","unstructured":"Ko, C.-Y. , Lyu, Z. , Weng, L. , Daniel, L. , Wong, N. and Lin, D. (2019). POPQORN: Quantifying robustness of recurrent neural networks. In: Chaudhuri, K. and Salakhutdinov, R. (eds.) Proceedings of the 36th International Conference on Machine Learning, Proceedings of Machine Learning Research, vol. 97, 3468\u20133477."},{"key":"S0960129523000142_ref70","unstructured":"Rudd, K. (2013). Solving Partial Differential Equations Using Artificial Neural Networks. Phd thesis. Department of Mechanical Engineering and Material Sciences, Duke University."},{"key":"S0960129523000142_ref22","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2012.11.006"},{"key":"S0960129523000142_ref86","unstructured":"Weng, T.-W. , Zhang, H. , Chen, P.-Y. , Yi, J. , Su, D. , Gao, Y. , Hsieh, C.-J. and Daniel, L. (2018a). Evaluating the robustness of neural networks: An extreme value theory approach. In: International Conference on Learning Representations."},{"key":"S0960129523000142_ref16","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0046"},{"key":"S0960129523000142_ref51","unstructured":"Jordan, M. and Dimakis, A. G. (2021). Provable Lipschitz certification for generative models. In: Meila, M. and Zhang, T. (eds.) Proceedings of the 38th International Conference on Machine Learning, Proceedings of Machine Learning Research, vol. 139, 5118\u20135126."},{"key":"S0960129523000142_ref30","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004359"},{"key":"S0960129523000142_ref68","unstructured":"Prabhakar, P. and Afzal, Z. R. (2019). Abstraction based output range analysis for neural networks. In: Proceedings of the 33rd International Conference on Neural Information Processing Systems (NeurIPS 2019), 15788\u201315798."},{"key":"S0960129523000142_ref25","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00097-8"},{"key":"S0960129523000142_ref59","unstructured":"Lee, S. , Lee, J. and Park, S. (2020). Lipschitz-certifiable training with a tight outer bound. In: Larochelle, H. , Ranzato, M. , Hadsell, R. , Balcan, M. F. , and Lin, H. (eds.) Advances in Neural Information Processing Systems, vol. 33, Curran Associates, Inc., 16891\u201316902."},{"key":"S0960129523000142_ref84","unstructured":"Wang, S. , Pei, K. , Whitehouse, J. , Yang, J. and Jana, S. (2018). Formal security analysis of neural networks using symbolic intervals. In: Proceedings of the 27th USENIX Conference on Security Symposium. SEC\u201918, Baltimore, MD, USA, USENIX Association, 1599\u20131614."},{"key":"S0960129523000142_ref21","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1096"},{"volume-title":"Berlin Heidelberg","year":"1980","author":"Gierz","key":"S0960129523000142_ref40"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129523000142","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,12,13]],"date-time":"2023-12-13T18:19:44Z","timestamp":1702491584000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129523000142\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,2]]},"references-count":90,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2023,2]]}},"alternative-id":["S0960129523000142"],"URL":"https:\/\/doi.org\/10.1017\/s0960129523000142","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"type":"print","value":"0960-1295"},{"type":"electronic","value":"1469-8072"}],"subject":[],"published":{"date-parts":[[2023,2]]},"assertion":[{"value":"\u00a9 The Author(s), 2023. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}}]}}