Branch-and-Bound Verification¶
Complete verification methods like SMT and MILP provide definitive answers but struggle with large networks. Incomplete methods like bound propagation scale beautifully but sometimes return “unknown.” What if you could combine both—using incomplete methods for speed and complete methods for precision exactly where needed?
Branch-and-bound verification does exactly this: it partitions the input space into smaller regions, uses fast incomplete methods to verify each region, and refines (branches) only on regions where bounds are too loose. This hybrid approach achieves near-complete verification with much better scalability than pure complete methods.
This guide explores how branch-and-bound works for neural network verification, why it’s become the state-of-the-art for many benchmarks, and how to use it effectively.
The Core Idea: Divide and Conquer¶
Verification asks: does a property hold for all inputs in a region? When the region is large, incomplete methods return loose bounds—too conservative to verify. But if you partition the region into smaller pieces, bounds get tighter.
Key insight: Incomplete verification [Gowal et al., 2019, Singh et al., 2019, Weng et al., 2018, Zhang et al., 2018] works much better on small input regions than large ones. Approximation error accumulates less when the input region is tight.
Branch-and-Bound Strategy
Try incomplete verification on the full region
If verified: Done—the property holds
If falsified: Found counterexample—property violated
If unknown: Bounds are too loose
Branch: Split the region into smaller subregions
Bound: Verify each subregion with incomplete methods
Repeat: Refine further if needed
Continue until all regions are verified, a counterexample is found, or computational budget is exhausted.
This is complete verification (eventually tries all possible input combinations) achieved through incremental refinement rather than upfront enumeration.
Mathematical Formulation¶
Verification problem: Determine if property \(\phi\) holds for all \(x \in \mathcal{X}\):
Incomplete verification computes bounds on \(f(x)\) for \(x \in \mathcal{X}\):
If these bounds satisfy the property (e.g., \(\underline{y}_{y_0} > \max_{c \neq y_0} \overline{y}_c\)), verification succeeds. If they violate it, verification fails. Otherwise, unknown.
Branch-and-bound partitions \(\mathcal{X}\) into subregions \(\mathcal{X}_1, \ldots, \mathcal{X}_k\) where \(\mathcal{X} = \bigcup_i \mathcal{X}_i\):
Verify each \(\mathcal{X}_i\) separately. If all verify, the full region is verified. If any region is falsified, the full verification fails.
Branching Strategies¶
How you partition the input space dramatically affects efficiency.
Input Space Branching¶
Idea: Split the input region \(\mathcal{X}\) directly.
For an \(\ell_\infty\) ball \(\mathcal{B}_\epsilon(x_0) = \{x : \|x - x_0\|_\infty \leq \epsilon\}\):
Dimension selection: Choose a dimension \(i\) to split
Split: Create \(\mathcal{X}_1 = \{x \in \mathcal{X} : x_i \leq (x_0)_i\}\) and \(\mathcal{X}_2 = \{x \in \mathcal{X} : x_i > (x_0)_i\}\)
Recurse: Verify each subregion
Dimension selection heuristics:
Largest interval: Split dimension with widest bound
Gradient-based: Split dimension with largest gradient (most influential)
Adaptive: Learn which dimensions benefit most from splitting
Pros: Intuitive, directly reduces input uncertainty
Cons: High-dimensional inputs require many splits; doesn’t exploit network structure
Activation Space Branching¶
Idea: Split based on ReLU activation states, not inputs.
For a ReLU with uncertain activation (pre-activation \(z\) could be positive or negative):
Branch 1: Assume ReLU is active (\(z \geq 0\), so \(y = z\))
Branch 2: Assume ReLU is inactive (\(z < 0\), so \(y = 0\))
Verify: Each branch with ReLU constraint fixed
ReLU selection heuristics:
Largest uncertainty: Split ReLU with widest pre-activation bounds
Output sensitivity: Split ReLU that most affects output bounds
Layer-wise: Prioritize earlier layers (impacts more subsequent computations)
Pros: Exploits network structure; fewer branches than input space splitting for deep networks
Cons: Requires tracking activation states; doesn’t directly reduce input region
Strategy |
Partitions |
Best For |
Complexity per Branch |
|---|---|---|---|
Input space |
Input dimensions |
Shallow networks, small input dimensions |
Low (just tightens bounds) |
Activation space |
ReLU states |
Deep networks, many ReLUs |
Low (adds constraints) |
Hybrid |
Both input and activation |
General networks |
Medium (adaptive) |
Bounding Methods¶
Once you’ve branched, you need to verify each subregion. Branch-and-bound uses incomplete methods for this:
Bound Propagation Options¶
Interval Bound Propagation (IBP) [Gowal et al., 2019]:
Fastest: propagates interval bounds layer-by-layer
Loosest: most conservative approximation
Use for: initial coarse bounds, rapid screening
CROWN [Weng et al., 2018, Zhang et al., 2018]:
Fast: backward linear bound propagation
Tighter: better approximation than IBP
Use for: most branch-and-bound implementations
DeepPoly [Singh et al., 2019]:
Moderate speed: abstract interpretation with polyhedra
Tight: more precise than CROWN for some networks
Use for: when tightness matters more than speed
α-β-CROWN [Wang et al., 2021, Zhang et al., 2022]:
Adaptive: optimizes bound parameters (α, β coefficients)
Tightest: state-of-the-art bound tightness
Use for: production-grade verification, when computational budget allows
Tightness-Speed Tradeoff
Tighter bounds reduce branching (fewer subregions needed) but cost more per region. The optimal choice depends on:
Network size: Larger networks benefit more from tight bounds (less branching)
Property difficulty: Hard properties need tight bounds
Computational budget: Limited time favors faster bounds
The α-β-CROWN Algorithm¶
α-β-CROWN [Wang et al., 2021, Zhang et al., 2022] represents the current state-of-the-art, winning multiple verification competitions (VNN-COMP).
Key Innovation: Optimized Bounds¶
Standard bound propagation fixes relaxation parameters. α-β-CROWN optimizes them:
For ReLU relaxation: Instead of fixed linear upper/lower bounds, parameterize them with \(\alpha, \beta\):
Then optimize \(\alpha, \beta\) to minimize the output bounds. This tightens approximation significantly.
Optimization: Use gradient descent to optimize bound parameters:
Multi-Neuron Constraints¶
α-β-CROWN considers relationships between multiple ReLUs simultaneously (multi-neuron relaxation) rather than treating each ReLU independently. This captures more network structure, tightening bounds further.
Result: Much tighter bounds than standard CROWN, often reducing branching by orders of magnitude.
Branch-and-Bound Integration¶
α-β-CROWN uses optimized bounds within branch-and-bound:
Initial verification: Run α-β-CROWN on full input region
If unknown: Branch on most uncertain domain or activation
Re-optimize: For each subregion, re-optimize α, β parameters
Verify subregions: Use optimized bounds
Repeat: Continue until all regions verified or budget exhausted
Practical Implementation¶
Algorithm Workflow¶
def branch_and_bound_verify(network, input_region, property, bound_method):
# Priority queue: (estimated_difficulty, region)
queue = [(0, input_region)]
while queue:
_, region = queue.pop()
# Compute bounds using incomplete method
bounds = bound_method(network, region)
# Check if bounds satisfy property
if bounds.satisfies(property):
continue # Region verified
elif bounds.violates(property):
return FALSIFIED, bounds.counterexample
else: # Unknown
# Branch: split region
subregions = branch(region, network, bounds)
queue.extend(subregions)
return VERIFIED
Key components:
Queue management: Priority queue orders regions by estimated difficulty
Bounding: Use incomplete method (CROWN, α-β-CROWN) for each region
Branching: Split unverified regions
Termination: Verify all regions, find counterexample, or timeout
Performance Optimizations¶
Early termination: If any region is falsified, stop immediately—you’ve found a counterexample.
Bound caching: Reuse bound computations for overlapping regions when possible.
GPU acceleration [Xu et al., 2020]: Parallelize bound computation across multiple regions. α-β-CROWN on GPU can verify thousands of regions in parallel.
Adaptive branching: Use tight bounds to guide where to branch. Branch on dimensions/activations that most reduce uncertainty.
Timeout per region: Set timeouts for each subregion. If a region times out, count it as unverified and move on.
When to Use Branch-and-Bound¶
Use when:
Network is too large for pure complete methods (SMT, MILP)
You need tighter guarantees than pure incomplete methods provide
Willing to spend hours/days for near-complete verification
Have GPU available for parallel bound computation
Properties are moderately difficult (not trivial, not impossibly hard)
Don’t use when:
Network is small enough for Marabou [Katz et al., 2019] (pure complete is faster)
Need instant results (pure incomplete methods are faster)
Network has millions of parameters (even branch-and-bound won’t scale)
Properties are extremely loose (incomplete methods suffice)
State-of-the-Art Results¶
α-β-CROWN has achieved impressive results in verification competitions:
VNN-COMP: Consistently top-ranked verifier across multiple years and benchmarks.
Scalability: Verifies networks with hundreds of thousands of neurons—orders of magnitude larger than pure complete methods.
Certified accuracy: On standard benchmarks (MNIST, CIFAR-10), achieves the highest certified accuracy at various perturbation radii.
Competition Success
α-β-CROWN [Wang et al., 2021, Zhang et al., 2022] demonstrates that hybrid approaches combining incomplete and complete methods outperform pure approaches. It’s faster than pure complete methods and more definitive than pure incomplete methods.
Limitations¶
Still exponential worst-case: Branch-and-bound faces the same NP-completeness barrier [Katz et al., 2017, Weng et al., 2018] as other complete methods. Some problems will explode exponentially.
Incomplete regions: If computational budget is exhausted, some regions remain unverified. You get “partial verification” (verified for most of input space, unknown for some regions).
Tuning required: Branching strategies, bound methods, and timeout parameters significantly affect performance. Optimal settings vary by network and property.
Memory consumption: Tracking many subregions consumes memory. Very deep branching can exhaust available memory.
Final Thoughts¶
Branch-and-bound verification represents the current state-of-the-art for neural network verification at scale. By combining incomplete methods (for speed) with systematic refinement (for tightness), it achieves practical verification of networks that pure complete methods cannot handle.
α-β-CROWN [Wang et al., 2021, Zhang et al., 2022] exemplifies this approach: optimized bound propagation [Weng et al., 2018, Zhang et al., 2018] plus intelligent branching yields verification of networks with hundreds of thousands of neurons. This is several orders of magnitude beyond what SMT [Katz et al., 2017, Katz et al., 2019] or MILP [Tjeng et al., 2019] can achieve.
Understanding branch-and-bound clarifies the frontier of neural network verification: we can verify non-trivial networks through clever algorithms and hybrid approaches, but fundamental complexity barriers remain. The field advances by pushing these boundaries incrementally, making verification practical for ever-larger networks.
Further Reading
This guide provides comprehensive coverage of branch-and-bound verification for neural networks. For readers interested in diving deeper, we recommend the following resources organized by topic:
Incomplete Bound Propagation Methods:
Branch-and-bound relies on incomplete methods for bounding. CROWN [Weng et al., 2018, Zhang et al., 2018] provides fast backward linear bound propagation. DeepPoly [Singh et al., 2019] uses abstract interpretation with carefully designed abstract domains. IBP [Gowal et al., 2019] offers the fastest but loosest bounds. Understanding these methods is essential for effective branch-and-bound implementation.
α-β-CROWN State-of-the-Art:
The α-β-CROWN verifier [Wang et al., 2021, Zhang et al., 2022] combines optimized bound propagation with branch-and-bound, achieving state-of-the-art results in verification competitions. It optimizes linear relaxation parameters (α, β coefficients) to tighten bounds dramatically, reducing the number of branches needed. GPU acceleration [Xu et al., 2020] enables parallel verification of thousands of subregions.
Complete Verification for Comparison:
Pure complete methods provide context for branch-and-bound’s hybrid approach. SMT-based verification [Katz et al., 2017, Katz et al., 2019] handles small networks definitively but struggles with scale. MILP-based approaches [Tjeng et al., 2019, Cheng et al., 2017] face similar scalability limits. Branch-and-bound extends complete verification to larger networks by accepting partial incompleteness.
Complexity Foundations:
The NP-completeness of neural network verification [Katz et al., 2017, Weng et al., 2018] means that all complete methods—including branch-and-bound—face exponential worst-case complexity. Understanding this fundamental barrier helps set realistic expectations: branch-and-bound extends the frontier of tractable verification but doesn’t eliminate complexity barriers.
Incomplete Methods as Alternative:
When branch-and-bound is too expensive, pure incomplete methods [Gowal et al., 2019, Singh et al., 2019, Weng et al., 2018, Zhang et al., 2018] provide fast but potentially loose verification. For very large networks, accepting “unknown” results may be necessary. Randomized smoothing [Cohen et al., 2019] offers an alternative probabilistic certification approach that scales even better.
Related Topics:
For understanding the incomplete methods that branch-and-bound uses for bounding, see Bound Propagation Approaches. For complete methods that branch-and-bound extends, see SMT and MILP Solvers for Verification and Marabou and Reluplex: Extended Simplex for Verification. For the mathematical foundations of the verification problem, see The Verification Problem: Mathematical Formulation. For understanding the theoretical guarantees, see Soundness and Completeness.
Next Phase
Congratulations on completing Phase 2: Core Verification Techniques! Continue to Phase 3: Robust Training & Practical Implementation to learn about robust training, formal specifications, and practical implementation workflows.
Chih-Hong Cheng, Georg Nührenberg, and Harald Ruess. Maximum resilience of artificial neural networks. In International Symposium on Automated Technology for Verification and Analysis, 251–268. Springer, 2017.
Jeremy Cohen, Elan Rosenfeld, and Zico Kolter. Certified adversarial robustness via randomized smoothing. In International Conference on Machine Learning. 2019.
Sven Gowal, Krishnamurthy Dj Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Uesato, Relja Arandjelovic, Timothy Mann, and Pushmeet Kohli. Scalable verified training for provably robust image classification. In Proceedings of the IEEE International Conference on Computer Vision, 4842–4851. 2019.
Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel J Kochenderfer. Reluplex: an efficient smt solver for verifying deep neural networks. In International Conference on Computer Aided Verification, 97–117. Springer, 2017.
Guy Katz, Derek A Huang, Duligur Ibeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zeljić, and others. The marabou framework for verification and analysis of deep neural networks. In International Conference on Computer Aided Verification, 443–452. Springer, 2019.
Gagandeep Singh, Rupanshu Ganvir, Markus Püschel, and Martin Vechev. Beyond the single neuron convex barrier for neural network certification. In Advances in Neural Information Processing Systems, 15072–15083. 2019.
Vincent Tjeng, Kai Y. Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming. In International Conference on Learning Representations. 2019.
Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. Beta-crown: efficient bound propagation with per-neuron split constraints for neural network robustness verification. Advances in Neural Information Processing Systems, 2021.
Lily Weng, Huan Zhang, Hongge Chen, Zhao Song, Cho-Jui Hsieh, Luca Daniel, Duane Boning, and Inderjit Dhillon. Towards fast computation of certified robustness for relu networks. In International Conference on Machine Learning, 5276–5285. 2018.
Kaidi Xu, Zhouxing Shi, Huan Zhang, Yihan Wang, Kai-Wei Chang, Minlie Huang, Bhavya Kailkhura, Xue Lin, and Cho-Jui Hsieh. Automatic perturbation analysis for scalable certified robustness and beyond. Advances in Neural Information Processing Systems, 2020.
Comments & Discussion