diff options
| -rw-r--r-- | chapters/01-introduction.tex | 32 | ||||
| -rw-r--r-- | chapters/03-core.tex | 2 | ||||
| -rw-r--r-- | chapters/04-related-work.tex | 25 | ||||
| -rw-r--r-- | chapters/05-conclusion.tex | 16 | ||||
| -rw-r--r-- | chapters/background/01-neural-networks.tex | 11 | ||||
| -rw-r--r-- | chapters/background/02-interaction-nets.tex | 18 | ||||
| -rw-r--r-- | chapters/background/03-satisfiability-modulo-theories.tex | 11 | ||||
| -rw-r--r-- | chapters/core/03-benchmarks.tex | 140 | ||||
| -rw-r--r-- | chapters/core/implementation/01-inpla.tex | 8 | ||||
| -rw-r--r-- | chapters/core/implementation/02-interaction-rules.tex | 6 | ||||
| -rw-r--r-- | chapters/core/implementation/03-translation.tex | 7 | ||||
| -rw-r--r-- | chapters/core/implementation/04-python-module.tex | 6 | ||||
| -rw-r--r-- | chapters/core/soundness-proof/02-soundness-of-translation.tex | 3 | ||||
| -rw-r--r-- | chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex | 95 | ||||
| -rw-r--r-- | chapters/core/soundness-proof/04-soundness-of-reduction.tex | 40 | ||||
| -rw-r--r-- | main.tex | 17 |
16 files changed, 254 insertions, 183 deletions
diff --git a/chapters/01-introduction.tex b/chapters/01-introduction.tex index 8f46660..47b7d57 100644 --- a/chapters/01-introduction.tex +++ b/chapters/01-introduction.tex @@ -4,15 +4,15 @@ % Context 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. +exceptional capacity for representing non-linear functions. However, 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 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: +either hold or are violated. The two kinds of properties that can be verified are: \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. @@ -26,16 +26,16 @@ neuron.} (ReLU) activation function, creates an exponential search space for the 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 +not able to directly feed a neural network to an SMT solver, a sound and deterministic model of representation is needed to bridge this gap. % Solution To address the computational bottleneck, symbolic simplification is performed 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 +easily map the layers and neurons of neural networks to graph nodes and that the input of an 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 +use a graph rewriting system as an 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 @@ -74,7 +74,7 @@ the original neural network. In addition to this formal analysis, we conducted s 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 +The development of the \textbf{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: @@ -98,8 +98,12 @@ contributions: \label{sec:outline} This section outlines the organization of the thesis: \begin{itemize} - \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... + \item \textbf{\Cref{ch:background}}: This chapter introduces key concepts needed to understand the + main work. + \item \textbf{\Cref{ch:core}}: This chapter dives deeper into the implementation details and + soundness proof. + \item \textbf{\Cref{ch:related-work}}: This chapter analyzes existing neural network verification + approaches. + \item \textbf{\Cref{ch:conclusion}}: This chapter summarizes the findings and discusses future + work. \end{itemize} diff --git a/chapters/03-core.tex b/chapters/03-core.tex index 170cf06..c222f0d 100644 --- a/chapters/03-core.tex +++ b/chapters/03-core.tex @@ -1,4 +1,4 @@ -\chapter{VEIN: VErification via Interaction Nets} +\chapter{VEIN} \label{ch:core} This chapter contains details on framework implementation (\textbf{\Cref{sec:implementation}}), the diff --git a/chapters/04-related-work.tex b/chapters/04-related-work.tex index 9378dd3..d43cb0e 100644 --- a/chapters/04-related-work.tex +++ b/chapters/04-related-work.tex @@ -9,10 +9,10 @@ Existing verification techniques can be classified into complete and incomplete 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. +the standard simplex method, originally created by Dantzig (as described by +Nash~\cite{dantzig1947simplex}), to handle ReLU constraints directly. Katz et +al.~\cite{katz2019marabou} also presented \textit{Marabou}, the 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. @@ -22,10 +22,19 @@ 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} +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 +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. +\textit{$\alpha$-$\beta$-CROWN} achieved state-of-the-art performance and won VNNCOMP 2021-2025. + +\paragraph{Equivalence Checking} +Closest to the scope of this work, Eleftheriadis et al.~\cite{eleftheriadis2022equivalence} study +the problem of neural network equivalence checking using SMT solvers, and define the notions of +strict, epsilon, and argmax equivalence adopted in \textbf{\Cref{sec:benchmarks}}. They approach the +equivalence problem by directly encoding an SMT formula and relying on internal heuristics of the +solver to handle the search space. Instead, \textbf{VEIN} introduces an explicit, formally verified +preprocessing stage that reduces the networks to a normal form before encoding it into an SMT +formula. 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. diff --git a/chapters/background/01-neural-networks.tex b/chapters/background/01-neural-networks.tex index a1ecad2..dc3e2d4 100644 --- a/chapters/background/01-neural-networks.tex +++ b/chapters/background/01-neural-networks.tex @@ -2,8 +2,8 @@ \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~\cite{rosenblatt1958perceptron}. -\textit{Multi-Layer Perceptrons} is an architecture composed of sequential layers, trained using +connected nodes called neurons, introduced in its early form by Rosenblatt~\cite{rosenblatt1958perceptron}. +The \textit{Multi-Layer Perceptrons} is an architecture composed of sequential layers, trained using backpropagation as popularized by Rumelhart et al.~\cite{rumelhart1986learning}. \subsection{Neuron} @@ -51,7 +51,7 @@ The output $y$ is defined as: \draw[->] (act) -- (y); \end{tikzpicture} - \caption{Mathematical model of an artificial neuron.} + \caption{Graphical representation of a neuron.} \label{fig:single-neuron} \end{figure} @@ -101,14 +101,15 @@ the outputs. \node[above] at (7, 1.2) {Output Layer}; \end{tikzpicture} - \caption{Architecture of a Multi-Layer Perceptron (MLP) with one hidden layer.} + \caption{Architecture of an MLP with one hidden layer.} \label{fig:mlp} \end{figure} -One of the most common activation function is the ReLU, defined as: +One of the most common activation functions is the ReLU, defined as: \begin{equation} \text{ReLU}(z) = \max(0, z) \end{equation} +The framework focuses on MLP with ReLU activation functions. \subsection{Neural Network Verification} The verification problem of a neural network $F: \mathbb{R}^n \to \mathbb{R}^m$ with input constraint diff --git a/chapters/background/02-interaction-nets.tex b/chapters/background/02-interaction-nets.tex index 36a7a32..874110e 100644 --- a/chapters/background/02-interaction-nets.tex +++ b/chapters/background/02-interaction-nets.tex @@ -1,11 +1,11 @@ \section{Interaction Nets} \label{sec:interaction-nets} -Interaction Nets, introduced by Yves Lafont et al.~\cite{lafont1990interactionnets}, are a +\textit{Interaction Nets} (IN), introduced by Lafont~\cite{lafont1990interactionnets}, are a graphical model of computation based on graph rewriting. \subsection{Basic Concepts} -An interaction net is an undirected graph with labelled vertices, called \textit{agents}. Each agent +An IN is an undirected graph with labelled vertices, called \textit{agents}. Each agent is an instance of a \textit{symbol}, which has a principal port and a fixed number of auxiliary ports: \begin{figure}[H] \centering @@ -16,11 +16,12 @@ is an instance of a \textit{symbol}, which has a principal port and a fixed numb \node[left] at (A.above pax 2) {$\mathit{y}$}; \node[right] at (A.above pal) {$\mathit{x}$}; \end{tikzpicture} - \caption{Example of an agent \textit{Add} with two auxiliary ports.} + \caption{Example of an agent \textit{Add} with two auxiliary ports connected to $x, y, z$ wires.} \label{fig:agent} \end{figure} -Each port can be wired to at most one other port. When two different agents are wired to their respective principal ports they are called an \textit{active pair}: +Each port can be wired to at most one other port. When two different agents are wired to their +respective principal ports they are called an \textit{active pair}: \begin{figure}[H] \centering @@ -38,8 +39,8 @@ Each port can be wired to at most one other port. When two different agents are \end{figure} \subsection{Interaction Rules} -Computation in interaction nets proceeds by rewriting the net using local \emph{interaction rules}. A rule -is defined only for an active pair and, for any pair of agent types, there is at most one +Computation in IN proceeds by rewriting the net using local \emph{interaction rules}. A rule +is defined only for an active pair and for any pair of symbols there is at most one interaction rule. \begin{figure}[H] @@ -66,10 +67,11 @@ interaction rule. \end{figure} \subsection{Properties} -Interaction nets possess the following properties: +IN possess the following properties: \begin{itemize} \item \textbf{Locality}: only active pairs can be rewritten. - \item \textbf{Linearity}: each interaction rule can be applied in constant time. + \item \textbf{Linearity}: each interaction rule rewrites a constant-size subgraph, independent of + the overall size of the net. \item \textbf{Strong Confluence}: given a net $\text{IN}$ that can reduce to $\text{IN}_1$ and $\text{IN}_2$ in one step, then both $\text{IN}_1$ and $\text{IN}_2$ reduce to some net $\text{IN}'$ in one step. \end{itemize} diff --git a/chapters/background/03-satisfiability-modulo-theories.tex b/chapters/background/03-satisfiability-modulo-theories.tex index a55d54d..80e9932 100644 --- a/chapters/background/03-satisfiability-modulo-theories.tex +++ b/chapters/background/03-satisfiability-modulo-theories.tex @@ -1,7 +1,7 @@ \section{Satisfiability Modulo Theories} \label{sec:satisfiability-modulo-theories} -Satisfiability Modulo Theories (SMT) is the problem of determining whether a mathematical formula is +\textit{Satisfiability Modulo Theories} (SMT) is the problem of determining whether a mathematical formula is satisfiable within a certain formal theory in first-order logic. Barrett et al.~\cite{barrett2016smtlib} defined the SMT-LIB standard for input format and theory definitions. @@ -11,14 +11,13 @@ multiplication by constants, and equality/inequality relations: \begin{equation} \phi ::= t_1 \sim t_2 \mid \phi_1 \lor \phi_2 \mid \phi_1 \land \phi_2 \mid \neg \phi_1 \end{equation} -where $t_1, t_2$ are linear terms of the form $c_1 x_1 + \dots + c_k x_k + c_0$ (with $c_i \in \mathbb{R}$ and $x_i$ being real +where $t_1, t_2$ are linear terms of the form $c_1 \cdot x_1 + \dots + c_k \cdot x_k + c_0$ (with $c_i \in \mathbb{R}$ and $x_i$ being real variables), and $\sim \;\in \{=, \le, <, \ge, >\}$. To represent a ReLU activation $y = \max(0, x)$ in LRA, we must introduce a disjunction: \begin{equation} (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 De Moura et al.~\cite{demoura2008z3}, -to implicitly explore this branching search space. - +For a network with $n$ ReLU neurons, there are up to $2^n$ possible activation patterns. Solving the +verification problem 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 a8c1317..31b61a7 100644 --- a/chapters/core/03-benchmarks.tex +++ b/chapters/core/03-benchmarks.tex @@ -3,83 +3,101 @@ This section contains the benchmark data, illustrated in \textbf{\Cref{tab:benchmarks}}. -VEIN was tested with the following hardware: +\textbf{VEIN} was tested with the following hardware: \begin{itemize} \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~\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} -A neural safety certificate for stabilizing a pendulum to its upright position under a bound on its -angle $\theta$, with state $x=[\theta,\dot\theta]\in\mathbb{R}^2$ and nonlinear dynamics. -\paragraph{Double Integrator} -A neural safety certificate for stabilizing a second-order linear system to the origin under a bound -on its position $p$, with state $x=[p,\dot p]\in\mathbb{R}^2$. -\paragraph{MNIST} -Widely known dataset of handwritten digits presented by LeCun et al.~\cite{lecun2010mnist}. It -consists of 60'000 training images and 10'000 testing images. +using the 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. For longer runs, only execution is reported. We defined the following benchmarks: +\begin{itemize} + \item \textbf{Iris}: Network trained on the Iris flowers dataset 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. + \item \textbf{Pendulum}: A neural safety certificate for stabilizing a pendulum to its upright position + under a bound on its angle $\theta$, with state $x=[\theta,\dot\theta]\in\mathbb{R}^2$. + \item \textbf{Double Integrator}: A neural safety certificate for stabilizing a second-order linear system + to the origin under a bound on its position $p$, with state $x=[p,\dot p]\in\mathbb{R}^2$. + \item \textbf{MNIST}: Network trained on the widely known dataset of handwritten digits presented by + LeCun et al.~\cite{lecun2010mnist}. It consists of 60'000 training images and 10'000 testing + images. +\end{itemize} Pendulum and Double Integrator are taken from \textit{cersyve}, a benchmark presented by Kaulen et al.~\cite{kaulen20256thinternationalverificationneural}. We check equivalence between a pre-trained and a fine-tuned network for each task. -In the Iris and MNIST dataset, we tested equivalence between a NN and its ad-hoc transformation, -such as pruning always positive or negative ReLUs, as presented by Kumar et al.~\cite{kumar2019equivalentapproximatetransformationsdeep}, -or changing the architecture from wide to deep and viceversa, as presented by Fan et al.~\cite{JMLR:v24:21-0579}. +In the Iris and MNIST datasets, we tested equivalence between a neural network and its ad-hoc +transformation, such as pruning always positive or negative ReLUs, as presented by Kumar et +al.~\cite{kumar2019equivalentapproximatetransformationsdeep}, or changing the architecture from wide +to deep and viceversa, as presented by Fan et al.~\cite{JMLR:v24:21-0579}. -For two NN $F: \mathbb{R}^n \to \mathbb{R}^m$ and $F': \mathbb{R}^n \to \mathbb{R}^m$, Eleftheriadis et al.~\cite{eleftheriadis2022equivalence} -define three kinds of equivalence: +For two neural networks $F: \mathbb{R}^n \to \mathbb{R}^m$ and $F': \mathbb{R}^n \to \mathbb{R}^m$, Eleftheriadis et +al.~\cite{eleftheriadis2022equivalence} define three kinds of equivalence: \begin{itemize} - \item \textbf{Strict equivalence}: $\forall x \in \mathbb{R}^n \quad F(x) = F'(x)$. - \item \textbf{Epsilon equivalence}: $\forall x \in \mathbb{R}^n \quad ||F(x) - F'(x)|| < \epsilon$ for some $\epsilon > 0$. - \item \textbf{Argmax equivalence}: $\forall x \in \mathbb{R}^n \quad \mathtt{argmax}(F(x))=\mathtt{argmax}(F'(x))$ where \texttt{argmax} + \item \textbf{Strict equivalence}: $\forall x \in \mathbb{R}^n \; F(x) = F'(x)$. + \item \textbf{Epsilon equivalence}: $\forall x \in \mathbb{R}^n \; ||F(x) - F'(x)|| < \epsilon$ for some $\epsilon > 0$. + \item \textbf{Argmax equivalence}: $\forall x \in \mathbb{R}^n \; \mathtt{argmax}(F(x))=\mathtt{argmax}(F'(x))$ where \texttt{argmax} is the function that returns the index of the maximum value of a vector. \end{itemize} +We compare the verification time between a direct translation of the ONNX network into a Z3 formula +and the \textbf{VEIN} framework. + \begin{table}[H] \centering - \begin{tabular}[t]{ccccc} - \hline - Benchmark & Equivalence & Time & Status \\ - \hline - 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} + \resizebox{\textwidth}{!}{ + \begin{tabular}[t]{ccccc} + \hline + Benchmark & Equivalence & Direct & VEIN & Status \\ + \hline + Iris (Stably Active) & Strict & 265.2ms ± 6.8ms & 521.6ms ± 11.5ms & SAT \\ + Iris (Stably Active) & Epsilon $\epsilon=0.1$ & 271.4ms ± 5.2ms & 515.9ms ± 4.2ms & UNSAT \\ + Iris (Stably Active) & Argmax & 267.9ms ± 9.5ms & 519.5ms ± 6.0ms & UNSAT \\ + Iris (Stably Inactive) & Strict & 278.3ms ± 7.7ms & 581.9ms ± 6.2ms & UNSAT \\ + Iris (Stably Inactive) & Epsilon $\epsilon=0.1$ & 283.2ms ± 9.0ms & 593.8ms ± 6.9ms & UNSAT \\ + Iris (Stably Inactive) & Argmax & 287.6ms ± 2.6ms & 886.4ms ± 10.3ms & UNSAT \\ + Iris (Deep To Wide) & Strict & 269.5ms ± 5.1ms & 595.4ms ± 11.3ms & UNSAT \\ + Iris (Deep To Wide) & Epsilon $\epsilon=0.1$ & 273.7ms ± 5.6ms & 587.0ms ± 4.9ms & UNSAT \\ + Iris (Deep To Wide) & Argmax & 296.5ms ± 8.5ms & 783.5ms ± 4.4ms & UNSAT \\ + Iris (Wide To Deep) & Strict & 271.5ms ± 7.7ms & 581.4ms ± 6.6ms & UNSAT \\ + Iris (Wide To Deep) & Epsilon $\epsilon=0.1$ & 272.3ms ± 6.6ms & 583.1ms ± 5.7ms & UNSAT \\ + Iris (Wide To Deep) & Argmax & 1.280s ± 0.019s & 716.3ms ± 4.7ms & UNSAT \\ + Pendulum & Strict & 20m 47.679s & 43.276s ± 0.143s & SAT \\ + Pendulum & Epsilon $\epsilon=0.1$ & 37m 54.754s & 340.293s ± 2.843s & UNSAT \\ + Pendulum & Argmax & 24m 56.327s & 61.935s ± 0.148s & SAT \\ + Double Integrator & Strict & 27m 45.657s & 538.952s ± 7.207s & SAT \\ + Double Integrator & Epsilon $\epsilon=0.1$ & 59m 51.718s & 137.720s ± 0.419s & SAT \\ + Double Integrator & Argmax & 41m 21.147s & 618.705s ± 6.821s & SAT \\ + MNIST (Stably Active) & Strict & 740.5ms ± 4.7ms & 18.947s ± 0.034s & SAT \\ + MNIST (Stably Active) & Epsilon $\epsilon=0.1$ & 1.571s ± 0.010s & 18.980s ± 0.032s & UNSAT \\ + MNIST (Stably Active) & Argmax & 794.7ms ± 7.3ms & 18.906s ± 0.019s & UNSAT \\ + MNIST (Stably Inactive) & Strict & TIMEOUT & 14.699s ± 0.024s & UNSAT \\ + MNIST (Stably Inactive) & Epsilon $\epsilon=0.1$ & TIMEOUT & 14.702s ± 0.012s & UNSAT \\ + MNIST (Stably Inactive) & Argmax & TIMEOUT & TIMEOUT & UNKNOWN \\ + MNIST (Deep To Wide) & Strict & 692.2ms ± 5.6ms & 20.990s ± 0.181s & UNSAT \\ + MNIST (Deep To Wide) & Epsilon $\epsilon=0.1$ & 691.4ms ± 3.2 ms & 20.860s ± 0.022s & UNSAT \\ + MNIST (Deep To Wide) & Argmax & TIMEOUT & TIMEOUT & UNKNOWN \\ + MNIST (Wide To Deep) & Strict & 718.3ms ± 4.8ms & 20.901s ± 0.027s & UNSAT \\ + MNIST (Wide To Deep) & Epsilon $\epsilon=0.1$ & 722.1ms ± 6.0 ms & 20.947s ± 0.035s & UNSAT \\ + MNIST (Wide To Deep) & Argmax & TIMEOUT & TIMEOUT & UNKNOWN \\ + \end{tabular} + } \caption{Benchmark table.} \label{tab:benchmarks} \end{table} + +We make three observations: +\begin{itemize} + \item On Iris, the direct translation is consistently faster by a roughly constant + margin, suggesting a fixed \textbf{VEIN} pipeline overhead. + \item On Pendulum and Double Integrator, the pattern reverses: \textbf{VEIN} outperforms the direct + translation by up to two orders of magnitude. + \item MNIST is mixed: most variants favor the direct translation, except Stably Inactive, + where the direct encoding times out while \textbf{VEIN} finishes in ~15s. We hypothesize this is because + direct encoding may face branching from the unpruned network that \textbf{VEIN} folds during + preprocessing. +\end{itemize} +Additionally, we identify two false SAT results (Stably Active transformation). These are caused +by floating-point error introduced by the INPLA float attributes instead of using real numbers. diff --git a/chapters/core/implementation/01-inpla.tex b/chapters/core/implementation/01-inpla.tex index eeebf47..57d3195 100644 --- a/chapters/core/implementation/01-inpla.tex +++ b/chapters/core/implementation/01-inpla.tex @@ -1,7 +1,7 @@ \subsection{INPLA fork} \label{sec:inpla} -The VEIN reduction engine utilizes a modified version of INPLA\footnote{\textbf{\href{https://github.com/inpla/inpla/blob/main/Gentle_introduction_Inpla.md}{INPLA documentation.}}}, +The \textbf{VEIN} reduction engine utilizes a modified version of INPLA\footnote{\textbf{\href{https://github.com/inpla/inpla/blob/main/Gentle_introduction_Inpla.md}{INPLA documentation.}}}, a multi-threaded parallel interpreter of IN. Performance and ease of use motivated the choice of INPLA. Additionally, it supports attribute values, which is a special extension that allows agents to hold numerical values at their ports. @@ -24,7 +24,7 @@ INPLA evaluates nets which consist of connections between terms. Terms are built <term> ::= <name> | <agent> <name> ::= <nameID> <agent> ::= <agentID> - | <agentID> ['(' <term> ',' ... ',' <term> ')'] + | <agentID> ['(' <term> ',' ... ',' <term> ')'] \end{verbatim} \end{small} \begin{itemize} @@ -37,12 +37,12 @@ Interaction rules rewrite connections between agents: \begin{verbatim} <interaction-rule> ::= <rule-agent> '><' <rule-agent> '=>' <connections> ';' <rule-agent> ::= <agentID> - | <agentID> '(' <name> ',' ... ',' <name> ')' + | <agentID> '(' <name> ',' ... ',' <name> ')' \end{verbatim} \end{small} \paragraph{Example} -Unary natural numbers are built by $\texttt{Z}$ (zero) and $\texttt{S}$ (successive function). For +Unary natural numbers are built by $\texttt{Z}$ (zero) and $\texttt{S}$ (successor function). For instance, 0, 1, 2, 3 are expressed as \texttt{Z}, \texttt{S(Z)}, \texttt{S(S(Z))}, \texttt{S(S(S(Z)))}. Here, let's think about an increment operation ``inc'' such that: \begin{small} diff --git a/chapters/core/implementation/02-interaction-rules.tex b/chapters/core/implementation/02-interaction-rules.tex index 49a8a70..8b02c3c 100644 --- a/chapters/core/implementation/02-interaction-rules.tex +++ b/chapters/core/implementation/02-interaction-rules.tex @@ -1,7 +1,7 @@ \subsection{Interaction Rules} \label{sec:interaction-rules} -The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into four groups: +The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into five groups: \begin{itemize} \item \textbf{Carriers}: Agents that contain float attributes. @@ -179,7 +179,7 @@ The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into f (m) $\mathit{TermAdd}$ & (n) $\mathit{TermMul}$ & (o) $\mathit{TermReLU}$ & (p) $\mathit{TermSymbolic}$ & (q) $\mathit{TermConcrete}$ \\[0.5cm] \end{tabular} } - \caption{Agents used in VEIN.} + \caption{Agents used in \textbf{VEIN}.} \label{fig:agents} \end{figure} @@ -495,7 +495,7 @@ If, instead, the first operand is a \textit{Linear} agents and the second is a \ are applied. In the case of addition (\textbf{\Cref{fig:rule-concrete-addchecklinear}}) the system adds the attribute of the \textit{Concrete} agent to the attribute that represents the constant of the \textit{Linear} agent. For multiplication (\textbf{\Cref{fig:rule-concrete-mulchecklinear}}) the system multiplies the attribute of -the \textit{Concrete} agent to both the attributes of the \textit{Linear} +the \textit{Concrete} agent to both the attributes of the \textit{Linear}. % Concrete >< AddCheckLinear \begin{figure}[H] diff --git a/chapters/core/implementation/03-translation.tex b/chapters/core/implementation/03-translation.tex index 0a2eec0..b86e060 100644 --- a/chapters/core/implementation/03-translation.tex +++ b/chapters/core/implementation/03-translation.tex @@ -9,7 +9,8 @@ necessary copies of a value required by the next operations. Since nodes do not nodes will utilize their outputs, the translation layer traverses the DAG in reverse order to be able to instantiate the correct number of \textit{Dup} agents. The main algorithm, illustrated in \textbf{\Cref{alg:onnx-to-in}}, maintains an \textit{interactions} dictionary data-structure, that maps each tensor -name to a list of ports, to keep track of the graph traversal. +name to a list of ports, to keep track of the graph traversal. The ONNX operators supported are Gemm +(General matrix multiplication) and ReLU. \begin{algorithm}[H] \caption{Backwards ONNX-to-IN Translation} @@ -79,9 +80,9 @@ To maximize the concurrency of the INPLA engine, the translation layer avoids ge chains of agents, opting instead for balanced binary trees for signal distribution (single input to multiple output) and signal reduction (multiple input to single output). As \textbf{\Cref{alg:balanced-fan-in}} and \textbf{\Cref{alg:balanced-fan-out}} illustrate, the depth of agent chains (especially \textit{Dup} chains) -is limited to $O(\log N)$. The two algorithms are very similar, the difference is in how they wire the +is limited to $O(\log N)$. The two algorithms are very similar; the difference is in how they wire the agents together: in the \textit{Fan-In} the principal port of the agents are facing the leaves, while in the -\textit{Fan-Out} they are facing the root. +\textit{Fan-Out} they face the root. \begin{algorithm}[H] \caption{Balanced Fan-In} diff --git a/chapters/core/implementation/04-python-module.tex b/chapters/core/implementation/04-python-module.tex index a40df41..6023c2e 100644 --- a/chapters/core/implementation/04-python-module.tex +++ b/chapters/core/implementation/04-python-module.tex @@ -1,8 +1,8 @@ \subsection{Python Module} \label{sec:python-module} -The core functionality of the VEIN system is implemented via the \texttt{vein.Solver}, an extension of -the \texttt{z3.Solver} class offered in the Z3 python +The core functionality of the \textbf{VEIN} system is implemented via the \texttt{vein.Solver}, an extension of +the \texttt{z3.Solver} class offered in the Z3 Python package\footnote{\href{https://pypi.org/project/z3-solver}{\textbf{PyPi package}}}. This design choice ensures flexibility and ease of use for researchers already familiar with using the Z3 Python API. @@ -19,7 +19,7 @@ into a pending queue and it is reduced to normal form only after the \texttt{che called. The specification follows the SMT-LIB\footnote{\href{https://smt-lib.org}{\textbf{SMT-LIB Website}}} -format. It should contain the input and output symbolic variables declaration, optional range +format. It should contain the input and output symbolic variables declarations, optional range constraints on the input variables and the properties to be verified. For Multi-Network (relational) verification, the system ensures that multiple networks share the same input symbolic variables. This approach allows Z3 to compare their outputs directly given the same inputs. diff --git a/chapters/core/soundness-proof/02-soundness-of-translation.tex b/chapters/core/soundness-proof/02-soundness-of-translation.tex index 800e085..4477581 100644 --- a/chapters/core/soundness-proof/02-soundness-of-translation.tex +++ b/chapters/core/soundness-proof/02-soundness-of-translation.tex @@ -20,8 +20,7 @@ Which is identical to the ONNX definition. \end{lemma} \begin{lemma} -The ONNX Gemm (General Matrix Multiplication) operator for input tensors A, B, C, input $\alpha$ -and $\beta$ and output tensor Y is defined as: +The ONNX Gemm operator for input tensors A, B, C, input $\alpha$ and $\beta$ and output tensor Y is defined as: $$ Y = \alpha \cdot A \cdot B + \beta \cdot C $$ 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 26f7e13..6957c3c 100644 --- a/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex +++ b/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex @@ -1,6 +1,8 @@ \subsection{Soundness of Interaction Rules} \label{sec:soundness-of-interaction-rules} +We need to prove that each interaction rule does not alter the semantics of the IN. + \begin{lemma} For the \textit{Linear} and \textit{Add} agents we have the interaction rule: $$ @@ -146,8 +148,7 @@ & \llbracket \mathit{AddCheckLinear}(\mathit{out}, x, q, r) \sim w \rrbracket \Rightarrow \mathit{out} = q \cdot x + (r + w) \\ & \Rightarrow \mathit{out} = q \cdot x + (r + s \cdot y + t) \end{aligned} \\ - & \begin{aligned} - \text{RHS: } + & \text{RHS: } \resizebox{0.85\linewidth}{!}{$ \begin{cases} \llbracket \mathit{out} \sim \mathit{Concrete}(0); x \sim \mathit{Eraser}; y \sim \mathit{Eraser} \rrbracket \Rightarrow \mathit{out} = 0 & \text{if } q,r,s,t = 0 \\ \llbracket \mathit{out} \sim \mathit{Linear}(x, q, r); y \sim \mathit{Eraser} \rrbracket \Rightarrow \mathit{out} = q \cdot x + r & \text{if } s,t = 0 \\ @@ -161,7 +162,7 @@ \end{aligned}\\ \Rightarrow \mathit{out} = 1 \cdot (q \cdot x + r + s \cdot y + t) + 0 & \text{otherwise} \end{cases} - \end{aligned} + $} \end{aligned} $$ Since: @@ -200,8 +201,7 @@ & \llbracket \mathit{MulCheckLinear}(\mathit{out}, x, q, r) \sim w \rrbracket \Rightarrow \mathit{out} = q \cdot w \cdot x + r \cdot w \\ & \Rightarrow \mathit{out} = q \cdot (s \cdot y + t) \cdot x + r \cdot (s \cdot y + t) \end{aligned} \\ - & \begin{aligned} - \text{RHS: } + & \text{RHS: } \resizebox{0.85\linewidth}{!}{$ \begin{cases} \llbracket \mathit{out} \sim \mathit{Concrete}(0); x \sim \mathit{Eraser}; y \sim \mathit{Eraser} \rrbracket \Rightarrow \mathit{out} = 0 & \text{if } q,r = 0 \lor s,t = 0 \\ \begin{aligned} @@ -213,15 +213,17 @@ \end{aligned}\\ \Rightarrow \mathit{out} = 1 \cdot (q \cdot x + r) \cdot (s \cdot y + t) + 0 & \text{otherwise} \end{cases} - \end{aligned} + $} \end{aligned} $$ Since: $$ + \resizebox{0.95\linewidth}{!}{$ \begin{cases} 0 \cdot (s \cdot y + t) \cdot x + 0 \cdot (s \cdot y + t) = 0 \lor q \cdot (0 \cdot y + 0) \cdot x + r \cdot (0 \cdot y + 0) = 0 & \text{if } q,r = 0 \lor s,t = 0 \\ 1 \cdot (q \cdot x + r) \cdot (s \cdot y + t) + 0 = q \cdot (s \cdot y + t) \cdot x + r \cdot (s \cdot y + t) & \text{otherwise} \end{cases} + $} $$ the rule is sound. \end{lemma} @@ -317,11 +319,13 @@ \begin{lemma} For the \textit{Concrete} and \textit{AddCheckConcrete} agents we have the interaction rule: $$ - \mathit{Concrete}(j) \bowtie \mathit{AddCheckConcrete}(\mathit{out}, k) \Rightarrow - \begin{cases} - \mathit{out} \sim \mathit{Concrete}(k) & \text{if } j = 0 \\ - \mathit{out} \sim \mathit{Concrete}(k + j) & \text{otherwise} - \end{cases} + \begin{aligned} + & \mathit{Concrete}(j) \bowtie \mathit{AddCheckConcrete}(\mathit{out}, k) \Rightarrow \\ + & \quad \begin{cases} + \mathit{out} \sim \mathit{Concrete}(k) & \text{if } j = 0 \\ + \mathit{out} \sim \mathit{Concrete}(k + j) & \text{otherwise} + \end{cases} + \end{aligned} $$ We need to show that the LHS and RHS are semantically equivalent: $$ @@ -353,12 +357,14 @@ \begin{lemma} For the \textit{Concrete} and \textit{MulCheckConcrete} agents we have the interaction rule: $$ - \mathit{Concrete}(j) \bowtie \mathit{MulCheckConcrete}(\mathit{out}, k) \Rightarrow - \begin{cases} - \mathit{out} \sim \mathit{Concrete}(0) & \text{if } j = 0 \\ - \mathit{out} \sim \mathit{Concrete}(k) & \text{if } j = 1 \\ - \mathit{out} \sim \mathit{Concrete}(k \cdot j) & \text{otherwise} - \end{cases} + \begin{aligned} + & \mathit{Concrete}(j) \bowtie \mathit{MulCheckConcrete}(\mathit{out}, k) \Rightarrow \\ + & \quad \begin{cases} + \mathit{out} \sim \mathit{Concrete}(0) & \text{if } j = 0 \\ + \mathit{out} \sim \mathit{Concrete}(k) & \text{if } j = 1 \\ + \mathit{out} \sim \mathit{Concrete}(k \cdot j) & \text{otherwise} + \end{cases} + \end{aligned} $$ We need to show that the LHS and RHS are semantically equivalent: $$ @@ -458,13 +464,13 @@ $$ \begin{aligned} & \mathit{Linear}(x, q, r) \bowtie \mathit{Materialize}(\mathit{out}) \Rightarrow \\ - & \quad \begin{cases} + & \quad \resizebox{0.85\linewidth}{!}{$ \begin{cases} \mathit{out} \sim \mathit{TermConcrete}(r); x \sim \mathit{Eraser} & \text{if } q = 0 \\ \mathit{out} \sim x & \text{if } q = 1, r = 0 \\ \mathit{out} \sim \mathit{TermAdd}(x, \mathit{TermConcrete}(r)) & \text{if } q = 1 \\ \mathit{out} \sim \mathit{TermMul}(\mathit{TermConcrete}(q), x) & \text{if } r = 0 \\ \mathit{out} \sim \mathit{TermAdd}(\mathit{TermMul}(\mathit{TermConcrete}(q), x), \mathit{TermConcrete}(r)) & \text{otherwise} - \end{cases} + \end{cases} $} \end{aligned} $$ We need to show that the LHS and RHS are semantically equivalent: @@ -477,13 +483,16 @@ \end{aligned} \\ & \begin{aligned} \text{RHS: } - \begin{cases} + \resizebox{0.9\linewidth}{!}{$ \begin{cases} \llbracket \mathit{out} \sim \mathit{TermConcrete}(r); x \sim \mathit{Eraser} \rrbracket \Rightarrow \mathit{out} = r & \text{if } q = 0 \\ \llbracket \mathit{out} \sim x \rrbracket \Rightarrow \mathit{out} = x & \text{if } q = 1, r = 0 \\ \llbracket \mathit{out} \sim \mathit{TermAdd}(x, \mathit{TermConcrete}(r)) \rrbracket \Rightarrow \mathit{out} = x + r & \text{if } q = 1 \\ \llbracket \mathit{out} \sim \mathit{TermMul}(\mathit{TermConcrete}(q), x) \rrbracket \Rightarrow \mathit{out} = q \cdot x & \text{if } r = 0 \\ - \llbracket \mathit{out} \sim \mathit{TermAdd}(\mathit{TermMul}(\mathit{TermConcrete}(q), x), \mathit{TermConcrete}(r)) \rrbracket \Rightarrow \mathit{out} = q \cdot x + r & \text{otherwise} \\ - \end{cases} + \begin{aligned} + & \llbracket \mathit{out} \sim \mathit{TermAdd}(\mathit{TermMul}(\mathit{TermConcrete}(q), x), \mathit{TermConcrete}(r)) \rrbracket \\ + & \Rightarrow \mathit{out} = q \cdot x + r + \end{aligned} & \text{otherwise} \\ + \end{cases} $} \end{aligned} \end{aligned} $$ @@ -526,9 +535,10 @@ For the \textit{Linear} and \textit{Dup} agents we have the interaction rule: $$ \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 + & \mathit{Linear}(z, q, r) \bowtie \mathit{Dup}(x, y) \Rightarrow \\ + & \quad \mathit{Linear}(z_1, q, r) \sim x; \\ + & \quad \mathit{Linear}(z_2, q, r) \sim y; \\ + & \quad \mathit{Dup}(z_1, z_2) \sim z \end{aligned} $$ We need to show that the LHS and RHS are semantically equivalent: @@ -620,8 +630,11 @@ For the \textit{TermAdd} and \textit{Dup} agents we have the interaction rule: $$ \begin{aligned} - \mathit{TermAdd}(a, b) \bowtie \mathit{Dup}(x, y) \Rightarrow & \mathit{TermAdd}(a_1, b_1) \sim x; \mathit{TermAdd}(a_2, b_2) \sim y; \\ - & \mathit{Dup}(a_1, a_2) \sim a; \mathit{Dup}(b_1, b_2) \sim b\\ + & \mathit{TermAdd}(a, b) \bowtie \mathit{Dup}(x, y) \Rightarrow \\ + & \quad \mathit{TermAdd}(a_1, b_1) \sim x; \\ + & \quad \mathit{TermAdd}(a_2, b_2) \sim y; \\ + & \quad \mathit{Dup}(a_1, a_2) \sim a; \\ + & \quad \mathit{Dup}(b_1, b_2) \sim b \end{aligned} $$ We need to show that the LHS and RHS are semantically equivalent: @@ -671,9 +684,11 @@ 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 \\ + & \quad \mathit{TermMul}(a_1, b_1) \sim x; \\ + & \quad \mathit{TermMul}(a_2, b_2) \sim y; \\ + & \quad \mathit{Dup}(a_1, a_2) \sim a; \\ + & \quad \mathit{Dup}(b_1, b_2) \sim b \end{aligned} $$ We need to show that the LHS and RHS are semantically equivalent: @@ -723,10 +738,10 @@ For the \textit{TermReLU} and \textit{Dup} agents we have the interaction rule: $$ \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 + & \mathit{TermReLU}(z) \bowtie \mathit{Dup}(x, y) \Rightarrow \\ + & \quad \mathit{TermReLU}(z_1) \sim x; \\ + & \quad \mathit{TermReLU}(z_2) \sim y; \\ + & \quad \mathit{Dup}(z_1, z_2) \sim z \end{aligned} $$ We need to show that the LHS and RHS are semantically equivalent: @@ -774,9 +789,9 @@ For the \textit{TermConcrete} and \textit{Dup} agents we have the interaction rule: $$ \begin{aligned} - \mathit{TermConcrete}(k) \bowtie \mathit{Dup}(x, y) \Rightarrow - & \mathit{TermConcrete}(k) \sim x; \\ - & \mathit{TermConcrete}(k) \sim y + & \mathit{TermConcrete}(k) \bowtie \mathit{Dup}(x, y) \Rightarrow \\ + & \quad \mathit{TermConcrete}(k) \sim x; \\ + & \quad \mathit{TermConcrete}(k) \sim y \end{aligned} $$ We need to show that the LHS and RHS are semantically equivalent: @@ -822,9 +837,9 @@ For the \textit{TermSymbolic} and \textit{Dup} agents we have the interaction rule: $$ \begin{aligned} - \mathit{TermSymbolic}(id) \bowtie \mathit{Dup}(x, y) \Rightarrow - & \mathit{TermSymbolic}(id) \sim x; \\ - & \mathit{TermSymbolic}(id) \sim y + & \mathit{TermSymbolic}(id) \bowtie \mathit{Dup}(x, y) \Rightarrow \\ + & \quad \mathit{TermSymbolic}(id) \sim x; \\ + & \quad \mathit{TermSymbolic}(id) \sim y \end{aligned} $$ We need to show that the LHS and RHS are semantically equivalent: diff --git a/chapters/core/soundness-proof/04-soundness-of-reduction.tex b/chapters/core/soundness-proof/04-soundness-of-reduction.tex index d0cec53..15cc4f4 100644 --- a/chapters/core/soundness-proof/04-soundness-of-reduction.tex +++ b/chapters/core/soundness-proof/04-soundness-of-reduction.tex @@ -1,7 +1,7 @@ \subsection{Soundness of Reduction} \label{sec:soundness-of-reduction} -\begin{lemma} +\begin{property} A valid IN satisfies the following properties: \begin{itemize} \item \textbf{DAG}: the net forms a DAG where the roots are the free wires representing the network @@ -15,7 +15,7 @@ carrier nor operator agents interact with agents of the same type. Terminal agents do not interact with computational operators because they are wrapped in a \textit{Linear} agent. \end{itemize} -\end{lemma} +\end{property} \begin{theorem} Let $\text{IN}_0$ be the valid IN translated from a neural network $\text{NN}$. Let $\text{IN}_n$ be @@ -65,9 +65,9 @@ \Phi(\text{IN}_n) = \sum_{a \in \text{Agents}(\text{IN}_n)} \begin{cases} 4 + 3^{D-d(a)} & \text{ if }a\text{ is of type computational operator} \\ 3 + 3^{D-d(a)} & \text{ if }a\text{ is of type intermediate} \\ - 1 + 3^{D-d(a)} & \text{ if }a\text{ is a Materialize agent} \\ + 1 + 3^{D-d(a)} & \text{ if }a\text{ is a \textit{Materialize} agent} \\ 3^{D-d(a)} & \text{ if }a\text{ is of type structural operator} \\ - 0 & \text{ if }a\text{ is a Carrier, Terminal} + 0 & \text{ if }a\text{ is a carrier, terminal} \end{cases} \end{equation} where $d(a)$ is the distance of the agent $a$ from the nearest output wire and $D$ the maximum depth @@ -88,30 +88,44 @@ \begin{equation} \Phi(\text{IN}_n) = 3 + 3^{D-d(i)} > 0 = \Phi(\text{IN}_{n+1}) \end{equation} - or temporary Linear agents are wired with Materialize agents, which are then forced to - interact to produce terminal agents, then wrapped into a new Linear agent: + or temporary Linear agents are wired with \textit{Materialize} agents, which are then forced to + interact to produce terminal agents, then wrapped into a new \textit{Linear} agent: \begin{equation} - \Phi(\text{IN}_n) = 3 + 3^{D-d(i)} > 1 + 3^{D-d(i)-2} + 1 + 3^{D-d(i)-2} = 2 + 2 \cdot 3^{D-d(i)-2} = \Phi(\text{IN}_{n+1}) + \begin{aligned} + \Phi(\text{IN}_n) &= 3 + 3^{D-d(i)} \\ + &> 1 + 3^{D-d(i)-2} + 1 + 3^{D-d(i)-2} \\ + &= 2 + 2 \cdot 3^{D-d(i)-2} = \Phi(\text{IN}_{n+1}) + \end{aligned} \end{equation} - If the carrier $c$ interacts with a Materialize agent $i$: + If the carrier $c$ interacts with a \textit{Materialize} agent $i$: \begin{equation} \Phi(\text{IN}_n) = 1 + 3^{D-d(i)} > 0 = \Phi(\text{IN}_{n+1}) \end{equation} - \item \textbf{Carrier with Structural Operator}: If a carrier $c$ is duplicated with the \textit{Dup} or \textit{Eraser} + \item \textbf{Carrier with Structural Operator}: If a carrier $c$ interacts with a \textit{Dup} or \textit{Eraser} agent $a$, it traverses the agent structure: \begin{equation} \Phi(\text{IN}_n) = 3^{D-d(a)} > 3^{D-d(a)-1} = \Phi(\text{IN}_{n+1}) \end{equation} - if the Dup or Eraser agent interacts with a TermAdd or TermMul, two new agents are created at - each auxillary port: + if the \textit{Dup} or \textit{Eraser} agent interacts with a \textit{TermAdd} or \textit{TermMul}, two new agents are created at + each auxiliary port: \begin{equation} \Phi(\text{IN}_n) = 3^{D-d(a)} > 2 * 3^{D-d(a)-1} = \Phi(\text{IN}_{n+1}) \end{equation} + if the \textit{Dup} or \textit{Eraser} agent interacts with a \textit{TermReLU}, one new agent is created at the + auxiliary port: + \begin{equation} + \Phi(\text{IN}_n) = 3^{D-d(a)} > 3^{D-d(a)-1} = \Phi(\text{IN}_{n+1}) + \end{equation} + if the \textit{Dup} or \textit{Eraser} agent interacts with a \textit{TermConcrete} or \textit{TermSymbolic}, no new agents are + created: + \begin{equation} + \Phi(\text{IN}_n) = 3^{D-d(a)} > 0 = \Phi(\text{IN}_{n+1}) + \end{equation} \end{itemize} Since $\Phi$ is a non-negative strictly decreasing function, the reduction process must terminate in a finite number of steps $n$. - Additionally, since each active pair has exactly one applicable rule the reduction is + Additionally, since each active pair has exactly one applicable rule, the reduction is deterministic. Strong confluence follows immediately, meaning that the normal form is unique - regardless of order in which rules are applied. + regardless of the order in which rules are applied. \end{proof} @@ -15,11 +15,13 @@ \usepackage{tikz-inet} \usepackage{stmaryrd} \usepackage{float} +\usepackage{tablefootnote} \usetikzlibrary{calc} \linenumbers \crefname{algocf}{alg.}{algs.} \Crefname{algocf}{Algorithm}{Algorithms} +\crefformat{footnote}{#2\footnotemark[#1]#3} \input{macros} \input{cmds} @@ -33,7 +35,14 @@ \maketitle \begin{abstract} - Summary + This thesis introduces \textbf{VEIN} (VErification via Interaction Nets), a framework for neural network + verification with a focus on neural network equivalence. It acts as a formally verified + preprocessor that reduces neural networks to a normal form before they can be compared by a solver. + To enable this reduction, \textbf{VEIN} translates neural networks into Interaction Nets, a graph rewriting + computational model, and applies a set of graph rewriting rules to reduce the network into an + Abstract Syntax Tree. We present the complete framework and provide in detail: the translation + process, the graph rewriting rules and rigorous proofs of both soundness and termination for the + reduction process. \end{abstract} \tableofcontents @@ -41,13 +50,13 @@ % Introduction: Context -> Problem -> Solution -> Validation -> Outline \input{chapters/01-introduction} -% Background: Concepts and notions +% Background \input{chapters/02-background} -% Core: The main work +% Core \input{chapters/03-core} -% Related Work: At the end, before conclusions +% Related Work \input{chapters/04-related-work} % Conclusion |