refined introduction

2 files changed, 103 insertions, 49 deletions

diff --git a/chapters/01-introduction.tex b/chapters/01-introduction.tex
index a6a69c5..8b912db 100644
--- a/chapters/01-introduction.tex
+++ b/chapters/01-introduction.tex
@@ -1,67 +1,106 @@
 \chapter{Introduction}
 \label{ch:introduction}
 
-This chapter provides an overview of the thesis.
-
 % Context
-Artificial Intelligence systems 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 their exceptional
-capacity of representing non-linear functions. But they don't come without drawbacks: neural
-networks are ``black boxes'' that lack transparency. To take advantage of these powerful tools in
-critical system guarantees need to be provided.
+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
-Neural networks can be viewed as mathematical functions and SMT solvers are used to check properties,
-like equivalence, against them. Running a solver against a complex function is computationally
-expensive, it is important to make sure that the function is simplified as much as possible to take
-away useless burden from the solver.
+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 if we want to replace 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
-We present VEIN, a framework that leverages the computational properties of interaction nets to
-perform symbolic simplification of neural networks prior to formal verification.
-The system is composed of two primary modules: a modified version of Inpla and the Z3 SMT solver for
-property validation.
-The tool is divided into three steps:
+To address the computational bottleneck, we can perform symbolic simplification 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{Translation}: a neural network in ONNX format is translated into an interaction net using
-		the Inpla string representation;
-	\item \textbf{Reduction}: the interaction net gets reduced to its normal form by Inpla;
-	\item \textbf{Evaluation}: the normal form gets processed along with the property to verify by Z3.
+	\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}
-Z3 is not optimized for ReLU splitting, but it was chosen for its mature Python package.
-In any case a specialized solver like Marabou can be integrated to improve performance.
-Our contributions are:
+The tool runtime follows three steps:
 \begin{itemize}
-	\item \textbf{Interaction Rules}: we designed a set of interaction rules to enable symbolic constant
-		folding;
-	\item \textbf{ONNX-Interaction Net Translation}: we developed a translation procedure for ONNX models to
-		interaction net;
-	\item \textbf{Soundness Analysis}: we provided a formal proof that the interaction net reduction preserves
-		the mathematical properties of the neural network;
-	\item \textbf{Experimental Evaluation}: we conducted an extensive benchmarking on widely known datasets and
-		common VNN-COMP datasets of varying complexity.
+	\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
-Our interaction nets pipeline soundness is proven by induction on the number of interaction steps,
-demonstrating that the ONNX translation and each interaction rule preserves the semantic meaning of
-the original neural network. Furthermore, interaction nets are deterministic and strongly confluent,
-meaning they will always reduce to the same normal form because interactions are local and linear. 
-In addition to this formal analysis, we conducted several benchmarks on checking equivalence between
-a neural network trained on a dataset and a transformation.
+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 to understand the contributions...
-	\begin{itemize}
-		\item \textbf{\Cref{sec:neural-networks}}: Introduces the concepts of neural networks and deep learning...
-		\item \textbf{\Cref{sec:interaction-nets}}: Introduces the interaction net computational model...
-		\item \textbf{\Cref{sec:satisfiability-modulo-theories}}: Introduces SMT solvers...
-	\end{itemize}
-	\item \textbf{\Cref{ch:core}}: Dives deeper into the implementation...
+	\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}
diff --git a/chapters/core/implementation/02-interaction-rules.tex b/chapters/core/implementation/02-interaction-rules.tex
index 1cf4d26..84dc27b 100644
--- a/chapters/core/implementation/02-interaction-rules.tex
+++ b/chapters/core/implementation/02-interaction-rules.tex
@@ -8,7 +8,7 @@ The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into t
 	\item
 		\textbf{Carriers}: Agents that contain float attributes.
 		\begin{itemize}
-			\item \textbf{Linear}: Represents the linear transformation $f(x) = q \cdot x + r$.
+			\item \textbf{Linear}: Represents the affine transformation $f(x) = q \cdot x + r$.
 			\item \textbf{Concrete}: Represents a constant value $k$.
 		\end{itemize}
 	\item
