diff options
Diffstat (limited to 'chapters/core/03-benchmarks.tex')
| -rw-r--r-- | chapters/core/03-benchmarks.tex | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/chapters/core/03-benchmarks.tex b/chapters/core/03-benchmarks.tex index 31b61a7..25cc0ab 100644 --- a/chapters/core/03-benchmarks.tex +++ b/chapters/core/03-benchmarks.tex @@ -9,12 +9,13 @@ This section contains the benchmark data, illustrated in \textbf{\Cref{tab:bench \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 standard deviation -of execution time. For longer runs, only execution is reported. We defined the following benchmarks: +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: width and length of sepals and petals. + 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 @@ -25,13 +26,13 @@ of execution time. For longer runs, only execution is reported. We defined the f \end{itemize} 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 +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 viceversa, as presented by Fan et al.~\cite{JMLR:v24:21-0579}. +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: @@ -100,4 +101,4 @@ We make three observations: preprocessing. \end{itemize} Additionally, we identify two false SAT results (Stably Active transformation). These are caused -by floating-point error introduced by the INPLA float attributes instead of using real numbers. +by floating-point errors introduced by the INPLA float attributes instead of using real numbers. |