\section{Benchmarks}
\label{sec:benchmarks}

This section contains the benchmark data, illustrated in \textbf{\Cref{tab:benchmarks}}.

VEIN was tested with the following hardware:
\begin{itemize}
	\item \textbf{CPU}: AMD Ryzen 7 5700x3D
	\item \textbf{RAM}: 16GiB
\end{itemize}
using 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 standard deviation of
execution time.

\paragraph{Iris}
Dataset of iris flowers 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: width and length of sepals and petals.
\paragraph{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$ and nonlinear dynamics.
\paragraph{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$.
\paragraph{MNIST}
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.

Pendulum and Double Integrator are taken from \textit{cersyve}, a benchmark presented by Kaulen et
al.~\cite{kaulen20256thinternationalverificationneural}. We check equivalence between a pre-trained
and a fine-tuned network for each task.

In the Iris and MNIST dataset, we tested equivalence between a NN 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 viceversa, as presented by Fan et al.~\cite{JMLR:v24:21-0579}.

For two NN $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 \quad F(x) = F'(x)$.
	\item \textbf{Epsilon equivalence}: $\forall x \in \mathbb{R}^n \quad ||F(x) - F'(x)|| < \epsilon$ for some $\epsilon > 0$.
	\item \textbf{Argmax equivalence}: $\forall x \in \mathbb{R}^n \quad \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}

\begin{table}[H]
	\centering
	\begin{tabular}[t]{ccccc}
		\hline
		Benchmark & Equivalence & Time & Status \\
		\hline
		Iris (Stably Active) & Strict & 521.6ms ± 11.5ms & SAT \\
		Iris (Stably Active) & Epsilon & 515.9ms ± 4.2ms & UNSAT \\
		Iris (Stably Active) & Argmax & 519.5ms ± 6.0ms & UNSAT \\
		Iris (Stably Inactive) & Strict & 581.9ms ± 6.2ms & UNSAT \\
		Iris (Stably Inactive) & Epsilon & 593.8ms ± 6.9ms & UNSAT \\
		Iris (Stably Inactive) & Argmax & 886.4ms ± 10.3ms & UNSAT \\
		Iris (To Wide) & Strict & 595.4ms ± 11.3ms & UNSAT \\
		Iris (To Wide) & Epsilon & 587.0ms ± 4.9ms & UNSAT \\
		Iris (To Wide) & Argmax & 783.5ms ± 4.4ms & UNSAT \\
		Iris (To Deep) & Strict & 581.4ms ± 6.6ms & UNSAT \\
		Iris (To Deep) & Epsilon & 583.1ms ± 5.7ms & UNSAT \\
		Iris (To Deep) & Argmax & 716.3ms ± 4.7ms & UNSAT \\
		Pendulum & Strict & 43.276s ± 0.143s & SAT \\
		Pendulum & Epsilon & 340.293s ± 2.843s & UNSAT \\
		Pendulum & Argmax & 61.935s ± 0.148s & SAT \\
		Double Integrator & Strict & 538.952s ± 7.207s & SAT \\
		Double Integrator & Epsilon & 137.720s ± 0.419s & SAT \\
		Double Integrator & Argmax & 618.705s ± 6.821s & SAT \\
		MNIST (Stably Active) & Strict & 18.947s ± 0.034s & SAT \\
		MNIST (Stably Active) & Epsilon & 18.980s ± 0.032s & UNSAT \\
		MNIST (Stably Active) & Argmax & 18.906s ± 0.019s & UNSAT \\
		MNIST (Stably Inactive) & Strict & 14.699s ± 0.024s & UNSAT \\
		MNIST (Stably Inactive) & Epsilon & 14.702s ± 0.012s & UNSAT \\
		MNIST (Stably Inactive) & Argmax & TIMEOUT & UNKNOWN \\
		MNIST (To Wide) & Strict & 20.990s ± 0.181s & UNSAT \\
		MNIST (To Wide) & Epsilon & 20.860s ± 0.022s & UNSAT \\
		MNIST (To Wide) & Argmax & TIMEOUT & UNKNOWN \\
		MNIST (To Deep) & Strict & 20.901s ± 0.027s & UNSAT \\
		MNIST (To Deep) & Epsilon & 20.947s ± 0.035s & UNSAT \\
		MNIST (To Deep) & Argmax & TIMEOUT & UNKNOWN \\
	\end{tabular}
	\caption{Benchmark table.}
	\label{tab:benchmarks}
\end{table}