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
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
|
\section{Benchmarks}
\label{sec:benchmarks}
This section contains the benchmark data, illustrated in \textbf{\Cref{tab:benchmarks}}.
\textbf{VEIN} was tested with the following hardware:
\begin{itemize}
\item \textbf{CPU}: AMD Ryzen 7 5700x3D
\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 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: 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
to the origin under a bound on its position $p$, with state $x=[p,\dot p]\in\mathbb{R}^2$.
\item \textbf{MNIST}: Network trained on the widely known dataset of handwritten digits presented by
LeCun et al.~\cite{lecun2010mnist}. It consists of 60'000 training images and 10'000 testing
images.
\end{itemize}
Pendulum and Double Integrator are taken from \textit{cersyve}, a benchmark presented by Kaulen et
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 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:
\begin{itemize}
\item \textbf{Strict equivalence}: $\forall x \in \mathbb{R}^n \; F(x) = F'(x)$.
\item \textbf{Epsilon equivalence}: $\forall x \in \mathbb{R}^n \; ||F(x) - F'(x)|| < \epsilon$ for some $\epsilon > 0$.
\item \textbf{Argmax equivalence}: $\forall x \in \mathbb{R}^n \; \mathtt{argmax}(F(x))=\mathtt{argmax}(F'(x))$ where \texttt{argmax}
is the function that returns the index of the maximum value of a vector.
\end{itemize}
We compare the verification time between a direct translation of the ONNX network into a Z3 formula
and the \textbf{VEIN} framework.
\begin{table}[H]
\centering
\resizebox{\textwidth}{!}{
\begin{tabular}[t]{ccccc}
\hline
Benchmark & Equivalence & Direct & VEIN & Status \\
\hline
Iris (Stably Active) & Strict & 265.2ms ± 6.8ms & 521.6ms ± 11.5ms & SAT \\
Iris (Stably Active) & Epsilon $\epsilon=0.1$ & 271.4ms ± 5.2ms & 515.9ms ± 4.2ms & UNSAT \\
Iris (Stably Active) & Argmax & 267.9ms ± 9.5ms & 519.5ms ± 6.0ms & UNSAT \\
Iris (Stably Inactive) & Strict & 278.3ms ± 7.7ms & 581.9ms ± 6.2ms & UNSAT \\
Iris (Stably Inactive) & Epsilon $\epsilon=0.1$ & 283.2ms ± 9.0ms & 593.8ms ± 6.9ms & UNSAT \\
Iris (Stably Inactive) & Argmax & 287.6ms ± 2.6ms & 886.4ms ± 10.3ms & UNSAT \\
Iris (Deep To Wide) & Strict & 269.5ms ± 5.1ms & 595.4ms ± 11.3ms & UNSAT \\
Iris (Deep To Wide) & Epsilon $\epsilon=0.1$ & 273.7ms ± 5.6ms & 587.0ms ± 4.9ms & UNSAT \\
Iris (Deep To Wide) & Argmax & 296.5ms ± 8.5ms & 783.5ms ± 4.4ms & UNSAT \\
Iris (Wide To Deep) & Strict & 271.5ms ± 7.7ms & 581.4ms ± 6.6ms & UNSAT \\
Iris (Wide To Deep) & Epsilon $\epsilon=0.1$ & 272.3ms ± 6.6ms & 583.1ms ± 5.7ms & UNSAT \\
Iris (Wide To Deep) & Argmax & 1.280s ± 0.019s & 716.3ms ± 4.7ms & UNSAT \\
Pendulum & Strict & 20m 47.679s & 43.276s ± 0.143s & SAT \\
Pendulum & Epsilon $\epsilon=0.1$ & 37m 54.754s & 340.293s ± 2.843s & UNSAT \\
Pendulum & Argmax & 24m 56.327s & 61.935s ± 0.148s & SAT \\
Double Integrator & Strict & 27m 45.657s & 538.952s ± 7.207s & SAT \\
Double Integrator & Epsilon $\epsilon=0.1$ & 59m 51.718s & 137.720s ± 0.419s & SAT \\
Double Integrator & Argmax & 41m 21.147s & 618.705s ± 6.821s & SAT \\
MNIST (Stably Active) & Strict & 740.5ms ± 4.7ms & 18.947s ± 0.034s & SAT \\
MNIST (Stably Active) & Epsilon $\epsilon=0.1$ & 1.571s ± 0.010s & 18.980s ± 0.032s & UNSAT \\
MNIST (Stably Active) & Argmax & 794.7ms ± 7.3ms & 18.906s ± 0.019s & UNSAT \\
MNIST (Stably Inactive) & Strict & TIMEOUT & 14.699s ± 0.024s & UNSAT \\
MNIST (Stably Inactive) & Epsilon $\epsilon=0.1$ & TIMEOUT & 14.702s ± 0.012s & UNSAT \\
MNIST (Stably Inactive) & Argmax & TIMEOUT & TIMEOUT & UNKNOWN \\
MNIST (Deep To Wide) & Strict & 692.2ms ± 5.6ms & 20.990s ± 0.181s & UNSAT \\
MNIST (Deep To Wide) & Epsilon $\epsilon=0.1$ & 691.4ms ± 3.2 ms & 20.860s ± 0.022s & UNSAT \\
MNIST (Deep To Wide) & Argmax & TIMEOUT & TIMEOUT & UNKNOWN \\
MNIST (Wide To Deep) & Strict & 718.3ms ± 4.8ms & 20.901s ± 0.027s & UNSAT \\
MNIST (Wide To Deep) & Epsilon $\epsilon=0.1$ & 722.1ms ± 6.0 ms & 20.947s ± 0.035s & UNSAT \\
MNIST (Wide To Deep) & Argmax & TIMEOUT & TIMEOUT & UNKNOWN \\
\end{tabular}
}
\caption{Benchmark table.}
\label{tab:benchmarks}
\end{table}
We make three observations:
\begin{itemize}
\item On Iris, the direct translation is consistently faster by a roughly constant
margin, suggesting a fixed \textbf{VEIN} pipeline overhead.
\item On Pendulum and Double Integrator, the pattern reverses: \textbf{VEIN} outperforms the direct
translation by up to two orders of magnitude.
\item MNIST is mixed: most variants favor the direct translation, except Stably Inactive,
where the direct encoding times out while \textbf{VEIN} finishes in ~15s. We hypothesize this is because
direct encoding may face branching from the unpruned network that \textbf{VEIN} folds during
preprocessing.
\end{itemize}
Additionally, we identify two false SAT results (Stably Active transformation). These are caused
by floating-point errors introduced by the INPLA float attributes instead of using real numbers.
|
