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

• URL: http://arxiv.org/abs/2602.05068v1
• Date: Wed, 04 Feb 2026 21:42:29 GMT
• Title: E-Globe: Scalable $ε$-Global Verification of Neural Networks via Tight Upper Bounds and Pattern-Aware Branching
• Authors: Wenting Li, Saif R. Kazi, Russell Bent, Duo Zhou, Huan Zhang,
• Abstract summary: Formal verification provides robustness guarantees, but current methods face a scalability-completeness trade-off.<n>We propose a hybrid verifier that efficiently tightens both upper and lower bounds until an $-$global optimum is reached or early stop is triggered.
• Score: 9.161865803917847
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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.

Related papers

• BandPO: Bridging Trust Regions and Ratio Clipping via Probability-Aware Bounds for LLM Reinforcement Learning [49.25750348525603]
  BandPO replaces canonical clipping with Band, a unified theoretical operator that projects trust regions into dynamic, probability-aware clipping intervals.<n>We show that BandPO consistently outperforms canonical clipping and Clip-Higher, while robustly mitigating entropy collapse.
  arXiv  Detail & Related papers  (2026-03-05T08:03:05Z)
• Exact and Asymptotically Complete Robust Verifications of Neural Networks via Quantum Optimization [9.728049285140736]
  We introduce two quantum-optimization-based models for robust verification of deep neural networks.<n>Experiments on benchmarks show high certification accuracy, indicating that quantum optimization can serve as a principled primitive for robustness guarantees.
  arXiv  Detail & Related papers  (2026-02-28T02:05:02Z)
• Overcoming Joint Intractability with Lossless Hierarchical Speculative Decoding [58.92526489742584]
  We propose provably lossless.<n> verification method that significantly boosts the expected number of accepted tokens.<n>We show that HSD yields consistent improvements in acceptance rates across diverse model families and benchmarks.
  arXiv  Detail & Related papers  (2026-01-09T11:10:29Z)
• Clip-and-Verify: Linear Constraint-Driven Domain Clipping for Accelerating Neural Network Verification [9.733843486234878]
  State-of-the-art neural network (NN) verifiers demonstrate that applying the branch-and-bound (BaB) procedure with fast bounding techniques plays a key role in tackling many challenging verification properties.<n>We introduce the linear constraint-driven clipping framework, a class of scalable and efficient methods designed to enhance the efficacy of NN verifiers.
  arXiv  Detail & Related papers  (2025-12-11T19:59:37Z)
• Scalable First-order Method for Certifying Optimal k-Sparse GLMs [9.613635592922174]
  We propose a first-order proximal gradient algorithm to solve the perspective relaxation of the problem within a BnB framework.<n>We show that our approach significantly accelerates dual bound computations and is highly effective in providing optimality certificates for large-scale problems.
  arXiv  Detail & Related papers  (2025-02-13T17:14:18Z)
• Robust Stochastically-Descending Unrolled Networks [85.6993263983062]
  Deep unrolling is an emerging learning-to-optimize method that unrolls a truncated iterative algorithm in the layers of a trainable neural network.<n>We show that convergence guarantees and generalizability of the unrolled networks are still open theoretical problems.<n>We numerically assess unrolled architectures trained under the proposed constraints in two different applications.
  arXiv  Detail & Related papers  (2023-12-25T18:51:23Z)
• Achieving Constraints in Neural Networks: A Stochastic Augmented Lagrangian Approach [49.1574468325115]
  Regularizing Deep Neural Networks (DNNs) is essential for improving generalizability and preventing overfitting. We propose a novel approach to DNN regularization by framing the training process as a constrained optimization problem. We employ the Augmented Lagrangian (SAL) method to achieve a more flexible and efficient regularization mechanism.
  arXiv  Detail & Related papers  (2023-10-25T13:55:35Z)
• Fast Global Convergence of Policy Optimization for Constrained MDPs [17.825031573375725]
  We show that gradient-based methods can achieve an $mathcalO(log(T)/T)$ global convergence rate both for the optimality gap and the constraint violation. When Slater's condition is satisfied and known a priori, zero constraint violation can be further guaranteed for a sufficiently large $T$.
  arXiv  Detail & Related papers  (2021-10-31T17:46:26Z)
• Improved Branch and Bound for Neural Network Verification via Lagrangian Decomposition [161.09660864941603]
  We improve the scalability of Branch and Bound (BaB) algorithms for formally proving input-output properties of neural networks. We present a novel activation-based branching strategy and a BaB framework, named Branch and Dual Network Bound (BaDNB) BaDNB outperforms previous complete verification systems by a large margin, cutting average verification times by factors up to 50 on adversarial properties.
  arXiv  Detail & Related papers  (2021-04-14T09:22:42Z)
• Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers [112.23981192818721]
  We propose to use backward mode linear relaxation based analysis (LiRPA) to replace Linear Programming (LP) during the BaB process. Unlike LP, LiRPA when applied naively can produce much weaker bounds and even cannot check certain conflicts of sub-domains during splitting. We demonstrate an order of magnitude speedup compared to existing LP-based approaches.
  arXiv  Detail & Related papers  (2020-11-27T16:42:12Z)
• On Lower Bounds for Standard and Robust Gaussian Process Bandit Optimization [55.937424268654645]
  We consider algorithm-independent lower bounds for the problem of black-box optimization of functions having a bounded norm. We provide a novel proof technique for deriving lower bounds on the regret, with benefits including simplicity, versatility, and an improved dependence on the error probability.
  arXiv  Detail & Related papers  (2020-08-20T03:48:14Z)
• PEREGRiNN: Penalized-Relaxation Greedy Neural Network Verifier [1.1011268090482575]
  We introduce a new approach to formally verify the most commonly considered safety specifications for ReLU NNs. We use a convex solver not only as a linear feasibility checker, but also as a means of penalizing the amount of relaxation allowed in solutions.
  arXiv  Detail & Related papers  (2020-06-18T21:33:07Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.