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. And it is worth being exact about the result, because the tempting description here — near-complete — is not a category a verification method can occupy, and using it hides the thing that actually differs.

A branch-and-bound run is complete. Given unbounded time it terminates with either a proof or a witness, for the same reason an exact solver does: it keeps splitting regions until each is decided, and it never discards a region it could not decide. What it is not is fast, and the two are independent — the soundness and completeness chapter is about exactly this. Three things follow, and each is a fact about a different object:

• The method is complete. Its guarantee does not weaken when it is hybrid.
• The run may not conclude, because a timeout stops it. A timeout is a fact about that run, not a downgrade of the method.
• The cost is what makes it impractical on a large network, since the region count can grow exponentially and nothing prunes it except a bound that decides a region early.

This guide explores how branch-and-bound works for neural network verification, why it performs strongly on 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

1. Try incomplete verification on the full region

2. If verified: Done---the property holds

3. If falsified: Found counterexample---property violated

4. 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 affects the whole cost of the search, because every region that cannot be decided immediately has to be split and re-bounded.

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

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 (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

alpha-beta-CROWN (Xu et al. 2021, Wang et al. 2021):

• Adaptive: optimizes bound parameters (alpha, beta coefficients)
• Tightest: among the strongest bound tightness available in practice
• 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 is a leading branch-and-bound verifier with strong results in VNN-COMP (Bak et al. 2021) and related benchmark evaluations.

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

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

Optimization: Use gradient descent to optimize bound parameters:

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: Tighter bounds than standard CROWN, and the number of branches is where that tightness is cashed in — a tighter per-region bound decides more regions without splitting, so the tree is smaller. The reduction factor depends on the network, so it is not stated here; what transfers is that the two improvements compound, because each branch that is never created is also never bounded.

Branch-and-Bound Integration

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

1. Initial verification: Run alpha-beta-CROWN on full input region
2. If unknown: Branch on most uncertain domain or activation
3. Re-optimize: For each subregion, re-optimize alpha, beta parameters
4. Verify subregions: Use optimized bounds
5. 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 or days, because completeness is bought with search rather than with a looser guarantee
• 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)

Representative Results

alpha-beta-CROWN has achieved impressive results in verification competitions:

VNN-COMP: Repeatedly strong performance across multiple years and benchmark categories.

Scalability: Handles networks with hundreds of thousands of neurons, which is far beyond what a complete solver is applied to in practice. The comparison is about what gets attempted, not about a limit: the exponential worst case is the same for both, and the difference is that branch-and-bound’s search is pruned in a way SMT and MILP’s is not.

Certified accuracy: On standard benchmarks such as MNIST and CIFAR-10, reported certified accuracy is among the strongest for branch-and-bound-based pipelines.

Competition Success: alpha-beta-CROWN illustrates why hybrid approaches are effective: they are often faster than pure complete methods while being more decisive than purely incomplete ones.

Where the cost goes

The worst case is unchanged. Branch-and-bound is exponential in the worst case, exactly as SMT and MILP are, and the same instances that are hard for one are hard for the other. What differs is the constant and the pruning, not the asymptotics — so an instance that defeats it will defeat a complete solver too, and the honest statement is about what gets attempted rather than about a ceiling the method has.

Budget exhaustion produces a run that concluded nothing. This is the point most worth being careful about, because it is where a tool’s output invites a misreading. If the budget runs out, the regions already decided were decided correctly and the rest are simply undecided — and a property is verified only when every input is decided. So the output is UNKNOWN for the property. A tool may print a progress figure, and “80% of the space is decided” is a true statement about the run; what it is not is a partial guarantee. A property that is 80% decided is not 80% verified.

The search is sensitive to configuration. Branching strategy, which bound method supplies the per-region bounds, and the timeout all change the outcome, and the best settings move with the network and the property. This is ordinary for a heuristic search and worth knowing before reading a number off a single run.

Memory grows with the frontier. Keeping the undecided regions alive costs memory, and a deep enough tree exhausts it before the timeout does — which is a failure mode that looks like a hang rather than like a budget stop, and is worth distinguishing from one.

Key Takeaways

Branch-and-bound verification is one of the strongest approaches 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, verified on networks with hundreds of thousands of neurons. That is well beyond the size at which a complete solver is practical, and the reason is pruning rather than a different worst case — both remain exponential in the worst case, and only one of them discards most of its search tree.

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.