Counter-Example Guided Abstract Refinement for Verification of Neural Networks

In the last few decades, the employment of machine learning (ML) models has been increasingly common in the Artificial Intelligence community, with a particular focus on neural networks (NNs). However, even though they are widely adopted, the lack of formal guarantees on their behavior still restrain their use in safety-critical applications, such as avionics and self-driving vehicles. Formal Verification has been proposed to tackle the reliability issues of NNs, but its complexity and the sheer size of the models of interest have been proven to be hard challenges. In this paper we present an enhancement of our verification algorithm based on counter-example guided abstraction refinement (CEGAR) and show how it performs with respect to other approximate star-based methods.