Source-linked AI summary
The Second International Verification of Neural Networks Competition (VNN-COMP 2021): Summary and Results
Stanley Bak, Changliu Liu, Taylor Johnson
TL;DR
Neural networks are used in many applications, but few tools provide formal guarantees about their behavior. VNN-COMP 2021 standardized formats and execution hardware to compare verification tools; tools showed progress on shared benchmarks, though hardware differences complicate year-to-year speed comparisons.
Problem
Neural networks are used in many applications, but few tools provide formal guarantees about their behavior.
Source: §1 · p. 1Method
VNN-COMP 2021 compared verification tools using ONNX networks, VNNLIB specifications, organizer-run AWS hardware, and tool parameters supplied by authors.
Source: §1 · p. 1Results
Tools showed significant progress in scalability and speed on the common CIFAR2020 and ACASXU benchmarks versus previous years, but hardware differences leave the source of speed gains unclear.
Source: §6 · p. 24Takeaways & Limitations
Open benchmarks and execution scripts support replication, while common input formats may lower barriers for industry participants to use the tools.
Source: §6 · p. 24Odd-one-out scoring can misjudge incorrect results, and scoring choices can affect the third-place ranking.
Source: §5.1 · p. 16
Abstract
from arXiv · showhide
This report summarizes the second International Verification of Neural Networks Competition (VNN-COMP 2021), held as a part of the 4th Workshop on Formal Methods for ML-Enabled Autonomous Systems that was collocated with the 33rd International Conference on Computer-Aided Verification (CAV). Twelve teams participated in this competition. The goal of the competition is to provide an objective comparison of the state-of-the-art methods in neural network verification, in terms of scalability and speed. Along this line, we used standard formats (ONNX for neural networks and VNNLIB for specifications), standard hardware (all tools are run by the organizers on AWS), and tool parameters provided by the tool authors. This report summarizes the rules, benchmarks, participating tools, results, and lessons learned from this competition.
1 Introduction
Neural networks are increasingly used in applications, but few tools formally guarantee their behavior; such guarantees matter for safety-critical use. VNN-COMP 2021 sought a fair comparison of verification tools using standardized formats and hardware.
1 Introduction
- Few tools provide formal guarantees about neural-network behavior, despite neural networks' growing use across applications.The report identifies this gap as relevant to safety-critical applications that need behavior understood and predicted at design time.Source: §1 · p. 1
- VNN-COMP was established in 2020 to bring together researchers working on neural-network verification, and its 2021 edition was part of FoMLAS at CAV.The competition sought to compare methods in terms of scalability and speed.Source: §1 · p. 1
- The competition aimed to make tool comparisons fairer by standardizing neural-network and specification formats and running tools on organizer-selected AWS hardware.The chosen formats were ONNX and VNNLIB; tools ran on CPU instances or cost-equivalent GPU instances.Source: §1 · p. 1
- Twelve teams submitted tools, which organizers ran on AWS for two weeks before reporting the results in July 2021.The final results were reported at FoMLAS on July 19, 2021.Source: §1 · p. 2
2 Rules
The rules define verification instances and benchmarks, cap execution time, and score correctness and speed. They also correct runtimes for tool overhead, with a separate adjustment for the CPU or GPU mode used.
2 Rules
- An instance is a specification, network, and timeout; a benchmark is a set of instances.The rules illustrate a benchmark with one classifier and multiple input images, each with its own timeout.Source: §2 · p. 2
- Each instance had a proposer-set timeout, while each benchmark had a six-hour runtime cap.The rules also subtract startup overhead from total runtime.Source: §2 · p. 2
- Correct holds and nontrivial violations earned 10 points, easily found violations 1 point, and incorrect results -100 points.The rules distinguish violations found by random tests or simple adversarial generation from those that were not.Source: §2 · pp. 2–3
- The fastest tool on a solved instance received 2 bonus points and the second-fastest received 1.Runtimes below 1.0 seconds counted as 1.0 seconds, and times within 0.2 seconds counted as equal for scoring.Source: §2 · p. 3
- Organizers estimated startup overhead using trivial network instances and subtracted it from runtimes; multi-overhead scoring used the overhead measured for the tool's actual CPU or GPU mode.A single overhead measure could unintentionally penalize GPU mode when CPU and GPU overheads differed.Source: §2 · p. 3
3 Participants
The report lists participating teams and summarizes tool features. Marabou handles varied network queries and, for the competition, combined bound tightening with parallel complete-verification approaches.
3 Participants
- The report lists participating teams and summarizes their key tool features in Table 1.The Marabou entry identifies team members from Hebrew University of Jerusalem, Stanford University, Amazon Web Services, and NRI Secure.Source: §3 · p. 3, §3.1 · p. 3, Table 1 · p. 4
3.1 Marabou
- Marabou encodes network-property queries as constraint satisfaction problems and supports multiple activation functions and network topologies.Its listed activations include ReLU, Leaky ReLU, Sign, Max, and absolute value; its topologies include feed-forward, convolutional, and residual networks.Source: §3.1 · p. 4
- For the competition, Marabou used DeepPoly to tighten variable bounds, then split complete verification between a Gurobi MILP encoding and a newer complete procedure.The two approaches ran on separate portions of the CPUs.Source: §3.1 · p. 4
3.2 VeriNet
VeriNet is a complete verifier for feed-forward networks that uses symbolic interval propagation to build a linear abstraction and an LP encoding. It refines results with branch and bound and includes several search, relaxation, and splitting optimizations.
3.2 VeriNet
- VeriNet uses symbolic interval propagation to form a linear abstraction, analyzes the verification problem with an LP encoding, and applies branch-and-bound refinement for completeness.The tool is described as a complete verifier for feed-forward neural networks.Source: §3.2 · p. 5
- VeriNet adds gradient-based counterexample search, optimal Sigmoid relaxations, adaptive node splitting, succinct LP encodings, and a splitting heuristic that accounts for downstream effects.The heuristic considers indirect effects of splits on succeeding relaxations.Source: §3.2 · p. 5
- VeriNet supports multiple activations and layer types, including convolution, pooling, batch normalization, reshape, crop, transpose, and additive residual connections.It participated in benchmarks including ACASXu, CIFAR10 ResNet, CIFAR2020, MNISTFC, and others.Source: §3.2 · p. 5
3.3 ERAN
ERAN combines abstract-interpretation encodings with multiple relaxations and bound refinement, while α,β-CROWN combines optimized bound propagation with branch-and-bound. Both descriptions emphasize methods for producing tighter bounds or precise network encodings.
3.3 ERAN
- ERAN combines single- and multi-neuron relaxations, partial MILP encoding, and neuron-wise bound refinement to build a precise network encoding.It uses 64-bit precision and floating-point-sound arithmetic up to the LP solver, and its GPU-and-CPU use requires both resources to avoid bottlenecks.Source: §3.3 · p. 5
- ERAN’s incomplete mode runs PGD before increasingly expensive abstractions, but reusing the same abstractions across a benchmark can leave properties unverified at timeout.A more expensive abstraction might have verified such a property in time.Source: §3.3 · p. 5
3.3 ERAN; 3.4 α,β-CROWN
- α,β-CROWN participated in nine benchmarks: ACASXu, cifar10 resnet, cifar2020, eran, marabou-cifar10, mnistfc, nn4sys, oval21, and verivital.Source: §3.4 · p. 6
3.4 α,β-CROWN
- α,β-CROWN jointly optimizes intermediate and final bounds, then uses β-CROWN branch-and-bound with split constraints incorporated into bound propagation [49] [53] [54].Its generalized CROWN implementation supports varied architectures and activation functions and is GPU-accelerated.Source: §3.4 · p. 6
- α,β-CROWN uses Gurobi to tighten as many intermediate bounds as possible within the CPU timeout budget, then α-CROWN for the rest and β-CROWN branch-and-bound.The authors report that MIP helps on some benchmarks and could be more beneficial on hardware with stronger CPUs and GPUs.Source: §3.4 · p. 6
3.5 DNNF
DNNF targets property falsification rather than proof: it reduces specifications and networks to robustness problems, then applies adversarial attacks to search for counterexamples.
3.5 DNNF
- DNNF only searches for counterexamples and will not prove that a property holds.Its reduction to robustness problems supports more complex specifications, including direct input-output relations such as y > x.Source: §3.5 · p. 6
- For VNN-COMP, DNNF uses a custom PGD implementation, while also supporting off-the-shelf methods from Foolbox or CleverHans.The tool can run on GPUs, which can speed falsification for large models.Source: §3.5 · pp. 6–7
- DNNF uses DNNV to load networks and properties and perform network simplifications, and supports ONNX models with a broad set of operations.The listed operations include convolution, pooling, matrix multiplication, and common nonlinear activations.Source: §3.5 · p. 7
3.6 NNV
NNV uses geometric reachability analysis for neural-network verification, while OVAL uses a specialized branch-and-bound framework with adaptive bounds and falsification.
3.6 NNV
- NNV computes exact reachable sets layer by layer using star sets and can construct and visualize the complete set of counterexample inputs when a safety property is violated [43] [46].Its focus includes closed-loop neural-network control systems in autonomous cyber-physical systems.Source: §3.6 · p. 7
3.7 OVAL
- OVAL uses branch-and-bound with branching, over-approximation bounds, and counterexample search; its competition entry uses MI-FGSM adapted for general property falsification [9] [14].It adaptively selects between Beta-CROWN and Active Set bounds [49, 11].Source: §3.7 · pp. 7–8
- For medium-to-large input dimensions, OVAL uses FSB branching, while for small input dimensions it can use input splitting [13] [9] [10].FSB combines dual-based ReLU scoring with inexpensive strong-branching approximations.Source: §3.7 · p. 7
- OVAL’s PyTorch implementation exploits GPU acceleration and parallelizes over branch-and-bound subproblems and intermediate computations [8].It supports fully connected and convolutional networks with ReLU, maxpool, and average-pooling layers.Source: §3.7 · p. 8
3.8 RPM
RPM incrementally computes reachable sets, NV.jl brings multiple verification approaches to ONNX and VNNLIB inputs, and Venus uses MILP-based verification with ReLU dependency handling.
3.8 RPM
- RPM computes exact forward and backward reachable sets for ReLU feedforward networks, and its incremental computation can find unsafe inputs before completing the reachable set [47].The tool has no parallel implementation, though the algorithm is amenable to parallelization.Source: §3.8 · p. 8
3.9 ComposableNeuralVerification (NV.jl)
- NV.jl adapts a Julia toolbox of reachability-, optimization-, and search-based verification algorithms and adds support for ONNX networks and VNNLIB specifications.It participated in nn4sys and ACASXu.Source: §3.9 · pp. 8–9
3.10 Venus
- Venus uses MILP verification and exploits ReLU dependencies through callback cuts and branching that reduces the required integrality constraints.Its symbolic interval propagation optimizes each ReLU’s linear relaxation to reduce over-approximation error in later layers.Source: §3.10 · p. 9
3.11 Debona
The tool descriptions contrast Debona’s independent upper and lower bounds with nnenum’s layered abstractions and parallelized ReLU splitting. The section also lists benchmark coverage and provides an overview of benchmarks.
3.11 Debona
- Independent upper and lower bounds let Debona obtain tighter relaxations, especially for ReLUs where a zero lower bound may outperform bounds that are broadly negative.Debona is a fork of VeriNet.Source: §3.11 · p. 9
3.12 nnenum
- nnenum combines three types of zonotopes with star-set overapproximations and parallelized ReLU case splitting to verify ReLU networks without sacrificing completeness.Its ImageStar method propagates sets through ONNX-supported layers, including convolutional layers with arbitrary parameters.Source: §3.12 · p. 9
- The benchmark overview is presented in Table 2, and nnenum participated in AcasXu, cifar2020, mnistfc, and oval.The tool added VNNLIB support and optimized some ACASXu LP timeout parameters for this competition.Source: §3.12 · pp. 9–10, Table 2 · p. 10
4 Benchmarks
The benchmarks cover neural-network verification across aircraft collision advisories, image classification, learned database indexes, and pooling architectures. They vary network structures, specifications, perturbations, and timeouts to assess verification tools across different settings.
4.1 ACAS Xu
- ACAS Xu comprises 186 properties over 45 advisory networks, with properties 1–4 checked on all networks and 5–10 on one network; each property has a 116-second timeout.The original verification times ranged from seconds to days, including unfinished instances.Source: §4.1 · p. 10
4.2 Cifar10 resnet
- The CIFAR-10 ResNet benchmark targets more generic verification tools with two residual-network models; specifications test correct classification on selected images under ℓ∞ perturbations.ResNet-2B has 2 residual blocks and ResNet-4B has 4; the ResNet-4B model has over 10K neurons. Table 3 reports clean, PGD, and vanilla CROWN/DeepPoly verified accuracy, not α,β-CROWN competition results.Source: §4.2 · pp. 10–11
4.3 Cifar2020 (unscored)
- Cifar2020 combines two earlier CIFAR-10 convolutional networks with a larger ConvBig model to evaluate progress in neural-network verification.Specifications use correctly classified test images and ℓ∞ perturbations, with a five-minute per-sample timeout.Source: §4.3 · p. 11
4.4 eran
- The eran benchmark compares ReLU and Sigmoid networks to examine how piecewise-linear versus non-piecewise-linear activations relate to certifiability under ℓ∞ adversaries.It uses 36 correctly classified MNIST images per network, with five-minute per-sample timeouts.Source: §4.4 · p. 12
4.5 Marabou-cifar10
- Marabou-cifar10 provides three CIFAR-10 convolutional ReLU networks, ranging from 2,568 to 10,528 ReLUs, for targeted adversarial-robustness specifications.The two perturbation bounds are 0.012 and 0.024, with a five-minute per-query timeout.Source: §4.5 · p. 12
4.6 Mnistfc
- Mnistfc tests fully connected ReLU classifiers with 2, 4, and 6 layers, using 15 correctly classified MNIST images and perturbation bounds of 0.03 and 0.05.The per-instance timeout is two minutes for the 2-layer network and five minutes for the others.Source: §4.6 · p. 12
4.7 NN4Sys
- NN4Sys benchmarks learned database indexes by specifying bounds on prediction error for input-output intervals, with pairs chosen to span user needs and verifier difficulty.The original two-stage learned index is converted to an integrated network by adding handcrafted layers, avoiding its unsupported switch operation; the benchmark aims to provide safety guarantees for all keys.Source: §4.7 · p. 13
4.8 Oval21
- OVAL21 assigns image-network-specific perturbation radii through binary searches intended to make each robustness property challenging for verification.It includes three robustly trained CIFAR-10 ReLU convolutional networks and uses a 720-second per-instance timeout.Source: §4.8 · pp. 13–14
5 Results
VNN-COMP 2021 reports an overall ranking and individual benchmark results, with scoring affected by overhead correction and how mismatching results were judged. Results and scoring scripts were reviewed and made available alongside statistics on participation and verification outcomes.
5 Results
- Organizers ran tools across the benchmarks, sent CSV results to authors for review, and published detailed logs, scoring scripts, and result files.The logs include runtimes and scores and can help identify challenging instances for tool development.Source: §5 · p. 15
5.1 Overall Score
- α,β-CROWN ranked first overall, followed by VeriNet; oval and ERAN shared third place, with their order depending on overhead and incorrect-result scoring.Table 4 reports scores under two overhead measurements; the remaining tables use multi-overhead measurements.Source: §5.1 · p. 15, Table 4 · p. 16
- Voting and odd-one-out judgments of incorrect results could change the total ranking, and either strategy may misclassify a tool when results mismatch.The report displays odd-one-out scores for category results and suggests standardizing counterexample outputs in future editions.Source: §5.1 · pp. 15–16
5.2 Other Stats
- The other-statistics tables cover overhead, benchmark participation, instances verified, violations, and holds; ERAN's overhead columns distinguish CPU-mode and GPU runs.For ERAN, CPU Mode applies to ACASXu and ERAN, while Seconds corresponds to GPU runs for the other tools.Source: §5.2 · p. 17, Table 5 · p. 17, Table 6 · p. 17
5.3 Benchmark Scores
- Tools participating in all or almost all benchmarks did best overall, although some tools ranked lower overall while performing well on individual benchmarks.The reported benchmark scores use multi-overhead measurements and odd-one-out scoring; alternate parameter choices caused minor ranking changes.Source: §5.3 · p. 20
6 Conclusion and Ideas for Future Competitions
VNN-COMP 2021 standardized neural-network and specification formats and measurement hardware, and its common benchmarks showed progress in scalability and speed over previous years. Hardware differences limit how clearly that progress can be attributed to algorithmic improvements, while the report identifies competition changes for future editions.
6 Conclusion and Ideas for Future Competitions
- On common CIFAR2020 and ACASXU benchmarks, tools showed significant scalability and speed progress over previous years, but nonstandardized hardware in the prior competition leaves the source of speed gains unclear.The report notes that algorithmic improvements and better hardware may both account for the observed speed improvement.Source: §6 · p. 24
- The benchmarks and execution scripts are openly available for replication, while common input formats are intended to reduce barriers for industry participants.The report hopes the setup will support fair comparisons of future verification-method improvements.Source: §6 · p. 24
- Future editions could allow more hardware choices and standardize counterexample formats; custom per-benchmark hardware would require additional automation, including license installation.The report also notes that some tool authors said their tools could run faster with both a strong CPU and GPU.Source: §6 · p. 24