Research map / Learning theory and algorithms / Combinatorial and search optimization
Solving Probabilistic Verification Problems of Neural Networks using Branch and Bound
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes ProbBounds, a massively parallel input-splitting branch-and-bound method that iteratively tightens sound lower/upper bounds on probabilities of neural network output events, enabling sound probabilistic verification (ToolName: probabilistic branch and bound).
Problem
Probabilistic verification of neural networks: proving statements about the output distribution of a neural network under an input probability distribution, such as demographic parity, safety violation rates, and #DNN verification, soundly and efficiently.
Approach
Compute and iteratively refine lower and upper bounds on probabilities of satisfaction events by applying non-probabilistic branch-and-bound techniques (linear bound propagation with CROWN/interval arithmetic, BaBSB and longest-edge splitting) to hyperrectangular partitions, pruning branches whose satisfaction is certain and summing their probability masses.
Key results
- On the FairSquare benchmark, the method solves four more instances than FairSquare within the 15-minute timeout; median runtime 4s vs 44s for FairSquare on commonly solved instances.
- On ACAS Xu robustness (125 instances), mean runtime is 22 seconds versus 33 minutes reported for SpaceScanner.
- On MiniACSIncome, seven of eight instances are solved within one hour, with the largest (eight inputs) timing out.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| use the probabilistic verifier instead of FairSquare | FairSquare benchmark · FairSquare benchmark instances solved by both tools | median runtime: 44s -> 4s | Helped |
| use the probabilistic verifier instead of FairSquare | FairSquare benchmark · FairSquare benchmark instances solved by both tools | mean runtime: 109s -> 5s | Helped |
| use the probabilistic verifier instead of SpaceScanner | ACAS Xu N1,1 robustness · 125 ACAS Xu robustness instances | mean runtime per instance: 33 minutes -> 22 seconds | Helped |
| use the probabilistic verifier instead of PreimgApprox | VCAS correctness verification · VCAS correctness | runtime: 16.42s -> 0.13s | Helped |
| use ProbBounds rather than ProVeSLR | ACAS Xu safety verification · ACAS Xu safety networks | runtime to obtain violation-rate bounds: at least four hours; within one hour | Helped |
| use ProbBounds rather than eProVe | ACAS Xu safety verification · two of three ACAS Xu safety networks | time to obtain tighter sound bounds: within 10 seconds; at least 57 seconds | Helped |
| apply the probabilistic verifier to MiniACSIncome | MiniACSIncome verification · MiniACSIncome | instances solved within one hour: seven of eight | Helped |
| use the probabilistic verifier rather than enumeration as input size grows beyond one-batch evaluation capacity | MiniACSIncome shallow 10-neuron networks · MiniACSIncome | runtime | Helped |
Surprising findings
- Runtime is largely unaffected by network size on MiniACSIncome, attributed to large and small networks learning similar decision boundaries.
- Enumeration baseline is faster than the method when the network can be evaluated on all discrete inputs in one batch.
Limitations
- Requires input spaces to be hyperrectangles and input distributions to allow exact computation of hyperrectangle probabilities in closed form or via terminating algorithms.
- Completeness does not hold for the BaBSB heuristic alone; only the BaBSB-LongestEdge variant is proven complete.
- Completeness requires a mild assumption that the satisfaction function is nonzero and that the satisfaction boundary has zero probability mass.
Experimental setup
Datasets: ACSIncome Adult ACAS Xu property specifications VCAS
Benchmarks: FairSquare benchmark ACAS Xu safety ACAS Xu robustness VCAS correctness MiniACSIncome
Metrics: runtime solved instances lower and upper probability bounds
Baselines: FairSquare SpaceScanner ProVeS-LR eProVe PreimgApprox Enumeration
Builds on: CROWN BaBSB auto_LiRPA FairSquare alpha-beta-CROWN
Closest papers by meaning
- Dynamic Algorithm Termination for Branch-and-Bound-based Neural Network Verification (AAAI 2025 · similarity 0.85)
- Probabilistic Neural Circuits (AAAI 2024 · similarity 0.85)
- On the Hardness of Probabilistic Neurosymbolic Learning (ICML 2024 · similarity 0.85)
- Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes (NeurIPS 2024 · similarity 0.85)
- Certified but Private: Scalable Zero-Knowledge Proofs for the Formal Verification of Neural Networks (NeurIPS 2026 · similarity 0.84)
- Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification (NeurIPS 2025 · similarity 0.84)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.