First Three Years of the International Verification of Neural Networks
  Competition (VNN-COMP)
This paper presents a summary and meta-analysis of the first three iterations
of the annual International Verification of Neural Networks Competition
(VNN-COMP) held in 2020, 2021, and 2022. In the VNN-COMP, participants submit
software tools that analyze whether given neural networks satisfy
specifications describing their input-output behavior. These neural networks
and specifications cover a variety of problem classes and tasks, corresponding
to safety and robustness properties in image classification, neural control,
reinforcement learning, and autonomous systems. We summarize the key processes,
rules, and results, present trends observed over the last three years, and
provide an outlook into possible future developments.
Christopher Brix, Mark Niklas MÃ¼ller, Stanley Bak, Taylor T. Johnson, Changliu Liu
# First Three Years of the International Verification of Neural Networks Competition (VNN-COMP)

###### Abstract

This paper presents a summary and meta-analysis of the first three iterations of the annual International Verification of Neural Networks Competition (VNN-COMP) held in 2020, 2021, and 2022. In the VNN-COMP, participants submit software tools that analyze whether given neural networks satisfy specifications describing their input-output behavior. These neural networks and specifications cover a variety of problem classes and tasks, corresponding to safety and robustness properties in image classification, neural control, reinforcement learning, and autonomous systems. We summarize the key processes, rules, and results, present trends observed over the last three years, and provide an outlook into possible future developments.

Keywords:certified robustness, adversarial robustness, formal verification, formal methods, neural networks, machine learning, deep learning 

## 1 Introduction

Neural networks are increasingly used in safety-critical applications [7; 23]. However, it has become apparent that they are highly susceptible to adversarial examples [47], i.e., minor and possibly imperceptible input perturbations can cause the output to change significantly. As such perturbations can occur in the real world either at random or due to malicious actors, it is of utmost importance to analyze the robustness of deep learning based systems in a mathematically rigorous manner before applying them in safety-critical domains. To this end, a wide range of methods and corresponding software tools have been developed [12; 16; 22; 24]. However, with tools becoming ever more numerous and specialized, it became increasingly difficult for practitioners to decide which tool to use.

In 2020, the inaugural VNN-COMP was organized to tackle this problem and allow researchers to compare their neural network verifiers on a wide set of benchmarks. Initially conceived as a friendly competition with little standardization, it was increasingly standardized and automated to ensure a fair comparison on cost-equivalent hardware using standardized formats for both properties and networks.

In this work, we outline this development, summarize key rules and results, describe the high-level trends observed over the last three years, and provide an outlook on possible future developments.

## 2 Neural Network Verification

We consider the neural network verification problem defined as follows: Given an input specification \(\phi\subseteq\mathds{R}^{d_{\text{in}}}\), also called pre-condition, an output specification
\(\psi\subseteq\mathds{R}^{d_{\text{out}}}\), also called post-condition, and a neural network \(N:\mathds{R}^{d_{\text{in}}}\mapsto\mathds{R}^{d_{\text{out}}}\), we aim to prove that the precondition implies the post-condition, i.e.,

\[\forall x:x\vDash\phi\Rightarrow N(x)\vDash\psi, \tag{2.1}\]

or provide a counterexample.

Inspired by the notation common in the SAT-solver community, we encode this problem by specifying a constraint set describing an adversarial example, i.e.,

\[\exists x:x\vDash\phi\wedge N(x)\vDash\neg\psi. \tag{2.2}\]

Therefore, we call instances where Equation (2.2) is satisfiable and thus the property encoded by Equation (2.1) does _not_ hold SAT and instances where Equation (2.2) is unsatisfiable and the property encoded by Equation (2.1) has been shown to hold UNSAT. Note that while it is possible to show SAT by directly searching for counter-examples using adversarial attacks [17; 32], those approaches are not complete, i.e., if they are not successful in finding a counter-example this does _not_ imply that a property holds.

