Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees

• URL: http://arxiv.org/abs/2507.17453v1
• Date: Wed, 23 Jul 2025 12:20:20 GMT
• Title: Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees
• Abstract summary: 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.
• Score: 8.804277530769532
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The vulnerability of neural networks to adversarial perturbations has necessitated formal verification techniques that can rigorously certify the quality of neural networks. As the 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. While BaB can identify the sub-problems that are necessary to be split, it explores the space of these sub-problems in a naive "first-come-first-serve" manner, thereby suffering from an issue of inefficiency to reach a verification conclusion. To bridge this gap, we introduce an order over different sub-problems produced by BaB, concerning with their different likelihoods of containing counterexamples. Based on this order, 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, in order to efficiently reach the conclusion of the verification. Even if no counterexample can be found in any sub-problem, it only changes the order of visiting different sub-problem and so will not lead to a performance degradation. Specifically, Oliva has two variants, including $Oliva^{GR}$, a greedy strategy that always prioritizes the sub-problems that are more likely to find counterexamples, and $Oliva^{SA}$, a balanced strategy inspired by simulated annealing that gradually shifts from exploration to exploitation to locate the globally optimal sub-problems. We experimentally evaluate the performance of Oliva on 690 verification problems spanning over 5 models with datasets MNIST and CIFAR10. Compared to the state-of-the-art approaches, we demonstrate the speedup of Oliva for up to 25X in MNIST, and up to 80X in CIFAR10.

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)
• Locally Confident, Globally Stuck: The Quality-Exploration Dilemma in Diffusion Language Models [52.61023005303122]
  We show that low-confidence remasking improves a proxy for quality while constraining the entropy of the induced sequence distribution.<n>We develop a simple Independent--Hastings sampler that approximately targets this distribution during decoding.
  arXiv  Detail & Related papers  (2026-04-01T02:01:30Z)
• A First Proof Sprint [0.0]
  This monograph reports a multi-agent proof sprint on ten research-level problems.<n>Problem3 has a validation-complete existence path under the scoped criterion used here.<n>Problem5 is solved in a scope-limited form for $F_O$-local connective spectra.<n>Problem6 is partial with named remaining obligations in the general case.<n>Problem7 and9 have node-level validation artifacts but still contain unresolved verifier gaps.
  arXiv  Detail & Related papers  (2026-02-14T04:09:30Z)
• 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)
• BaB-prob: Branch and Bound with Preactivation Splitting for Probabilistic Verification of Neural Networks [13.26751081683149]
  Branch-and-bound with preactivation splitting has been shown highly effective for deterministic verification of neural networks.<n>We propose BaB-prob that iteratively divides the original problem into subproblems by splitting preactivations.<n>We prove soundness and completeness of BaB-prob for feedforward-ReLU neural networks.
  arXiv  Detail & Related papers  (2025-09-30T01:39:39Z)
• Adaptive Branch-and-Bound Tree Exploration for Neural Network Verification [8.733719614108102]
  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.
  arXiv  Detail & Related papers  (2025-05-02T02:41:02Z)
• Identifying General Mechanism Shifts in Linear Causal Representations [58.6238439611389]
  We consider the linear causal representation learning setting where we observe a linear mixing of $d$ unknown latent factors. Recent work has shown that it is possible to recover the latent factors as well as the underlying structural causal model over them. We provide a surprising identifiability result that it is indeed possible, under some very mild standard assumptions, to identify the set of shifted nodes.
  arXiv  Detail & Related papers  (2024-10-31T15:56:50Z)
• Distributed Extra-gradient with Optimal Complexity and Communication Guarantees [60.571030754252824]
  We consider monotone variational inequality (VI) problems in multi-GPU settings where multiple processors/workers/clients have access to local dual vectors. Extra-gradient, which is a de facto algorithm for monotone VI problems, has not been designed to be communication-efficient. We propose a quantized generalized extra-gradient (Q-GenX), which is an unbiased and adaptive compression method tailored to solve VIs.
  arXiv  Detail & Related papers  (2023-08-17T21:15:04Z)
• Towards understanding neural collapse in supervised contrastive learning with the information bottleneck method [26.874007846077884]
  Neural collapse describes the geometry of activation in the final layer of a deep neural network when it is trained beyond performance plateaus. We demonstrate that neural collapse leads to good generalization specifically when it approaches an optimal IB solution of the classification problem.
  arXiv  Detail & Related papers  (2023-05-19T18:41:17Z)
• Latent Feature Relation Consistency for Adversarial Robustness [80.24334635105829]
  misclassification will occur when deep neural networks predict adversarial examples which add human-imperceptible adversarial noise to natural examples. We propose textbfLatent textbfFeature textbfRelation textbfConsistency (textbfLFRC) LFRC constrains the relation of adversarial examples in latent space to be consistent with the natural examples.
  arXiv  Detail & Related papers  (2023-03-29T13:50:01Z)
• Distributionally Robust Bayesian Optimization with $\varphi$-divergences [45.48814080654241]
  We consider robustness against data-shift in $varphi$-divergences, which subsumes many popular choices, such as the Total Variation, and the extant Kullback-Leibler divergence. We show that the DRO-BO problem in this setting is equivalent to a finite-dimensional optimization problem which, even in the continuous context setting, can be easily implemented with provable sublinear regret bounds.
  arXiv  Detail & Related papers  (2022-03-04T04:34:52Z)
• Deep Hierarchy in Bandits [51.22833900944146]
  Mean rewards of actions are often correlated. To maximize statistical efficiency, it is important to leverage these correlations when learning. We formulate a bandit variant of this problem where the correlations of mean action rewards are represented by a hierarchical Bayesian model.
  arXiv  Detail & Related papers  (2022-02-03T08:15:53Z)
• Mapping conditional distributions for domain adaptation under generalized target shift [0.0]
  We consider the problem of unsupervised domain adaptation (UDA) between a source and a target domain under conditional and label shift a.k.a Generalized Target Shift (GeTarS) Recent approaches learn domain-invariant representations, yet they have practical limitations and rely on strong assumptions that may not hold in practice. In this paper, we explore a novel and general approach to align pretrained representations, which circumvents existing drawbacks.
  arXiv  Detail & Related papers  (2021-10-26T14:25: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)
• Continuous Profit Maximization: A Study of Unconstrained Dr-submodular Maximization [4.649999862713523]
  We form continuous profit (CPM-MS) problem, whose domain is on integer lattices. We introduce lattice-based double greedy algorithm, which can obtain a constant approximation. We propose a technique, called lattice-based iterative pruning. It can shrink the search space effectively.
  arXiv  Detail & Related papers  (2020-04-12T05:35:19Z)
• The Simulator: Understanding Adaptive Sampling in the Moderate-Confidence Regime [52.38455827779212]
  We propose a novel technique for analyzing adaptive sampling called the em Simulator. We prove the first instance-based lower bounds the top-k problem which incorporate the appropriate log-factors. Our new analysis inspires a simple and near-optimal for the best-arm and top-k identification, the first em practical of its kind for the latter problem.
  arXiv  Detail & Related papers  (2017-02-16T23:42:02Z)

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.