blob: 36919e59160bac0f32b427c451081b1578ea691a (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
|
\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.
% 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.
% 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:
\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.
\end{itemize}
Z3 is not optimized for ReLU splitting, but it was chosen for it's mature Python package.
In any case a specialized solver like Marabou can be integrated to improve performance.
Our contributions are:
\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.
\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.
% 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:related-work}}: Analyzes existing verification approaches...
\item \textbf{\Cref{ch:conclusion}}: Summarizes the findings and discusses future work...
\end{itemize}
|
