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

arXiv: https://arxiv.org/abs/2509.25647 · HTML: https://mlsanity.com/paper/2509.25647/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 15 of its 20 references that are in the map.
- First posted on arXiv 30 Sep 2025.

## Builds on (most cited first, 15 of 15)

- [Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks](https://mlsanity.com/paper/1702.01135/) (2017)
- [Efficient Neural Network Robustness Certification with General Activation Functions](https://mlsanity.com/paper/1811.00866/) (2018)
- [Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Complete and Incomplete Neural Network Robustness Verification](https://mlsanity.com/paper/2103.06624/) (2021)
- [Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers](https://mlsanity.com/paper/2011.13824/) (2020)
- [Efficient Formal Safety Analysis of Neural Networks](https://mlsanity.com/paper/1809.08098/) (2018)
- [Branch and Bound for Piecewise Linear Neural Network Verification](https://mlsanity.com/paper/1909.06588/) (2019)
- [General Cutting Planes for Bound-Propagation-Based Neural Network Verification](https://mlsanity.com/paper/2208.05740/) (2022)
- [Robustness of Neural Networks: A Probabilistic and Practical Approach](https://mlsanity.com/paper/1902.05983/) (2019)
- [CC-Cert: A Probabilistic Approach to Certify General Robustness of Neural Networks](https://mlsanity.com/paper/2109.10696/) (2021)
- [Enumerating Safe Regions in Deep Neural Networks with Provable Probabilistic Guarantees](https://mlsanity.com/paper/2308.09842/) (2023)
- [Probabilistic Verification and Reachability Analysis of Neural Networks via Semidefinite Programming](https://mlsanity.com/paper/1910.04249/) (2019)
- [Data-Driven Certification of Neural Networks with Random Input Noise](https://mlsanity.com/paper/2010.01171/) (2020)
- [Probabilistic Verification of ReLU Neural Networks via Characteristic Functions](https://mlsanity.com/paper/2212.01544/) (2022)
- [Solving Probabilistic Verification Problems of Neural Networks using Branch and Bound](https://mlsanity.com/paper/2405.17556/) (2024)
- [SAVER: A Toolbox for Sampling-Based, Probabilistic Verification of Neural Networks](https://mlsanity.com/paper/2412.02940/) (2024)

## Abstract (arXiv)

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.