BaB-prob: Branch and Bound with Preactivation Splitting for Probabilistic Verification of Neural Networks
This addresses the problem of verifying neural network reliability under uncertainty for safety-critical applications, representing an incremental extension of existing deterministic methods.
The paper tackles probabilistic verification of neural networks by extending branch-and-bound with preactivation splitting to this setting, proving soundness and completeness for feedforward-ReLU networks. The proposed BaB-prob method outperforms state-of-the-art approaches in medium- to high-dimensional input problems across untrained networks, MNIST and CIFAR-10 models, and VNN-COMP 2025 benchmarks.
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.