An Abstraction-Refinement Approach to Verification of Artificial Neural Networks
A key problem in the adoption of artificial neural networks in safety-related applications is that misbehaviors can be hardly ruled out with traditional analytical or probabilistic techniques. In this paper we focus on specific networks known as Multi-Layer Perceptrons (MLPs), and we propose a solution to verify their safety using abstractions to Boolean combinations of linear arithmetic constraints. We show that our abstractions are consistent, i.e., whenever the abstract MLP is declared to be safe, the same holds for the concrete one. Spurious counterexamples, on the other hand, trigger refinements and can be leveraged to automate the correction of misbehaviors. We describe an implementation of our approach based on the HySAT solver, detailing the abstraction-refinement process and the automated correction strategy. Finally, we present experimental results confirming the feasibility of our approach on a realistic case study.
KeywordsRoot Mean Square Error Hide Layer Input Vector Generalization Error Abstract Domain
Unable to display preview. Download preview PDF.
- 2.Smith, D.J., Simpson, K.G.L.: Functional Safety – A Straightforward Guide to applying IEC 61505 and Related Standards, 2nd edn. Elsevier, Amsterdam (2004)Google Scholar
- 3.Kurd, Z., Kelly, T., Austin, J.: Developing artificial neural networks for safety critical systems. Neural Computing & Applications 16(1), 11–19 (2007)Google Scholar
- 5.Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pp. 238–252 (1977)Google Scholar
- 6.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)Google Scholar
- 9.Pulina, L., Tacchella, A.: NEVER: A tool for Neural Network Verification (2010), http://www.mind-lab.it/never
- 10.Igel, C., Glasmachers, T., Heidrich-Meisner, V.: Shark. Journal of Machine Learning Research 9, 993–996 (2008)Google Scholar
- 11.Haykin, S.: Neural networks: a comprehensive foundation. Prentice Hall, Englewood Cliffs (2008)Google Scholar
- 12.Gordeau, R.: Roboop – a robotics object oriented package in C++ (2005), http://www.cours.polymtl.ca/roboop
- 14.Schumann, J., Gupta, P., Nelson, S.: On verification & validation of neural network based controllers. In: Proc. of International Conf. on Engineering Applications of Neural Networks, EANN’03 (2003)Google Scholar
- 16.Pappas, G., Kress-Gazit, H. (eds.): ICRA Workshop on Formal Methods in Robotics and Automation (2009)Google Scholar