related work + conclusion

6 files changed, 127 insertions, 47 deletions

diff --git a/chapters/04-related-work.tex b/chapters/04-related-work.tex
index 1f01b8e..9378dd3 100644
--- a/chapters/04-related-work.tex
+++ b/chapters/04-related-work.tex
@@ -1,4 +1,31 @@
 \chapter{Related Work}
 \label{ch:related-work}
 
-% This chapter discusses related literature and positions this work within the field.
+The field of neural network verification is a highly active research area, driven by the need to
+provide formal safety for artificial intelligence applications in safety-critical systems.
+Existing verification techniques can be classified into complete and incomplete methods.
+
+\paragraph{Complete solvers}
+Complete verification methods guarantee to either find a counterexample violating the property or
+prove that the property holds. Katz et al.~\cite{katz2017reluplex} presented \textit{Reluplex}, a
+pioneering SMT solver designed specifically for networks with ReLU activation functions. It extends
+the standard simplex method, originally created by Dantzig~\cite{dantzig1947simplex}, to handle ReLU
+constraints directly. Katz et al.~\cite{katz2019marabou} also presented \textit{Marabou}, successor
+of \textit{Reluplex}, a more modular and highly optimized framework that supports a wider range of
+activation functions.
+
+\paragraph{Incomplete solvers}
+Incomplete verification methods use abstract interpretation to soundly approximate neural networks.
+Wang et al.~\cite{wang2018efficientformalsafetyanalysis} presented \textit{Neurify}, a tool that
+utilizes symbolic interval analysis to compute tight bounds on neurons and prune ReLUs that are
+guaranteed to be stably active or inactive.
+
+\paragraph{Hybrid solvers}
+\textit{$\alpha$-$\beta$-CROWN} is a neural network verifier that combines a series of complete
+verification methods, based on branch-and-bound, and incomplete verification methods, based on
+bound-propagation: \textit{CROWN} (Zhang et al.~\cite{zhang2018efficient}), \textit{auto\_LiRPA}
+(Xu et al.~\cite{xu2020automatic}), \textit{$\alpha$-CROWN} (Xu et al.~\cite{xu2021fast}),
+\textit{$\beta$-CROWN} (Wang et al.~\cite{wang2021beta}), \textit{GenBaB} (Shi et
+al~\cite{shi2024genbab}), \textit{GCP-CROWN} (Zhang et al~\cite{zhang2022general}) and
+\textit{BICCOS} (Zhou et al.~\cite{zhou2024scalable}). Thanks to this hybrid approach, 
+\textit{$\alpha$-$\beta$-CROWN} achieved state-of-the-art perfomance and won VNNCOMP 2021-2025.
diff --git a/chapters/05-conclusion.tex b/chapters/05-conclusion.tex
index d90f15c..271c45a 100644
--- a/chapters/05-conclusion.tex
+++ b/chapters/05-conclusion.tex
@@ -1,4 +1,40 @@
-\chapter{Conclusion}
+\chapter{Conclusion and Future Work}
 \label{ch:conclusion}
 
-% This chapter provides concluding remarks and potentially directions for future work.
+In this thesis, we introduced \textbf{VEIN}, a novel framework for neural network verification with
+a particular focus on network equivalence checking. The key achievements of this work include:
+\begin{itemize}
+	\item The formalization and implementation of an ONNX-to-IN translation pipeline.
+	\item The design of interaction rules implementing symbolic constant folding, constant
+		propagation, and identity elimination.
+	\item A soundness proof of the reduction engine, demonstrating that each graph rewriting step
+		preserves the semantic of the original neural network.
+	\item An experimental evaluation verifying the effectiveness of VEIN on multiple benchmarks
+		across strict, epsilon, and argmax equivalence metrics.
+\end{itemize}
+
+While the current version of VEIN establishes a solid foundation for IN-based verification, several
+limitations remain to be addressed in future research. The future roadmap focuses on performance
+optimizations, modeling expressiveness and advanced interaction rules.
+
+\paragraph{Custom Reduction Engine}
+The current reduction engine relies on a modified version of the INPLA interpreter. While
+practical, it is prone to high memory overhead. A core objective of future work is to replace
+INPLA with a custom reduction engine written in Rust. Implementing the engine in Rust will provide:
+memory safety without garbage collection, high-performance concurrency and flexibility.
+
+\paragraph{Complex Agent Attributes}
+Currently, interaction net agents in VEIN are limited to simple scalar attributes. This restriction
+prevents the direct translation of complex operations into single agents. Future work will extend
+the framework to support complex attributes, such as tensors and boundary intervals.
+
+\paragraph{Advanced Interaction Rules and Symbolic ReLU Pruning}
+The interaction rules implemented in VEIN are currently limited to constant folding of linear
+operations. Non-linear activation functions, specifically ReLUs, are passed through without
+modification unless their inputs are concrete constants. To improve simplification efficiency, we
+plan to implement range analysis and interval arithmetic directly within the IN, substantially
+reducing the number of split constraints faced by the SMT solver.
+
+\paragraph{Integration with Specialized Solvers}
+The current evaluation of VEIN targets the Z3 solver, the intermediate SMT-LIB representation can be
+adapted to other backends like Marabou~\cite{katz2019marabou}.
diff --git a/chapters/background/01-neural-networks.tex b/chapters/background/01-neural-networks.tex
index 848f65a..a1ecad2 100644
--- a/chapters/background/01-neural-networks.tex
+++ b/chapters/background/01-neural-networks.tex
@@ -2,7 +2,7 @@
 \label{sec:neural-networks}
 
 A neural network is a computational model inspired by biological neural networks. It consists of
