diff options
| -rw-r--r-- | chapters/01-introduction.tex | 127 | ||||
| -rw-r--r-- | chapters/core/implementation/02-interaction-rules.tex | 25 | ||||
| -rw-r--r-- | main.tex | 2 | ||||
| -rw-r--r-- | references.bib | 32 |
4 files changed, 136 insertions, 50 deletions
diff --git a/chapters/01-introduction.tex b/chapters/01-introduction.tex index a6a69c5..8b912db 100644 --- a/chapters/01-introduction.tex +++ b/chapters/01-introduction.tex @@ -1,67 +1,106 @@ \chapter{Introduction} \label{ch:introduction} -This chapter provides an overview of the thesis. - % Context -Artificial Intelligence systems 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 their exceptional -capacity of representing non-linear functions. But they don't come without drawbacks: neural -networks are ``black boxes'' that lack transparency. To take advantage of these powerful tools in -critical system guarantees need to be provided. +Artificial Intelligence systems have made significant advancements in the last few years and enabled +us to enter a new age of computing. Most of the credit goes to deep neural networks, and to their +exceptional capacity for representing non-linear functions. But they do not come without drawbacks: +neural networks are ``black boxes'' that lack transparency. To take advantage of these powerful +tools in critical systems such as medicine and aerospace, we need to provide formal guarantees to +ensure their safety and trustworthiness. % Problem -Neural networks can be viewed as mathematical functions and SMT solvers are used to check properties, -like equivalence, against them. Running a solver against a complex function is computationally -expensive, it is important to make sure that the function is simplified as much as possible to take -away useless burden from the solver. +In the field of neural network verification, a verification problem is composed of: a trained neural +network and a set of specifications. Then a verification algorithm checks whether the specifications +either hold or are violated. The kind of properties that can be verified are two: +\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. +\end{itemize} +An example of a Multi-Network property is equivalence between different neural networks; this +verification is crucial if we want to replace 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 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. + +Furthermore, we lack a formal intermediate representation. Since we are +not able to directly feed a neural network to a SMT solver, a sound and deterministic model of +representation is needed to bridge this gap. % Solution -We present VEIN, a framework that leverages the computational properties of interaction nets to -perform symbolic simplification of neural networks prior to formal verification. -The system is composed of two primary modules: a modified version of Inpla and the Z3 SMT solver for -property validation. -The tool is divided into three steps: +To address the computational bottleneck, we can perform symbolic simplification on the neural +network as a pre-processing step to reduce the burden on the SMT solver. Considering that we can +easily map the layers and neurons of neural networks to graph nodes and that the input of a SMT +solver is a mathematical formula that can be represented by an \textit{Abstract Syntax Tree} (AST), we can +use a graph rewriting system as intermediate model. The motivation behind this choice is that this +type of model would enable us to simultaneously apply the simplification and produce the AST by +directly rewriting the graph obtained from the neural network. +To model such graphs and these rewriting mechanisms, we leverage \textit{Interaction Nets} +(IN)~\cite{lafont1990interactionnets}, a graphical model of computation characterized by local and +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, +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: \begin{itemize} - \item \textbf{Translation}: a neural network in ONNX format is translated into an interaction net using - the Inpla string representation; - \item \textbf{Reduction}: the interaction net gets reduced to its normal form by Inpla; - \item \textbf{Evaluation}: the normal form gets processed along with the property to verify by Z3. + \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; + \item \textbf{Solver}: Z3~\cite{demoura2008z3} for property validation. \end{itemize} -Z3 is not optimized for ReLU splitting, but it was chosen for its mature Python package. -In any case a specialized solver like Marabou can be integrated to improve performance. -Our contributions are: +The tool runtime follows three steps: \begin{itemize} - \item \textbf{Interaction Rules}: we designed a set of interaction rules to enable symbolic constant - folding; - \item \textbf{ONNX-Interaction Net Translation}: we developed a translation procedure for ONNX models to - interaction net; - \item \textbf{Soundness Analysis}: we provided a formal proof that the interaction net reduction preserves - the mathematical properties of the neural network; - \item \textbf{Experimental Evaluation}: we conducted an extensive benchmarking on widely known datasets and - common VNN-COMP datasets of varying complexity. + \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 + 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 + solver to evaluate it along with the provided specification. \end{itemize} % Validation -Our interaction nets pipeline soundness is proven by induction on the number of interaction steps, -demonstrating that the ONNX translation and each interaction rule preserves the semantic meaning of -the original neural network. Furthermore, interaction nets are deterministic and strongly confluent, -meaning they will always reduce to the same normal form because interactions are local and linear. -In addition to this formal analysis, we conducted several benchmarks on checking equivalence between -a neural network trained on a dataset and a transformation. +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. + +% Contributions +The development of the VEIN framework and the design of its underlying simplification layer +constitute the primary work of this thesis. To address the challenges of verification complexity (A) +and the need for a formal model of representation (B), this thesis introduces several key +contributions: +\begin{itemize} + \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 + models to IN; + \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 + 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 + \href{https://vnn-comp.github.io/}{\textbf{website}}.} (VNN-COMP) datasets of varying complexity. +\end{itemize} % Outline \section{Outline} \label{sec:outline} This section outlines the organization of the thesis: \begin{itemize} - \item \textbf{\Cref{ch:background}}: Introduces key concepts to understand the contributions... - \begin{itemize} - \item \textbf{\Cref{sec:neural-networks}}: Introduces the concepts of neural networks and deep learning... - \item \textbf{\Cref{sec:interaction-nets}}: Introduces the interaction net computational model... - \item \textbf{\Cref{sec:satisfiability-modulo-theories}}: Introduces SMT solvers... - \end{itemize} - \item \textbf{\Cref{ch:core}}: Dives deeper into the implementation... + \item \textbf{\Cref{ch:background}}: Introduces key concepts needed to understand the main work... + \item \textbf{\Cref{ch:core}}: Dives deeper into the details... \item \textbf{\Cref{ch:related-work}}: Analyzes existing verification approaches... \item \textbf{\Cref{ch:conclusion}}: Summarizes the findings and discusses future work... \end{itemize} diff --git a/chapters/core/implementation/02-interaction-rules.tex b/chapters/core/implementation/02-interaction-rules.tex index 1cf4d26..84dc27b 100644 --- a/chapters/core/implementation/02-interaction-rules.tex +++ b/chapters/core/implementation/02-interaction-rules.tex @@ -8,7 +8,7 @@ The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into t \item \textbf{Carriers}: Agents that contain float attributes. \begin{itemize} - \item \textbf{Linear}: Represents the linear transformation $f(x) = q \cdot x + r$. + \item \textbf{Linear}: Represents the affine transformation $f(x) = q \cdot x + r$. \item \textbf{Concrete}: Represents a constant value $k$. \end{itemize} \item @@ -17,8 +17,8 @@ The agents, illustrated in \textbf{\Cref{fig:agents}}, can be categorized into t \item \textbf{Add}: Binary operator for addition. \item \textbf{Mul}: Binary operator for multiplication. \item \textbf{ReLU}: Unary operator for rectified linear unit. - \item \textbf{Eraser}: Built-in Inpla unary operator to delete other agents. - \item \textbf{Duplicator}: Built-in Inpla unary operator to duplicate other agents. + \item \textbf{Eraser}: Built-in INPLA unary operator to delete other agents. + \item \textbf{Duplicator}: Built-in INPLA unary operator to duplicate other agents. \end{itemize} \item \textbf{Intermediates}: Agents needed to perform each step of the operators. @@ -227,7 +227,7 @@ enables short-circuiting. In \textbf{\Cref{fig:rule-concrete-add}} we can see th 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 the SMT solver is even invoked. +before is even invoked. % Concrete >< Add \begin{figure}[ht] @@ -249,6 +249,7 @@ before the SMT solver is even invoked. \node[right] at (AC.above pal) {$\mathit{b}$}; \node[left] at (AC.above pax) {$\mathit{out}$}; } \\ + \hline % k == 0 \interactionrule[$k=0$]{ \agentConcrete{C}{0}[90] @@ -288,6 +289,7 @@ before the SMT solver is even invoked. \node[right] at (MC.above pal) {$\mathit{b}$}; \node[left] at (MC.above pax) {$\mathit{out}$}; } \\ + \hline % k == 0 \interactionrule[$k=0$]{ \agentConcrete{C}{0}[90] @@ -303,6 +305,7 @@ before the SMT solver is even invoked. \node[right] at (C.above pal) {$\mathit{out}$}; \node[right] at (E.above pal) {$\mathit{b}$}; } \\ + \hline % k == 1 \interactionrule[$k=1$]{ \agentConcrete{C}{1}[90] @@ -359,6 +362,7 @@ $q=1,r=0$. \node[left] at (L2.above pax) {$\mathit{y}$}; \node[right] at (L3.above pal) {$\mathit{out}$}; } \\ + \hline % (s == 0) && (t == 0) \interactionrule[$(s=0)\land(t=0)$]{ \agentLinear{L}{0}{0}[90] @@ -376,6 +380,7 @@ $q=1,r=0$. \node[right] at (L.above pal) {$\mathit{out}$}; \node[right] at (E.above pal) {$\mathit{y}$}; } \\ + \hline % (q == 0) && (r == 0) \interactionrule[$(q=0)\land(r=0)$]{ \agentLinear{L}{s}{t}[90] @@ -393,6 +398,7 @@ $q=1,r=0$. \node[right] at (L.above pal) {$\mathit{out}$}; \node[right] at (E.above pal) {$\mathit{x}$}; } \\ + \hline % (q == 0) && (r == 0) && (s == 0) && (t == 0) \interactionrule[$(q=0)\land(r=0)\land(s=0)\land(t=0)$]{ \agentLinear{L}{0}{0}[90] @@ -444,6 +450,7 @@ $q=1,r=0$. \node[left] at (L2.above pax) {$\mathit{y}$}; \node[right] at (L3.above pal) {$\mathit{out}$}; } \\ + \hline % ((q == 0) && (r == 0)) || ((s == 0) && (t == 0)) \interactionrule[$((q=0)\land(r=0))\lor((s=0)\land(t=0))$]{ \agentLinear{L}{s}{t}[90] @@ -578,6 +585,7 @@ or short-circuited as illustrated in \textbf{\Cref{fig:rule-concrete-addcheckcon \inetwirefree(C.pal) \node[right] at (C.above pal) {$\mathit{out}$}; } \\ + \hline % j == 0 \interactionrule[$j=0$]{ \agentConcrete{C}{0}[90] @@ -613,6 +621,7 @@ or short-circuited as illustrated in \textbf{\Cref{fig:rule-concrete-addcheckcon \inetwirefree(C.pal) \node[right] at (C.above pal) {$\mathit{out}$}; } \\ + \hline % j == 0 \interactionrule[$j = 0$]{ \agentConcrete{C}{0}[90] @@ -625,6 +634,7 @@ or short-circuited as illustrated in \textbf{\Cref{fig:rule-concrete-addcheckcon \inetwirefree(C.pal) \node[right] at (C.above pal) {$\mathit{out}$}; } \\ + \hline % j == 1 \interactionrule[$j = 1$]{ \agentConcrete{C}{1}[90] @@ -644,7 +654,7 @@ or short-circuited as illustrated in \textbf{\Cref{fig:rule-concrete-addcheckcon \end{figure} When the \textit{Linear} carrier agent interacts with the \textit{ReLU} operator agents there is no -enough informations to perform any simplification so, as shown in \textbf{\Cref{fig:rule-linear-relu}}, +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 meets the \textit{ReLU} agent, a \textit{Concrete} is wired to the output either with attribute $k$ @@ -693,6 +703,7 @@ if $k>0$ or with attribute equal $0$ otherwise. \inetwirefree(C.pal) \node[right] at (C.above pal) {$\mathit{out}$}; } \\ + \hline % k > 0 \interactionrule[$k > 0$]{ \agentConcrete{C}{k}[90] @@ -739,6 +750,7 @@ When a \textit{Concrete} needs to be materialized nothing needs to be done and i \node [left] at (TM.above pax 2) {$\mathit{x}$}; \node [right] at (TA.above pal) {$\mathit{out}$}; } \\ + \hline % q == 0 \interactionrule[$q=0$]{ \agentLinear{L}{0}{r}[90] @@ -754,6 +766,7 @@ When a \textit{Concrete} needs to be materialized nothing needs to be done and i \node [right] at (C.above pal) {$\mathit{out}$}; \node [right] at (E.above pal) {$\mathit{x}$}; } \\ + \hline % (q == 1) && (r == 0) \interactionrule[$(q=1)\land(r=0)$]{ \agentLinear{L}{1}{0}[90] @@ -767,6 +780,7 @@ When a \textit{Concrete} needs to be materialized nothing needs to be done and i \node(x) at (1, 0) {$\mathit{x}$}; \draw[\inetwirestyle] (x) -- (out); } \\ + \hline % (q == 1) && (r != 0) \interactionrule[$(q=1)\land(r\neq0)$]{ \agentLinear{L}{1}{r}[90] @@ -783,6 +797,7 @@ When a \textit{Concrete} needs to be materialized nothing needs to be done and i \node [left] at (TA.above pax 1) {$\mathit{x}$}; \node [right] at (TA.above pal) {$\mathit{out}$}; } \\ + \hline % (q != 0) && (r == 0) \interactionrule[$(q\neq0)\land(r=0)$]{ \agentLinear{L}{q}{0}[90] @@ -12,7 +12,9 @@ % \usepackage[scaled=.83]{beramono} \usepackage{lineno} \usepackage{tikz-inet} + \usetikzlibrary{calc} +\linenumbers \input{macros} diff --git a/references.bib b/references.bib index ed5d88f..8ddabea 100644 --- a/references.bib +++ b/references.bib @@ -1 +1,31 @@ -% Empty bibliography file +@inproceedings{lafont1990interactionnets, + author = {Lafont, Yves}, + title = {Interaction nets}, + year = {1989}, + isbn = {0897913434}, + publisher = {Association for Computing Machinery}, + address = {New York, NY, USA}, + url = {https://doi.org/10.1145/96709.96718}, + doi = {10.1145/96709.96718}, + abstract = {We propose a new kind of programming language, with the following features:Interaction nets generalize Girard's proof nets of linear logic and illustrate the advantage of an integrated logic approach, as opposed to the external one. In other words, we did not try to design a logic describing the behaviour of some given computational system, but a programming language for which the type discipline is already (almost) a logic.In fact, we shall scarcely refer to logic, because we adopt a na\"{\i}ve and pragmatic style. A typical application we have in mind for this language is the design of interactive softwares such as editors or window managers.}, + booktitle = {Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages}, + pages = {95–108}, + numpages = {14}, + location = {San Francisco, California, USA}, + series = {POPL '90} +} +@inproceedings{demoura2008z3, + author="de Moura, Leonardo + and Bj{\o}rner, Nikolaj", + editor="Ramakrishnan, C. R. + and Rehof, Jakob", + title="Z3: An Efficient SMT Solver", + booktitle="Tools and Algorithms for the Construction and Analysis of Systems", + year="2008", + publisher="Springer Berlin Heidelberg", + address="Berlin, Heidelberg", + pages="337--340", + abstract="Satisfiability Modulo Theories (SMT) problem is a decision problem for logical first order formulas with respect to combinations of background theories such as: arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 is a new and efficient SMT Solver freely available from Microsoft Research. It is used in various software verification and analysis applications.", + isbn="978-3-540-78800-3" +} + |