diff options
Diffstat (limited to 'chapters/core')
| -rw-r--r-- | chapters/core/03-benchmarks.tex | 71 | ||||
| -rw-r--r-- | chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex | 30 |
2 files changed, 59 insertions, 42 deletions
diff --git a/chapters/core/03-benchmarks.tex b/chapters/core/03-benchmarks.tex index 132b56d..a8c1317 100644 --- a/chapters/core/03-benchmarks.tex +++ b/chapters/core/03-benchmarks.tex @@ -3,18 +3,17 @@ This section contains the benchmark data, illustrated in \textbf{\Cref{tab:benchmarks}}. -VEIN was tested on a laptop Zenbook UX3402ZA with: +VEIN was tested with the following hardware: \begin{itemize} - \item \textbf{CPU}: 12th Gen Intel Core i5-1240P - \item \textbf{RAM}: 8GiB - \item \textbf{SWAP}: 16GiB on NVMe + \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 et al.~\cite{fisher1936iris}. It consists of three +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} @@ -48,38 +47,38 @@ define three kinds of equivalence: \centering \begin{tabular}[t]{ccccc} \hline - Benchmark & Equivalence & Direct [s] & VEIN [s] & Status \\ + Benchmark & Equivalence & Time & Status \\ \hline - Iris (Stably Active) & Strict & 0.0 & 0.0 & X \\ - Iris (Stably Active) & Epsilon & 0.0 & 0.0 & X \\ - Iris (Stably Active) & Argmax & 0.0 & 0.0 & X \\ - Iris (Stably Inactive) & Strict & 0.0 & 0.0 & X \\ - Iris (Stably Inactive) & Epsilon & 0.0 & 0.0 & X \\ - Iris (Stably Inactive) & Argmax & 0.0 & 0.0 & X \\ - Iris (To Wide) & Strict & 0.0 & 0.0 & X \\ - Iris (To Wide) & Epsilon & 0.0 & 0.0 & X \\ - Iris (To Wide) & Argmax & 0.0 & 0.0 & X \\ - Iris (To Deep) & Strict & 0.0 & 0.0 & X \\ - Iris (To Deep) & Epsilon & 0.0 & 0.0 & X \\ - Iris (To Deep) & Argmax & 0.0 & 0.0 & X \\ - Pendulum & Strict & 0.0 & 88.427 ± 0.670 & SAT \\ - Pendulum & Epsilon & 0.0 & 0.0 & X \\ - Pendulum & Argmax & 0.0 & 0.0 & X \\ - Double Integrator & Strict & 0.0 & 0.0 & X \\ - Double Integrator & Epsilon & 0.0 & 0.0 & X \\ - Double Integrator & Argmax & 0.0 & 0.0 & X \\ - MNIST (Stably Active) & Strict & 0.0 & 0.0 & X \\ - MNIST (Stably Active) & Epsilon & 0.0 & 0.0 & X \\ - MNIST (Stably Active) & Argmax & 0.0 & 0.0 & X \\ - MNIST (Stably Inactive) & Strict & 0.0 & 0.0 & X \\ - MNIST (Stably Inactive) & Epsilon & 0.0 & 0.0 & X \\ - MNIST (Stably Inactive) & Argmax & 0.0 & 0.0 & X \\ - MNIST (To Wide) & Strict & 0.0 & 0.0 & X \\ - MNIST (To Wide) & Epsilon & 0.0 & 0.0 & X \\ - MNIST (To Wide) & Argmax & 0.0 & 0.0 & X \\ - MNIST (To Deep) & Strict & 0.0 & 0.0 & X \\ - MNIST (To Deep) & Epsilon & 0.0 & 0.0 & X \\ - MNIST (To Deep) & Argmax & 0.0 & 0.0 & X \\ + 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} diff --git a/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex b/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex index be0870d..26f7e13 100644 --- a/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex +++ b/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex @@ -525,7 +525,11 @@ \begin{lemma} For the \textit{Linear} and \textit{Dup} agents we have the interaction rule: $$ - \mathit{Linear}(z, q, r) \bowtie \mathit{Dup}(x, y) \Rightarrow \mathit{Linear}(z_1, q, r) \sim x; \mathit{Linear}(z_2, q, r) \sim y; \mathit{Dup}(z_1, z_2) \sim z \\ + \begin{aligned} + \mathit{Linear}(z, q, r) \bowtie \mathit{Dup}(x, y) \Rightarrow + & \mathit{Linear}(z_1, q, r) \sim x; \mathit{Linear}(z_2, q, r) \sim y; \\ + & \mathit{Dup}(z_1, z_2) \sim z + \end{aligned} $$ We need to show that the LHS and RHS are semantically equivalent: $$ @@ -667,8 +671,9 @@ For the \textit{TermMul} and \textit{Dup} agents we have the interaction rule: $$ \begin{aligned} - \mathit{TermMul}(a, b) \bowtie \mathit{Dup}(x, y) \Rightarrow & \mathit{TermMul}(a_1, b_1) \sim x; \mathit{TermMul}(a_2, b_2) \sim y; \\ - & \mathit{Dup}(a_1, a_2) \sim a; \mathit{Dup}(b_1, b_2) \sim b\\ + \mathit{TermMul}(a, b) \bowtie \mathit{Dup}(x, y) \Rightarrow + & \mathit{TermMul}(a_1, b_1) \sim x; \mathit{TermMul}(a_2, b_2) \sim y; \\ + & \mathit{Dup}(a_1, a_2) \sim a; \mathit{Dup}(b_1, b_2) \sim b \end{aligned} $$ We need to show that the LHS and RHS are semantically equivalent: @@ -717,7 +722,12 @@ \begin{lemma} For the \textit{TermReLU} and \textit{Dup} agents we have the interaction rule: $$ - \mathit{TermReLU}(z) \bowtie \mathit{Dup}(x, y) \Rightarrow \mathit{TermReLU}(z_1) \sim x; \mathit{TermReLU}(z_2) \sim y; \mathit{Dup}(z_1, z_2) \sim z \\ + \begin{aligned} + \mathit{TermReLU}(z) \bowtie \mathit{Dup}(x, y) \Rightarrow + & \mathit{TermReLU}(z_1) \sim x; \\ + &\mathit{TermReLU}(z_2) \sim y; \\ + & \mathit{Dup}(z_1, z_2) \sim z + \end{aligned} $$ We need to show that the LHS and RHS are semantically equivalent: $$ @@ -763,7 +773,11 @@ \begin{lemma} For the \textit{TermConcrete} and \textit{Dup} agents we have the interaction rule: $$ - \mathit{TermConcrete}(k) \bowtie \mathit{Dup}(x, y) \Rightarrow \mathit{TermConcrete}(k) \sim x; \mathit{TermConcrete}(k) \sim y \\ + \begin{aligned} + \mathit{TermConcrete}(k) \bowtie \mathit{Dup}(x, y) \Rightarrow + & \mathit{TermConcrete}(k) \sim x; \\ + & \mathit{TermConcrete}(k) \sim y + \end{aligned} $$ We need to show that the LHS and RHS are semantically equivalent: $$ @@ -807,7 +821,11 @@ \begin{lemma} For the \textit{TermSymbolic} and \textit{Dup} agents we have the interaction rule: $$ - \mathit{TermSymbolic}(id) \bowtie \mathit{Dup}(x, y) \Rightarrow \mathit{TermSymbolic}(id) \sim x; \mathit{TermSymbolic}(id) \sim y \\ + \begin{aligned} + \mathit{TermSymbolic}(id) \bowtie \mathit{Dup}(x, y) \Rightarrow + & \mathit{TermSymbolic}(id) \sim x; \\ + & \mathit{TermSymbolic}(id) \sim y + \end{aligned} $$ We need to show that the LHS and RHS are semantically equivalent: $$ |