SoundnessBench: A Soundness Benchmark for Neural Network Verifiers

Understand

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.