E-Globe：通过紧上界和模式感知分支实现神经网络的可扩展ε-全局验证
E-Globe: Scalable $ε$-Global Verification of Neural Networks via Tight Upper Bounds and Pattern-Aware Branching
AI总结：
E-Globe通过紧上界和模式感知分支实现神经网络的高效ε-全局验证，显著提升验证速度和精度。
摘要：
神经网络在经验性能上表现强劲，但稳健性问题仍阻碍其在安全关键应用中的部署。形式验证提供稳健性保证，但当前方法面临可扩展性与完备性之间的权衡。我们提出了一种混合验证器，采用分支定界（BaB）框架，在高效紧缩上界和下界直至达到ε-全局最优或提前停止。关键是一个精确的非线性规划问题（NLP-CC）用于上界估计，以保持ReLU输入输出图，因此任何可行解都产生有效的反例并能快速修剪不安全的子问题。我们进一步通过（i）需要最小约束矩阵更新的预热启动NLP求解和（ii）模式对齐的强分支来加速验证，优先选择最有效紧缩松弛的分裂。我们还提供了NLP-CC上界是紧的条件。在MNIST和CIFAR-10上的实验显示，比PGD在扰动半径跨度达三个数量级的上界更紧密，实际中每节点求解快，且比基于MIP的验证有显著的端到端加速，通过预热启动、GPU批处理和模式对齐分支进一步放大。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
