Branch and Bound for Relational Verification of Neural Networks

• URL: http://arxiv.org/abs/2608.13118v1
• Date: Thu, 13 Aug 2026 11:47:46 GMT
• Title: Branch and Bound for Relational Verification of Neural Networks
• Abstract summary: Verification of neural networks against relational specifications, such as global robustness, is crucial for safety-critical applications of cyber-physical systems.<n>We propose a branch-and-bound (BaB) framework to mitigate the issue, which iteratively splits the problem until all sub-problems are verified.<n>We evaluate SaBRe on 817 verification problems across ACAS Xu, MNIST-F, MNIST-C, CIFAR and GTSRB.
• Score: 2.593237301046536
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Verification of neural networks against relational specifications, such as global robustness, is crucial for safety-critical applications of cyber-physical systems (CPS), given their increasing adoption of AI components. Compared to simple trace properties (e.g., local robustness), verifying relational specifications requires reasoning about the relationship between multiple network inferences, which brings significant technical challenges. Existing research has explored abstraction techniques based on sound and convex over-approximation of neural network outputs; however, since these approaches are inherently incomplete and may raise false alarms, they further underscore the need of effective abstraction refinement. In this paper, we propose a branch-and-bound (BaB) framework to mitigate the issue, which iteratively splits the problem until all sub-problems are verified. Specifically, our BaB framework features splitting of relational neurons rather than individual neurons as prior works do, and as the core of our technique, we devise a relational neuron selection strategy based on the dual formulation of the verification problem, which allows us to efficiently select the (most likely) optimal relational neuron that maximizes the refinement brought by problem splitting. We evaluate SaBRe on 817 verification problems across ACAS Xu, MNIST-F, MNIST-C, CIFAR and GTSRB. The results show that SaBRe outperforms different baseline approaches, in terms of the number of solved instances and verification efficiency, which demonstrates the effectiveness of our proposed techniques.

Related papers

• Constraints Matrix Diffusion based Generative Neural Solver for Vehicle Routing Problems [16.541111954252397]
  We propose a novel fusion neural network framework that employs a discrete noise graph diffusion model to learn the underlying constraints of vehicle routing problems.<n>This work represents the first comprehensive experimental investigation of neural network model solvers across a 378-combinatorial space.
  arXiv  Detail & Related papers  (2026-03-08T10:03:34Z)
• Verification of Bit-Flip Attacks against Quantized Neural Networks [14.673682037450321]
  We introduce BFAVerifier, the first verification framework designed to formally verify the absence of bit-flip attacks.<n> BFAVerifier comprises two integral components: an abstraction-based method and an MILP-based method.
  arXiv  Detail & Related papers  (2025-02-22T16:35:38Z)
• Implicit Generative Prior for Bayesian Neural Networks [8.013264410621357]
  We propose a novel neural adaptive empirical Bayes (NA-EB) framework for complex data structures. The proposed NA-EB framework combines variational inference with a gradient ascent algorithm. We demonstrate the practical applications of our framework through extensive evaluations on a variety of tasks.
  arXiv  Detail & Related papers  (2024-04-27T21:00:38Z)
• Zonotope Domains for Lagrangian Neural Network Verification [102.13346781220383]
  We decompose the problem of verifying a deep neural network into the verification of many 2-layer neural networks. Our technique yields bounds that improve upon both linear programming and Lagrangian-based verification techniques.
  arXiv  Detail & Related papers  (2022-10-14T19:31:39Z)
• Knowledge Enhanced Neural Networks for relational domains [83.9217787335878]
  We focus on a specific method, KENN, a Neural-Symbolic architecture that injects prior logical knowledge into a neural network. In this paper, we propose an extension of KENN for relational data.
  arXiv  Detail & Related papers  (2022-05-31T13:00:34Z)
• Generalization of Neural Combinatorial Solvers Through the Lens of Adversarial Robustness [68.97830259849086]
  Most datasets only capture a simpler subproblem and likely suffer from spurious features. We study adversarial robustness - a local generalization property - to reveal hard, model-specific instances and spurious features. Unlike in other applications, where perturbation models are designed around subjective notions of imperceptibility, our perturbation models are efficient and sound. Surprisingly, with such perturbations, a sufficiently expressive neural solver does not suffer from the limitations of the accuracy-robustness trade-off common in supervised learning.
  arXiv  Detail & Related papers  (2021-10-21T07:28:11Z)
• 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)
• Online neural connectivity estimation with ensemble stimulation [5.156484100374058]
  We propose a method based on noisy group testing that drastically increases the efficiency of this process in sparse networks. We show that it is possible to recover binarized network connectivity with a number of tests that grows only logarithmically with population size. We also demonstrate the feasibility of inferring connectivity for networks of up to tens of thousands of neurons online.
  arXiv  Detail & Related papers  (2020-07-27T23:47:03Z)
• Parallelization Techniques for Verifying Neural Networks [52.917845265248744]
  We introduce an algorithm based on the verification problem in an iterative manner and explore two partitioning strategies. We also introduce a highly parallelizable pre-processing algorithm that uses the neuron activation phases to simplify the neural network verification problems.
  arXiv  Detail & Related papers  (2020-04-17T20:21:47Z)
• Branch and Bound for Piecewise Linear Neural Network Verification [46.49816596173425]
  We propose a family of algorithms based on Branch-and-Bound (BaB)<n>We identify new methods that combine the strengths of multiple existing approaches.<n>We introduce an effective branching strategy on ReLU non-linearities.
  arXiv  Detail & Related papers  (2019-09-14T12:44:35Z)

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.