@@ -17,8 +17,8 @@ The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into t
 			\item \textbf{Add}: Binary operator for addition.
 			\item \textbf{Mul}: Binary operator for multiplication.
 			\item \textbf{ReLU}: Unary operator for rectified linear unit.
-			\item \textbf{Eraser}: Built-in Inpla unary operator to delete other agents.
-			\item \textbf{Duplicator}: Built-in Inpla unary operator to duplicate other agents.
+			\item \textbf{Eraser}: Built-in INPLA unary operator to delete other agents.
+			\item \textbf{Duplicator}: Built-in INPLA unary operator to duplicate other agents.
 		\end{itemize}
 	\item
 		\textbf{Intermediates}: Agents needed to perform each step of the operators.
@@ -227,7 +227,7 @@ enables short-circuiting. In \textbf{\Cref{fig:rule-concrete-add}} we can see th
 with $k=0$ we do not need to check the other operand and we simply wire it to the output.
 This rewiring is also implemented when multiplying a \textit{Concrete} with $k=1$, as shown in
 \textbf{\Cref{fig:rule-concrete-mul}}, with the addition that when $k=0$ the other operand is deleted
-before the SMT solver is even invoked.
+before is even invoked.
 
 % Concrete >< Add
 \begin{figure}[ht]
@@ -249,6 +249,7 @@ before the SMT solver is even invoked.
 				\node[right] at (AC.above pal) {$\mathit{b}$};
 				\node[left] at (AC.above pax) {$\mathit{out}$};
 			} \\
+			\hline
 			% k == 0
 			\interactionrule[$k=0$]{
 				\agentConcrete{C}{0}[90]
@@ -288,6 +289,7 @@ before the SMT solver is even invoked.
 				\node[right] at (MC.above pal) {$\mathit{b}$};
 				\node[left] at (MC.above pax) {$\mathit{out}$};
 			} \\
+			\hline
 			% k == 0
 			\interactionrule[$k=0$]{
 				\agentConcrete{C}{0}[90]
@@ -303,6 +305,7 @@ before the SMT solver is even invoked.
 				\node[right] at (C.above pal) {$\mathit{out}$};
 				\node[right] at (E.above pal) {$\mathit{b}$};
 			} \\
+			\hline
 			% k == 1
 			\interactionrule[$k=1$]{
 				\agentConcrete{C}{1}[90]
@@ -359,6 +362,7 @@ $q=1,r=0$.
 				\node[left] at (L2.above pax) {$\mathit{y}$};
 				\node[right] at (L3.above pal) {$\mathit{out}$};
 			} \\
+			\hline
 			% (s == 0) && (t == 0)
 			\interactionrule[$(s=0)\land(t=0)$]{
 				\agentLinear{L}{0}{0}[90]
@@ -376,6 +380,7 @@ $q=1,r=0$.
 				\node[right] at (L.above pal) {$\mathit{out}$};
 				\node[right] at (E.above pal) {$\mathit{y}$};
 			} \\
+			\hline
 			% (q == 0) && (r == 0)
 			\interactionrule[$(q=0)\land(r=0)$]{
 				\agentLinear{L}{s}{t}[90]
@@ -393,6 +398,7 @@ $q=1,r=0$.
 				\node[right] at (L.above pal) {$\mathit{out}$};
 				\node[right] at (E.above pal) {$\mathit{x}$};
 			} \\
+			\hline
 			% (q == 0) && (r == 0) && (s == 0) && (t == 0)
 			\interactionrule[$(q=0)\land(r=0)\land(s=0)\land(t=0)$]{
 				\agentLinear{L}{0}{0}[90]
@@ -444,6 +450,7 @@ $q=1,r=0$.
 				\node[left] at (L2.above pax) {$\mathit{y}$};
 				\node[right] at (L3.above pal) {$\mathit{out}$};
 			} \\
