Mining Verdict Boundaries for Neural Network Verification

• URL: http://arxiv.org/abs/2607.28954v1
• Date: Fri, 31 Jul 2026 02:16:55 GMT
• Title: Mining Verdict Boundaries for Neural Network Verification
• Abstract summary: 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.
• Score: 10.091802208162585
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Branch and Bound (BaB) aims to achieve complete verification of neural networks by adaptively partitioning the problem and applying off-the-shelf verifiers to subproblems. Its problem-splitting history can be represented as a tree, where each subproblem corresponds to a child node. A key problem of BaB lies in searching for the verdict boundaries across all the paths that divide the verified and unverified subproblems. We observe that the existing BaB approach tackles this problem by solving each expensive subproblem sequentially along the tree path as its depth increases, requiring costly bounds propagation at every visited BaB tree node (i.e., subproblem), which is inefficient. To address this issue, we propose effective search approaches that leverage the monotonicity of each path to efficiently and precisely locate the verdict boundary by simultaneously splitting multiple activation functions (e.g., ReLU), rather than processing them one at a time as in the classical approach. Our approach performs an effective exponential search along each path, allowing us to skip many boundary-unrelated subproblems when identifying the verdict boundary. The enhanced version further improves this process by estimating the boundary's position using quantitative information obtained from subproblem solving. We perform experimental evaluation on commonly-used benchmarks to assess our proposed techniques, and compare them with recent BaB-based approaches.

Related papers

• How Many Trees in a Random Forest? A Revisited Approach with Plateau Search and Optuna Integration [0.30586855806896046]
  We propose an integrated triplet-based plateau-search algorithm for HPO for Random Forest.<n>The method adaptively tracks a near-minimal sufficient ensemble size by monitoring relative changes in the out-of-bag score.<n>Experiments show that the selected number of trees can differ substantially from the common absolute.
  arXiv  Detail & Related papers  (2026-06-02T12:10:43Z)
• 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)
• 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)
• 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)
• Training Greedy Policy for Proposal Batch Selection in Expensive Multi-Objective Combinatorial Optimization [52.80408805368928]
  We introduce a novel greedy-style subset selection algorithm for batch acquisition. Our experiments on the red fluorescent proteins show that our proposed method achieves the baseline performance in 1.69x fewer queries.
  arXiv  Detail & Related papers  (2024-06-21T05:57:08Z)
• Optimizing Solution-Samplers for Combinatorial Problems: The Landscape of Policy-Gradient Methods [52.0617030129699]
  We introduce a novel theoretical framework for analyzing the effectiveness of DeepMatching Networks and Reinforcement Learning methods. Our main contribution holds for a broad class of problems including Max-and Min-Cut, Max-$k$-Bipartite-Bi, Maximum-Weight-Bipartite-Bi, and Traveling Salesman Problem. As a byproduct of our analysis we introduce a novel regularization process over vanilla descent and provide theoretical and experimental evidence that it helps address vanishing-gradient issues and escape bad stationary points.
  arXiv  Detail & Related papers  (2023-10-08T23:39:38Z)
• Decision Diagram-Based Branch-and-Bound with Caching for Dominance and Suboptimality Detection [9.175779296469194]
  This paper presents new ingredients to speed up the search by exploiting the structure of dynamic programming models. The key idea is to prevent the repeated expansion of nodes corresponding to the same dynamic programming states by querying expansion thresholds cached throughout the search. Experiments show that the pruning brought by this caching mechanism allows significantly reducing the number of nodes expanded by the algorithm.
  arXiv  Detail & Related papers  (2022-11-22T10:18:33Z)
• Quant-BnB: A Scalable Branch-and-Bound Method for Optimal Decision Trees with Continuous Features [5.663538370244174]
  We present a new discrete optimization method based on branch-and-bound (BnB) to obtain optimal decision trees. Our proposed algorithm Quant-BnB shows significant speedups compared to existing approaches for shallow optimal trees on various real datasets.
  arXiv  Detail & Related papers  (2022-06-23T17:19:29Z)
• Frequent Itemset-driven Search for Finding Minimum Node Separators in Complex Networks [61.2383572324176]
  We propose a frequent itemset-driven search approach, which integrates the concept of frequent itemset mining in data mining into the well-known memetic search framework. It iteratively employs the frequent itemset recombination operator to generate promising offspring solution based on itemsets that frequently occur in high-quality solutions. In particular, it discovers 29 new upper bounds and matches 18 previous best-known bounds.
  arXiv  Detail & Related papers  (2022-01-18T11:16:40Z)
• Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition [161.09660864941603]
  We improve the scalability of Branch and Bound (BaB) algorithms for formally proving input-output properties of neural networks. We present a novel activation-based branching strategy and a BaB framework, named Branch and Dual Network Bound (BaDNB) BaDNB outperforms previous complete verification systems by a large margin, cutting average verification times by factors up to 50 on adversarial properties.
  arXiv  Detail & Related papers  (2021-04-14T09:22:42Z)
• Batched Neural Bandits [107.5072688105936]
  BatchNeuralUCB combines neural networks with optimism to address the exploration-exploitation tradeoff. We prove that BatchNeuralUCB achieves the same regret as the fully sequential version while reducing the number of policy updates considerably.
  arXiv  Detail & Related papers  (2021-02-25T17:36:44Z)
• Solving Sparse Linear Inverse Problems in Communication Systems: A Deep Learning Approach With Adaptive Depth [51.40441097625201]
  We propose an end-to-end trainable deep learning architecture for sparse signal recovery problems. The proposed method learns how many layers to execute to emit an output, and the network depth is dynamically adjusted for each task in the inference phase.
  arXiv  Detail & Related papers  (2020-10-29T06:32:53Z)

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.