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

TL;DR

This paper introduces E-Globe, a scalable and efficient hybrid verification method for neural networks that provides tight bounds and robustness guarantees by combining nonlinear programming with strategic branching, significantly improving over existing approaches.

Contribution

E-Globe presents a novel hybrid branch-and-bound verifier using an exact NLP-CC for tight bounds, along with warm-starting and pattern-aware branching to enhance scalability and accuracy.

Findings

Tighter upper bounds than PGD across various perturbation radii

Fast per-node solves enabling practical scalability

Significant speedups over MIP-based verification methods

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 $\epsilon-$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.