Abstract
In this paper we evaluate state-of-the-art SMT solvers on encodings of verification problems involving Multi-Layer Perceptrons (MLPs), a widely used type of neural network. Verification is a key technology to foster adoption of MLPs in safety-related applications, where stringent requirements about performance and robustness must be ensured and demonstrated. While safety problems for MLPs can be attacked solving Boolean combinations of linear arithmetic constraints, the generated encodings are hard for current state-of-the-art SMT solvers, limiting our ability to verify MLPs in practice.
This research has received funding from the European Community’s Information and Communication Technologies Seventh Framework Programme [FP7/2007-2013] under grant agreement N. 215805, the CHRIS project.
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
Preview
Unable to display preview. Download preview PDF.
References
Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Satisfiability, pp. 825–885. IOS Press, Amsterdam (2009)
Fontaine, P., Marion, J.Y., Merz, S., Nieto, L., Tiu, A.: Expressiveness+ automation+ soundness: Towards combining SMT solvers and interactive proof assistants. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol. 3920, pp. 167–181. Springer, Heidelberg (2006)
DeLine, R., Leino, K.R.M.: BoogiePL: A typed procedural language for checking object-oriented programs (2005)
Ray, S.: Connecting External Deduction Tools with ACL2. In: Scalable Techniques for Formal Verification, pp. 195–216 (2010)
Armando, A., Mantovani, J., Platania, L.: Bounded model checking of software using SMT solvers instead of SAT solvers. International Journal on Software Tools for Technology Transfer (STTT) 11(1), 69–83 (2009)
Hoang, T.A., Binh, N.N.: Extending CREST with Multiple SMT Solvers and Real Arithmetic. In: 2010 Second International Conference on Knowledge and Systems Engineering (KSE), pp. 183–187. IEEE, Los Alamitos (2010)
Barrett, C., de Moura, L., Stump, A.: SMT-COMP: Satisfiability Modulo Theories Competition. In: Etessami, K., Rajamani, S. (eds.) CAV 2005. LNCS, vol. 3576, pp. 20–23. Springer, Heidelberg (2005)
Bishop, C.M.: Neural networks and their applications. Review of Scientific Instruments 65(6), 1803–1832 (2009)
Schumann, J., Liu, Y. (eds.): Applications of Neural Networks in High Assurance Systems. SCI, vol. 268. Springer, Heidelberg (2010)
Haykin, S.: Neural networks: a comprehensive foundation. Prentice Hall, Englewood Cliffs (2008)
Hornik, K., Stinchcombe, M., White, H.: Multilayer feedforward networks are universal approximators. Neural Networks 2(5), 359–366 (1989)
Cok, D.R.: The SMT-LIBv2 Language and Tools: A Tutorial (2011), http://www.grammatech.com/resources/smt/
Franzle, M., Herde, C., Teige, T., Ratschan, S., Schubert, T.: Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. Journal on Satisfiability, Boolean Modeling and Computation 1, 209–236 (2007)
Bruttomesso, R., Cimatti, A., Franzén, A., Griggio, A., Sebastiani, R.: The MathSAT 4 SMT Solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 299–303. Springer, Heidelberg (2008)
Dutertre, B., De Moura, L.: A fast linear-arithmetic solver for DPLL (T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006)
Fumagalli, M., Gijsberts, A., Ivaldi, S., Jamone, L., Metta, G., Natale, L., Nori, F., Sandini, G.: Learning to Exploit Proximal Force Sensing: a Comparison Approach. In: Sigaud, O., Peters, J. (eds.) From Motor Learning to Interaction Learning in Robots. SCI, vol. 264, pp. 149–167. Springer, Heidelberg (2010)
Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 298–302. Springer, Heidelberg (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pulina, L., Tacchella, A. (2011). Checking Safety of Neural Networks with SMT Solvers: A Comparative Evaluation. In: Pirrone, R., Sorbello, F. (eds) AI*IA 2011: Artificial Intelligence Around Man and Beyond. AI*IA 2011. Lecture Notes in Computer Science(), vol 6934. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-23954-0_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-23954-0_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-23953-3
Online ISBN: 978-3-642-23954-0
eBook Packages: Computer ScienceComputer Science (R0)