Top

Published in:

2023 | OriginalPaper | Chapter

Formalizing Piecewise Affine Activation Functions of Neural Networks in Coq

Authors : Andrei Aleksandrov, Kim Völlinger

Published in: NASA Formal Methods

Publisher: Springer Nature Switzerland

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Verification of neural networks relies on activation functions being piecewise affine (pwa)—enabling an encoding of the verification problem for theorem provers. In this paper, we present the first formalization of pwa activation functions for an interactive theorem prover tailored to verifying neural networks within Coq using the library Coquelicot for real analysis. As a proof-of-concept, we construct the popular pwa activation function ReLU. We integrate our formalization into a Coq model of neural networks, and devise a verified transformation from a neural network \(\mathcal {N}\) to a pwa function representing \(\mathcal {N}\) by composing pwa functions that we construct for each layer. This representation enables encodings for proof automation, e.g. Coq ’s tactic lra – a decision procedure for linear real arithmetic. Further, our formalization paves the way for integrating Coq in frameworks of neural network verification as a fallback prover when automated proving fails.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Verifying Attention Robustness of Deep Neural Networks Against Semantic Perturbations

next chapter Verifying an Aircraft Collision Avoidance Neural Network with Marabou

At https://github.com/verinncoq/formalizing-pwa with matrix_extensions.v (Sect. 2), piecewise_affine.v (Sect. 3.1), neuron_functions.v (Sect. 3.2), neural_networks.v (Sect. 4.1 and 4.4) and pwaf_operations.v (Sect. 4.2 and 4.3).

In literature often referred to as a convex, closed polyhedron.

A linear function is a special case of an affine function [32]. However, in literature, the term linear is sometimes used for both.

https://github.com/math-comp/analysis.

https://github.com/math-comp/algebra-tactics/pull/54.

Matrices involved are one-dimensional vectors since ReLU is one-dimensional. For technical reasons, in Coq, the spaces \(\mathbb {R}\) and \(\mathbb {R}^1\) differ with the latter working on one-dimensional vectors instead on scalars.

Mone is Coquelicot ’s identity matrix which in this case is a one-dimensional vector.

We use the customized identity function flex_dim_copy.

A bachelor thesis supervised by one of the authors and scheduled for publication.

Aggarwal, C.C.: Neural Networks, pp. 211–251. Springer, Cham (2021)

Albarghouthi, A.: Introduction to neural network verification. Found. Trends Program. Lang. 7(1–2), 1–157 (2021). https://doi.org/10.1561/2500000051

Bagnall, A., Stewart, G.: Certifying the true error: machine learning in coq with verified generalization guarantees. In: AAAI Conference on Artificial Intelligence (2019)

Bai, J., Lu, F., Zhang, K., et al.: ONNX: Open Neural Network Exchange. https://github.com/onnx/onnx (2019)

Bentkamp, A., Blanchette, J.C., Klakow, D.: A formal proof of the expressiveness of deep learning. J. Autom. Reas. (2019). https://doi.org/10.1007/s10817-018-9481-5

Boldo, S., Lelay, C., Melquiond, G.: Coquelicot: a user-friendly library of real analysis for Coq. Math. Comput. Sci. 9(1), 41–62 (2015)MathSciNetCrossRefMATH

Botoeva, E., Kouvaros, P., Kronqvist, J., Lomuscio, A., Misener, R.: Efficient verification of ReLU-based neural networks via dependency analysis. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 34, pp. 3291–3299 (2020). https://doi.org/10.1609/aaai.v34i04.5729

Brucker, A.D., Stell, A.: Verifying feedforward neural networks for classification in Isabelle/HOL. In: Proceedings of the 25th International Symposium on Formal Methods. Springer, Heidelberg (2023). https://doi.org/10.1007/978-3-031-27481-7_24

Bunel, R., Turkaslan, I., Torr, P.H., Kohli, P., Kumar, M.P.: A unified view of piecewise linear neural network verification. In: Proceedings of the 32nd International Conference on Neural Information Processing Systems, NIPS 2018, pp. 4795–4804. Curran Associates Inc., Red Hook (2018)

10.

Calin, O.: Deep Learning Architectures: A Mathematical Approach. Springer, Heidelberg (2020). https://doi.org/10.1007/978-3-030-36721-3

11.

Cybenko, G.: Approximation by superpositions of a sigmoidal function. Math. Control Signals Syst. 2(4), 303–314 (1989)MathSciNetCrossRefMATH

12.

De Moura, L., Bjørner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69–77 (2011)CrossRef

13.

Ehlers, R.: Formal verification of piece-wise linear feed-forward neural networks. In: Automated Technology for Verification and Analysis (2017)

14.

