Abstract
The demand for formal verification tools for neural networks has increased as neural networks have been deployed in a growing number of safety-critical applications. Matrices are a data structure essential to formalising neural networks. Functional programming languages encourage diverse approaches to matrix definitions. This feature has already been successfully exploited in different applications. The question we ask is whether, and how, these ideas can be applied in neural network verification. A functional programming language Imandra combines the syntax of a functional programming language and the power of an automated theorem prover. Using these two key features of Imandra, we explore how different implementations of matrices can influence automation of neural network verification.
E. Komendantskaya—Acknowledges support of EPSRC grant EP/T026952/1.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Note that in these experiments, the implementation of weight matrices as lists of lists is implicit – we redefine matrix manipulation functions that are less general but more convenient for proofs by induction.
References
VNN (2022). https://sites.google.com/view/vnn2022
Lee, R., Jha, S., Mavridou, A., Giannakopoulou, D. (eds.): NFM 2020. LNCS, vol. 12229. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-55754-6
Bagnall, A., Stewart, G.: Certifying true error: machine learning in Coq with verified generalization guarantees. AAAI 33, 2662–2669 (2019)
Boyer, R.S., Moore, J.S.: A Computational Logic. ACM Monograph Series. Academic Press, New York (1979)
Casadio, M., et al.: Neural network robustness as a verification property: a principled case study. In: Computer Aided Verification (CAV 2022). Lecture Notes in Computer Science, Springer, Cham (2022) https://doi.org/10.1007/978-3-031-13185-1_11
Desmartin, R., Passmore, G., Komendantskaya, E., Daggitt, M.L.: CNN library in Imandra. https://github.com/aisec-private/ImandraNN (2022)
Dutta, S., Jha, S., Sankaranarayanan, S., Tiwari, A.: Output range analysis for deep feedforward neural networks. In: Dutle, A., Muñoz, C., Narkawicz, A. (eds.) NFM 2018. LNCS, vol. 10811, pp. 121–138. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-77935-5_9
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: S &P (2018)
Grant, P.W., Sharp, J.A., Webster, M.F., Zhang, X.: Sparse matrix representations in a functional language. J. Funct. Program. 6(1), 143–170 (1996). https://doi.org/10.1017/S095679680000160X, https://www.cambridge.org/core/journals/journal-of-functional-programming/article/sparse-matrix-representations-in-a-functional-language/669431E9C12EDC16F02603D833FAC31B, publisher: Cambridge University Press
Heras, J., Poza, M., Dénès, M., Rideau, L.: Incidence simplicial matrices formalized in Coq/SSReflect. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) CICM 2011. LNCS (LNAI), vol. 6824, pp. 30–44. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22673-1_3
Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24–28, 2017, Proceedings, Part I. Lecture Notes in Computer Science, vol. 10426, pp. 3–29 (2017)
Katz, G., Barrett, C., Dill, D., Ju-lian, K., Kochenderfer, M.: Reluplex: an Efficient SMT solver for verifying deep neural networks. In: CAV (2017)
Katz, G., et al.: The marabou framework for verification and analysis of deep neural networks. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 443–452. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-25540-4_26
Kokke, W., Komendantskaya, E., Kienitz, D., Atkey, R., Aspinall, D.: Neural networks, secure by construction. In: Oliveira, B.C.S. (ed.) APLAS 2020. LNCS, vol. 12470, pp. 67–85. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-64437-6_4
LeCun, Y., Denker, J., Solla, S.: Optimal Brain Damage. In: Advances in Neural Information Processing Systems, vol. 2. Morgan-Kaufmann (1989). https://papers.nips.cc/paper/1989/hash/6c9882bbac1c7093bd25041881277658-Abstract.html
De Maria, E., et al.: On the use of formal methods to model and verify neuronal archetypes. Front. Comput. Sci. 16(3), 1–22 (2022). https://doi.org/10.1007/s11704-020-0029-6
Passmore, G., et al.: The Imandra automated reasoning system (System Description). In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12167, pp. 464–471. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-51054-1_30
Passmore, G.O.: Some lessons learned in the industrialization of formal methods for financial algorithms. In: Huisman, M., Păsăreanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 717–721. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-90870-6_39
Sill, J.: Monotonic Networks. California Institute of Technology, Pasadena (1998)
Singh, G., Gehr, T., Püschel, M., Vechev, M.T.: An abstract domain for certifying neural networks. PACMPL 3(POPL), 41:1–41:30 (2019). https://doi.org/10.1145/3290354
Wehenkel, A., Louppe, G.: Unconstrained monotonic neural networks. In: Advances in Neural Information Processing Systems : Annual Conference on Neural Information Processing Systems 2019, IPS 2019, December 8–14, 2019, Vancouver, BC, Canada 32, pp. 1543–1553 (2019)
Wood, J.: Vectors and Matrices in Agda (Aug 2019). https://personal.cis.strath.ac.uk/james.wood.100/blog/html/VecMat.html
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2022 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Desmartin, R., Passmore, G., Kommendentskaya, E. (2022). Neural Networks in Imandra: Matrix Representation as a Verification Choice. In: Isac, O., Ivanov, R., Katz, G., Narodytska, N., Nenzi, L. (eds) Software Verification and Formal Methods for ML-Enabled Autonomous Systems. NSV FoMLAS 2022 2022. Lecture Notes in Computer Science, vol 13466. Springer, Cham. https://doi.org/10.1007/978-3-031-21222-2_6
Download citation
DOI: https://doi.org/10.1007/978-3-031-21222-2_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-21221-5
Online ISBN: 978-3-031-21222-2
eBook Packages: Computer ScienceComputer Science (R0)