BaB-prob: Branch and Bound with Preactivation Splitting for Probabilistic Verification of Neural Networks
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Probabilistic Verification of Neural Networks using Branch and Bound
Probabilistic verification of neural networks is concerned with formally analysing the output distribution of a neural network under a probability distribution of the inputs. Examples of probabilistic verification includ…
FairnessTreeDQN: Learning to minimize Branch-and-Bound tree
Combinatorial optimization problems require an exhaustive search to find the optimal solution. A convenient approach to solving combinatorial optimization tasks in the form of Mixed Integer Linear Programs is Branch-and-…
Combinatorial Optimizationreinforcement-learningReinforcement LearningVariable SelectionOptimized Symbolic Interval Propagation for Neural Network Verification
Neural networks are increasingly applied in safety critical domains, their verification thus is gaining importance. A large class of recent algorithms for proving input-output relations of feed-forward neural networks ar…
Collision AvoidanceBilateral Network with Channel Splitting Network and Transformer for Thermal Image Super-Resolution
In recent years, the Thermal Image Super-Resolution (TISR) problem has become an attractive research topic. TISR would been used in a wide range of fields, including military, medical, agricultural and animal ecology. Du…
Image Super-ResolutionSSIMSuper-ResolutionBranch and Bound for Relational Verification of Neural Networks
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.…