Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Fangji Wang, Panagiotis Tsiotras

TL;DR

The paper addresses probabilistic verification of neural networks under input distributions and introduces BaB-prob, a branch-and-bound method that uses preactivation splitting and LiRPA-based bounds to certify $\mathbb{P}(f(\mathbf{X})>0) \ge \eta$ for feedforward-ReLU nets. It proves soundness and completeness for ReLU networks, and introduces the concept of uncertainty level with two strategies, BaB-prob-ordered and BaB+BaBSR-prob, to efficiently select preactivations to split. Through extensive experiments on untrained and trained MLP/CNN models, MNIST, CIFAR-10, and VNN-COMP 2025 benchmarks, BaB-prob variants consistently outperform state-of-the-art probabilistic verifiers in medium- to high-dimensional settings, with high statistical confidence in the estimates. The approach offers a scalable, rigorous framework for probabilistic neural network verification with practical impact on safety-critical applications.

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.

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

TL;DR

The paper addresses probabilistic verification of neural networks under input distributions and introduces BaB-prob, a branch-and-bound method that uses preactivation splitting and LiRPA-based bounds to certify for feedforward-ReLU nets. It proves soundness and completeness for ReLU networks, and introduces the concept of uncertainty level with two strategies, BaB-prob-ordered and BaB+BaBSR-prob, to efficiently select preactivations to split. Through extensive experiments on untrained and trained MLP/CNN models, MNIST, CIFAR-10, and VNN-COMP 2025 benchmarks, BaB-prob variants consistently outperform state-of-the-art probabilistic verifiers in medium- to high-dimensional settings, with high statistical confidence in the estimates. The approach offers a scalable, rigorous framework for probabilistic neural network verification with practical impact on safety-critical applications.

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.

Paper Structure

This paper contains 21 sections, 8 theorems, 45 equations, 4 figures, 3 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Notation
  4. Linear Bound Propagation for Deterministic Verification
  5. BaB-prob
  6. Overall Framework
  7. Probability Bounds for Branches
  8. Splitting Strategies
  9. Theoretical Results
  10. Experiments
  11. Untrained MLP and CNN models
  12. MNIST and CIFAR-10 models
  13. Results for VNN-COMP 2025 models
  14. Conclusions
  15. Detailed Framework of BaB-prob
  16. ...and 6 more sections

Key Result

Proposition 1

The values of $p_\ell$ and $p_u$ computed in Equation (eq:compute_branch_prob_bounds) are lower and upper bounds on $\mathbb{P} \left(f(\mathbf{X}\xspace)>0,\,\mathcal{C}\xspace\right)$.

Figures (4)

  • Figure 1: An illustrative example of the key idea behind BaB-prob. Two preactivations have negative lower bounds and positive upper bounds. BaB-prob iteratively splits them into negative and nonnegative cases to tighten the global probability bound, until the original problem is verified.
  • Figure 2: Success rate results for untrained models.
  • Figure 3: Comparison of number of splits between BaB-prob-ordered and BaB+BaBSR-prob.
  • Figure 4: ECDF of confidence for BaB-prob-ordered and BaB+BaBSR-prob.

Theorems & Definitions (16)

  • Proposition 1
  • Proposition 2
  • Proposition 3
  • Proposition 4
  • Proposition 5
  • Corollary 1
  • Lemma 1
  • proof
  • proof : Proof of Proposition \ref{['prop:branch_prob_bounds']}
  • proof : Proof of Proposition \ref{['prop:branch_prob_gap']}
  • ...and 6 more