Testing Neural Network Verifiers: A Soundness Benchmark with Hidden Counterexamples

• URL: http://arxiv.org/abs/2412.03154v1
• Date: Wed, 04 Dec 2024 09:24:33 GMT
• Title: Testing Neural Network Verifiers: A Soundness Benchmark with Hidden Counterexamples
• Authors: Xingjian Zhou, Hongji Xu, Andy Xu, Zhouxing Shi, Cho-Jui Hsieh, Huan Zhang,
• Abstract summary: We propose to develop a soundness benchmark for NN verification. Our benchmark contains instances with deliberately inserted counterexamples. Our benchmark successfully identifies bugs in state-of-the-art NN verifiers, as well as synthetic bugs.
• Score: 52.564617070814485
• License:
• Abstract: In recent years, many neural network (NN) verifiers have been developed to formally verify certain properties of neural networks such as robustness. Although many benchmarks have been constructed to evaluate the performance of NN verifiers, they typically lack a ground-truth for hard instances where no current verifier can verify and no counterexample can be found, which makes it difficult to check the soundness of a new verifier if it claims to verify hard instances which no other verifier can do. We propose to develop a soundness benchmark for NN verification. Our benchmark contains instances with deliberately inserted counterexamples while we also try to hide the counterexamples from regular adversarial attacks which can be used for finding counterexamples. We design a training method to produce neural networks with such hidden counterexamples. Our benchmark aims to be used for testing the soundness of NN verifiers and identifying falsely claimed verifiability when it is known that hidden counterexamples exist. We systematically construct our benchmark and generate instances across diverse model architectures, activation functions, input sizes, and perturbation radii. We demonstrate that our benchmark successfully identifies bugs in state-of-the-art NN verifiers, as well as synthetic bugs, providing a crucial step toward enhancing the reliability of testing 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

• Exact Certification of (Graph) Neural Networks Against Label Poisoning [50.87615167799367]
  Machine learning models are vulnerable to label flipping, i.e., the adversarial modification (poisoning) of training labels to compromise performance. We introduce an exact certification method, deriving both sample-wise and collective certificates. Our work presents the first exact certificate to a poisoning attack ever derived for neural networks, which could be of independent interest.
  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)
• 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)
• 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)

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.