diff options
Diffstat (limited to 'chapters/core/implementation')
| -rw-r--r-- | chapters/core/implementation/01-inpla.tex | 53 | ||||
| -rw-r--r-- | chapters/core/implementation/02-interaction-rules.tex | 43 | ||||
| -rw-r--r-- | chapters/core/implementation/03-translation.tex | 142 | ||||
| -rw-r--r-- | chapters/core/implementation/04-python-module.tex | 34 |
4 files changed, 250 insertions, 22 deletions
diff --git a/chapters/core/implementation/01-inpla.tex b/chapters/core/implementation/01-inpla.tex index b534705..5b2eab9 100644 --- a/chapters/core/implementation/01-inpla.tex +++ b/chapters/core/implementation/01-inpla.tex @@ -1,4 +1,55 @@ \subsection{Inpla fork} \label{sec:inpla} -% This subsection talks about my Inpla fork +The VEIN reduction engine utilizes a modified version of INPLA\footnote{\textbf{\href{https://github.com/inpla/inpla/blob/main/Gentle_introduction_Inpla.md}{INPLA documentation.}}}, +a multi-threaded parallel interpreter of IN. Performance and ease of use motivated the choice of +INPLA. Additionally, it supports attribute values, which is a special extension that allows agents +to hold numerical values at their ports. + +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 + 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. +\end{itemize} + +\paragraph{INPLA syntax} +INPLA evaluates nets, they consist of connections between terms. Terms are built on names and agents: +\begin{verbatim} +<term> ::= <name> | <agent> +<name> ::= <nameID> +<agent> ::= <agentID> + | <agentID> ['(' <term> ',' ... ',' <term> ')'] +\end{verbatim} +\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). +\end{itemize} +A connection is a relation between two terms and the symbol \texttt{\~} expresses this relation. +Interaction rules rewrite connections between agents: +\begin{verbatim} +<interaction-rule> ::= <rule-agent> '><' <rule-agent> '=>' <connections> ';' +<rule-agent> ::= <agentID> + | <agentID> '(' <name> ',' ... ',' <name> ')' +\end{verbatim} + +\paragraph{Example} +Unary natural numbers are built by $\texttt{Z}$ (zero) and $\texttt{S}$ (successive function). For +instance, 0, 1, 2, 3 are expressed as \texttt{Z}, \texttt{S(Z)}, \texttt{S(S(Z))}, \texttt{S(S(S(Z)))}. Here, let's think about an +increment operation "inc" such that: +\begin{verbatim} +inc(n) = S(n). +\end{verbatim} +This is written as the following rules: +\begin{verbatim} +inc(r) >< Z => r ~ S(Z); +inc(r) >< S(x) => r ~ S(S(x)); +\end{verbatim} +Then, the result of \texttt{inc(r) \~{} S(S(Z))} is: +\begin{verbatim} +r ~ S(S(S(Z))); +\end{verbatim} diff --git a/chapters/core/implementation/02-interaction-rules.tex b/chapters/core/implementation/02-interaction-rules.tex index 84dc27b..b657ee9 100644 --- a/chapters/core/implementation/02-interaction-rules.tex +++ b/chapters/core/implementation/02-interaction-rules.tex @@ -1,9 +1,7 @@ \subsection{Interaction Rules} \label{sec:interaction-rules} -This subsection contains the definition of the agents and the interaction rules that implement the symbolic simplification. - -The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into three groups: +The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into four groups: \begin{itemize} \item \textbf{Carriers}: Agents that contain float attributes. @@ -30,12 +28,12 @@ The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into t \item \textbf{Materialize}: Converts a Linear agent into an explicit representation for the SMT solver. \end{itemize} \item - \textbf{Inerts}: Agents that will compose the normal form. + \textbf{Inerts}: Agents that compose the normal form. \begin{itemize} - \item \textbf{TermAdd}: This agent that will be parsed as addition for the SMT solver. - \item \textbf{TermMul}: This agent that will be parsed as multiplication for the SMT solver. - \item \textbf{TermReLU}: This agent that will be parsed as rectified linear unit for the SMT solver. - \item \textbf{Symbolic}: This agent that will be parsed as specific variable for the SMT solver. + \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{Symbolic}: This agent is parsed as specific variable for the SMT solver. \end{itemize} \end{itemize} @@ -172,11 +170,12 @@ The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into t \label{fig:agents} \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 \textbf{\Cref{fig:rule-linear-add}} and \textbf{\Cref{fig:rule-linear-mul}}. Because interactions are local, the binary -operators need to check one operator at the time. For this reason \textit{Add} and \textit{Mul} gets replaced by +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 -principal port is faced toward the other operand. +principal port faces the other operand. % Linear >< Add \begin{figure}[ht] @@ -222,12 +221,13 @@ principal port is faced toward the other operand. \label{fig:rule-linear-mul} \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. 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 -before is even invoked. +before it is even invoked. % Concrete >< Add \begin{figure}[ht] @@ -325,11 +325,13 @@ before is even invoked. \label{fig:rule-concrete-mul} \end{figure} +\paragraph{Linear with AddCheckLinear/MulCheckLinear} 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 \textit{Linear} agent -only supports one. A solution to this could be storing a dictionay of variables instead of a single one. +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 to a TermAdd or TermMul, for Add and Mul respectively, and then to a \textit{Linear} with attributes @@ -475,10 +477,11 @@ $q=1,r=0$. \label{fig:rule-linear-mulchecklinear} \end{figure} -Instead if 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}}) we add 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}}) we multiply the attribute of +\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 +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} % Concrete >< AddCheckLinear @@ -521,6 +524,7 @@ the \textit{Concrete} agent to both the attributes of the \textit{Linear} \label{fig:rule-concrete-mulchecklinear} \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}. @@ -564,6 +568,7 @@ we follow the exact same logic except the first operand is a \textit{Concrete} a \label{fig:rule-linear-mulcheckconcrete} \end{figure} +\paragraph{Concrete with AddCheckConcrete/MulCheckConcrete} 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. @@ -653,6 +658,7 @@ or short-circuited as illustrated in \textbf{\Cref{fig:rule-concrete-addcheckcon \label{fig:rule-concrete-mulcheckconcrete} \end{figure} +\paragraph{Linear/Concrete with ReLU} When the \textit{Linear} carrier agent interacts with the \textit{ReLU} operator agents there is no 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}. @@ -722,7 +728,8 @@ if $k>0$ or with attribute equal $0$ otherwise. \label{fig:rule-concrete-relu} \end{figure} -When a \textit{Linear} is materialized it will explicitly build an AST using \textit{TermAdd} and \textit{TermMul} +\paragraph{Linear/Concrete with Materialize} +When a \textit{Linear} is materialized it explicitly build an AST using \textit{TermAdd} and \textit{TermMul} to recreate $q*x+r$ as shown in \textbf{\Cref{fig:rule-linear-materialize}}. When a \textit{Concrete} needs to be materialized nothing needs to be done and it is directly wired to output \textbf{\Cref{fig:rule-concrete-materialize}}. diff --git a/chapters/core/implementation/03-translation.tex b/chapters/core/implementation/03-translation.tex index 4f2064c..638ff17 100644 --- a/chapters/core/implementation/03-translation.tex +++ b/chapters/core/implementation/03-translation.tex @@ -1,4 +1,142 @@ -\subsection{ONNX Translation} +\subsection{ONNX-to-IN Translation} \label{sec:translation} -% This subsection talks about the function used to translate ONNX to Inpla syntax +An ONNX neural network is organized as a \textit{Directed Acyclic Graph} (DAG), where nodes represent +a specific mathematical operation. While in a standard DAG, a node can be connected to many nodes to +share its value or result, in an IN, an agent has a fixed number of ports, with each port supporting +at most one connection. This limitation is solved by utilizing the \textit{Dup} agent to create the +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. + +To maximize the concurrency of the INPLA engine, the translation layer avoids generating linear +chains of agents, opting instead for balanced binary trees for signal distribution (single input to +multiple output) and signal reduction (multiple input to single output). As \textbf{\Cref{alg:balanced-fan-in}} +and \textbf{\Cref{alg:balanced-fan-out}} illustrate, the depth of agent chains (especially \textit{Dup} chains) +is limited to $O(\log N)$. The two algorithms are very similar, the difference is in how they wire the +agents together: in the \textit{Fan-In} the principal port of the agents are facing the leaves, while in the +\textit{Fan-Out} they are facing the root. + +\begin{algorithm}[ht] + \caption{Backwards ONNX-to-IN Translation} + \label{alg:onnx-to-in} + \SetKwInOut{Input}{Input}\SetKwInOut{Output}{Output} + \Input{ONNX Graph $G$} + \Output{Inpla script $S$} + + $interactions \leftarrow \emptyset$ \tcp*{Map: Tensor Name $\rightarrow$ List of ports} + $S \leftarrow \emptyset$ + + \ForEach{neuron $y$ in $G.output$}{ + $interactions[G.output][y] \leftarrow [\text{Materialize}(result_y)]$ + } + + \ForEach{node $N$ in \textbf{reverse}($G.nodes$)}{ + \Switch{$N.type$}{ + \Case{ReLU}{ + \ForEach{neuron $i$ in $N.output$}{ + $sink \leftarrow \text{BalancedFanOut}(interactions[N.output][i], \text{Dup}, S)$ + + $v \leftarrow \text{generate\_wire}()$ + + $interactions[N.input][i].\text{append}(\text{ReLU}(v))$ + + $S.\text{append}(v \sim sink)$ + } + } + \Case{Gemm}{ + \ForEach{neuron $j$ in $N.output$}{ + $sink \leftarrow \text{BalancedFanOut}(interactions[N.output][j], \text{Dup}, S)$ + + $neuron\_terms \leftarrow \emptyset$ + + \ForEach{neuron $i$ in $N.input$}{ + $v \leftarrow \text{generate\_wire}()$ + + $interactions[N.input][i].\text{append}(\text{Mul}(v, \text{Concrete}(N.alpha * N.weight[j, i])))$ + + $neuron\_terms.\text{append}(v)$ + } + + $neuron\_terms.\text{append}(\text{Concrete}(N.beta * N.bias[j]))$ + + $root \leftarrow \text{BalancedFanIn}(neuron\_terms, \text{Add}, S)$ + + $S.\text{append}(root \sim sink)$ + } + } + \Case{Identity}{ + $interactions[N.input] \leftarrow interactions[N.output]$ + } + } + } + + \ForEach{neuron $x$ in $G.input$}{ + $sink \leftarrow \text{BalancedFanOut}(interactions[G.input][x], \text{Dup}, S)$ + + $S.\text{append}(sink \sim \text{Linear}(\text{Symbolic}(x), 1.0, 0.0))$ + } + + \Return{S} +\end{algorithm} + +\begin{algorithm}[ht] + \caption{Balanced Fan-In} + \label{alg:balanced-fan-in} + \SetKwInOut{Input}{Input}\SetKwInOut{Output}{Output} + \Input{A list of input signal wires $T$, Agent type $A$, Script $S$} + \Output{A single wire connected to the output of the balanced tree} + + \If{$T = \emptyset$}{\Return{\text{Eraser}}} + \If{$|T| = 1$}{\Return{$T[0]$}} + + \While{$|T| > 1$}{ + $T' \leftarrow \emptyset$ + + \For{$i \leftarrow 0$ \KwTo $|T|-1$ \textbf{by} 2}{ + \eIf{$i+1 < |T|$}{ + $w_{out} \leftarrow \text{generate\_wire}()$ + + $S.\text{append}(T[i] \sim A(w_{out}, T[i+1]))$ + + $T'.\text{append}(w_{out})$ + }{ + $T'.\text{append}(T[i])$ + } + } + $T \leftarrow T'$ + } + \Return{$T[0]$} +\end{algorithm} + + +\begin{algorithm}[ht] + \caption{Balanced Fan-Out} + \label{alg:balanced-fan-out} + \SetKwInOut{Input}{Input}\SetKwInOut{Output}{Output} + \Input{A list of output signal wires $T$, Agent type $A$, Script $S$} + \Output{A single wire connected to the input of the balanced tree} + + \If{$T = \emptyset$}{\Return{\text{Eraser}}} + \If{$|T| = 1$}{\Return{$T[0]$}} + + \While{$|T| > 1$}{ + $T' \leftarrow \emptyset$ + + \For{$i \leftarrow 0$ \KwTo $|T|-1$ \textbf{by} 2}{ + \eIf{$i+1 < |T|$}{ + $w_{out} \leftarrow \text{generate\_wire}()$ + + $S.\text{append}(w_{out} \sim A(T[i], T[i+1]))$ + + $T'.\text{append}(w_{out})$ + }{ + $T'.\text{append}(T[i])$ + } + } + $T \leftarrow T'$ + } + \Return{$T[0]$} +\end{algorithm} diff --git a/chapters/core/implementation/04-python-module.tex b/chapters/core/implementation/04-python-module.tex index 7f144db..a40df41 100644 --- a/chapters/core/implementation/04-python-module.tex +++ b/chapters/core/implementation/04-python-module.tex @@ -1,4 +1,36 @@ \subsection{Python Module} \label{sec:python-module} -% This subsection talks how the tool is contained in a neat python module and various optimizations +The core functionality of the VEIN system is implemented via the \texttt{vein.Solver}, an extension of +the \texttt{z3.Solver} class offered in the Z3 python +package\footnote{\href{https://pypi.org/project/z3-solver}{\textbf{PyPi package}}}. This design choice +ensures flexibility and ease of use for researchers already familiar with using the Z3 Python API. + +The methods offered by \texttt{vein.Solver} are: +\begin{itemize} + \item \texttt{load\_onnx}: loads a neural network in ONNX file format. + \item \texttt{load\_smtlib}: loads a file containing the specification. + \item \texttt{check}: orchestrates the translation and reduction pipeline before invoking the + solver to check the specification against one or many neural networks. +\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 +called. + +The specification follows the SMT-LIB\footnote{\href{https://smt-lib.org}{\textbf{SMT-LIB Website}}} +format. It should contain the input and output symbolic variables declaration, optional range +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. + +The execution pipeline is implemented within the \texttt{check} method: +\begin{itemize} + \item \texttt{inpla\_export}: invokes the translation layer to generate an IN. + \item \texttt{inpla\_run}: executes INPLA as a subprocess. + \item \texttt{z3\_evaluate}: parses the normal form, represented by an AST, and constructs the + Z3 expression. +\end{itemize} +This method utilizes a memoization technique to increase performance: if a specific pair of (neural +network, range constraints) has been previously reduced to a normal form, the system retrieves the +cached Z3 expression, instead of running the pipeline redundantly. |