-connected nodes called neuron, introduced in its early form by Rosenblatt et al.~\cite{rosenblatt1958perceptron}.
+connected nodes called neuron, introduced in its early form by Rosenblatt~\cite{rosenblatt1958perceptron}.
 \textit{Multi-Layer Perceptrons} is an architecture composed of sequential layers, trained using
 backpropagation as popularized by Rumelhart et al.~\cite{rumelhart1986learning}.
 
diff --git a/chapters/background/03-satisfiability-modulo-theories.tex b/chapters/background/03-satisfiability-modulo-theories.tex
index bd90559..a55d54d 100644
--- a/chapters/background/03-satisfiability-modulo-theories.tex
+++ b/chapters/background/03-satisfiability-modulo-theories.tex
@@ -19,6 +19,6 @@ To represent a ReLU activation $y = \max(0, x)$ in LRA, we must introduce a disj
     (x > 0 \land y = x) \lor (x \le 0 \land y = 0)
 \end{equation}
 For a network with $N$ ReLU neurons, there are up to $2^N$ possible activation patterns. Solving the
-verification property requires the SMT solver, such as Z3 presented by Demura et al.~\cite{demoura2008z3},
+verification property requires the SMT solver, such as Z3 presented by De Moura et al.~\cite{demoura2008z3},
 to implicitly explore this branching search space.
 
diff --git a/chapters/core/03-benchmarks.tex b/chapters/core/03-benchmarks.tex
index 132b56d..a8c1317 100644
--- a/chapters/core/03-benchmarks.tex
+++ b/chapters/core/03-benchmarks.tex
@@ -3,18 +3,17 @@
 
 This section contains the benchmark data, illustrated in \textbf{\Cref{tab:benchmarks}}.
 
-VEIN was tested on a laptop Zenbook UX3402ZA with:
+VEIN was tested with the following hardware:
 \begin{itemize}