+			\hline
 			% ((q == 0) && (r == 0)) || ((s == 0) && (t == 0))
 			\interactionrule[$((q=0)\land(r=0))\lor((s=0)\land(t=0))$]{
 				\agentLinear{L}{s}{t}[90]
@@ -578,6 +585,7 @@ or short-circuited as illustrated in \textbf{\Cref{fig:rule-concrete-addcheckcon
 				\inetwirefree(C.pal)
 				\node[right] at (C.above pal) {$\mathit{out}$};
 			} \\
+			\hline
 			% j == 0
 			\interactionrule[$j=0$]{
 				\agentConcrete{C}{0}[90]
@@ -613,6 +621,7 @@ or short-circuited as illustrated in \textbf{\Cref{fig:rule-concrete-addcheckcon
 				\inetwirefree(C.pal)
 				\node[right] at (C.above pal) {$\mathit{out}$};
 			} \\
+			\hline
 			% j == 0
 			\interactionrule[$j = 0$]{
 				\agentConcrete{C}{0}[90]
@@ -625,6 +634,7 @@ or short-circuited as illustrated in \textbf{\Cref{fig:rule-concrete-addcheckcon
 				\inetwirefree(C.pal)
 				\node[right] at (C.above pal) {$\mathit{out}$};
 			} \\
+			\hline
 			% j == 1
 			\interactionrule[$j = 1$]{
 				\agentConcrete{C}{1}[90]
@@ -644,7 +654,7 @@ or short-circuited as illustrated in \textbf{\Cref{fig:rule-concrete-addcheckcon
 \end{figure}
 
 When the \textit{Linear} carrier agent interacts with the \textit{ReLU} operator agents there is no
-enough informations to perform any simplification so, as shown in \textbf{\Cref{fig:rule-linear-relu}},
+enough information to perform any simplification so, as shown in \textbf{\Cref{fig:rule-linear-relu}},
 the agent is just materialized, passed to a \textit{TermReLU} and then wrapped in a \textit{Linear}.
 In \textbf{\Cref{fig:rule-concrete-relu}} is illustrated that when the \textit{Concrete} carrier agent
 meets the \textit{ReLU} agent, a \textit{Concrete} is wired to the output either with attribute $k$
@@ -693,6 +703,7 @@ if $k>0$ or with attribute equal $0$ otherwise.
 				\inetwirefree(C.pal)
 				\node[right] at (C.above pal) {$\mathit{out}$};
 			} \\
+			\hline
 			% k > 0
 			\interactionrule[$k > 0$]{
 				\agentConcrete{C}{k}[90]
@@ -739,6 +750,7 @@ When a \textit{Concrete} needs to be materialized nothing needs to be done and i
 				\node [left] at (TM.above pax 2) {$\mathit{x}$};
 				\node [right] at (TA.above pal) {$\mathit{out}$};
 			} \\
+			\hline
 			% q == 0
 			\interactionrule[$q=0$]{
 				\agentLinear{L}{0}{r}[90]
@@ -754,6 +766,7 @@ When a \textit{Concrete} needs to be materialized nothing needs to be done and i
 				\node [right] at (C.above pal) {$\mathit{out}$};
 				\node [right] at (E.above pal) {$\mathit{x}$};
 			} \\
+			\hline
 			% (q == 1) && (r == 0)
 			\interactionrule[$(q=1)\land(r=0)$]{
 				\agentLinear{L}{1}{0}[90]
@@ -767,6 +780,7 @@ When a \textit{Concrete} needs to be materialized nothing needs to be done and i
 				\node(x) at (1, 0) {$\mathit{x}$};
 				\draw[\inetwirestyle] (x) -- (out);
 			} \\
+			\hline
 			% (q == 1) && (r != 0)
 			\interactionrule[$(q=1)\land(r\neq0)$]{
 				\agentLinear{L}{1}{r}[90]
@@ -783,6 +797,7 @@ When a \textit{Concrete} needs to be materialized nothing needs to be done and i
 				\node [left] at (TA.above pax 1) {$\mathit{x}$};
 				\node [right] at (TA.above pal) {$\mathit{out}$};
 			} \\
+			\hline
 			% (q != 0) && (r == 0)
 			\interactionrule[$(q\neq0)\land(r=0)$]{
 				\agentLinear{L}{q}{0}[90]