E-Globe: Scalable $ε$-Global Verification of Neural Networks via Tight Upper Bounds and Pattern-Aware Branching

TL;DR

The paper tackles robustness verification for neural networks under input perturbations by casting verification as a minimization of a specification $f(x)$ over a perturbation set, with $f^\star$ indicating safety via $f^\star \ge 0$. It introduces E-Globe, a hybrid verifier that achieves $ε$-global optimization by combining an activation-exact NLP-CC upper bound with a bound-propagation lower bound (via $β$-CROWN) inside a branch-and-bound framework, guided by activation-pattern information. Key innovations include exact NLP-CC reformulations with invariant input–output graphs, warm-started KKT updates for fast re-solves, and pattern-aligned strong branching to aggressively tighten lower bounds. Empirical results on MNIST and CIFAR-10 show significantly tighter upper bounds than PGD and other relaxations, substantial speedups over MIP-based verification, and effective scaling aided by warm-starts and GPU batching. Overall, E-Globe delivers practical, near-global robustness certificates for moderate-sized networks and paves the way toward scalable, real-time verification.

Abstract

Neural networks achieve strong empirical performance, but robustness concerns still hinder deployment in safety-critical applications. Formal verification provides robustness guarantees, but current methods face a scalability-completeness trade-off. We propose a hybrid verifier in a branch-and-bound (BaB) framework that efficiently tightens both upper and lower bounds until an $ε-$global optimum is reached or early stop is triggered. The key is an exact nonlinear program with complementarity constraints (NLP-CC) for upper bounding that preserves the ReLU input-output graph, so any feasible solution yields a valid counterexample and enables rapid pruning of unsafe subproblems. We further accelerate verification with (i) warm-started NLP solves requiring minimal constraint-matrix updates and (ii) pattern-aligned strong branching that prioritizes splits most effective at tightening relaxations. We also provide conditions under which NLP-CC upper bounds are tight. Experiments on MNIST and CIFAR-10 show markedly tighter upper bounds than PGD across perturbation radii spanning up to three orders of magnitude, fast per-node solves in practice, and substantial end-to-end speedups over MIP-based verification, amplified by warm-starting, GPU batching, and pattern-aligned branching.

Figures (10)

• Figure 1: Verification is to decide whether the worst-case output $f^\star \!=\! \min_{x\in\mathcal{C}} f(x)$ is nonnegative.
• Figure 2: By tightening the lower and upper bounds, branch-and-bound progressively narrows the $\bar{u} -\underline{l}$ from (a) to (b), enabling fast verification without exploring all subproblems.
• Figure 3: Flowchart of E-Globe with bidirectional flow.$\beta$-CROWN supplies lower bounds to NLP-CC, and NLP-CC returns upper bounds and activation patterns that guide branching.
• Figure 4: Early stopping rules that cut search cost.
• Figure 5: The size of $I_0$ compared with the number of binary variables for the first 100 cases

Theorems & Definitions (4)

• Proposition 4.1: Exact Reformulation
• Proposition 4.2: Invariant Input--Output Feasible Region
• Proposition 4.3: Soundness of the NLP--CC Upper Bound
• Proposition 5.1: Region optimality under strict complementarity