diff options
Diffstat (limited to 'chapters/core/implementation')
| -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 |
4 files changed, 44 insertions, 44 deletions
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} |