提出可扩展的神经网络验证方法，通过推理剪枝平面提升大规模网络验证效率。
Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes
- 利用分支定界搜索中神经元的逻辑关系生成针对性剪枝平面。
- 在多个基准上验证了数百个有效剪枝平面，显著提升可验证实例数。
- 适用于大规模神经网络验证，适合追求高精度验证的研究者。
近年来，基于切割平面的方法（如 GCP-CROWN）被用于增强神经网络验证器并取得显著进展。然而，当前 GCP-CROWN 依赖外部混合整数规划（MIP）求解器生成通用切割平面，由于 MIP 求解器扩展性差，大型神经网络无法从中获益。本文利用神经网络验证问题的结构特性，提出一种新型可扩展切割平面生成方法——分支定界推理剪枝平面与约束强化（BICCOS）。该方法利用分支定界搜索树中子问题内神经元的逻辑关系，在其他子问题中预排除这些关系以生成剪枝平面，并引入影响得分机制对路径中神经元进行加权以强化切割平面。此外，设计多树搜索技术以发现更多有效切割平面，显著缩小搜索空间并加速分支定界算法。实验表明，BICCOS 在分支定界过程中可生成数百个有效切割平面，在包括大型网络在内的多种基准上，一致提升了可验证实例数量，超越现有先进验证器。BICCOS 是 $α,β$-CROWN 验证器的核心组件，荣获 VNN-COMP 2024 冠军。代码已开源：http://github.com/Lemutisme/BICCOS。
原文摘要 · Abstract (English)
Recently, cutting-plane methods such as GCP-CROWN have been explored to enhance neural network verifiers and made significant advances. However, GCP-CROWN currently relies on generic cutting planes (cuts) generated from external mixed integer programming (MIP) solvers. Due to the poor scalability of MIP solvers, large neural networks cannot benefit from these cutting planes. In this paper, we exploit the structure of the neural network verification problem to generate efficient and scalable cutting planes specific for this problem setting. We propose a novel approach, Branch-and-bound Inferred Cuts with COnstraint Strengthening (BICCOS), which leverages the logical relationships of neurons within verified subproblems in the branch-and-bound search tree, and we introduce cuts that preclude these relationships in other subproblems. We develop a mechanism that assigns influence scores to neurons in each path to allow the strengthening of these cuts. Furthermore, we design a multi-tree search technique to identify more cuts, effectively narrowing the search space and accelerating the BaB algorithm. Our results demonstrate that BICCOS can generate hundreds of useful cuts during the branch-and-bound process and consistently increase the number of verifiable instances compared to other state-of-the-art neural network verifiers on a wide range of benchmarks, including large networks that previous cutting plane methods could not scale to. BICCOS is part of the $α,β$-CROWN verifier, the VNN-COMP 2024 winner. The code is available at http://github.com/Lemutisme/BICCOS .
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。