基于分支界限推断割平面的可扩展神经网络验证
机器学习
2026-03-31 v2 密码学与安全
最优化与控制
摘要
最近，诸如 GCP-CROWN 等割平面方法被用于增强神经网络验证器并取得了显著进展。然而，GCP-CROWN 当前依赖来自外部混合整数规划（MIP）求解器生成的通用割平面（cuts）。由于 MIP 求解器的规模较差，大型神经网络无法从这些割平面中受益。在本文中，我们利用神经网络验证问题的结构生成高效且可扩展的专用割平面。我们提出了一种新方法，分支界限推断割平面（Branch-and-bound Inferred Cuts with COnstraint Strengthening, BICCOS），该方法利用在分支界限搜索树中验证子问题中神经元之间的逻辑关系，并引入这些关系在其他子问题中不可行的割。我们开发了一种将每个路径中神经元的影响分数分配给神经元的机制，以允许加强这些割。此外，我们设计了一种多树搜索技术以识别更多割，从而有效缩小搜索空间并加速 BaB 算法。我们的结果表明，BICCOS 在分支界限过程中可以生成数百个有用的割，并在广泛的基准测试中持续增加可验证实例的数量，包括以前的割平面方法无法规模化的大型网络。BICCOS 是 -CROWN 验证器之一，VNN-COMP 2024 获奖者。代码可在 http://github.com/Lemutisme/BICCOS 查看。
引用
@article{arxiv.2501.00200,
title = {Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes},
author = {Duo Zhou and Christopher Brix and Grani A Hanasusanto and Huan Zhang},
journal= {arXiv preprint arXiv:2501.00200},
year = {2026}
}
备注
Accepted by NeurIPS 2024. BICCOS is part of the alpha-beta-CROWN verifier, the VNN-COMP 2024 winner; fixed Theorem 3.2 and clarified experimental results