\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 non-linear functions. But 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 kind of properties that can be verified are two:
\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 non-linear 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 a 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 a 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 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 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} (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 on
checking equivalence between a neural network trained on a dataset and a transformation.

% Contributions
The development of the 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}}: Introduces key concepts needed to understand the main work...
	\item \textbf{\Cref{ch:core}}: Dives deeper into the details...
	\item \textbf{\Cref{ch:related-work}}: Analyzes existing verification approaches...
	\item \textbf{\Cref{ch:conclusion}}: Summarizes the findings and discusses future work...
\end{itemize}