-	\item \textbf{CPU}: 12th Gen Intel Core i5-1240P
-	\item \textbf{RAM}: 8GiB
-	\item \textbf{SWAP}: 16GiB on NVMe
+	\item \textbf{CPU}: AMD Ryzen 7 5700x3D
+	\item \textbf{RAM}: 16GiB
 \end{itemize}
 using Hyperfine\footnote{\href{https://github.com/sharkdp/hyperfine}{\textbf{Hyperfine Github repository}}.}
 benchmarking tool. Hyperfine runs the test ten times, then reports the mean and standard deviation of
 execution time.
 
 \paragraph{Iris}
-Dataset of iris flowers presented by Fisher et al.~\cite{fisher1936iris}. It consists of three
+Dataset of iris flowers presented by Fisher~\cite{fisher1936iris}. It consists of three
 species of flower (\textit{Iris setosa}, \textit{Iris virginica} and \textit{Iris versicolor}) with fifty samples each. Each
 sample has four features: width and length of sepals and petals.
 \paragraph{Pendulum}
@@ -48,38 +47,38 @@ define three kinds of equivalence:
 	\centering
 	\begin{tabular}[t]{ccccc}
 		\hline
-		Benchmark & Equivalence & Direct [s] & VEIN [s] & Status \\
+		Benchmark & Equivalence & Time & Status \\
 		\hline
-		Iris (Stably Active) & Strict & 0.0 & 0.0 & X \\
-		Iris (Stably Active) & Epsilon & 0.0 & 0.0 & X \\
-		Iris (Stably Active) & Argmax & 0.0 & 0.0 & X \\
-		Iris (Stably Inactive) & Strict & 0.0 & 0.0 & X \\
-		Iris (Stably Inactive) & Epsilon & 0.0 & 0.0 & X \\
-		Iris (Stably Inactive) & Argmax & 0.0 & 0.0 & X \\
-		Iris (To Wide) & Strict & 0.0 & 0.0 & X \\
-		Iris (To Wide) & Epsilon & 0.0 & 0.0 & X \\
-		Iris (To Wide) & Argmax & 0.0 & 0.0 & X \\
-		Iris (To Deep) & Strict & 0.0 & 0.0 & X \\
-		Iris (To Deep) & Epsilon & 0.0 & 0.0 & X \\
-		Iris (To Deep) & Argmax & 0.0 & 0.0 & X \\
-		Pendulum & Strict & 0.0 & 88.427 ± 0.670 & SAT \\
-		Pendulum & Epsilon & 0.0 & 0.0 & X \\
-		Pendulum & Argmax & 0.0 & 0.0 & X \\
-		Double Integrator & Strict & 0.0 & 0.0 & X \\
-		Double Integrator & Epsilon & 0.0 & 0.0 & X \\
-		Double Integrator & Argmax & 0.0 & 0.0 & X \\
-		MNIST (Stably Active) & Strict & 0.0 & 0.0 & X \\
-		MNIST (Stably Active) & Epsilon & 0.0 & 0.0 & X \\
-		MNIST (Stably Active) & Argmax & 0.0 & 0.0 & X \\
-		MNIST (Stably Inactive) & Strict & 0.0 & 0.0 & X \\
-		MNIST (Stably Inactive) & Epsilon & 0.0 & 0.0 & X \\
-		MNIST (Stably Inactive) & Argmax & 0.0 & 0.0 & X \\
-		MNIST (To Wide) & Strict & 0.0 & 0.0 & X \\
-		MNIST (To Wide) & Epsilon & 0.0 & 0.0 & X \\
-		MNIST (To Wide) & Argmax & 0.0 & 0.0 & X \\
-		MNIST (To Deep) & Strict & 0.0 & 0.0 & X \\
-		MNIST (To Deep) & Epsilon & 0.0 & 0.0 & X \\
-		MNIST (To Deep) & Argmax & 0.0 & 0.0 & X \\
+		Iris (Stably Active) & Strict & 521.6ms ± 11.5ms & SAT \\
+		Iris (Stably Active) & Epsilon & 515.9ms ± 4.2ms & UNSAT \\
+		Iris (Stably Active) & Argmax & 519.5ms ± 6.0ms & UNSAT \\
+		Iris (Stably Inactive) & Strict & 581.9ms ± 6.2ms & UNSAT \\
+		Iris (Stably Inactive) & Epsilon & 593.8ms ± 6.9ms & UNSAT \\
+		Iris (Stably Inactive) & Argmax & 886.4ms ± 10.3ms & UNSAT \\
+		Iris (To Wide) & Strict & 595.4ms ± 11.3ms & UNSAT \\
+		Iris (To Wide) & Epsilon & 587.0ms ± 4.9ms & UNSAT \\
+		Iris (To Wide) & Argmax & 783.5ms ± 4.4ms & UNSAT \\
+		Iris (To Deep) & Strict & 581.4ms ± 6.6ms & UNSAT \\
+		Iris (To Deep) & Epsilon & 583.1ms ± 5.7ms & UNSAT \\
+		Iris (To Deep) & Argmax & 716.3ms ± 4.7ms & UNSAT \\
+		Pendulum & Strict & 43.276s ± 0.143s & SAT \\
+		Pendulum & Epsilon & 340.293s ± 2.843s & UNSAT \\
+		Pendulum & Argmax & 61.935s ± 0.148s & SAT \\
+		Double Integrator & Strict & 538.952s ± 7.207s & SAT \\
+		Double Integrator & Epsilon & 137.720s ± 0.419s & SAT \\
+		Double Integrator & Argmax & 618.705s ± 6.821s & SAT \\
+		MNIST (Stably Active) & Strict & 18.947s ± 0.034s & SAT \\
+		MNIST (Stably Active) & Epsilon & 18.980s ± 0.032s & UNSAT \\
+		MNIST (Stably Active) & Argmax & 18.906s ± 0.019s & UNSAT \\
+		MNIST (Stably Inactive) & Strict & 14.699s ± 0.024s & UNSAT \\
+		MNIST (Stably Inactive) & Epsilon & 14.702s ± 0.012s & UNSAT \\
+		MNIST (Stably Inactive) & Argmax & TIMEOUT & UNKNOWN \\
+		MNIST (To Wide) & Strict & 20.990s ± 0.181s & UNSAT \\
+		MNIST (To Wide) & Epsilon & 20.860s ± 0.022s & UNSAT \\
+		MNIST (To Wide) & Argmax & TIMEOUT & UNKNOWN \\
+		MNIST (To Deep) & Strict & 20.901s ± 0.027s & UNSAT \\
+		MNIST (To Deep) & Epsilon & 20.947s ± 0.035s & UNSAT \\
+		MNIST (To Deep) & Argmax & TIMEOUT & UNKNOWN \\
 	\end{tabular}
 	\caption{Benchmark table.}
 	\label{tab:benchmarks}
diff --git a/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex b/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex
index be0870d..26f7e13 100644
--- a/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex
+++ b/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex
@@ -525,7 +525,11 @@
 \begin{lemma}
 	For the \textit{Linear} and \textit{Dup} agents we have the interaction rule:
 	$$
-	\mathit{Linear}(z, q, r) \bowtie \mathit{Dup}(x, y) \Rightarrow \mathit{Linear}(z_1, q, r) \sim x; \mathit{Linear}(z_2, q, r) \sim y; \mathit{Dup}(z_1, z_2) \sim z \\
+	\begin{aligned}
+		\mathit{Linear}(z, q, r) \bowtie \mathit{Dup}(x, y) \Rightarrow
+		& \mathit{Linear}(z_1, q, r) \sim x; \mathit{Linear}(z_2, q, r) \sim y;	\\
+		& \mathit{Dup}(z_1, z_2) \sim z
+	\end{aligned}
 	$$
 	We need to show that the LHS and RHS are semantically equivalent:
 	$$
@@ -667,8 +671,9 @@
 	For the \textit{TermMul} and \textit{Dup} agents we have the interaction rule:
 	$$
 	\begin{aligned}
-		\mathit{TermMul}(a, b) \bowtie \mathit{Dup}(x, y) \Rightarrow & \mathit{TermMul}(a_1, b_1) \sim x; \mathit{TermMul}(a_2, b_2) \sim y; \\
-		& \mathit{Dup}(a_1, a_2) \sim a; \mathit{Dup}(b_1, b_2) \sim b\\
+		\mathit{TermMul}(a, b) \bowtie \mathit{Dup}(x, y) \Rightarrow
+		& \mathit{TermMul}(a_1, b_1) \sim x; \mathit{TermMul}(a_2, b_2) \sim y; \\
+		& \mathit{Dup}(a_1, a_2) \sim a; \mathit{Dup}(b_1, b_2) \sim b
 	\end{aligned}
 	$$
 	We need to show that the LHS and RHS are semantically equivalent:
@@ -717,7 +722,12 @@
 \begin{lemma}
 	For the \textit{TermReLU} and \textit{Dup} agents we have the interaction rule:
 	$$
-	\mathit{TermReLU}(z) \bowtie \mathit{Dup}(x, y) \Rightarrow \mathit{TermReLU}(z_1) \sim x; \mathit{TermReLU}(z_2) \sim y; \mathit{Dup}(z_1, z_2) \sim z \\
+	\begin{aligned}
+		\mathit{TermReLU}(z) \bowtie \mathit{Dup}(x, y) \Rightarrow
+		& \mathit{TermReLU}(z_1) \sim x; \\
+		&\mathit{TermReLU}(z_2) \sim y; \\
+		& \mathit{Dup}(z_1, z_2) \sim z
+	\end{aligned}
 	$$
 	We need to show that the LHS and RHS are semantically equivalent:
 	$$
@@ -763,7 +773,11 @@
 \begin{lemma}
 	For the \textit{TermConcrete} and \textit{Dup} agents we have the interaction rule:
 	$$
-	\mathit{TermConcrete}(k) \bowtie \mathit{Dup}(x, y) \Rightarrow \mathit{TermConcrete}(k) \sim x; \mathit{TermConcrete}(k) \sim y \\
+	\begin{aligned}
+		\mathit{TermConcrete}(k) \bowtie \mathit{Dup}(x, y) \Rightarrow
+		& \mathit{TermConcrete}(k) \sim x; \\
+		& \mathit{TermConcrete}(k) \sim y
+	\end{aligned}
 	$$
 	We need to show that the LHS and RHS are semantically equivalent:
 	$$
@@ -807,7 +821,11 @@
 \begin{lemma}
 	For the \textit{TermSymbolic} and \textit{Dup} agents we have the interaction rule:
 	$$
-	\mathit{TermSymbolic}(id) \bowtie \mathit{Dup}(x, y) \Rightarrow \mathit{TermSymbolic}(id) \sim x; \mathit{TermSymbolic}(id) \sim y \\
+	\begin{aligned}
+		\mathit{TermSymbolic}(id) \bowtie \mathit{Dup}(x, y) \Rightarrow
+		& \mathit{TermSymbolic}(id) \sim x; \\
+		& \mathit{TermSymbolic}(id) \sim y
+	\end{aligned}
 	$$
 	We need to show that the LHS and RHS are semantically equivalent:
 	$$