Example ProblemsOne particularly popular property is the robustness to adversarial \(\ell_{\infty}\)-norm bounded perturbations in image classification. There, the network \(N\) computes a numerical score \(y\in\mathds{R}^{d_{\text{out}}}\) corresponding to its confidence that the input belongs to each of the \(d_{\text{out}}\) classes for each input \(x\in\mathds{R}^{d_{\text{in}}}\). The final classification \(c\) is then computed as \(c=\operatorname*{arg\,max}_{i}N(x)_{i}\). In this setting, an adversary may want to perturb the input such that the classification changes. Therefore, the verification intends to prove that

\[\operatorname*{arg\,max}_{i}N(x^{\prime})_{i}=t,\] \[\forall x^{\prime}\in\{x^{\prime}\in\mathds{R}^{d_{\text{in}}}\mid \|x-x^{\prime}\|_{\infty}\leq\epsilon\},\]

where \(t\) is the target class, \(x\) is the original image and \(\epsilon\) is the maximal permissible perturbation magnitude. There, the pre-condition \(\phi\) describes the inputs an attacker can choose from (\(\phi=\{x^{\prime}\in\mathds{R}^{d_{\text{in}}}\mid\|x-x^{\prime}\|_{\infty}\leq \epsilon\}\)), i.e., an \(\ell_{\infty}\)-ball of radius \(\epsilon\), and the post-condition \(\psi\) describes the output space corresponding to a classification to the target class \(t\) (\(\psi=\{y\in\mathds{R}^{d_{\text{out}}}\mid y_{t}>y_{i},\forall i\neq t\}\)).

When neural networks are used as controllers, more complex properties can be relevant. For example, in the ACAS Xu setting [23] a neural controller gives action recommendations based on the relative position and heading of the controlled and intruder aircraft. There, we want to, e.g., ensure that for inputs \(\mathcal{D}\) corresponding to the intruder aircraft being straight ahead and heading our way, neither of the evasive maneuvers "strong left" (SL) or "strong right" (SR) is considered the worst option. More formally, we want to verify that

\[\operatorname*{arg\,min}_{i}N(x^{\prime})_{i}\notin\{\operatorname*{SL}, \operatorname*{SR}\},\;\forall x^{\prime}\in\mathcal{D}.\]

Here, we obtain a more complex, non-convex post-condition

\[\psi= \mathds{R}^{d_{\text{out}}}\backslash\] \[\big{(}\{y\in\mathds{R}^{d_{\text{out}}}\mid y_{\operatorname*{SL }}<y_{i},\;\forall i\notin\{\operatorname*{SL},\operatorname*{SR}\}\}\] \[\cup\{y\in\mathds{R}^{d_{\text{out}}}\mid y_{\operatorname*{SR}}<y _{i},\;\forall i\notin\{\operatorname*{SL},\operatorname*{SR}\}\}\big{)}.\]

## 3 Competition Goals

VNN-COMP is organized to further the following goals.

Define StandardsTo enable practitioners to easily use and evaluate a range of different verification approaches and tools without substantial overhead, it is essential that all tools can process both networks and specifications in a standardized file format. To this end, the second iteration of the VNN-COMP established such a standard. Problem specifications (pre- and post-condition) are defined using the VNN-LIB[48] format and neural networks are defined using the ONNX[3] standard. In 2022, additionally, a standardized format for counterexamples was introduced.

Facilitate Verification Tool ComparisonEvery year, dozens of papers are published on neural network verification, many proposing not only new methods but also new benchmarks. With authors potentially investing more time into tuning their method to the chosen benchmarks, a fair comparison between all these methods is difficult. VNN-COMP facilitates such a comparison between a large number of tools on a diverse set of benchmarks, using cost-equivalent hardware, and test instances not available to participants. Letting participants and industry practitioners propose a wide range of interesting benchmarks, yields not only a ranking on the problems typically used in the field but also highlights which tools are particularly suitable for more specialized problems. Further, by ensuring a standardized installation and evaluation process is in place, the comparison to a large number of state-of-the-art tools for any publication is enabled.

Shape Future Work DirectionsThe visibility VNN-COMP tends to the problems underlying the considered benchmarks has the potential to raise their profile in the community. As benchmarks are developed jointly by industry and academia, this constitutes a great opportunity to shape future research to be as
impactful as possible. Over the last years, benchmarks have featured ever-increasing network sizes (see Table 2), promoting scalability, more complex networks (including, e.g., residual [19] and max-pooling layers [64]), promoting generalizability, and more complex specifications, enabling more interesting properties to be analyzed.

