\chapter{Conclusion and Future Work}
\label{ch:conclusion}

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}.
