From dbdd3ea807232b0be83d6a0eba9eb13011eb48e5 Mon Sep 17 00:00:00 2001
From: ericmarin <maarin.eric@gmail.com>
Date: Sun, 21 Jun 2026 15:38:35 +0200
Subject: related work + conclusion

---
 chapters/05-conclusion.tex | 40 ++++++++++++++++++++++++++++++++++++++--
 1 file changed, 38 insertions(+), 2 deletions(-)

(limited to 'chapters/05-conclusion.tex')

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}.
-- 
cgit v1.2.3

