refinement

1 files changed, 8 insertions, 8 deletions

diff --git a/chapters/05-conclusion.tex b/chapters/05-conclusion.tex
index 271c45a..b178b7f 100644
--- a/chapters/05-conclusion.tex
+++ b/chapters/05-conclusion.tex
@@ -8,12 +8,12 @@ a particular focus on network equivalence checking. The key achievements of this
 	\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
+		preserves the semantics of the original neural network.
+	\item An experimental evaluation verifying the effectiveness of \textbf{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
+While the current version of \textbf{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.
 
@@ -24,17 +24,17 @@ INPLA with a custom reduction engine written in Rust. Implementing the engine in
 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
+Currently, interaction net agents in \textbf{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.
+the framework to support complex attributes, such as tensors, boundary intervals and real numbers.
 
 \paragraph{Advanced Interaction Rules and Symbolic ReLU Pruning}
-The interaction rules implemented in VEIN are currently limited to constant folding of linear
+The interaction rules implemented in \textbf{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}.
+The current evaluation of \textbf{VEIN} targets the Z3 solver. However, the intermediate SMT-LIB
+representation can be easily adapted to other backends like Marabou.