Gummersbach, L.: Ein verifizierter Converter für neuronale Netze von ONNX nach Coq. Bachelor’s thesis, Technische Universität Berlin (2023). to appear at Technische Universität Berlin

15.

Hanin, B.: universal function approximation by deep neural nets with bounded width and ReLU activations. Mathematics 7(10) (2019). https://doi.org/10.3390/math7100992

16.

Tran, H.-D., Bak, S., Xiang, W., Johnson, T.T.: Verification of deep convolutional neural networks using imagestars. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 18–42. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-53288-8_2CrossRefMATH

17.

Hornik, K.: Approximation capabilities of multilayer feedforward networks. Neural Netw. 4(2), 251–257 (1991)MathSciNetCrossRef

18.

Kruse, R., Mostaghim, S., Borgelt, C., Braune, C., Steinbrecher, M.: General Neural Networks, pp. 39–52. Springer, Cham (2022). https://doi.org/10.1007/978-1-4471-5013-8_4

19.

Lin, W., et al.: Robustness verification of classification deep neural networks via linear programming, pp. 11410–11419 (2019). https://doi.org/10.1109/CVPR.2019.01168

20.

Liu, C., Arnon, T., Lazarus, C., Strong, C., Barrett, C., Kochenderfer, M.J.: Algorithms for verifying deep neural networks. Found. Trends Optim. 4(3–4), 244–404 (2021). https://doi.org/10.1561/2400000035

21.

Montesinos López, O.A., Montesinos López, A., Crossa, J.: Fundamentals of artificial neural networks and deep learning. In: Multivariate Statistical Machine Learning Methods for Genomic Prediction, pp. 379–425. Springer, Cham (2022). https://doi.org/10.1007/978-3-030-89010-0_10CrossRef

22.

Montúfar, G., Pascanu, R., Cho, K., Bengio, Y.: On the number of linear regions of deep neural networks. In: Proceedings of the 27th International Conference on Neural Information Processing Systems, NIPS 2014, vol. 2, pp. 2924–2932. MIT Press, Cambridge (2014)

23.

Murphy, C., Gray, P., Stewart, G.: Verified perceptron convergence theorem. In: Proceedings of the 1st ACM SIGPLAN International Workshop on Machine Learning and Programming Languages, MAPL 2017, pp. 43–50. Association for Computing Machinery, New York (2017). https://doi.org/10.1145/3088525.3088673

24.

Rourke, C., Sanderson, B.: Introduction to Piecewise-Linear Topology. Springer, Heidelberg (1982). https://doi.org/10.1007/978-3-642-81735-9CrossRefMATH

25.

Scheibler, K., Winterer, L., Wimmer, R., Becker, B.: Towards verification of artificial neural networks. In: Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (2015)

26.

Scholtes, S.: Introduction to Piecewise Differentiable Equations. Springer, New York (2012). https://doi.org/10.1007/978-1-4614-4340-7CrossRefMATH

27.

Schrijver, A.: Combinatorial Optimization: Polyhedra and Efficiency. Springer, Heidelberg (2002)MATH

28.

Selsam, D., Liang, P., Dill, D.L.: Developing bug-free machine learning systems with formal mathematics. In: Proceedings of the 34th International Conference on Machine Learning, ICML2017, vol. 70, pp. 3047–3056. JMLR.org (2017)

29.

Team, T.C.D.: The Coq Proof Assistant (2022). https://doi.org/10.5281/zenodo.7313584

30.

Vanderbei, R.J.: Linear Programming: Foundations and Extensions. Springer, Heidelberg (2020). https://doi.org/10.1007/978-3-030-39415-8

31.

Vincent, J.A., Schwager, M.: Reachable polyhedral marching (RPM): a safety verification algorithm for robotic systems with deep neural network components. In: 2021 IEEE International Conference on Robotics and Automation (ICRA), pp. 9029–9035 (2021). https://doi.org/10.1109/ICRA48506.2021.9561956

32.

Yang, X.S.: Mathematical foundations. In: Yang, X.S. (ed.) Introduction to Algorithms for Data Mining and Machine Learning, pp. 19–43. Academic Press, Cambridge (2019). https://doi.org/10.1016/B978-0-12-817216-2.00009-0

33.

Ziegler, G.M.: Lectures on Polytopes. Springer, New York (1995). https://doi.org/10.1007/978-1-4613-8431-1

Title: Formalizing Piecewise Affine Activation Functions of Neural Networks in Coq
Authors: Andrei Aleksandrov
Kim Völlinger
Publisher: Springer Nature Switzerland
Book: NASA Formal Methods
Print ISBN: 978-3-031-33169-5

Electronic ISBN: 978-3-031-33170-1

Copyright Year: 2023
DOI: https://doi.org/10.1007/978-3-031-33170-1_4

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner