Adaptive Branch-and-Bound Tree Exploration for Neural Network Verification

• URL: http://arxiv.org/abs/2505.00963v1
• Date: Fri, 02 May 2025 02:41:02 GMT
• Title: Adaptive Branch-and-Bound Tree Exploration for Neural Network Verification
• Abstract summary: ABONN explores the sub-problem space of BaB adaptively, in a Monte-Carlo tree search (MCTS) style.<n>ABONN demonstrates speedups of up to $15.2times$ on MNIST and $24.7times$ on CIFAR-10.
• Score: 8.733719614108102
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Formal verification is a rigorous approach that can provably ensure the quality of neural networks, and to date, Branch and Bound (BaB) is the state-of-the-art that performs verification by splitting the problem as needed and applying off-the-shelf verifiers to sub-problems for improved performance. However, existing BaB may not be efficient, due to its naive way of exploring the space of sub-problems that ignores the \emph{importance} of different sub-problems. To bridge this gap, we first introduce a notion of ``importance'' that reflects how likely a counterexample can be found with a sub-problem, and then we devise a novel verification approach, called ABONN, that explores the sub-problem space of BaB adaptively, in a Monte-Carlo tree search (MCTS) style. The exploration is guided by the ``importance'' of different sub-problems, so it favors the sub-problems that are more likely to find counterexamples. As soon as it finds a counterexample, it can immediately terminate; even though it cannot find, after visiting all the sub-problems, it can still manage to verify the problem. We evaluate ABONN with 552 verification problems from commonly-used datasets and neural network models, and compare it with the state-of-the-art verifiers as baseline approaches. Experimental evaluation shows that ABONN demonstrates speedups of up to $15.2\times$ on MNIST and $24.7\times$ on CIFAR-10. We further study the influences of hyperparameters to the performance of ABONN, and the effectiveness of our adaptive tree exploration.

Related papers

• Mining Verdict Boundaries for Neural Network Verification [10.091802208162585]
  Branch and Bound aims to achieve complete verification of neural networks by adaptively partitioning the problem and applying off-the-shelf verifiers to subproblems.<n>A key problem of BaB lies in searching for the verdict boundaries across all the paths that divide the verified and unverified subproblems.<n>We propose effective search approaches that leverage the monotonicity of each path to efficiently and precisely locate the verdict boundary.
  arXiv  Detail & Related papers  (2026-07-31T02:16:55Z)
• Graph Neural Network with One-side Edge Sampling for Fraud Detection [0.0]
  One-Side Edge Sampling (OES) can potentially reduce training duration as well as the effects of over-smoothing and over-fitting.<n>OES can empirically outperform backbone models in both shallow and deep architectures.
  arXiv  Detail & Related papers  (2026-01-11T07:59:39Z)
• Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification [9.733843486234878]
  State-of-the-art neural network (NN) verifiers demonstrate that applying the branch-and-bound (BaB) procedure with fast bounding techniques plays a key role in tackling many challenging verification properties.<n>We introduce the linear constraint-driven clipping framework, a class of scalable and efficient methods designed to enhance the efficacy of NN verifiers.
  arXiv  Detail & Related papers  (2025-12-11T19:59:37Z)
• Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees [8.804277530769532]
  State-of-the-art, branch and bound (BaB) is a "divide-and-conquer" strategy that applies off-the-shelf verifiers to sub-problems for which they perform better.<n>We propose a novel verification framework Oliva that explores the sub-problem space by prioritizing those sub-problems that are more likely to find counterexamples.<n>Oliva has two variants, including $OlivaGR$, a greedy strategy that always prioritizes the sub-problems that are more likely to find counterexamples.
  arXiv  Detail & Related papers  (2025-07-23T12:20:20Z)
• Testing Neural Network Verifiers: A Soundness Benchmark with Hidden Counterexamples [52.564617070814485]
  We propose to develop a soundness benchmark for NN verification.<n>Our benchmark contains instances with deliberately inserted counterexamples.<n>Our benchmark successfully identifies bugs in state-of-the-art NN verifiers, as well as synthetic bugs.
  arXiv  Detail & Related papers  (2024-12-04T09:24:33Z)
• A DPLL(T) Framework for Verifying Deep Neural Networks [9.422860826278788]
  Like human-written software, Deep Neural Networks (DNNs) can have bugs and can be attacked. We introduce NeuralSAT, a new verification approach that adapts the widely-used DPLL(T) algorithm used in modern SMT solvers.
  arXiv  Detail & Related papers  (2023-07-17T18:49:46Z)
• Deep Graph Neural Networks via Posteriori-Sampling-based Node-Adaptive Residual Module [65.81781176362848]
  Graph Neural Networks (GNNs) can learn from graph-structured data through neighborhood information aggregation. As the number of layers increases, node representations become indistinguishable, which is known as over-smoothing. We propose a textbfPosterior-Sampling-based, Node-distinguish Residual module (PSNR).
  arXiv  Detail & Related papers  (2023-05-09T12:03:42Z)
• OccRob: Efficient SMT-Based Occlusion Robustness Verification of Deep Neural Networks [7.797299214812479]
  Occlusion is a prevalent and easily realizable semantic perturbation to deep neural networks (DNNs) It can fool a DNN into misclassifying an input image by occluding some segments, possibly resulting in severe errors. Most existing robustness verification approaches for DNNs are focused on non-semantic perturbations.
  arXiv  Detail & Related papers  (2023-01-27T18:54:00Z)
• 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)
• The Devil is in the Conflict: Disentangled Information Graph Neural Networks for Fraud Detection [17.254383007779616]
  We argue that the performance degradation is mainly attributed to the inconsistency between topology and attribute. We propose a simple and effective method that uses the attention mechanism to adaptively fuse two views. Our model can significantly outperform stateof-the-art baselines on real-world fraud detection datasets.
  arXiv  Detail & Related papers  (2022-10-22T08:21:49Z)
• Revisiting Heterophily For Graph Neural Networks [42.41238892727136]
  Graph Neural Networks (GNNs) extend basic Neural Networks (NNs) by using graph structures based on the relational inductive bias (homophily assumption) Recent work has identified a non-trivial set of datasets where their performance compared to NNs is not satisfactory.
  arXiv  Detail & Related papers  (2022-10-14T08:00:26Z)
• 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)
• Abstraction and Refinement: Towards Scalable and Exact Verification of Neural Networks [9.85360493553261]
  Deep neural networks (DNNs) have been increasingly deployed in practice, but the lack of robustness hinders their applications in safety-critical domains. We present a novel abstraction-refinement approach for scalable and exact DNN verification.
  arXiv  Detail & Related papers  (2022-07-02T07:04:20Z)
• Online Limited Memory Neural-Linear Bandits with Likelihood Matching [53.18698496031658]
  We study neural-linear bandits for solving problems where both exploration and representation learning play an important role. We propose a likelihood matching algorithm that is resilient to catastrophic forgetting and is completely online.
  arXiv  Detail & Related papers  (2021-02-07T14:19:07Z)
• Global Optimization of Objective Functions Represented by ReLU Networks [77.55969359556032]
  Neural networks can learn complex, non- adversarial functions, and it is challenging to guarantee their correct behavior in safety-critical contexts. Many approaches exist to find failures in networks (e.g., adversarial examples), but these cannot guarantee the absence of failures. We propose an approach that integrates the optimization process into the verification procedure, achieving better performance than the naive approach.
  arXiv  Detail & Related papers  (2020-10-07T08:19:48Z)
• Exact posterior distributions of wide Bayesian neural networks [51.20413322972014]
  We show that the exact BNN posterior converges (weakly) to the one induced by the GP limit of the prior. For empirical validation, we show how to generate exact samples from a finite BNN on a small dataset via rejection sampling.
  arXiv  Detail & Related papers  (2020-06-18T13:57:04Z)

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.