diff options
Diffstat (limited to 'chapters')
| -rw-r--r-- | chapters/01-introduction.tex | 42 | ||||
| -rw-r--r-- | chapters/02-background.tex | 4 | ||||
| -rw-r--r-- | chapters/03-core.tex | 4 | ||||
| -rw-r--r-- | chapters/04-related-work.tex | 2 | ||||
| -rw-r--r-- | chapters/05-conclusion.tex | 15 | ||||
| -rw-r--r-- | chapters/background/01-neural-networks.tex | 4 | ||||
| -rw-r--r-- | chapters/background/02-interaction-nets.tex | 12 | ||||
| -rw-r--r-- | chapters/core/01-implementation.tex | 2 | ||||
| -rw-r--r-- | chapters/core/02-soundness-proof.tex | 4 | ||||
| -rw-r--r-- | chapters/core/03-benchmarks.tex | 15 | ||||
| -rw-r--r-- | chapters/core/implementation/01-inpla.tex | 18 | ||||
| -rw-r--r-- | chapters/core/implementation/02-interaction-rules.tex | 56 | ||||
| -rw-r--r-- | chapters/core/implementation/03-translation.tex | 8 | ||||
| -rw-r--r-- | chapters/core/implementation/04-python-module.tex | 6 | ||||
| -rw-r--r-- | chapters/core/soundness-proof/02-soundness-of-translation.tex | 4 | ||||
| -rw-r--r-- | chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex | 66 | ||||
| -rw-r--r-- | chapters/core/soundness-proof/04-soundness-of-reduction.tex | 10 |
17 files changed, 138 insertions, 134 deletions
diff --git a/chapters/01-introduction.tex b/chapters/01-introduction.tex index 47b7d57..2139af7 100644 --- a/chapters/01-introduction.tex +++ b/chapters/01-introduction.tex @@ -3,24 +3,24 @@ % 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. However, they do not come without +us to enter a new age of computing. Most of the credit goes to deep neural networks and to their +exceptional capacity for representing nonlinear 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 +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 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. + \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. \end{itemize} An example of a Multi-Network property is equivalence between different neural networks; this verification is crucial when replacing a neural network with a smaller, equivalent one. Techniques based on specialized \textit{Satisfiability Modulo Theories} (SMT) solvers may be used in the verification -algorithm. However, as networks grow in depth and width, the number of non-linear components, most +algorithm. However, as networks grow in depth and width, the number of nonlinear components, most notably the \textit{Rectified Linear Unit}\footnote{Defined as $f(x)=\max(0, x)$, where $x$ is the input to the neuron.} (ReLU) activation function, creates an exponential search space for the solver. Because of this issue, running a solver against a raw, unoptimized network is often computationally prohibitive. @@ -42,15 +42,17 @@ To model such graphs and these rewriting mechanisms, we leverage \textit{Interac parallel graph rewriting rules. Additionally, IN are \textit{strongly confluent}, meaning that they always reduce to a unique normal form regardless of the order in which simplification rules are applied. Thanks to these properties, the simplification of neural network graphs can be parallelized -while maintaining determinism of the resulting AST. In the context of neural network equivalence, +while maintaining the determinism of the resulting AST. In the context of neural network equivalence, this is useful because comparing two neural networks becomes a comparison of two simplified canonical forms of the same intermediate model. -Building on this capability, we developed \textbf{VEIN} (VErification via Interaction Nets), a -framework for neural network verification focused on equivalence. This tool aims to verify both -Single-Network and Multi-Network properties. The tool is composed of two primary modules: +Building on this capability, we developed +\textbf{VEIN}\footnote{\href{https://github.com/eric-marin/VEIN}{\textbf{VEIN Github repository.}}} +(VErification via Interaction Nets), a framework for neural network verification focused on +equivalence. This tool aims to verify both Single-Network and Multi-Network properties. The tool is +composed of two primary modules: \begin{itemize} - \item \textbf{Reduction engine}: a modified version of \textit{Interaction Nets as a Programming + \item \textbf{Reduction engine}: A modified version of \textit{Interaction Nets as a Programming LAnguage}\footnote{\href{https://github.com/inpla/inpla}{\textbf{INPLA Github repository}}.} (INPLA), a multi-threaded parallel interpreter of IN, to simplify the neural network graph; @@ -58,20 +60,20 @@ Single-Network and Multi-Network properties. The tool is composed of two primary \end{itemize} The tool runtime follows three steps: \begin{itemize} - \item \textbf{Translation}: the system translates a neural network in \textit{Open Neural Network + \item \textbf{Translation}: The system translates a neural network in \textit{Open Neural Network Exchange}\footnote{\href{https://onnx.ai/}{\textbf{ONNX Website}}.} (ONNX) file format, an open format built to represent machine learning models, into an IN; - \item \textbf{Reduction}: the INPLA engine reduces the IN to its normal form using the graph + \item \textbf{Reduction}: The INPLA engine reduces the IN to its normal form using the graph rewriting rules that implement symbolic constant folding and identity elimination; - \item \textbf{Evaluation}: then we parse the resulting normal form into Z3 representation and run the + \item \textbf{Evaluation}: Then we parse the resulting normal form into Z3 representation and run the solver to evaluate it along with the provided specification. \end{itemize} % Validation We prove the soundness of our IN pipeline by induction on the number of interaction steps, demonstrating that the ONNX translation and each interaction rule preserve the semantic meaning of -the original neural network. In addition to this formal analysis, we conducted several benchmarks on -checking equivalence between a neural network trained on a dataset and a transformation. +the original neural network. In addition to this formal analysis, we conducted several benchmarks to +check the equivalence between a neural network trained on a dataset and a transformation. % Contributions The development of the \textbf{VEIN} framework and the design of its underlying simplification layer @@ -79,14 +81,14 @@ constitute the primary work of this thesis. To address the challenges of verific and the need for a formal model of representation (B), this thesis introduces several key contributions: \begin{itemize} - \item \textbf{Interaction Rules (Solves A)}: we designed a set of interaction rules to enable graph + \item \textbf{Interaction Rules (Solves A)}: We designed a set of interaction rules to enable graph rewriting for symbolic constant folding while producing an AST ready to be parsed for the SMT solver; - \item \textbf{ONNX-Interaction Net Translation (Solves B)}: we developed a translation procedure for ONNX + \item \textbf{ONNX-Interaction Net Translation (Solves B)}: We developed a translation procedure for ONNX models to IN; - \item \textbf{Soundness Analysis (Validates A/B)}: we provide a formal proof that the IN reduction + \item \textbf{Soundness Analysis (Validates A/B)}: We provide a formal proof that the IN reduction preserves the mathematical properties of the neural network; - \item \textbf{Experimental Evaluation (Validates A/B Empirically)}: we conducted an extensive benchmarking + \item \textbf{Experimental Evaluation (Validates A/B Empirically)}: We conducted an extensive benchmarking on widely known datasets and common \textit{International Verification of Neural Networks Competition}\footnote{The premier international competition dedicated to evaluating and advancing the state-of-the-art in neural network verification, see the diff --git a/chapters/02-background.tex b/chapters/02-background.tex index ca6160e..c306e2e 100644 --- a/chapters/02-background.tex +++ b/chapters/02-background.tex @@ -1,9 +1,9 @@ \chapter{Background} \label{ch:background} -This chapter contains the background theory necessary to understand the rest of the thesis such as: +This chapter contains the background theory necessary to understand the rest of the thesis, such as neural networks (\textbf{\Cref{sec:neural-networks}}), interaction nets -(\textbf{\Cref{sec:interaction-nets}}) and SMT solvers (\textbf{\Cref{sec:satisfiability-modulo-theories}}). +(\textbf{\Cref{sec:interaction-nets}}), and SMT solvers (\textbf{\Cref{sec:satisfiability-modulo-theories}}). \input{chapters/background/01-neural-networks} diff --git a/chapters/03-core.tex b/chapters/03-core.tex index c222f0d..96cd0f1 100644 --- a/chapters/03-core.tex +++ b/chapters/03-core.tex @@ -1,8 +1,8 @@ -\chapter{VEIN} +\chapter{VEIN: VErification via Interaction Nets} \label{ch:core} This chapter contains details on framework implementation (\textbf{\Cref{sec:implementation}}), the -proof of soundness of the pipeline (\textbf{\Cref{sec:soundness-proof}}) and a collection of data +proof of soundness of the pipeline (\textbf{\Cref{sec:soundness-proof}}), and a collection of data gathered from benchmarks (\textbf{\Cref{sec:benchmarks}}). \input{chapters/core/01-implementation} diff --git a/chapters/04-related-work.tex b/chapters/04-related-work.tex index d43cb0e..8e0c760 100644 --- a/chapters/04-related-work.tex +++ b/chapters/04-related-work.tex @@ -36,5 +36,5 @@ the problem of neural network equivalence checking using SMT solvers, and define 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 +preprocessing stage that reduces the networks to a normal form before encoding them into an SMT formula. diff --git a/chapters/05-conclusion.tex b/chapters/05-conclusion.tex index b178b7f..089acfb 100644 --- a/chapters/05-conclusion.tex +++ b/chapters/05-conclusion.tex @@ -2,10 +2,11 @@ \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: +a particular focus on neural 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 + \item The design of interaction rules implements symbolic constant folding, constant propagation, and identity elimination. \item A soundness proof of the reduction engine, demonstrating that each graph rewriting step preserves the semantics of the original neural network. @@ -15,25 +16,25 @@ a particular focus on network equivalence checking. The key achievements of this 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. +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. +memory safety without garbage collection, high-performance concurrency, and flexibility. \paragraph{Complex Agent Attributes} 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, boundary intervals and real numbers. +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 \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. +plan to implement range analysis and interval arithmetic directly within the IN to determine prunable +ReLUs, substantially reducing the number of split constraints faced by the SMT solver. \paragraph{Integration with Specialized Solvers} The current evaluation of \textbf{VEIN} targets the Z3 solver. However, the intermediate SMT-LIB diff --git a/chapters/background/01-neural-networks.tex b/chapters/background/01-neural-networks.tex index dc3e2d4..5eed7bd 100644 --- a/chapters/background/01-neural-networks.tex +++ b/chapters/background/01-neural-networks.tex @@ -3,7 +3,7 @@ A neural network is a computational model inspired by biological neural networks. It consists of 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 +The \textit{Multi-Layer Perceptron} is an architecture composed of sequential layers, trained using backpropagation as popularized by Rumelhart et al.~\cite{rumelhart1986learning}. \subsection{Neuron} @@ -57,7 +57,7 @@ The output $y$ is defined as: \subsection{Multi-Layer Perceptron} A \textit{Multi-Layer Perceptron} (MLP), illustrated in \textbf{\Cref{fig:mlp}}, is a type of neural network organized -in fully connected layers of neurons: an input layer, one or more hidden layers and an output layer. +in fully connected layers of neurons: an input layer, one or more hidden layers, and an output layer. An MLP is \textit{feedforward}, meaning that the flow of information is strictly propagated from the input to the outputs. \begin{figure}[H] diff --git a/chapters/background/02-interaction-nets.tex b/chapters/background/02-interaction-nets.tex index 874110e..41488f1 100644 --- a/chapters/background/02-interaction-nets.tex +++ b/chapters/background/02-interaction-nets.tex @@ -5,7 +5,7 @@ graphical model of computation based on graph rewriting. \subsection{Basic Concepts} -An IN is an undirected graph with labelled vertices, called \textit{agents}. Each agent +An IN is an undirected graph with labeled 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 @@ -21,7 +21,7 @@ is an instance of a \textit{symbol}, which has a principal port and a fixed numb \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}: +respective principal ports, they are called an \textit{active pair}: \begin{figure}[H] \centering @@ -34,13 +34,13 @@ respective principal ports they are called an \textit{active pair}: \node[left] at (A.above pax 2) {$\mathit{y}$}; \node[right] at (S.above pax) {$\mathit{x}$}; \end{tikzpicture} - \caption{Example of an active pair, where a $\mathit{Add}$ agent and an $\mathit{S}$ agent are connected via their principal ports.} + \caption{Example of an active pair, where an $\mathit{Add}$ agent and an $\mathit{S}$ agent are connected via their principal ports.} \label{fig:active-pair} \end{figure} \subsection{Interaction Rules} 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 +is defined only for an active pair, and for any pair of symbols, there is at most one interaction rule. \begin{figure}[H] @@ -62,12 +62,12 @@ interaction rule. \node[left] at (A.above pax 2) {$\mathit{y}$}; \node[left] at (S.above pal) {$\mathit{z}$}; } - \caption{Interaction rule for $\mathit{S}$ and $\mathit{Add}$ that emulates Peano addition rule.} + \caption{Interaction rule for $\mathit{S}$ and $\mathit{Add}$ that emulates the Peano addition rule.} \label{fig:rule-concrete-zero} \end{figure} \subsection{Properties} -IN possess the following properties: +IN possesses the following properties: \begin{itemize} \item \textbf{Locality}: only active pairs can be rewritten. \item \textbf{Linearity}: each interaction rule rewrites a constant-size subgraph, independent of diff --git a/chapters/core/01-implementation.tex b/chapters/core/01-implementation.tex index 32154ef..9c25bef 100644 --- a/chapters/core/01-implementation.tex +++ b/chapters/core/01-implementation.tex @@ -3,7 +3,7 @@ This section contains details on the implementation of the reduction engine (\textbf{\Cref{sec:inpla}}), the interaction rules designed (\textbf{\Cref{sec:interaction-rules}}), the algorithm used in the -ONNX-to-IN translation (\textbf{\Cref{sec:translation}}) and the Python module (\textbf{\Cref{sec:python-module}}). +ONNX-to-IN translation (\textbf{\Cref{sec:translation}}), and the Python module (\textbf{\Cref{sec:python-module}}). \input{chapters/core/implementation/01-inpla} diff --git a/chapters/core/02-soundness-proof.tex b/chapters/core/02-soundness-proof.tex index 6b014da..fef6bec 100644 --- a/chapters/core/02-soundness-proof.tex +++ b/chapters/core/02-soundness-proof.tex @@ -1,9 +1,9 @@ \section{Soundness Proof} \label{sec:soundness-proof} -This section contains proof of soundness of the VEIN framework, which is organized in mathematical +This section contains proof of the soundness of the VEIN framework, which is organized in mathematical definitions (\textbf{\Cref{sec:mathematical-definitions}}), proof of the translation layer (\textbf{\Cref{sec:soundness-of-translation}}), -proof of the interaction rules (\textbf{\Cref{sec:soundness-of-interaction-rules}}) and the final +proof of the interaction rules (\textbf{\Cref{sec:soundness-of-interaction-rules}}), and the final induction proof (\textbf{\Cref{sec:soundness-of-reduction}}). \input{chapters/core/soundness-proof/01-mathematical-definitions} diff --git a/chapters/core/03-benchmarks.tex b/chapters/core/03-benchmarks.tex index 31b61a7..25cc0ab 100644 --- a/chapters/core/03-benchmarks.tex +++ b/chapters/core/03-benchmarks.tex @@ -9,12 +9,13 @@ This section contains the benchmark data, illustrated in \textbf{\Cref{tab:bench \item \textbf{RAM}: 16GiB \end{itemize} 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: +benchmarking tool. Hyperfine runs the test ten times, then reports the mean and the standard deviation +of execution time. For longer runs, only one 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. + 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: the width and length of the 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 @@ -25,13 +26,13 @@ of execution time. For longer runs, only execution is reported. We defined the f \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 +al.~\cite{kaulen20256thinternationalverificationneural}. We check the equivalence between a pre-trained and a fine-tuned network for each task. 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}. +to deep and vice versa, as presented by Fan et al.~\cite{JMLR:v24:21-0579}. 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: @@ -100,4 +101,4 @@ We make three observations: 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. +by floating-point errors 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 57d3195..ff6ef16 100644 --- a/chapters/core/implementation/01-inpla.tex +++ b/chapters/core/implementation/01-inpla.tex @@ -8,17 +8,17 @@ to hold numerical values at their ports. Several modifications adapt INPLA to the pipeline of the framework: \begin{itemize} - \item \textbf{Floating-Point arithmetic}: attributes were limited to integer values. To correctly + \item \textbf{Floating-Point arithmetic}: Attributes were limited to integer values. To correctly represent the computation performed by neural networks, the fork replaces the internal numerical representation by floating-point types. \item \textbf{Pipeline integration}: INPLA was designed for interactive use through the command line, so - various debugging and informational messages are printed along the actual output. To integrate - INPLA in our automated framework, the fork introduces a suppression flag to prevent unnecessary - printing from disrupting its execution. + various debugging and informational messages are printed along with the actual output. To + integrate INPLA in our automated framework, the fork introduces a suppression flag to prevent + unnecessary printing from disrupting its execution. \end{itemize} \paragraph{INPLA syntax} -INPLA evaluates nets which consist of connections between terms. Terms are built on names and agents: +INPLA evaluates nets composed of connections between terms. Terms are built on names and agents: \begin{small} \begin{verbatim} <term> ::= <name> | <agent> @@ -28,10 +28,10 @@ INPLA evaluates nets which consist of connections between terms. Terms are built \end{verbatim} \end{small} \begin{itemize} - \item \textbf{Name}: it works as a buffer between terms. - \item \textbf{Agent}: it works as a constructor and de-constructor (defined functions). + \item \textbf{Name}: It works as a buffer between terms. + \item \textbf{Agent}: It works as a constructor and a de-constructor. \end{itemize} -A connection is a relation between two terms and the symbol \texttt{\~} expresses this relation. +A connection is a relation between two terms, and the symbol \texttt{\~} expresses this relation. Interaction rules rewrite connections between agents: \begin{small} \begin{verbatim} @@ -50,7 +50,7 @@ increment operation ``inc'' such that: inc(n) = S(n). \end{verbatim} \end{small} -This is written as the following rules: +This is written according to the following rules: \begin{small} \begin{verbatim} inc(r) >< Z => r ~ S(Z); diff --git a/chapters/core/implementation/02-interaction-rules.tex b/chapters/core/implementation/02-interaction-rules.tex index 8b02c3c..433989d 100644 --- a/chapters/core/implementation/02-interaction-rules.tex +++ b/chapters/core/implementation/02-interaction-rules.tex @@ -17,7 +17,7 @@ The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into f \item \textbf{ReLU}: Unary operator for rectified linear unit. \end{itemize} \item - \textbf{Structural Operators}: Agents that perform some kind of operation on net structure. + \textbf{Structural Operators}: Agents that perform some kind of operation on the net structure. \begin{itemize} \item \textbf{Eraser}: Built-in INPLA unary operator to delete other agents. \item \textbf{Dup}: Built-in INPLA unary operator to duplicate other agents. @@ -34,9 +34,9 @@ The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into f \item \textbf{Terminals}: Agents that compose the normal form. \begin{itemize} - \item \textbf{TermAdd}: This agent is parsed as addition for the SMT solver. - \item \textbf{TermMul}: This agent is parsed as multiplication for the SMT solver. - \item \textbf{TermReLU}: This agent is parsed as rectified linear unit for the SMT solver. + \item \textbf{TermAdd}: This agent is parsed as an addition for the SMT solver. + \item \textbf{TermMul}: This agent is parsed as a multiplication for the SMT solver. + \item \textbf{TermReLU}: This agent is parsed as a rectified linear unit for the SMT solver. \item \textbf{TermSymbolic}: This agent is parsed as a specific variable for the SMT solver. \item \textbf{TermConcrete}: This agent is parsed as a real value for the SMT solver. \end{itemize} @@ -184,10 +184,10 @@ The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into f \end{figure} \paragraph{Linear with Add/Mul} -The \textit{Linear} carrier agent interacts directly with the \textit{Add} and \textit{Mul} operators agents as illustrated in +The \textit{Linear} carrier agent interacts directly with the \textit{Add} and \textit{Mul} operators agents, as illustrated in \textbf{\Cref{fig:rule-linear-add}} and \textbf{\Cref{fig:rule-linear-mul}}. Because interactions are local, the binary -operators need to check one operand a time. For this reason \textit{Add} and \textit{Mul} agents are replaced by -\textit{AddCheckLinear} and \textit{MulCheckLinear} intermediate agents that carry the attributes $q$ and $r$ and their +operators need to check one operand at a time. For this reason, \textit{Add} and \textit{Mul} agents are replaced by +\textit{AddCheckLinear} and \textit{MulCheckLinear} intermediate agents that carry the attributes $q$ and $r$, and their principal port faces the other operand. % Linear >< Add @@ -235,11 +235,11 @@ principal port faces the other operand. \end{figure} \paragraph{Concrete with Add/Mul} -The same logic is applied to the \textit{Concrete} carrier agent, but here analyzing the attribute $k$ -enables short-circuiting. In \textbf{\Cref{fig:rule-concrete-add}} we can see that when summing a \textit{Concrete} -with $k=0$ we do not need to check the other operand and we simply wire it to the output. +The same logic is applied to the \textit{Concrete} carrier agent, but here, analyzing the attribute $k$ +enables short-circuiting. In \textbf{\Cref{fig:rule-concrete-add}}, we can see that when summing a \textit{Concrete} +with $k=0$, we do not need to check the other operand, and we simply wire it to the output. This rewiring is also implemented when multiplying a \textit{Concrete} with $k=1$, as shown in -\textbf{\Cref{fig:rule-concrete-mul}}, with the addition that when $k=0$ the other operand is deleted +\textbf{\Cref{fig:rule-concrete-mul}}, with the addition that when $k=0$, the other operand is deleted before it is even invoked. % Concrete >< Add @@ -339,14 +339,14 @@ before it is even invoked. \end{figure} \paragraph{Linear with AddCheckLinear/MulCheckLinear} -If both operands are \textit{Linear} agents they need to be materialized before being wrapped in another +If both operands are \textit{Linear} agents, they need to be materialized before being wrapped in another \textit{Linear} to allow further simplification. This is done because multiplying two linear packets gives a non-linear result. -While adding two linear packets gives a linear result, it depends on two free variables and the +While adding two linear packets gives a linear result, it depends on two free variables, and the \textit{Linear} agent only supports keeping track of one; consequently, the addition of two linear packets results in their materialization. This is illustrated in \textbf{\Cref{fig:rule-linear-addchecklinear}} -and \textbf{\Cref{fig:rule-linear-mulchecklinear}} where the result of the materialization is passed +and \textbf{\Cref{fig:rule-linear-mulchecklinear}}, where the result of the materialization is passed to a TermAdd or TermMul, for Add and Mul respectively, and then to a \textit{Linear} with attributes $q=1,r=0$. @@ -491,11 +491,11 @@ $q=1,r=0$. \end{figure} \paragraph{Concrete with AddCheckLinear/MulCheckLinear} -If, instead, the first operand is a \textit{Linear} agents and the second is a \textit{Concrete} agent different rules -are applied. In the case of addition (\textbf{\Cref{fig:rule-concrete-addchecklinear}}) the system adds the +If, instead, the first operand is a \textit{Linear} agents and the second is a \textit{Concrete} agent, different rules +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}. +For multiplication (\textbf{\Cref{fig:rule-concrete-mulchecklinear}}), the system multiplies the attribute of +the \textit{Concrete} agent by both the attributes of the \textit{Linear}. % Concrete >< AddCheckLinear \begin{figure}[H] @@ -538,8 +538,8 @@ the \textit{Concrete} agent to both the attributes of the \textit{Linear}. \end{figure} \paragraph{Linear with AddCheckConcrete/MulCheckConcrete} -In the rules shown in \textbf{\Cref{fig:rule-linear-addcheckconcrete}} and \textbf{\Cref{fig:rule-linear-mulcheckconcrete}} -we follow the exact same logic except the first operand is a \textit{Concrete} and the second is a \textit{Linear}. +In the rules shown in \textbf{\Cref{fig:rule-linear-addcheckconcrete}} and \textbf{\Cref{fig:rule-linear-mulcheckconcrete}}, +we follow the exact same logic, except the first operand is a \textit{Concrete} and the second is a \textit{Linear}. % Linear >< AddCheckConcrete \begin{figure}[H] @@ -582,9 +582,9 @@ we follow the exact same logic except the first operand is a \textit{Concrete} a \end{figure} \paragraph{Concrete with AddCheckConcrete/MulCheckConcrete} -Finally if both operands are \textit{Concrete} agents they are either merged into a single \textit{Concrete} +Finally, if both operands are \textit{Concrete} agents, they are either merged into a single \textit{Concrete} or short-circuited as illustrated in \textbf{\Cref{fig:rule-concrete-addcheckconcrete}} and -\textbf{\Cref{fig:rule-concrete-mulcheckconcrete}} following a similar logic to the previous rules. +\textbf{\Cref{fig:rule-concrete-mulcheckconcrete}}, following a similar logic to the previous rules. % Concrete >< AddCheckConcrete \begin{figure}[H] @@ -672,10 +672,10 @@ or short-circuited as illustrated in \textbf{\Cref{fig:rule-concrete-addcheckcon \end{figure} \paragraph{Linear/Concrete with ReLU} -When the \textit{Linear} carrier agent interacts with the \textit{ReLU} operator agents there is not -enough information to perform any simplification so, as shown in \textbf{\Cref{fig:rule-linear-relu}}, -the agent is just materialized, passed to a \textit{TermReLU} and then wrapped in a \textit{Linear}. -In \textbf{\Cref{fig:rule-concrete-relu}} is illustrated that when the \textit{Concrete} carrier agent +When the \textit{Linear} carrier agent interacts with the \textit{ReLU} operator agents, there is not +enough information to perform any simplification, so, as shown in \textbf{\Cref{fig:rule-linear-relu}}, +the agent is just materialized, passed to a \textit{TermReLU}, and then wrapped in a \textit{Linear}. +In \textbf{\Cref{fig:rule-concrete-relu}}, it is illustrated that when the \textit{Concrete} carrier agent meets the \textit{ReLU} agent, a \textit{Concrete} is wired to the output either with attribute $k$ if $k>0$ or with attribute equal $0$ otherwise. @@ -742,9 +742,9 @@ if $k>0$ or with attribute equal $0$ otherwise. \end{figure} \paragraph{Linear/Concrete with Materialize} -When a \textit{Linear} is materialized it explicitly build an AST using \textit{TermAdd}, \textit{TermMul} and \textit{TermConcrete} +When a \textit{Linear} is materialized, it explicitly builds an AST using \textit{TermAdd}, \textit{TermMul}, and \textit{TermConcrete} to recreate $q*x+r$ as shown in \textbf{\Cref{fig:rule-linear-materialize}}. -When a \textit{Concrete} needs to be materialized it is converted into \textit{TermConcrete} as illustrated in +When a \textit{Concrete} needs to be materialized, it is converted into \textit{TermConcrete} as illustrated in \textbf{\Cref{fig:rule-concrete-materialize}}. % Linear >< Materialize diff --git a/chapters/core/implementation/03-translation.tex b/chapters/core/implementation/03-translation.tex index b86e060..92f47e5 100644 --- a/chapters/core/implementation/03-translation.tex +++ b/chapters/core/implementation/03-translation.tex @@ -8,8 +8,8 @@ at most one connection. This limitation is solved by utilizing the \textit{Dup} necessary copies of a value required by the next operations. Since nodes do not know how successor 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. The ONNX operators supported are Gemm +in \textbf{\Cref{alg:onnx-to-in}}, maintains an \textit{interaction} dictionary data structure that maps each tensor +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] @@ -81,8 +81,8 @@ chains of agents, opting instead for balanced binary trees for signal distributi 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 -agents together: in the \textit{Fan-In} the principal port of the agents are facing the leaves, while in the -\textit{Fan-Out} they face the root. +agents together: in the \textit{Fan-In}, the principal ports of the agents are facing the leaves, while in the +\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 6023c2e..ab817c4 100644 --- a/chapters/core/implementation/04-python-module.tex +++ b/chapters/core/implementation/04-python-module.tex @@ -15,14 +15,14 @@ The methods offered by \texttt{vein.Solver} are: \end{itemize} The framework uses a \textit{lazy evaluation} strategy: when loading a neural network, it is placed -into a pending queue and it is reduced to normal form only after the \texttt{check} method is +into a pending queue, and it is reduced to normal form only after the \texttt{check} method is 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 declarations, optional range -constraints on the input variables and the properties to be verified. For Multi-Network (relational) +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. +This approach allows Z3 to compare the outputs directly, given the same inputs. The execution pipeline is implemented within the \texttt{check} method: \begin{itemize} diff --git a/chapters/core/soundness-proof/02-soundness-of-translation.tex b/chapters/core/soundness-proof/02-soundness-of-translation.tex index 4477581..83c0f26 100644 --- a/chapters/core/soundness-proof/02-soundness-of-translation.tex +++ b/chapters/core/soundness-proof/02-soundness-of-translation.tex @@ -1,7 +1,7 @@ \subsection{Soundness of Translation} \label{sec:soundness-of-translation} -We need to prove that for each ONNX operator a semantically equivalent IN is produced. +We need to prove that for each ONNX operator, a semantically equivalent IN is produced. \begin{lemma} The ONNX ReLU operator for an input tensor X and output tensor Y is defined as: @@ -20,7 +20,7 @@ Which is identical to the ONNX definition. \end{lemma} \begin{lemma} -The ONNX Gemm 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 6957c3c..02005e3 100644 --- a/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex +++ b/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex @@ -4,7 +4,7 @@ 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: + For the \textit{Linear} and \textit{Add} agents, we have the interaction rule: $$ \mathit{Linear}(x, q, r) \bowtie \mathit{Add}(\mathit{out}, b) \Rightarrow \mathit{AddCheckLinear}(\mathit{out}, x, q, r) \sim b \\ $$ @@ -26,7 +26,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Linear} and \textit{Mul} agents we have the interaction rule: + For the \textit{Linear} and \textit{Mul} agents, we have the interaction rule: $$ \mathit{Linear}(x, q, r) \bowtie \mathit{Mul}(\mathit{out}, b) \Rightarrow \mathit{MulCheckLinear}(\mathit{out}, x, q, r) \sim b \\ $$ @@ -48,7 +48,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Concrete} and \textit{Add} agents we have the interaction rule: + For the \textit{Concrete} and \textit{Add} agents, we have the interaction rule: $$ \mathit{Concrete}(k) \bowtie \mathit{Add}(\mathit{out}, b) \Rightarrow \begin{cases} @@ -84,7 +84,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Concrete} and \textit{Mul} agents we have the interaction rule: + For the \textit{Concrete} and \textit{Mul} agents, we have the interaction rule: $$ \mathit{Concrete}(k) \bowtie \mathit{Mul}(\mathit{out}, b) \Rightarrow \begin{cases} @@ -123,7 +123,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Linear} and \textit{AddCheckLinear} agents we have the interaction rule: + For the \textit{Linear} and \textit{AddCheckLinear} agents, we have the interaction rule: $$ \begin{aligned} & \mathit{Linear}(y, s, t) \bowtie \mathit{AddCheckLinear}(\mathit{out}, x, q, r) \Rightarrow \\ @@ -178,7 +178,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Linear} and \textit{MulCheckLinear} agents we have the interaction rule: + For the \textit{Linear} and \textit{MulCheckLinear} agents, we have the interaction rule: $$ \begin{aligned} & \mathit{Linear}(y, s, t) \bowtie \mathit{MulCheckLinear}(\mathit{out}, x, q, r) \Rightarrow \\ @@ -229,7 +229,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Concrete} and \textit{AddCheckLinear} agents we have the interaction rule: + For the \textit{Concrete} and \textit{AddCheckLinear} agents, we have the interaction rule: $$ \mathit{Concrete}(j) \bowtie \mathit{AddCheckLinear}(\mathit{out}, x, q, r) \Rightarrow \mathit{Linear}(x, q, r + j) \sim \mathit{out} \\ $$ @@ -251,7 +251,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Concrete} and \textit{MulCheckLinear} agents we have the interaction rule: + For the \textit{Concrete} and \textit{MulCheckLinear} agents, we have the interaction rule: $$ \mathit{Concrete}(j) \bowtie \mathit{MulCheckLinear}(\mathit{out}, x, q, r) \Rightarrow \mathit{Linear}(x, q \cdot j, r \cdot j) \sim \mathit{out} \\ $$ @@ -273,7 +273,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Linear} and \textit{AddCheckConcrete} agents we have the interaction rule: + For the \textit{Linear} and \textit{AddCheckConcrete} agents, we have the interaction rule: $$ \mathit{Linear}(y, s, t) \bowtie \mathit{AddCheckConcrete}(\mathit{out}, k) \Rightarrow \mathit{Linear}(y, s, t + k) \sim \mathit{out} \\ $$ @@ -295,7 +295,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Linear} and \textit{MulCheckConcrete} agents we have the interaction rule: + For the \textit{Linear} and \textit{MulCheckConcrete} agents, we have the interaction rule: $$ \mathit{Linear}(y, s, t) \bowtie \mathit{MulCheckConcrete}(\mathit{out}, k) \Rightarrow \mathit{Linear}(y, s \cdot k, t \cdot k) \sim \mathit{out} \\ $$ @@ -317,7 +317,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Concrete} and \textit{AddCheckConcrete} agents we have the interaction rule: + For the \textit{Concrete} and \textit{AddCheckConcrete} agents, we have the interaction rule: $$ \begin{aligned} & \mathit{Concrete}(j) \bowtie \mathit{AddCheckConcrete}(\mathit{out}, k) \Rightarrow \\ @@ -355,7 +355,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Concrete} and \textit{MulCheckConcrete} agents we have the interaction rule: + For the \textit{Concrete} and \textit{MulCheckConcrete} agents, we have the interaction rule: $$ \begin{aligned} & \mathit{Concrete}(j) \bowtie \mathit{MulCheckConcrete}(\mathit{out}, k) \Rightarrow \\ @@ -396,7 +396,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Linear} and \textit{ReLU} agents we have the interaction rule: + For the \textit{Linear} and \textit{ReLU} agents, we have the interaction rule: $$ \begin{aligned} \mathit{Linear}(x, q, r) \bowtie \mathit{ReLU}(\mathit{out}) \Rightarrow @@ -424,7 +424,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Concrete} and \textit{ReLU} agents we have the interaction rule: + For the \textit{Concrete} and \textit{ReLU} agents, we have the interaction rule: $$ \mathit{Concrete}(k) \bowtie \mathit{ReLU}(\mathit{out}) \Rightarrow \begin{cases} @@ -460,7 +460,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Linear} and \textit{Materialize} agents we have the interaction rule: + For the \textit{Linear} and \textit{Materialize} agents, we have the interaction rule: $$ \begin{aligned} & \mathit{Linear}(x, q, r) \bowtie \mathit{Materialize}(\mathit{out}) \Rightarrow \\ @@ -510,7 +510,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Concrete} and \textit{Materialize} agents we have the interaction rule: + For the \textit{Concrete} and \textit{Materialize} agents, we have the interaction rule: $$ \mathit{Concrete}(k) \bowtie \mathit{Materialize}(\mathit{out}) \Rightarrow \mathit{TermConcrete}(k) \sim \mathit{out} \\ $$ @@ -532,7 +532,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Linear} and \textit{Dup} agents we have the interaction rule: + 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 \\ @@ -561,7 +561,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Linear} and \textit{Eraser} agents we have the interaction rule: + For the \textit{Linear} and \textit{Eraser} agents, we have the interaction rule: $$ \mathit{Linear}(x, q, r) \bowtie \mathit{Eraser} \Rightarrow \mathit{Eraser} \sim x \\ $$ @@ -583,7 +583,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Concrete} and \textit{Dup} agents we have the interaction rule: + For the \textit{Concrete} and \textit{Dup} agents, we have the interaction rule: $$ \mathit{Concrete}(k) \bowtie \mathit{Dup}(x, y) \Rightarrow \mathit{Concrete}(k) \sim x; \mathit{Concrete}(k) \sim y \\ $$ @@ -606,7 +606,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{Concrete} and \textit{Eraser} agents we have the interaction rule: + For the \textit{Concrete} and \textit{Eraser} agents, we have the interaction rule: $$ \mathit{Concrete}(k) \bowtie \mathit{Eraser} \Rightarrow \\ $$ @@ -623,11 +623,11 @@ We need to prove that each interaction rule does not alter the semantics of the \end{aligned} \end{aligned} $$ - Since $k \in \mathbb{R}$ is not violated by RHS, the rule is sound. + Since $k \in \mathbb{R}$ is not violated by the RHS, the rule is sound. \end{lemma} \begin{lemma} - For the \textit{TermAdd} and \textit{Dup} agents we have the interaction rule: + 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 \\ @@ -658,7 +658,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{TermAdd} and \textit{Eraser} agents we have the interaction rule: + For the \textit{TermAdd} and \textit{Eraser} agents, we have the interaction rule: $$ \mathit{TermAdd}(a, b) \bowtie \mathit{Eraser} \Rightarrow \mathit{Eraser} \sim a; \mathit{Eraser} \sim b \\ $$ @@ -681,7 +681,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{TermMul} and \textit{Dup} agents we have the interaction rule: + 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 \\ @@ -712,7 +712,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{TermMul} and \textit{Eraser} agents we have the interaction rule: + For the \textit{TermMul} and \textit{Eraser} agents, we have the interaction rule: $$ \mathit{TermMul}(a, b) \bowtie \mathit{Eraser} \Rightarrow \mathit{Eraser} \sim a; \mathit{Eraser} \sim b \\ $$ @@ -735,7 +735,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{TermReLU} and \textit{Dup} agents we have the interaction rule: + For the \textit{TermReLU} and \textit{Dup} agents, we have the interaction rule: $$ \begin{aligned} & \mathit{TermReLU}(z) \bowtie \mathit{Dup}(x, y) \Rightarrow \\ @@ -764,7 +764,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{TermReLU} and \textit{Eraser} agents we have the interaction rule: + For the \textit{TermReLU} and \textit{Eraser} agents, we have the interaction rule: $$ \mathit{TermReLU}(x) \bowtie \mathit{Eraser} \Rightarrow \mathit{Eraser} \sim x \\ $$ @@ -786,7 +786,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{TermConcrete} and \textit{Dup} agents we have the interaction rule: + For the \textit{TermConcrete} and \textit{Dup} agents, we have the interaction rule: $$ \begin{aligned} & \mathit{TermConcrete}(k) \bowtie \mathit{Dup}(x, y) \Rightarrow \\ @@ -813,7 +813,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{TermConcrete} and \textit{Eraser} agents we have the interaction rule: + For the \textit{TermConcrete} and \textit{Eraser} agents, we have the interaction rule: $$ \mathit{TermConcrete}(k) \bowtie \mathit{Eraser} \Rightarrow \\ $$ @@ -830,11 +830,11 @@ We need to prove that each interaction rule does not alter the semantics of the \end{aligned} \end{aligned} $$ - Since $k \in \mathbb{R}$ is not violated by RHS, the rule is sound. + Since $k \in \mathbb{R}$ is not violated by the RHS, the rule is sound. \end{lemma} \begin{lemma} - For the \textit{TermSymbolic} and \textit{Dup} agents we have the interaction rule: + For the \textit{TermSymbolic} and \textit{Dup} agents, we have the interaction rule: $$ \begin{aligned} & \mathit{TermSymbolic}(id) \bowtie \mathit{Dup}(x, y) \Rightarrow \\ @@ -861,7 +861,7 @@ We need to prove that each interaction rule does not alter the semantics of the \end{lemma} \begin{lemma} - For the \textit{TermSymbolic} and \textit{Eraser} agents we have the interaction rule: + For the \textit{TermSymbolic} and \textit{Eraser} agents, we have the interaction rule: $$ \mathit{TermSymbolic}(id) \bowtie \mathit{Eraser} \Rightarrow \\ $$ @@ -878,5 +878,5 @@ We need to prove that each interaction rule does not alter the semantics of the \end{aligned} \end{aligned} $$ - Since $x_{id} \in \mathbb{R}$ is not violated by RHS, the rule is sound. + Since $x_{id} \in \mathbb{R}$ is not violated by the RHS, the rule is sound. \end{lemma} diff --git a/chapters/core/soundness-proof/04-soundness-of-reduction.tex b/chapters/core/soundness-proof/04-soundness-of-reduction.tex index 15cc4f4..c373657 100644 --- a/chapters/core/soundness-proof/04-soundness-of-reduction.tex +++ b/chapters/core/soundness-proof/04-soundness-of-reduction.tex @@ -4,8 +4,8 @@ \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 - outputs. + \item \textbf{Acyclic}: the net forms a forest where the roots are the free wires representing + the network outputs. \item \textbf{Orientation}: carrier agents always have their principal ports oriented toward the outputs, while operator and intermediate agents always have their principal ports oriented toward the inputs. No interaction rule introduces carriers facing the input nor operators or @@ -29,7 +29,7 @@ We will proceed by induction on the number $n$ of reduction steps: \paragraph{Base case: $n = 0$} By \textbf{\Cref{sec:soundness-of-translation}}, the initial $\text{IN}_0$ is constructed such that its semantics $\llbracket \text{IN}_0 \rrbracket$ exactly - match the mathematical definition of the ONNX operators in $\text{NN}$, it follows that: + match the mathematical definition of the ONNX operators in $\text{NN}$; it follows that: \begin{equation} \llbracket \text{IN}_{0} \rrbracket = \llbracket \text{NN} \rrbracket \end{equation} @@ -37,7 +37,7 @@ \paragraph{Induction step: $n \to n + 1$} Assume $\llbracket \text{IN}_n \rrbracket = \llbracket \text{NN} \rrbracket$. If $\text{IN}_n$ is in normal form, the proof is complete. Otherwise, there exists an active pair $A \bowtie B$ that reduces $\text{IN}_n$ to $\text{IN}_{n+1}$. By \textbf{\Cref{sec:soundness-of-interaction-rules}}, - the mathematical definition is preserved after any reduction step, it follows that: + the mathematical definition is preserved after any reduction step; it follows that: \begin{equation} \llbracket \text{IN}_{n+1} \rrbracket = \llbracket \text{IN}_{n} \rrbracket \end{equation} @@ -122,7 +122,7 @@ \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 + 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 |