An Abstraction-Refinement Approach to Verification of Artificial Neural Networks

  • Luca Pulina
  • Armando Tacchella
Conference paper

DOI: 10.1007/978-3-642-14295-6_24

Volume 6174 of the book series Lecture Notes in Computer Science (LNCS)
Cite this paper as:
Pulina L., Tacchella A. (2010) An Abstraction-Refinement Approach to Verification of Artificial Neural Networks. In: Touili T., Cook B., Jackson P. (eds) Computer Aided Verification. CAV 2010. Lecture Notes in Computer Science, vol 6174. Springer, Berlin, Heidelberg

Abstract

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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Luca Pulina
    • 1
  • Armando Tacchella
    • 1
  1. 1.DISTUniversità di GenovaGenovaItaly