SoundnessBench: A Soundness Benchmark for Neural Network Verifiers

TL;DR

SoundnessBench is a new benchmark with hidden counterexamples designed to test the soundness of neural network verifiers, revealing bugs in state-of-the-art tools and improving verification reliability.

Contribution

We introduce SoundnessBench, a novel benchmark with deliberately inserted hidden counterexamples to evaluate and improve the soundness of neural network verifiers.

Findings

SoundnessBench effectively identifies bugs in current verifiers.

Our training method successfully produces neural networks with hidden counterexamples.

The benchmark covers various architectures and activation functions.

Abstract

Neural network (NN) verification aims to formally verify properties of NNs, which is crucial for ensuring the behavior of NN-based models in safety-critical applications. In recent years, the community has developed many NN verifiers and benchmarks to evaluate them. However, existing benchmarks typically lack ground-truth for hard instances where no current verifier can verify the property and no counterexample can be found. This makes it difficult to validate the soundness of a verifier, when it claims verification on such challenging instances that no other verifier can handle. In this work, we develop a new benchmark for NN verification, named SoundnessBench, specifically for testing the soundness of NN verifiers. SoundnessBench consists of instances with deliberately inserted counterexamples that are hidden from adversarial attacks commonly used to find counterexamples. Thereby, it can identify false verification claims when hidden counterexamples are known to exist. We design a training method to produce NNs with hidden counterexamples and systematically construct our SoundnessBench with instances across various model architectures, activation functions, and input data. We demonstrate that our training effectively produces hidden counterexamples and our SoundnessBench successfully identifies bugs in state-of-the-art NN verifiers. Our code is available at https://github.com/mvp-harry/SoundnessBench and our dataset is available at https://huggingface.co/datasets/SoundnessBench/SoundnessBench.