pith. sign in

arxiv: 2212.10376 · v2 · pith:NPRCJ6XHnew · submitted 2022-12-20 · 💻 cs.LG · cs.AI· cs.SE

The Third International Verification of Neural Networks Competition (VNN-COMP 2022): Summary and Results

Mark Niklas M\"uller , Christopher Brix , Stanley Bak , Changliu Liu , Taylor T. Johnson This is my paper
classification 💻 cs.LG cs.AIcs.SE
keywords verificationneuralwerecompetitioninternationalnetworkstoolsvnn-comp
0
0 comments X
read the original abstract

This report summarizes the 3rd International Verification of Neural Networks Competition (VNN-COMP 2022), held as a part of the 5th Workshop on Formal Methods for ML-Enabled Autonomous Systems (FoMLAS), which was collocated with the 34th International Conference on Computer-Aided Verification (CAV). VNN-COMP is held annually to facilitate the fair and objective comparison of state-of-the-art neural network verification tools, encourage the standardization of tool interfaces, and bring together the neural network verification community. To this end, standardized formats for networks (ONNX) and specification (VNN-LIB) were defined, tools were evaluated on equal-cost hardware (using an automatic evaluation pipeline based on AWS instances), and tool parameters were chosen by the participants before the final test sets were made public. In the 2022 iteration, 11 teams participated on a diverse set of 12 scored benchmarks. This report summarizes the rules, benchmarks, participating tools, results, and lessons learned from this iteration of this competition.

This paper has not been read by Pith yet.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 5 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Shifting-based Optimizable Linear Relaxations for General Activation Functions

    cs.LG 2026-06 unverdicted novelty 7.0

    SLiR parameterizes linear relaxations by slope and uses shifting to compute sound bounds for general activation functions, enabling up to 7.8x more verified properties than prior methods.

  2. Quantitative Linear Logic for Neuro-Symbolic Learning and Verification

    cs.LO 2026-05 unverdicted novelty 7.0

    QLL is a novel logic for neuro-symbolic learning that uses ML-native operations (sum, log-sum-exp) on logits to embed constraints, satisfying most linear logic properties and showing stronger correlation between empir...

  3. Analyzing Symbolic Properties for DRL Agents in Systems and Networking

    cs.NI 2026-04 unverdicted novelty 7.0

    diffRL enables verification of symbolic properties over input ranges for DRL agents in adaptive video streaming, wireless resource management, and congestion control by decomposing them into tractable sub-properties f...

  4. Scaling Neural Network Verification with Tensor Parallelism and Fully Sharded Data Parallelism

    cs.LG 2026-06 unverdicted novelty 6.0

    Adapts TP and FSDP to bound-propagation verification, with FSDP delivering bitwise-identical bounds and 80-90% baseline memory reduction while TP trades some tightness for ~2x peak-memory savings.

  5. Quantitative Linear Logic for Neuro-Symbolic Learning and Verification

    cs.LO 2026-05 unverdicted novelty 6.0

    Quantitative Linear Logic interprets logical connectives via natural ML operations on logits to embed constraints in neural training while satisfying most linear logic laws and correlating performance with independent...