diff options
Diffstat (limited to 'chapters/core')
| -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 |
10 files changed, 95 insertions, 94 deletions
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 |