{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,2]],"date-time":"2025-08-02T16:26:02Z","timestamp":1754151962085,"version":"3.41.2"},"publisher-location":"Cham","reference-count":72,"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>The classical universal approximation (UA) theorem for neural networks establishes mild conditions under which a feedforward neural network can approximate a continuous function <jats:italic>f<\/jats:italic> with arbitrary accuracy. A recent result shows that neural networks also enjoy a more general <jats:italic>interval<\/jats:italic> universal approximation (IUA) theorem, in the sense that the abstract interpretation semantics of the network using the interval domain can approximate the direct image map of <jats:italic>f<\/jats:italic> (i.e., the result of applying <jats:italic>f<\/jats:italic> to a set of inputs) with arbitrary accuracy. These theorems, however, rest on the unrealistic assumption that the neural network computes over infinitely precise real numbers, whereas their software implementations in practice compute over finite-precision floating-point numbers. An open question is whether the IUA theorem still holds in the floating-point setting.<\/jats:p>\n          <jats:p>This paper introduces the first IUA theorem for <jats:italic>floating-point<\/jats:italic> neural networks that proves their remarkable ability to <jats:italic>perfectly capture<\/jats:italic> the direct image map of any rounded target function <jats:italic>f<\/jats:italic>, showing no limits exist on their expressiveness. Our IUA theorem in the floating-point setting exhibits material differences from the real-valued setting, which reflects the fundamental distinctions between these two computational models. This theorem also implies surprising corollaries, which include (i) the existence of <jats:italic>provably robust<\/jats:italic> floating-point neural networks; and (ii) the <jats:italic>computational completeness<\/jats:italic> of the class of straight-line programs that use only floating-point additions and multiplications for the class of all floating-point programs that halt.<\/jats:p>","DOI":"10.1007\/978-3-031-98679-6_14","type":"book-chapter","created":{"date-parts":[[2025,7,21]],"date-time":"2025-07-21T09:21:05Z","timestamp":1753089665000},"page":"301-326","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Floating-Point Neural Networks are Provably Robust Universal Approximators"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7137-426X","authenticated-orcid":false,"given":"Geonho","family":"Hwang","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0301-0872","authenticated-orcid":false,"given":"Wonyeol","family":"Lee","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4211-6226","authenticated-orcid":false,"given":"Yeachan","family":"Park","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1580-5664","authenticated-orcid":false,"given":"Sejun","family":"Park","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0505-795X","authenticated-orcid":false,"given":"Feras","family":"Saad","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,22]]},"reference":[{"key":"14_CR1","doi-asserted-by":"publisher","unstructured":"Abadi, M., et\u00a0al.: TensorFlow: large-scale machine learning on heterogeneous distributed systems. arXiv 1603.04467 (2016). https:\/\/doi.org\/10.48550\/arXiv.1603.04467","DOI":"10.48550\/arXiv.1603.04467"},{"key":"14_CR2","doi-asserted-by":"publisher","unstructured":"Albarghouthi, A.: Introduction to neural network verification (2021). https:\/\/doi.org\/10.48550\/arXiv.2109.10317","DOI":"10.48550\/arXiv.2109.10317"},{"key":"14_CR3","doi-asserted-by":"publisher","unstructured":"Baader, M.: Expressivity of certified neural networks. Ph.D. thesis, ETH Zurich, Zurich, Switzerland (2024). https:\/\/doi.org\/10.3929\/ETHZ-B-000677199","DOI":"10.3929\/ETHZ-B-000677199"},{"key":"14_CR4","doi-asserted-by":"publisher","unstructured":"Baader, M., Mirman, M., Vechev, M.T.: Universal approximation with certified networks. In: Proceedings of the International Conference on Learning Representations (2020). https:\/\/doi.org\/10.48550\/arXiv.1909.13846","DOI":"10.48550\/arXiv.1909.13846"},{"key":"14_CR5","unstructured":"Baader, M., M\u00fcller, M.N., Mao, Y., Vechev, M.T.: Expressivity of ReLU-networks under convex relaxations. In: Proceedings of the International Conference on Learning Representations (2024). https:\/\/openreview.net\/forum?id=awHTL3Hpto"},{"key":"14_CR6","unstructured":"Barak, B.: Introduction to Theoretical Computer Science (2023). https:\/\/introtcs.org"},{"key":"14_CR7","doi-asserted-by":"publisher","unstructured":"Beebe, N.: The Mathematical-Function Computation Handbook: Programming Using the MathCW Portable Software Library. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-64110-2","DOI":"10.1007\/978-3-319-64110-2"},{"issue":"4","key":"14_CR8","doi-asserted-by":"publisher","first-page":"839","DOI":"10.2307\/1968702","volume":"34","author":"A Church","year":"1933","unstructured":"Church, A.: A set of postulates for the foundation of logic. Ann. Math. 34(4), 839\u2013864 (1933). https:\/\/doi.org\/10.2307\/1968702","journal-title":"Ann. Math."},{"issue":"2","key":"14_CR9","doi-asserted-by":"publisher","first-page":"345","DOI":"10.2307\/2371045","volume":"58","author":"A Church","year":"1936","unstructured":"Church, A.: An unsolvable problem of elementary number theory. Am. J. Math. 58(2), 345\u2013363 (1936). https:\/\/doi.org\/10.2307\/2371045","journal-title":"Am. J. Math."},{"key":"14_CR10","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the ACM Symposium on Principles of Programming Languages, pp. 238\u2013252 (1977). https:\/\/doi.org\/10.1145\/512950.512973","DOI":"10.1145\/512950.512973"},{"key":"14_CR11","doi-asserted-by":"publisher","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of generalized type unions. In: Proceedings of an ACM Conference on Language Design for Reliable Software, pp. 77\u201394 (1977). https:\/\/doi.org\/10.1145\/800022.808314","DOI":"10.1145\/800022.808314"},{"issue":"4","key":"14_CR12","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/BF02551274","volume":"2","author":"G Cybenko","year":"1989","unstructured":"Cybenko, G.: Approximation by superpositions of a sigmoidal function. Math. Control Sig. Syst. 2(4), 303\u2013314 (1989). https:\/\/doi.org\/10.1007\/BF02551274","journal-title":"Math. Control Sig. Syst."},{"key":"14_CR13","unstructured":"Daramy-Loirat, C., et al.: CR-LIBM: a library of correctly rounded elementary functions in double-precision. Research Report ENSL-01529804, Laboratoire de l\u2019Informatique du Parall\u00e8lisme, December 2006. https:\/\/ens-lyon.hal.science\/ensl-01529804"},{"key":"14_CR14","doi-asserted-by":"publisher","unstructured":"Dettmers, T., Pagnoni, A., Holtzman, A., Zettlemoyer, L.: QLoRA: efficient finetuning of quantized LLMs. In: Proceedings of the International Conference on Neural Information Processing Systems (2023). https:\/\/doi.org\/10.5555\/3666122.3666563","DOI":"10.5555\/3666122.3666563"},{"key":"14_CR15","doi-asserted-by":"publisher","unstructured":"Ding, Y., Liu, J., Xiong, J., Shi, Y.: On the universal approximability and complexity bounds of quantized ReLU neural networks. In: International Conference on Learning Representations (2019). https:\/\/doi.org\/10.48550\/arXiv.1802.03646","DOI":"10.48550\/arXiv.1802.03646"},{"key":"14_CR16","doi-asserted-by":"publisher","unstructured":"Eykholt, K., et al.: Robust physical-world attacks on deep learning visual classification. In: Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition, pp. 1625\u20131634 (2018). https:\/\/doi.org\/10.1109\/CVPR.2018.00175","DOI":"10.1109\/CVPR.2018.00175"},{"key":"14_CR17","doi-asserted-by":"publisher","unstructured":"Faissole, F., de Lamarli\u00e8re, P.G., Melquiond, G.: End-to-end formal verification of a fast and accurate floating-point approximation. In: Proceedings of the International Conference on Interactive Theorem Proving, pp. 14:1\u201314:18 (2024). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2024.14","DOI":"10.4230\/LIPIcs.ITP.2024.14"},{"issue":"6433","key":"14_CR18","doi-asserted-by":"publisher","first-page":"1287","DOI":"10.1126\/science.aaw4399","volume":"363","author":"SG Finlayson","year":"2019","unstructured":"Finlayson, S.G., Bowers, J.D., Ito, J., Zittrain, J.L., Beam, A.L., Kohane, I.S.: Adversarial attacks on medical machine learning. Science 363(6433), 1287\u20131289 (2019). https:\/\/doi.org\/10.1126\/science.aaw4399","journal-title":"Science"},{"key":"14_CR19","doi-asserted-by":"publisher","unstructured":"Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, P., Chaudhuri, S., Vechev, M.T.: AI2: safety and robustness certification of neural networks with abstract interpretation. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 3\u201318 (2018). https:\/\/doi.org\/10.1109\/SP.2018.00058","DOI":"10.1109\/SP.2018.00058"},{"key":"14_CR20","unstructured":"G\u00f6del, K.: On undecidable propositions of formal mathematics systems (Notes by Kleene, S.C., Rosser, J.B.) Institute for Advanced Study (1934). https:\/\/albert.ias.edu\/20.500.12111\/7996"},{"issue":"6","key":"14_CR21","doi-asserted-by":"publisher","first-page":"3960","DOI":"10.1109\/TIT.2023.3240360","volume":"69","author":"A Gonon","year":"2023","unstructured":"Gonon, A., Brisebarre, N., Gribonval, R., Riccietti, E.: Approximation speed of quantized versus unquantized ReLU neural networks and beyond. IEEE Trans. Inf. Theory 69(6), 3960\u20133977 (2023). https:\/\/doi.org\/10.1109\/TIT.2023.3240360","journal-title":"IEEE Trans. Inf. Theory"},{"key":"14_CR22","unstructured":"Goodfellow, I.J., Bengio, Y., Courville, A.C.: Deep Learning. MIT Press (2016). http:\/\/www.deeplearningbook.org\/"},{"key":"14_CR23","doi-asserted-by":"publisher","unstructured":"Goodfellow, I.J., Shlens, J., Szegedy, C.: Explaining and harnessing adversarial examples. In: Proceedings of the International Conference on Learning Representations (2015). https:\/\/doi.org\/10.48550\/arXiv.1412.6572","DOI":"10.48550\/arXiv.1412.6572"},{"key":"14_CR24","doi-asserted-by":"publisher","unstructured":"Gowal, S., et al.: Scalable verified training for provably robust image classification. In: Proceedings of the IEEE International Conference on Computer Vision, pp. 4841\u20134850 (2019). https:\/\/doi.org\/10.1109\/ICCV.2019.00494","DOI":"10.1109\/ICCV.2019.00494"},{"key":"14_CR25","doi-asserted-by":"publisher","unstructured":"Grigore, R.: Java generics are Turing complete. In: Proceedings of the ACM Symposium on Principles of Programming Languages, pp. 73\u201385 (2017). https:\/\/doi.org\/10.1145\/3093333.3009871","DOI":"10.1145\/3093333.3009871"},{"issue":"5","key":"14_CR26","doi-asserted-by":"publisher","first-page":"1038","DOI":"10.1145\/502102.502106","volume":"48","author":"TJ Hickey","year":"2001","unstructured":"Hickey, T.J., Ju, Q., van Emden, M.H.: Interval arithmetic: from principles to implementation. J. ACM 48(5), 1038\u20131068 (2001). https:\/\/doi.org\/10.1145\/502102.502106","journal-title":"J. ACM"},{"issue":"5","key":"14_CR27","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1016\/0893-6080(89)90020-8","volume":"2","author":"K Hornik","year":"1989","unstructured":"Hornik, K., Stinchcombe, M., White, H.: Multilayer feedforward networks are universal approximators. Neural Netw. 2(5), 359\u2013366 (1989). https:\/\/doi.org\/10.1016\/0893-6080(89)90020-8","journal-title":"Neural Netw."},{"issue":"5","key":"14_CR28","doi-asserted-by":"publisher","first-page":"551","DOI":"10.1016\/0893-6080(90)90005-6","volume":"3","author":"K Hornik","year":"1990","unstructured":"Hornik, K., Stinchcombe, M., White, H.: Universal approximation of an unknown mapping and its derivatives using multilayer feedforward networks. Neural Netw. 3(5), 551\u2013560 (1990). https:\/\/doi.org\/10.1016\/0893-6080(90)90005-6","journal-title":"Neural Netw."},{"key":"14_CR29","doi-asserted-by":"publisher","unstructured":"Hubara, I., Courbariaux, M., Soudry, D., El-Yaniv, R., Bengio, Y.: Quantized neural networks: training neural networks with low precision weights and activations. J. Mach. Learn. Res. 18(1), 6869\u20136898 (2017). https:\/\/doi.org\/10.5555\/3122009.3242044","DOI":"10.5555\/3122009.3242044"},{"key":"14_CR30","unstructured":"Hwang, G., Park, Y., Lee, W., Park, S.: Floating-point neural networks can represent almost all floating-point functions. In: Proceedings of the International Conference on Machine Learning (2025)"},{"key":"14_CR31","doi-asserted-by":"publisher","unstructured":"Institute of Electrical and Electronics Engineers: IEEE Standard for Floating-Point Arithmetic (IEEE Std 754-2019). IEEE, Piscataway, NJ, USA (2019). https:\/\/doi.org\/10.1109\/IEEESTD.2019.8766229","DOI":"10.1109\/IEEESTD.2019.8766229"},{"key":"14_CR32","doi-asserted-by":"publisher","unstructured":"Jin, J., Ohrimenko, O., Rubinstein, B.I.P.: Getting a-round guarantees: floating-point attacks on certified robustness. In: Proceedings of the Workshop on Artificial Intelligence and Security, pp. 53\u201364 (2024). https:\/\/doi.org\/10.1145\/3689932.3694761","DOI":"10.1145\/3689932.3694761"},{"key":"14_CR33","doi-asserted-by":"publisher","unstructured":"Jovanovic, N., Balunovic, M., Baader, M., Vechev, M.T.: On the paradox of certified training. Trans. Mach. Learn. Res. (2022). https:\/\/doi.org\/10.48550\/arXiv.2102.06700","DOI":"10.48550\/arXiv.2102.06700"},{"key":"14_CR34","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":"14_CR35","doi-asserted-by":"publisher","unstructured":"Kozen, D.: Automata and Computability. Springer (1997). https:\/\/doi.org\/10.1007\/978-1-4612-1844-9","DOI":"10.1007\/978-1-4612-1844-9"},{"key":"14_CR36","doi-asserted-by":"publisher","unstructured":"Lee, W., Sharma, R., Aiken, A.: On automatically proving the correctness of math.h implementations. Proc. ACM Programm. Lang. 2(POPL), 47:1\u201347:32 (2018). https:\/\/doi.org\/10.1145\/3158135","DOI":"10.1145\/3158135"},{"key":"14_CR37","doi-asserted-by":"crossref","unstructured":"Li, L., Xie, T., Li, B.: Leaderboard for \u201cSoK: certified robustness for deep neural networks\u201d (2023). https:\/\/sokcertifiedrobustness.github.io\/leaderboard\/. Accessed 19 May 2025","DOI":"10.1109\/SP46215.2023.10179303"},{"key":"14_CR38","doi-asserted-by":"publisher","unstructured":"Li, L., Xie, T., Li, B.: SoK: certified robustness for deep neural networks. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 1289\u20131310. IEEE Press (2023). https:\/\/doi.org\/10.1109\/SP46215.2023.10179303","DOI":"10.1109\/SP46215.2023.10179303"},{"key":"14_CR39","doi-asserted-by":"publisher","unstructured":"Lim, J.P., Nagarakatte, S.: High performance correctly rounded math libraries for 32-bit floating point representations. In: Proceedings of the ACM Conference on Programming Languages Design and Implementation, pp. 359\u2013374 (2021). https:\/\/doi.org\/10.1145\/3453483.3454049","DOI":"10.1145\/3453483.3454049"},{"key":"14_CR40","doi-asserted-by":"publisher","unstructured":"Lim, J.P., Nagarakatte, S.: One polynomial approximation to produce correctly rounded results of an elementary function for multiple representations and rounding modes. Proc. ACM Programm. Lang. 6(POPL), 1\u201328 (2022). https:\/\/doi.org\/10.1145\/3498664","DOI":"10.1145\/3498664"},{"key":"14_CR41","unstructured":"Lin, H., Jegelka, S.: ResNet with one-neuron hidden layers is a universal approximator. In: Proceedings of the International Conference on Neural Information Processing Systems (2018). https:\/\/dl.acm.org\/doi\/10.5555\/3327345.3327515"},{"issue":"3\u20134","key":"14_CR42","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1561\/2400000035","volume":"4","author":"C Liu","year":"2021","unstructured":"Liu, C., Arnon, T., Lazarus, C., Strong, C.A., Barrett, C.W., Kochenderfer, M.J.: Algorithms for verifying deep neural networks. Found. Trends Optim. 4(3\u20134), 244\u2013404 (2021). https:\/\/doi.org\/10.1561\/2400000035","journal-title":"Found. Trends Optim."},{"key":"14_CR43","doi-asserted-by":"publisher","unstructured":"Mao, Y., M\u00fcller, M.N., Fischer, M., Vechev, M.T.: Understanding certified training with interval bound propagation. In: Proceedings of the International Conference on Learning Representations (2024). https:\/\/doi.org\/10.48550\/arXiv.2306.10426","DOI":"10.48550\/arXiv.2306.10426"},{"key":"14_CR44","unstructured":"Markstein, P.: IA-64 and Elementary Functions: Speed and Precision. Hewlett-Packard Professional Books, Prentice Hall (2000)"},{"key":"14_CR45","doi-asserted-by":"publisher","unstructured":"Micikevicius, P., et al.: Mixed precision training. In: International Conference on Learning Representations (2018). https:\/\/doi.org\/10.48550\/arXiv.1710.03740","DOI":"10.48550\/arXiv.1710.03740"},{"key":"14_CR46","doi-asserted-by":"publisher","unstructured":"Micikevicius, P., et\u00a0al.: FP8 formats for deep learning. arXiv 2209.05433 (2022). https:\/\/doi.org\/10.48550\/arXiv.2209.05433","DOI":"10.48550\/arXiv.2209.05433"},{"key":"14_CR47","unstructured":"Mirman, M., Baader, M., Vechev, M.T.: The fundamental limits of neural networks for interval certified robustness. Trans. Mach. Learn. Res. (2022). https:\/\/openreview.net\/forum?id=fsacLLU35V"},{"key":"14_CR48","unstructured":"Mirman, M., Gehr, T., Vechev, M.T.: Differentiable abstract interpretation for provably robust neural networks. In: Proceedings of the International Conference on Machine Learning (2018). http:\/\/proceedings.mlr.press\/v80\/mirman18b.html"},{"key":"14_CR49","doi-asserted-by":"publisher","DOI":"10.1093\/acprof:oso\/9780199233212.001.0001","author":"C Moore","year":"2011","unstructured":"Moore, C., Mertens, S.: The Nature of Computation. Oxford University Press (2011). https:\/\/doi.org\/10.1093\/acprof:oso\/9780199233212.001.0001","journal-title":"Oxford University Press"},{"key":"14_CR50","doi-asserted-by":"publisher","DOI":"10.1137\/1.9780898717716","author":"RE Moore","year":"2009","unstructured":"Moore, R.E., Kearfott, R.B., Cloud, M.J.: Introduction to interval analysis. Soc. Ind. Appl. Math. (2009). https:\/\/doi.org\/10.1137\/1.9780898717716","journal-title":"Soc. Ind. Appl. Math."},{"key":"14_CR51","doi-asserted-by":"publisher","unstructured":"Muller, J.: Elementary Functions: Algorithms and Implementation, 3rd edn. Birkh\u00e4user, Boston, MA (2016). https:\/\/doi.org\/10.1007\/978-1-4899-7983-4","DOI":"10.1007\/978-1-4899-7983-4"},{"key":"14_CR52","doi-asserted-by":"publisher","unstructured":"Muller, J.M., et al.: Handbook of Floating-Point Arithmetic. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-76526-6","DOI":"10.1007\/978-3-319-76526-6"},{"key":"14_CR53","doi-asserted-by":"publisher","DOI":"10.1016\/j.neunet.2024.106297","author":"Y Park","year":"2024","unstructured":"Park, Y., Hwang, G., Lee, W., Park, S.: Expressive power of ReLU and step networks under floating-point operations. Neural Netw. (2024). https:\/\/doi.org\/10.1016\/j.neunet.2024.106297","journal-title":"Neural Netw."},{"key":"14_CR54","unstructured":"P\u00e9rez, J., Barcel\u00f3, P., Marinkovic, J.: Attention is Turing-complete. J. Mach. Learn. Res. 22, 75:1\u201375:35 (2021). https:\/\/dl.acm.org\/doi\/10.5555\/3546258.3546333"},{"key":"14_CR55","doi-asserted-by":"publisher","unstructured":"Pinkus, A.: Approximation theory of the MLP model in neural networks. Acta Numerica 8, 143\u2013195 (1999). https:\/\/doi.org\/10.1017\/S0962492900002919","DOI":"10.1017\/S0962492900002919"},{"key":"14_CR56","unstructured":"Raghunathan, A., Steinhardt, J., Liang, P.: Semidefinite relaxations for certifying robustness to adversarial examples. In: Proceedings of the International Conference on Neural Information Processing Systems (2018). https:\/\/dl.acm.org\/doi\/10.5555\/3327546.3327746"},{"key":"14_CR57","doi-asserted-by":"publisher","unstructured":"Rosenberg, I., Shabtai, A., Elovici, Y., Rokach, L.: Adversarial machine learning attacks and defense methods in the cyber security domain. ACM Comput. Surv. 54(5) (2021). https:\/\/doi.org\/10.1145\/3453158","DOI":"10.1145\/3453158"},{"key":"14_CR58","doi-asserted-by":"publisher","unstructured":"Sibidanov, A., Zimmermann, P., Glondu, S.: The CORE-MATH project. In: Proceedings of the IEEE Symposium on Computer Arithmetic, pp. 26\u201334 (2022). https:\/\/doi.org\/10.1109\/ARITH54963.2022.00014","DOI":"10.1109\/ARITH54963.2022.00014"},{"issue":"1","key":"14_CR59","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1006\/jcss.1995.1013","volume":"50","author":"H Siegelmann","year":"1995","unstructured":"Siegelmann, H., Sontag, E.: On the computational power of neural nets. J. Comput. Syst. Sci. 50(1), 132\u2013150 (1995). https:\/\/doi.org\/10.1006\/jcss.1995.1013","journal-title":"J. Comput. Syst. Sci."},{"key":"14_CR60","doi-asserted-by":"publisher","unstructured":"Singh, G.: Building trust and safety in artificial intelligence with abstract interpretation. In: Hermenegildo, M.V., Morales, J.F. (eds.) Static Analysis, pp. 28\u201338. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-44245-2_3","DOI":"10.1007\/978-3-031-44245-2_3"},{"key":"14_CR61","unstructured":"Singh, G., Gehr, T., Mirman, M., P\u00fcschel, M., Vechev, M.T.: Fast and effective robustness certification. In: Proceedings of the International Conference on Neural Information Processing Systems (2018). https:\/\/dl.acm.org\/doi\/10.5555\/3327546.3327739"},{"key":"14_CR62","doi-asserted-by":"publisher","unstructured":"Singh, G., Gehr, T., P\u00fcschel, M., Vechev, M.T.: An abstract domain for certifying neural networks. Proc. ACM Programm. Lang. 3(POPL), 41:1\u201341:30 (2019). https:\/\/doi.org\/10.1145\/3290354","DOI":"10.1145\/3290354"},{"key":"14_CR63","doi-asserted-by":"publisher","unstructured":"Szegedy, C., et al.: Intriguing properties of neural networks. In: Proceedings of the International Conference on Learning Representations (2014). https:\/\/doi.org\/10.48550\/arXiv.1312.6199","DOI":"10.48550\/arXiv.1312.6199"},{"key":"14_CR64","doi-asserted-by":"publisher","unstructured":"Turing, A.M.: On computable numbers, with an application to the Entscheidungsproblem. Proc. London Math. Soc. s2-42(1), 230\u2013265 (1937). https:\/\/doi.org\/10.1112\/plms\/s2-42.1.230","DOI":"10.1112\/plms\/s2-42.1.230"},{"key":"14_CR65","doi-asserted-by":"publisher","unstructured":"Wang, N., Choi, J., Brand, D., Chen, C.Y., Gopalakrishnan, K.: Training deep neural networks with 8-bit floating point numbers. In: Proceedings of the International Conference on Neural Information Processing Systems (2018). https:\/\/doi.org\/10.5555\/3327757.3327866","DOI":"10.5555\/3327757.3327866"},{"key":"14_CR66","doi-asserted-by":"publisher","unstructured":"Wang, Z., Albarghouthi, A., Prakriya, G., Jha, S.: Interval universal approximation for neural networks. Proc. ACM Programm. Lang. 6(POPL), 14.1\u201314.29 (2022). https:\/\/doi.org\/10.1145\/3498675","DOI":"10.1145\/3498675"},{"key":"14_CR67","unstructured":"Wansbrough, K.: Instance declarations are universal (1998). http:\/\/www.lochan.org\/keith\/publications\/undec.html"},{"key":"14_CR68","doi-asserted-by":"publisher","unstructured":"Wong, E., Kolter, J.Z.: Provable defenses against adversarial examples via the convex outer adversarial polytope. In: Proceedings of the International Conference on Machine Learning (2018). https:\/\/doi.org\/10.48550\/arXiv.1711.00851","DOI":"10.48550\/arXiv.1711.00851"},{"key":"14_CR69","doi-asserted-by":"publisher","unstructured":"Yarotsky, D.: Optimal approximation of continuous functions by very deep ReLU networks. In: Proceedings of the Conference on Learning Theory (2018). https:\/\/doi.org\/10.48550\/arXiv.1802.03620","DOI":"10.48550\/arXiv.1802.03620"},{"key":"14_CR70","doi-asserted-by":"publisher","unstructured":"Yun, C., Bhojanapalli, S., Rawat, A.S., Reddi, S., Kumar, S.: Are transformers universal approximators of sequence-to-sequence functions? In: Proceedings of the International Conference on Learning Representations (2020). https:\/\/doi.org\/10.48550\/arXiv.1912.10077","DOI":"10.48550\/arXiv.1912.10077"},{"issue":"2","key":"14_CR71","doi-asserted-by":"publisher","first-page":"787","DOI":"10.1016\/j.acha.2019.06.004","volume":"48","author":"DX Zhou","year":"2020","unstructured":"Zhou, D.X.: Universality of deep convolutional neural networks. Appl. Comput. Harmon. Anal. 48(2), 787\u2013794 (2020). https:\/\/doi.org\/10.1016\/j.acha.2019.06.004","journal-title":"Appl. Comput. Harmon. Anal."},{"key":"14_CR72","unstructured":"Ziv, A., Olshansky, M., Henis, E., Retiman, A.: IBM accurate portable Mathlib (2001). https:\/\/github.com\/dreal-deps\/mathlib"}],"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_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,21]],"date-time":"2025-07-21T09:21:15Z","timestamp":1753089675000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98679-6_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"ISBN":["9783031986789","9783031986796"],"references-count":72,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98679-6_14","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\u00a0to 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"}}]}}