SoundnessBench: A Soundness Benchmark for Neural Network Verifiers

• URL: http://arxiv.org/abs/2412.03154v2
• Date: Tue, 14 Oct 2025 19:22:14 GMT
• Title: SoundnessBench: A Soundness Benchmark for Neural Network Verifiers
• Authors: Xingjian Zhou, Keyi Shen, Andy Xu, Hongji Xu, Cho-Jui Hsieh, Huan Zhang, Zhouxing Shi,
• Abstract summary: We develop a new benchmark for NN verification, named "SoundnessBench", specifically for testing the soundness of NN verifiers.<n>SoundnessBench consists of instances with deliberately inserted counterexamples that are hidden from adversarial attacks.<n>We demonstrate that our training effectively produces hidden counterexamples and our SoundnessBench successfully identifies bugs in state-of-the-art NN verifiers.
• Score: 45.86647998712757
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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 benchmark is available at https://huggingface.co/datasets/SoundnessBench/SoundnessBench.

Related papers

• Floating-Point Neural Network Verification at the Software Level [2.228696309685013]
  The behaviour of neural network components must be proven correct before deployment in safety-critical systems.<n>Existing neural network verification techniques cannot certify the absence of faults at the software level.<n>We show how to specify and verify that neural networks are safe, by explicitly reasoning about their floating-point implementation.
  arXiv  Detail & Related papers  (2025-10-27T14:43:19Z)
• Exact Certification of (Graph) Neural Networks Against Label Poisoning [50.87615167799367]
  We introduce an exact certification method for label flipping in Graph Neural Networks (GNNs) We apply our method to certify a broad range of GNN architectures in node classification tasks. Our work presents the first exact certificate to a poisoning attack ever derived for neural networks.
  arXiv  Detail & Related papers  (2024-11-30T17:05:12Z)
• Revisiting Differential Verification: Equivalence Verification with Confidence [0.6562256987706128]
  When validated neural networks (NNs) are pruned (and retrained) before deployment, it is desirable to prove that the new NN behaves equivalently to the original NN. This paper revisits the idea of differential verification which performs reasoning on differences between NNs.
  arXiv  Detail & Related papers  (2024-10-26T15:53:25Z)
• A Certified Proof Checker for Deep Neural Network Verification [0.9895793818721335]
  We present an alternative implementation of the Marabou proof checking algorithm in Imandra. It allows us to obtain an implementation with formal guarantees, including proofs of mathematical results underlying the algorithm.
  arXiv  Detail & Related papers  (2024-05-17T08:16:32Z)
• Provably Safe Neural Network Controllers via Differential Dynamic Logic [2.416907802598482]
  We present the first general approach that allows reusing control theory results for NNCS verification. Based on provably safe control envelopes in dL, we derive specifications for the NN which is proven via NN verification. We show that a proof of the NN adhering to the specification is mirrored by a dL proof on the infinite-time safety of the NNCS.
  arXiv  Detail & Related papers  (2024-02-16T16:15:25Z)
• Towards a Certified Proof Checker for Deep Neural Network Verification [1.0485739694839669]
  We present a novel implementation of a proof checker for DNN verification. It improves on existing implementations by offering numerical stability and greater verifiability.
  arXiv  Detail & Related papers  (2023-07-12T16:53:32Z)
• The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural Networks [94.63547069706459]
  #DNN-Verification problem involves counting the number of input configurations of a DNN that result in a violation of a safety property. We propose a novel approach that returns the exact count of violations. We present experimental results on a set of safety-critical benchmarks.
  arXiv  Detail & Related papers  (2023-01-17T18:32:01Z)
• Certified Robustness of Quantum Classifiers against Adversarial Examples through Quantum Noise [68.1992787416233]
  We show that adding quantum random rotation noise can improve robustness in quantum classifiers against adversarial attacks. We derive a certified robustness bound to enable quantum classifiers to defend against adversarial examples.
  arXiv  Detail & Related papers  (2022-11-02T05:17:04Z)
• Sound and Complete Verification of Polynomial Networks [55.9260539566555]
  Polynomial Networks (PNs) have demonstrated promising performance on face and image recognition recently. Existing verification algorithms on ReLU neural networks (NNs) based on branch and bound (BaB) techniques cannot be trivially applied to PN verification. We devise a new bounding method, equipped with BaB for global convergence guarantees, called VPN.
  arXiv  Detail & Related papers  (2022-09-15T11:50:43Z)
• VPN: Verification of Poisoning in Neural Networks [11.221552724154988]
  We study another neural network security issue, namely data poisoning. In this case an attacker inserts a trigger into a subset of the training data, in such a way that at test time, this trigger in an input causes the trained model to misclassify to some target class. We show how to formulate the check for data poisoning as a property that can be checked with off-the-shelf verification tools.
  arXiv  Detail & Related papers  (2022-05-08T15:16:05Z)
• Spotting adversarial samples for speaker verification by neural vocoders [102.1486475058963]
  We adopt neural vocoders to spot adversarial samples for automatic speaker verification (ASV) We find that the difference between the ASV scores for the original and re-synthesize audio is a good indicator for discrimination between genuine and adversarial samples. Our codes will be made open-source for future works to do comparison.
  arXiv  Detail & Related papers  (2021-07-01T08:58:16Z)
• Adversarial Examples Detection with Bayesian Neural Network [57.185482121807716]
  We propose a new framework to detect adversarial examples motivated by the observations that random components can improve the smoothness of predictors. We propose a novel Bayesian adversarial example detector, short for BATer, to improve the performance of adversarial example detection.
  arXiv  Detail & Related papers  (2021-05-18T15:51:24Z)
• Understanding Classifier Mistakes with Generative Models [88.20470690631372]
  Deep neural networks are effective on supervised learning tasks, but have been shown to be brittle. In this paper, we leverage generative models to identify and characterize instances where classifiers fail to generalize. Our approach is agnostic to class labels from the training set which makes it applicable to models trained in a semi-supervised way.
  arXiv  Detail & Related papers  (2020-10-05T22:13:21Z)
• GraN: An Efficient Gradient-Norm Based Detector for Adversarial and Misclassified Examples [77.99182201815763]
  Deep neural networks (DNNs) are vulnerable to adversarial examples and other data perturbations. GraN is a time- and parameter-efficient method that is easily adaptable to any DNN. GraN achieves state-of-the-art performance on numerous problem set-ups.
  arXiv  Detail & Related papers  (2020-04-20T10:09:27Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.