BaB-prob: Branch and Bound with Preactivation Splitting for Probabilistic Verification of Neural Networks

• URL: http://arxiv.org/abs/2509.25647v1
• Date: Tue, 30 Sep 2025 01:39:39 GMT
• Title: BaB-prob: Branch and Bound with Preactivation Splitting for Probabilistic Verification of Neural Networks
• Authors: Fangji Wang, Panagiotis Tsiotras,
• Abstract summary: 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.
• Score: 13.26751081683149
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Branch-and-bound with preactivation splitting has been shown highly effective for deterministic verification of neural networks. In this paper, we extend this framework to the probabilistic setting. We propose BaB-prob that iteratively divides the original problem into subproblems by splitting preactivations and leverages linear bounds computed by linear bound propagation to bound the probability for each subproblem. We prove soundness and completeness of BaB-prob for feedforward-ReLU neural networks. Furthermore, we introduce the notion of uncertainty level and design two efficient strategies for preactivation splitting, yielding BaB-prob-ordered and BaB+BaBSR-prob. We evaluate BaB-prob on untrained networks, MNIST and CIFAR-10 models, respectively, and VNN-COMP 2025 benchmarks. Across these settings, our approach consistently outperforms state-of-the-art approaches in medium- to high-dimensional input problems.

Related papers

• Richer Bayesian Last Layers with Subsampled NTK Features [25.566044416945875]
  Bayesian Last Layers (BLLs) provide a convenient and computationally efficient way to estimate uncertainty in neural networks.<n>We propose a method that improves BLLs by leveraging a projection of Neural Tangent Kernel (NTK) features onto the space spanned by the last-layer features.<n>This enables posterior inference that accounts for variability of the full network while retaining the low computational cost of inference of a standard BLL.
  arXiv  Detail & Related papers  (2026-02-01T15:24:20Z)
• BAPE: Learning an Explicit Bayes Classifier for Long-tailed Visual Recognition [78.70453964041718]
  Current deep learning algorithms usually solve for the optimal classifier by emphimplicitly estimating the posterior probabilities.<n>This simple methodology has been proven effective for meticulously balanced academic benchmark datasets.<n>However, it is not applicable to the long-tailed data distributions in the real world.<n>This paper presents a novel approach (BAPE) that provides a more precise theoretical estimation of the data distributions.
  arXiv  Detail & Related papers  (2025-06-29T15:12:50Z)
• Last Layer Empirical Bayes [24.94944362766761]
  Bayesian neural networks (BNNs) and deep ensembles are among the most prominent approaches to tackle this task.<n>Inspired by recent work showing that the distribution used by ensembles can be understood as a posterior corresponding to a learned data-dependent prior, we propose last layer empirical Bayes (LLEB)<n>LLEB performs on par with existing approaches, highlighting that empirical Bayes is a promising direction for future research in uncertainty quantification.
  arXiv  Detail & Related papers  (2025-05-21T18:00:00Z)
• Neural Network Verification with Branch-and-Bound for General Nonlinearities [63.39918329535165]
  Branch-and-bound (BaB) is among the most effective techniques for neural network (NN) verification.<n>We develop a general framework, named GenBaB, to conduct BaB on general nonlinearities to verify NNs with general architectures.<n>Our framework also allows the verification of general nonlinear graphs and enables verification applications beyond simple NNs.
  arXiv  Detail & Related papers  (2024-05-31T17:51:07Z)
• Credal Wrapper of Model Averaging for Uncertainty Estimation in Classification [5.19656787424626]
  This paper presents an innovative approach, called credal wrapper, to formulating a credal set representation of model averaging for Bayesian neural networks (BNNs) and deep ensembles (DEs)<n>Given a finite collection of single predictive distributions derived from BNNs or DEs, the proposed credal wrapper approach extracts an upper and a lower probability bound per class.<n>Compared to the BNN and DE baselines, the proposed credal wrapper method exhibits superior performance in uncertainty estimation and achieves a lower expected calibration error on corrupted data.
  arXiv  Detail & Related papers  (2024-05-23T20:51:22Z)
• Bayesian Cramér-Rao Bound Estimation with Score-Based Models [3.4480437706804503]
  The Bayesian Cram'er-Rao bound (CRB) provides a lower bound on the mean square error of any Bayesian estimator under mild regularity conditions. This work introduces a new data-driven estimator for the CRB using score matching.
  arXiv  Detail & Related papers  (2023-09-28T00:22:21Z)
• The Cascaded Forward Algorithm for Neural Network Training [61.06444586991505]
  We propose a new learning framework for neural networks, namely Cascaded Forward (CaFo) algorithm, which does not rely on BP optimization as that in FF. Unlike FF, our framework directly outputs label distributions at each cascaded block, which does not require generation of additional negative samples. In our framework each block can be trained independently, so it can be easily deployed into parallel acceleration systems.
  arXiv  Detail & Related papers  (2023-03-17T02:01:11Z)
• Semantic Strengthening of Neuro-Symbolic Learning [85.6195120593625]
  Neuro-symbolic approaches typically resort to fuzzy approximations of a probabilistic objective. We show how to compute this efficiently for tractable circuits. We test our approach on three tasks: predicting a minimum-cost path in Warcraft, predicting a minimum-cost perfect matching, and solving Sudoku puzzles.
  arXiv  Detail & Related papers  (2023-02-28T00:04:22Z)
• Improved uncertainty quantification for neural networks with Bayesian last layer [0.0]
  Uncertainty quantification is an important task in machine learning. We present a reformulation of the log-marginal likelihood of a NN with BLL which allows for efficient training using backpropagation.
  arXiv  Detail & Related papers  (2023-02-21T20:23:56Z)
• On the Convergence of Certified Robust Training with Interval Bound Propagation [147.77638840942447]
  We present a theoretical analysis on the convergence of IBP training. We show that when using IBP training to train a randomly two-layer ReLU neural network with logistic loss, gradient descent can linearly converge to zero robust training error.
  arXiv  Detail & Related papers  (2022-03-16T21:49:13Z)
• PAC-Bayesian Learning of Aggregated Binary Activated Neural Networks with Probabilities over Representations [2.047424180164312]
  We study the expectation of a probabilistic neural network as a predictor by itself, focusing on the aggregation of binary activated neural networks with normal distributions over real-valued weights. We show that the exact computation remains tractable for deep but narrow neural networks, thanks to a dynamic programming approach.
  arXiv  Detail & Related papers  (2021-10-28T14:11:07Z)
• Certification of Iterative Predictions in Bayesian Neural Networks [79.15007746660211]
  We compute lower bounds for the probability that trajectories of the BNN model reach a given set of states while avoiding a set of unsafe states. We use the lower bounds in the context of control and reinforcement learning to provide safety certification for given control policies.
  arXiv  Detail & Related papers  (2021-05-21T05:23:57Z)
• 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)

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.