1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
|
\chapter{Introduction}
\label{ch:introduction}
% Context
Artificial Intelligence systems have made significant advancements in the last few years and enabled
us to enter a new age of computing. Most of the credit goes to deep neural networks and to their
exceptional capacity for representing nonlinear functions. However, they do not come without
drawbacks: neural networks are ``black boxes'' that lack transparency. To take advantage of these
powerful tools in critical systems such as medicine and aerospace, we need to provide formal
guarantees to ensure their safety and trustworthiness.
% Problem
In the field of neural network verification, a verification problem is composed of a trained neural
network and a set of specifications. Then a verification algorithm checks whether the specifications
either hold or are violated. The two kinds of properties that can be verified are:
\begin{itemize}
\item \textbf{Single-Network}: We check if a single neural network satisfies a given property.
\item \textbf{Multi-Network}: We check if multiple neural networks satisfy a given relation.
\end{itemize}
An example of a Multi-Network property is equivalence between different neural networks; this
verification is crucial when replacing a neural network with a smaller, equivalent one. Techniques
based on specialized \textit{Satisfiability Modulo Theories} (SMT) solvers may be used in the verification
algorithm. However, as networks grow in depth and width, the number of nonlinear components, most
notably the \textit{Rectified Linear Unit}\footnote{Defined as $f(x)=\max(0, x)$, where $x$ is the input to the
neuron.} (ReLU) activation function, creates an exponential search space for the solver. Because of
this issue, running a solver against a raw, unoptimized network is often computationally prohibitive.
Furthermore, we lack a formal intermediate representation. Since we are
not able to directly feed a neural network to an SMT solver, a sound and deterministic model of
representation is needed to bridge this gap.
% Solution
To address the computational bottleneck, symbolic simplification is performed on the neural
network as a pre-processing step to reduce the burden on the SMT solver. Considering that we can
easily map the layers and neurons of neural networks to graph nodes and that the input of an SMT
solver is a mathematical formula that can be represented by an \textit{Abstract Syntax Tree} (AST), we can
use a graph rewriting system as an intermediate model. The motivation behind this choice is that
this type of model would enable us to simultaneously apply the simplification and produce the AST by
directly rewriting the graph obtained from the neural network.
To model such graphs and these rewriting mechanisms, we leverage \textit{Interaction Nets}
(IN)~\cite{lafont1990interactionnets}, a graphical model of computation characterized by local and
parallel graph rewriting rules. Additionally, IN are \textit{strongly confluent}, meaning that they
always reduce to a unique normal form regardless of the order in which simplification rules are
applied. Thanks to these properties, the simplification of neural network graphs can be parallelized
while maintaining the determinism of the resulting AST. In the context of neural network equivalence,
this is useful because comparing two neural networks becomes a comparison of two simplified
canonical forms of the same intermediate model.
Building on this capability, we developed
\textbf{VEIN}\footnote{\href{https://github.com/eric-marin/VEIN}{\textbf{VEIN Github repository.}}}
(VErification via Interaction Nets), a framework for neural network verification focused on
equivalence. This tool aims to verify both Single-Network and Multi-Network properties. The tool is
composed of two primary modules:
\begin{itemize}
\item \textbf{Reduction engine}: A modified version of \textit{Interaction Nets as a Programming
LAnguage}\footnote{\href{https://github.com/inpla/inpla}{\textbf{INPLA Github repository}}.}
(INPLA), a multi-threaded parallel interpreter of IN, to simplify the neural
network graph;
\item \textbf{Solver}: Z3~\cite{demoura2008z3} for property validation.
\end{itemize}
The tool runtime follows three steps:
\begin{itemize}
\item \textbf{Translation}: The system translates a neural network in \textit{Open Neural Network
Exchange}\footnote{\href{https://onnx.ai/}{\textbf{ONNX Website}}.}
(ONNX) file format, an open format built to represent machine learning models, into an IN;
\item \textbf{Reduction}: The INPLA engine reduces the IN to its normal form using the graph
rewriting rules that implement symbolic constant folding and identity elimination;
\item \textbf{Evaluation}: Then we parse the resulting normal form into Z3 representation and run the
solver to evaluate it along with the provided specification.
\end{itemize}
% Validation
We prove the soundness of our IN pipeline by induction on the number of interaction steps,
demonstrating that the ONNX translation and each interaction rule preserve the semantic meaning of
the original neural network. In addition to this formal analysis, we conducted several benchmarks to
check the equivalence between a neural network trained on a dataset and a transformation.
% Contributions
The development of the \textbf{VEIN} framework and the design of its underlying simplification layer
constitute the primary work of this thesis. To address the challenges of verification complexity (A)
and the need for a formal model of representation (B), this thesis introduces several key
contributions:
\begin{itemize}
\item \textbf{Interaction Rules (Solves A)}: We designed a set of interaction rules to enable graph
rewriting for symbolic constant folding while producing an AST ready to be parsed for the SMT
solver;
\item \textbf{ONNX-Interaction Net Translation (Solves B)}: We developed a translation procedure for ONNX
models to IN;
\item \textbf{Soundness Analysis (Validates A/B)}: We provide a formal proof that the IN reduction
preserves the mathematical properties of the neural network;
\item \textbf{Experimental Evaluation (Validates A/B Empirically)}: We conducted an extensive benchmarking
on widely known datasets and common \textit{International Verification of Neural Networks
Competition}\footnote{The premier international competition dedicated to evaluating and advancing
the state-of-the-art in neural network verification, see the
\href{https://vnn-comp.github.io/}{\textbf{website}}.} (VNN-COMP) datasets of varying complexity.
\end{itemize}
% Outline
\section{Outline}
\label{sec:outline}
This section outlines the organization of the thesis:
\begin{itemize}
\item \textbf{\Cref{ch:background}}: This chapter introduces key concepts needed to understand the
main work.
\item \textbf{\Cref{ch:core}}: This chapter dives deeper into the implementation details and
soundness proof.
\item \textbf{\Cref{ch:related-work}}: This chapter analyzes existing neural network verification
approaches.
\item \textbf{\Cref{ch:conclusion}}: This chapter summarizes the findings and discusses future
work.
\end{itemize}
|
