Neural Network Verification via Set Analysis

Verification Neural NetworkCopy link to section

Institution: École Polytechnique, LIX
Degree: Master 1 research project Date: March 26, 2024
Author: Nassim Arifette
Supervisors: Éric Goubault, Sylvie Putot

AbstractCopy link to section

This thesis addresses a critical challenge in artificial intelligence: how can we guarantee that neural networks will behave safely and correctly, especially in life-critical applications? As neural networks become more prevalent in autonomous vehicles, medical diagnosis, and financial systems, we need mathematical methods to prove their reliability rather than just testing them empirically.

The ProblemCopy link to section

Neural networks are essentially black boxes that can make unpredictable decisions when faced with slightly modified inputs. For instance, a medical diagnostic system should give the same diagnosis whether an image is slightly brighter or darker. However, verifying this property for all possible inputs is computationally impossible since there are infinitely many possible variations.

Our ApproachCopy link to section

This work investigates abstraction-based verification by working with sets of inputs rather than individual data points. Instead of testing every possible image variation, the study represents regions of similar inputs mathematically and asks which properties can be checked over those regions at once.

The thesis explores two complementary mathematical frameworks. The first approach uses zone analysis with difference bound matrices, which efficiently represent relationships between neural network variables using systems of linear inequalities. This method tracks how sets of inputs propagate through the network layers, maintaining mathematical guarantees about the network's behavior.

The second approach leverages tropical geometry, a mathematical framework where traditional arithmetic operations are replaced by max and addition operations. This perspective reveals that ReLU neural networks can be naturally expressed as tropical rational functions, providing new geometric insights into their decision boundaries and enabling more efficient verification algorithms.

Technical ContributionsCopy link to section

The zone-based verification method represents neural network states using difference bound matrices and studies closure algorithms that tighten these representations. For linear layers, the report characterizes how input regions transform through matrix operations. The ReLU activation function is approached through approximations designed to preserve sound bounds.

The tropical geometry approach demonstrates that ReLU networks correspond to tropical rational functions, where decision boundaries align with tropical hypersurfaces. This connection enables the development of verification algorithms that exploit the geometric structure of these networks, potentially offering computational advantages over traditional methods.

Practical ImplementationCopy link to section

Selected operations were prototyped in Julia, including zone closure, tropical arithmetic, and abstract network propagation. The report documents an exploratory implementation, not a complete production verifier; the end-to-end tropical verification routine remained preliminary.

Impact and ApplicationsCopy link to section

The study is motivated by safety-critical settings such as autonomous systems and medical decision support, where testing isolated examples is not enough. Its contribution is a mathematical and computational exploration of stronger guarantees, together with clear implementation work still required before deployment.