Bring Researchers TogetherBoth the rule and benchmark discussion phase during the lead-up to the competition, as well as the in-person presentation of results at the Workshop on Formal Methods for ML-Enabled Autonomous Systems (FoMLAS)1 provide participants with a great opportunity to meet fellow researches and discuss the future of the field. Further, the tool and benchmark descriptions participants provide for the yearly report [2; 34; 5] serve as an excellent summary of state-of-the-art methods, allowing people entering the field to get a quick overview.

Footnote 1: [https://fomlas2022.wixsite.com/fomlas2022](https://fomlas2022.wixsite.com/fomlas2022)

## 4 Overview of Three Years of VNN-COMP

In this section, we provide a high-level description of how the VNN-COMP evolved from 2020 to 2022, listing all participants and the final rankings in Table 1. Generally, performance is measured on a set of equally weighted _benchmarks_, each consisting of a set of related _instances_. Each instance consists of a trained neural network, a timeout, and input and output constraints. Below, we group benchmarks into _categories_ to enable a quicker comparison between years.

### Vnn-Comp 2020

The inaugural VNN-COMP2[2] was held in 2020 as a "friendly competition" with no winner. Its main goal was to provide a stepping stone for future iterations by starting the process of defining common problem settings and identifying possible avenues for standardization.

Footnote 2: [https://sites.google.com/view/vnn20/vnncomp](https://sites.google.com/view/vnn20/vnncomp)

#### 4.1.1 Benchmarks

Three benchmark categories were considered with only one of the eight teams participating in all of them:

* two benchmarks, based on ACAS Xu and MNIST.
* one benchmark, based on MNIST.
* two benchmarks, based on MNIST and CIFAR10.

#### 4.1.2 Evaluation

Teams evaluated their tools using their own hardware. While this simplified the evaluation process, it made the reported results incomparable, due to the significant hardware differences. The teams reported that they used between 4 and 40 CPUs and between 16 and 756 GB of RAM.

### Vnn-Comp 2021

Based upon the insights gained in 2020, the second iteration of VNN-COMP3 was organized with a stronger focus on comparability between the participating tools [5].

Footnote 3: [https://sites.google.com/view/vnn2021](https://sites.google.com/view/vnn2021)

#### 4.2.1 Benchmarks

Teams were permitted to propose one benchmark with a total timeout of at most six hours split over its constituting instances. Networks were defined in the ONNX format [3] and problem specifications were given in the VNN-LIB format [48]. To prevent excessive tuning to specific benchmark instances, benchmark proposers were encouraged to provide a script enabling the generation of new random instances for the final tool evaluation. However, teams were allowed to tune their tools for each benchmark, using the initial set of benchmark instances.

In 2021, the benchmarks could be split into the following categories, with multiple teams participating in all of them:

* two benchmarks, based on ACAS Xu and MNIST.
* one benchmark, based on MNIST.
* three benchmarks, based on CIFAR10.
* one benchmark, based on MNIST.
* one benchmark, based on CIFAR10.
* one benchmark, based on database indexing.
#### 4.2.2 Evaluation

To allow for comparability of results, all tools were evaluated on equal-cost hardware using Amazon Web Services (AWS). Each team could decide whether they wanted their tool to be evaluated on a CPU-focused r5.12xlarge or a GPU-focused p3.2xlarge instance (see Table 4.1 for more details). Further, instead of providing results and runtimes themselves, teams had to prepare scripts automating the installation and execution of their tools. After the submission deadline, the organizers installed and evaluated each tool using the provided scripts. In many cases, this process required some debugging in a back and forth between the organizers and teams.

ScoringFor every benchmark, 10 points were awarded for correctly showing the instance to be SAT/UNSAT, with a 100 point penalty for incorrect results (see Table 4.2). A simple adversarial attack was used to identify "easy" SAT instances, on which the available points were reduced from 10 to 1. If tools reported contradicting results on an instance, the ground truth was decided by a majority vote. Bonus points were awarded to the fastest two tools on every instance (two points for the fastest and one point for the second fastest). Runtimes differing by less than 0.2 seconds or below one second were considered equal, so multiple teams could receive the two point bonus. To correct the notable differences in startup overhead, e.g., due to the need to acquire a GPU, it was measured as the runtime on a trivial instance and subtracted from every runtime. The benchmark score was computed from the points obtained as discussed above by normalizing with the maximum number of obtained points. Consequently, the tool with the most points was assigned a score of 100%. The total competition score was simply the sum of the per benchmark scores, corresponding to equal weighting.

ResultsIn 2021, 12 teams participated in the competition. \(\alpha\)-\(\beta\)-CROWN won first place, followed by VeriNet in second, and ERAN/OVAL in third, depending on the overhead measurement and voting scheme used to determine result-correctness. Except for VeriNet, they all used the GPU instance.

### Vnn-Comp 2022

In the most recent iteration of VNN-COMP4[34], the evaluation was fully automated, allowing the number of benchmarks to be increased.

Footnote 4: [https://sites.google.com/view/vnn2022](https://sites.google.com/view/vnn2022)

#### 4.3.1 Benchmarks

In 2022, each participating team could submit or endorse up to two benchmarks, allowing industry practitioners to propose benchmarks without entering a tool. Each benchmark had a total timeout of between three and six hours, with randomization of instances being mandatory this year. Tool tuning was still permitted on a per benchmark level and in practice also per network using the network's statistics.

The submitted benchmarks can be grouped into the following categories:

* three benchmarks, based on reinforcement tasks and MNIST.
* one benchmark.
* one benchmark, based on database indexing and cardinality estimation.

\begin{table}
\begin{tabular}{l c c c c} \hline \hline  & \multicolumn{3}{c}{Returned Result} \\ \cline{2-5} Ground Truth & SAT & UNSAT & Other \\ \hline SAT, simple & \(+1\) & \(-100\) & \(0\) \\ SAT, complex & \(+10\) & \(-100\) & \(0\) \\ UNSAT & \(-100\) & \(+10\) & \(0\) \\ \hline \hline \end{tabular}
\end{table}
Table 4.2: Points per instance in 2021. SAT instances were split into simple and complex based on whether a simple adversarial attack was successful.

\begin{table}
\begin{tabular}{l c c c c c} \hline \hline  & 2021 & 2022 & vCPUs & RAM [GB] & GPU \\ \hline r5.12xlarge & ✓ & ✗ & 48 & 384 & ✗ \\ p3.2xlarge & ✓ & ✓ & 8 & 61 & V100 GPU with 16 GB memory \\ m5.16xlarge & ✗ & ✓ & 64 & 256 & ✗ \\ g5.8xlarge & ✗ & ✓ & 32 & 128 & A10G GPU with 24 GB memory \\ t2.large & ✗ & ✓ & 2 & 8 & ✗ \\ \hline \hline \end{tabular}
\end{table}
Table 4.1: Available AWS instances.
- three benchmarks, based on CIFAR10.
* two benchmarks, based on CIFAR10, CIFAR100, and TinyImageNet.
* one benchmark based on image segmentation.

#### 4.3.2 Evaluation

Similar to the previous year, teams could choose between a range of AWS instance types (see Table 4.1) providing a CPU, GPU, or mixed focus. Except for the much weaker t2.large instance, all instances were priced at around three dollars per hour. In contrast to 2021 where organizers had to manually execute installation scripts and debug with the participants, an automated submission and testing pipeline was set up. Teams could submit their benchmarks and tools via a web interface by specifying a git repository, commit hash, and post-installation script (enabling, e.g., the acquisition of licenses). This triggered a new AWS instance to be spawned where all installation scripts were executed. If the installation succeeded, the tool was automatically evaluated on a previously selected set of benchmarks before the instance was terminated again. To enable debugging by the participants, all outputs were logged and made accessible live via the submission website, allowing them to monitor the progress. This automation allowed each team to perform as many tests as necessary without the need to wait for feedback from the organizers. Furthermore, teams could test on the same AWS instances used during final evaluation without having to pay for their usage, with the costs kindly covered by the SRI Lab of ETH Zurich.

ScoringUnlike during the VNN-COMP 2021, SAT instances were not divided into simple and complex for scoring purposes, leading to 10 points being awarded for all correct results (see Table 4.3). Further, instead of relying on a voting scheme to determine the ground truth in the presence of dissent among tools, the burden of proof was placed on the tool reporting SAT, requiring them to provide a concrete counter-example. If no valid counter-example was provided, the corresponding tool was judged to be incorrect and awarded the 100 point penalty.

ResultsOut of the eleven participating teams, \(\alpha\)-\(\beta\)-CROWN placed first, MN-BAB second, and VeriNet third. For a comparison of all participating tools across all benchmarks, see Figure 4.1.

## 5 Comparison Across the Years

In Table 5.1 we list all tools participating in any iteration of the VNN-COMP and refer the interested reader to the corresponding VNN-COMP report for a short description of the tools. In Table 5.2, we compare the scope of the competition across the last three years. As can be seen, the number, variety, complexity, and scale of benchmarks increased with every iteration. Starting with 5 benchmarks covering simple fully connected (FC) and convolutional (Conv) networks in 2020, the 2022 competition saw 12 benchmarks including a range of complex residual and U-Net architectures with up to 140 million parameters. Further, we believe that the increasing number of registered tools clearly shows that the interest in both the field in general and the competition in particular is growing year by year. However, the large and increasing discrepancy between registered and submitted tools might indicate that many teams feel like they are not able to invest the significant effort required to support not only the standardized network and specification formats but also the wide variety of different benchmarks. As tools are ranked by their total score with each benchmark providing a score of up to 100%, the final ranking is biased towards tools that support all benchmarks. While we believe that this is a valuable incentive for tool developers to develop methods that can be easily applied to new problems, it might be daunting for new teams to implement all necessary features, deterring them from participating at all.

Successful TrendsWhile all teams started out using only CPUs in 2020, only one of the top four teams relied solely on CPUs in 2021, and all top three teams chose GPU instances in 2022. This transition enabled both the more efficient evaluation of simple bound propagation methods such as DeepPoly [45], CROWN [62], and IBP [18] and approximate solutions of the linear programming (LP) problems arising during verification [55; 14; 58]. Similarly, the top two teams in 2021 and all top three teams in 2022 relied on a branch-and-bound (BaB) based approach, recursively breaking down the verification problem into easier subproblems until it becomes solvable, thus effectively enabling the use of GPUs to solve tighter mixed

\begin{table}
\begin{tabular}{l c c c} \hline \hline  & \multicolumn{3}{c}{Returned Result} \\ \cline{2-4} Ground Truth & SAT & UNSAT & Other \\ \hline SAT & \(+10\) & \(-100\) & \(0\) \\ UNSAT & \(-100\) & \(+10\) & \(0\) \\ \hline \hline \end{tabular}
\end{table}
Table 4.3: Points per instance in 2022.
integer linear programming (MILP) encodings of the verification problem [11; 14; 55; 61]. Both top two teams in the most recent iteration combined this approach with additional multi-neuron [14] and solver-generated cutting plane constraints [61], first introduced by the 3rd place ERAN in 2021 [36]. We thus conclude that successful tools leverage hardware accelerators such as GPUs to efficiently handle tight (MI)LP encodings of the verification problem.

## 6 Outlook

Below we discuss considerations that could enable future iterations of the VNN-COMP to serve its goals and the community, discussed in Section 3, even better.

### Tracking Year-on-Year Progress

While we believe VNN-COMP already provides reasonable mechanisms for comparing the tools submitted in every iteration, the changing benchmarks and tools make it hard to track the year-on-year progress of the field as a whole. Because some tools are heavily optimized for the specific benchmarks of that year's competition, simply evaluating them on the benchmarks of previous (or future) years (even if they support them) does not yield a meaningful progress metric. While one benchmark from the inaugural competition was included as an unsocred extra benchmark in the two following iterations (cifar2020), only few unsolved instances remain, making it a very insensitive measure for further improvements. While including all benchmarks from previous years in the (scored) benchmark selection would place an undue burden on participants, choosing one particularly challenging, representative, and interesting benchmark every year to be included as a (scored) extra benchmark in future iterations might be a good compromise. Additionally, a more restrictive stance on tool tuning could enable a much more representative evaluation of new tools on old benchmarks.

### Tool Tuning

Many of the most successful tools do not employ a single verification strategy, but a whole portfolio of different modes, all coming with different hyperparameters. Depending on their choice, tool performance can vary significantly, making it essential for practitioners to get their choice right when applying these tools to new problems. However, this can be highly challenging given the large number of parameters and their complex interactions, especially without in-depth knowledge of the tool.

For VNN-COMP, tuning tools was allowed explicitly on a per-benchmark basis and implicitly on a per-network basis, enabling teams to showcase the maximum performance of their tools. However, for future iterations it might be interesting to restrict tuning for some or all benchmarks to encourage authors to develop autotuning strategies, making the adaption of their tools to new problems much easier. This could,

Figure 4.1: Cactus plot for all tools in the VNN-COMP 2022 across all benchmarks.
for example, be implemented by not only generating random specifications but also random networks.

### Batch Processing

Every VNN-COMP benchmark consists of a set of instances that, while typically related, are evaluated in isolation, with the tool being terminated in between. Unfortunately, this means that any startup overhead such as acquiring a GPU or preprocessing the considered network is incurred for every instance. This is in contrast to most practical settings where a large number of input-output specifications are considered for the same network. This discrepancy is accounted for by measuring and subtracting this overhead from each individual runtime. However, not only is this overhead measurement process flawed and introduces noise, but it can also dominate the evaluation time for easy instances.

In future iterations, tools could be provided with a whole batch of properties at once to more closely relate to their typical application. Further, currently, timeouts are defined per instance, making a strategy of always attempting verification until timeout optimal.

\begin{table}
\begin{tabular}{l l l l l l} \hline \hline \multirow{2}{*}{Tool} & \multirow{2}{*}{Organization} & \multicolumn{3}{c}{Participation, Place} & References \\ \cline{3-6}  & & 2020 [2] & 2021 [5] & 2022 [34] & \\ \hline \(\alpha\)-\(\beta\)-CROWN & Carnegie Mellon, Northeastern, & ✗ & ✓(1/12) & ✓(1/11) & [63, 57, 58] \\  & Columbia, UCLA & & ✗ & ✓(11/11) & N/A \\ AveriNN & Kansas State University & ✗ & ✗ & ✓(11/11) & N/A \\ CGDTest & University of Waterloo & ✗ & ✗ & ✓(5/11) & N/A \\ Debona & RWTH Aachen University & ✗ & ✓(6/12) & ✓(8/11) & [9] \\ DNNF & University of Virginia & ✗ & ✓(12/12) & ✗ & [42] \\ ERAN & ETH Zurich, UIUC & ✓(3/12) & ✗ & [46, 43, 45, 36, 39] \\ FastBatLLNN & University of California & ✗ & ✗ & ✓(9/11) & N/A \\ Marabou & Hebrew University of Jerusalem, & ✗ & ✓(5/12) & ✓(7/11) & [25] \\  & Stanford University, Amazon Web & & & & \\ MIPVerify & Massachusetts Institute of Technology & ✓ & ✗ & ✗ & [49] \\  &ogy & & & & \\ MN-BaB & ETH Zurich & ✗ & ✗ & ✓(2/11) & [14] \\ nennum & Stony Brook University & ✓ & ✓(8/12) & ✓(4/11) & [4] \\ NNV & Vanderbilt University & ✓ & ✓(9/12) & ✗ & [50, 53, 52, 51, 56] \\ NV.jl & Carnegie Mellon, Northeastern & ✗ & ✓(10/12) & ✗ & [28] \\ Oval & University of Oxford & ✓ & ✓(3/12) & ✗ & [10, 11, 31] \\ PeergiNN & University of California & ✓ & ✗ & ✓(6/11) & [26] \\ RPM & Stanford & ✗ & ✓(11/12) & ✗ & [54] \\ Venus & Imperial College London & ✓ & ✓(7/12) & ✗ & [8, 27] \\ VeraPak & Utah State University & ✗ & ✗ & ✓(10/11) & N/A \\ VeriNet & Imperial College London & ✓ & ✓(2/12) & ✓(3/11) & [20, 21] \\ \hline \hline \end{tabular}
\end{table}
Table 5.1: Participating tools.

\begin{table}
\begin{tabular}{l l l l} \hline \hline  & 2020 & 2021 & 2022 \\ \hline Tools registered & N/A & 15 & 18 \\ Tools submitted & 8 & 13 & 11 \\ Benchmarks submitted & 5 & 8 (+1 unscored) & 12 (+1 unscored) \\ Max. network depth & 8 & 18 & 27 \\ Max. network parameters & 855,600 & 42,059,431 (sparse) & 138,356,520 \\ Activation functions & ReLU, tanh, sigmoid & ReLU, sigmoid, MaxPool, AveragePool \\ Layer types & Fully Connected, Conv & Fully Connected, Conv, Residual & Fully Connected, Conv, Residual, BatchNorm \\ Applications & Image Recognition, Control, Database Indexing & Image Recognition, Control, Database Indexing, Cardinality Estimation \\ Mean \#benchmarks/tool & 3.0 (min 2, max 5) & 5.5 (min 1, max 9) & 7.3 (min 1, max 13) \\ \hline \hline \end{tabular}
\end{table}
Table 5.2: Comparison across years.
However, in a practical setting, recognizing instances where verification is likely to fail and stopping early can significantly increase a method's throughput and thus utility. Switching to per benchmark timeouts for the VNN-COMP would incentivize the development of effective heuristics towards this goal. Furthermore, tools could benefit from proof-sharing approaches [15], where verified sub-problems from one instance are reused for following instances.

### Continuous Competition

In addition to a yearly VNN-COMP, tool submissions for the most recent benchmark set could be accepted on a rolling basis, made possible by the automated submission and evaluation process introduced this year. This would transform the competition from a yearly snapshot of the current research to a centralized repository of the state-of-the-art, updating as teams submit new methods that they publish. However, if not implemented with great care, this would enable tools to be tuned on the evaluation instances before submission, leading to a skewed comparison. Further, the question of funding the required cloud compute remains open.

### Soundness Evaluation

An inherent requirement for neural network verifiers is that they are sound, i.e., they never claim a safety property holds, when in fact it does not. However, assessing soundness is difficult as the ground truth for VNN-COMP problem instances is generally only known if it was shown to be SAT with a valid counter-example. This is particularly problematic when no instances in a benchmark are SAT and thus returning UNSAT for every instance immediately can not be demonstrated to be unsound. Requiring a certain portion of instances of every benchmark to be SAT (in expectation), could alleviate this issue. An interesting alternative avenue to tackle this challenge is proof generation [37]. An extra category could be introduced where tools are additionally required or incentivized to provide a verifiable proof if they claim a property is UNSAT.

While big soundness bugs are rare, few or none of the submitted tools are floating point sound, i.e., even tools that would be sound using exact arithmetic might become unsound due to imprecisions introduced by floating-point arithmetic. This is particularly pronounced if tools choose to use single precision computations for performance reasons. The sensitivity of different tools to such issues could be evaluated on a benchmark specifically designed to uncover floating point soundness issues.

### Other Competition Modes

A dedicated falsifier category could be added to encourage teams to develop and submit stronger attacks, going beyond the standard adversarial attacks. Further, a meta-solver category could be added to investigate whether approaches that heuristically pick from a range of methods, successful in other domains [59], can significantly outperform individual tools. However, it would need to be ensured that these tools provide sufficient value over individual submissions, which already combine different verification strategies.

### Promote Common Tool Development

Parsing large and complex VNN-LIB files or converting ONNX files to other common formats can be time-consuming to implement. While many teams implemented their own tools to this end, available, open-source tools for the parsing of VNN-LIB files [1] and the optimization of ONNX files (DNNV [41]) should be highlighted and their continued development encouraged.

### Remaining Challenges

We can broadly identify four groups of challenges in neural network verification:

* Verifying relatively small but only weakly regularized networks, which requires an extraordinarily precise analysis, can still be intractable with current methods.
* Scaling precise methods to medium-sized networks (e.g. small ResNets) and datasets (e.g. Cifar100 or TinyImageNet) with a large number of neurons is challenging, as the cost of branch-and-bound based algorithms scales exponentially with the required split depth, making branching decisions both harder and more important.
* Scaling verification to large networks (e.g. VGG-Net 16) and datasets (e.g. ImageNet) in the presence of dense input specifications requires particularly memory-efficient implementations due to a large number of neurons.
* Verification outside of the classification setting is underexplored leading to a lack of established approaches for, e.g., image segmentation or object detection.
Orthogonally, the training of certifiably robust networks remains an open problem. Despite significant progress over recent years [6; 18; 33; 35; 38; 40; 60], networks trained specifically to exhibit provable robustness guarantees still suffer from severely degraded standard accuracy. Therefore, most benchmarks considered in the VNN-COMP are based on networks trained without consideration for later certification. More broadly in the community, readers may also be interested in the International Competition on Verifying Continuous and Hybrid Systems (ARCHCOMP)5 category on Artificial Intelligence and Neural Network Control Systems (AINNCS), which has been held annually since 2019 [30; 29], and considers neural network verification in closed-loop systems.

Footnote 5: [https://cps-vo.org/group/ARCH/FriendlyCompetition](https://cps-vo.org/group/ARCH/FriendlyCompetition)

## 7 Advice for Participants

In this section, we provide some guidance for teams that are interested in the VNN-COMP but have not participated yet. Note that these are neither rules nor requirements.

### For Benchmark Authors

The VNN-COMP intends to highlight areas where neural network verification can be successfully applied and to showcase interesting differences between the participating tools. Thus, ideally, tasks are not so hard that none of the instances can be solved by any participant but also not so easy that every tool can solve all of them. For benchmarks related to real-world applications, we recommend including a detailed description of the background, to highlight the benchmark's relevance and the characteristics of the verification problem, e.g. sparseness of the input or some network layers. Further questions and requests for modifications should be expected while tool authors work on supporting the proposed benchmark.

### For Tool Authors

We recommend teams reference past benchmarks to test their tool before the new benchmarks are submitted. Given the ever-increasing diversity of submitted benchmarks, it may not be feasible to support all benchmarks from the get-go. If this is the case, we recommend focusing on the fully connected and convolutional ReLU networks, which in the past have covered a wide range of benchmarks, while minimizing implementation effort. Some operations, e.g., max-pooling can also be simplified to multiple ReLU layers using tools such as DNNV[41]. Further, we recommend extensive testing against adversarial attacks to minimize the chance for soundness errors. For tools that are designed for very specific problems, we also want to encourage authors to submit a relevant benchmark highlighting this specialization. Finally, we recommend reading publications associated with the well-performing tools (see Table 5.1) to gain a better understanding of the techniques used by successful teams.

## 8 Conclusions

In this report, we summarize the main processes and results of the three VNN-COMP held so far from 2020 to 2022. We highlight the growing interest in the field, expressed in an increasing number of registered teams and considered benchmarks, including some submitted by industry. Further, we observe that every year, the size and complexity not only of the considered networks but also specifications grew, driving and exemplifying progress in the field. Finally, we highlight the increase in accessibility of verification methods resulting from the standardized input and output formats and the automated installation and evaluation process required for participation in VNN-COMP.

###### Acknowledgements.

 This material is based upon work supported by the Air Force Office of Scientific Research and the Office of Naval Research under award numbers FA9550-19-1-0288, FA9550-21-1-0121, FA9550-22-1-0019, FA9550-22-1-0450, and N00014-22-1-2156, as well the Defense Advanced Research Projects Agency (DARPA) Assured Autonomy program through contract number FA8750-18-C-0089, and the National Science Foundation (NSF) under grants 1911017, 2028001, 2220401, and 2220426. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the United States Air Force, the United States Navy, DARPA, nor NSF.
