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 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}$ :

\forall x \in \mathcal{X}, \quad \phi(f(x)) = \text{true}

Incomplete verification computes bounds on $f(x)$ for $x \in \mathcal{X}$ :

\underline{y} \leq f(x) \leq \overline{y} \quad \forall 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$ :

\forall x \in \mathcal{X}, \phi(f(x)) \iff \bigwedge_i \left(\forall x \in \mathcal{X}_i, \phi(f(x))\right)

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):

Fastest: propagates interval bounds layer-by-layer
Loosest: most conservative approximation
Use for: initial coarse bounds, rapid screening

CROWN:

Fast: backward linear bound propagation
Tighter: better approximation than IBP
Use for: most branch-and-bound implementations

DeepPoly:

Moderate speed: abstract interpretation with polyhedra
Tight: more precise than CROWN for some networks
Use for: when tightness matters more than speed

alpha-beta-CROWN:

Adaptive: optimizes bound parameters (alpha, beta 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 alpha-beta-CROWN Algorithm

alpha-beta-CROWN represents the current state-of-the-art, winning multiple verification competitions (VNN-COMP).

Key Innovation: Optimized Bounds

Standard bound propagation fixes relaxation parameters. alpha-beta-CROWN optimizes them:

For ReLU relaxation: Instead of fixed linear upper/lower bounds, parameterize them with $\alpha, \beta$ :

y \leq \alpha z + \beta

Then optimize $\alpha, \beta$ to minimize the output bounds. This tightens approximation significantly.

Optimization: Use gradient descent to optimize bound parameters:

\min_{\alpha, \beta} \quad \text{output\_bound}(f(x); \alpha, \beta) \quad \text{s.t.} \quad \text{relaxation is sound}

Multi-Neuron Constraints

alpha-beta-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

alpha-beta-CROWN uses optimized bounds within branch-and-bound:

Initial verification: Run alpha-beta-CROWN on full input region
If unknown: Branch on most uncertain domain or activation
Re-optimize: For each subregion, re-optimize alpha, beta 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, alpha-beta-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: Parallelize bound computation across multiple regions. alpha-beta-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 (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

alpha-beta-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: alpha-beta-CROWN 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 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.

alpha-beta-CROWN exemplifies this approach: optimized bound propagation plus intelligent branching yields verification of networks with hundreds of thousands of neurons. This is several orders of magnitude beyond what SMT or MILP 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.