E-Globe：通过紧致上界和模式感知分支实现神经网络可扩展 $\epsilon$-全局验证
机器学习
2026-02-06 v1 人工智能
摘要
神经网络实现了强大的经验性能，但鲁棒性仍是阻碍在安全关键应用中部署的瓶颈。形式化验证提供鲁棒性保证，但当前方法面临可扩展性与完整性之间的权衡。我们提出一种在分支-界限（BaB）框架中实现高效紧致上下界的混合验证器，直至达到 -全局最优或触发提前停止。关键在于采用包含互补约束的精确非线性规划（NLP-CC）进行上界估计，该方法保留 ReLU 输入-输出图，使得任何可行解都产生有效的反例，从而实现对不安全子问题的快速修剪。我们进一步通过 (i) 热启动 NLP 求解，仅需最小限度的约束矩阵更新，以及 (ii) 面向模式的强分支策略来加速验证。我们还提供了 NLP-CC 上界紧致的条件。在 MNIST 和 CIFAR-10 上的实验表明，我们的 method 在扰动半径跨越三个数量级后，显著优于 PGD 的上界，实际操作中实现快速节点求解，并通过热启动、GPU 批量处理和模式对齐分支实现显著的端到端加速。
引用
@article{arxiv.2602.05068,
title = {E-Globe: Scalable $\epsilon$-Global Verification of Neural Networks via Tight Upper Bounds and Pattern-Aware Branching},
author = {Wenting Li and Saif R. Kazi and Russell Bent and Duo Zhou and Huan Zhang},
journal= {arXiv preprint arXiv:2602.05068},
year = {2026}
}
备注
16 pages, 10 figures