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 .

翻译：近年来，诸如GCP-CROWN等切割平面方法被用于增强神经网络验证器，并取得了显著进展。然而，当前GCP-CROWN依赖外部混合整数规划求解器生成的通用切割平面。由于混合整数规划求解器可扩展性差，大型神经网络无法从这些切割平面中受益。本文利用神经网络验证问题的结构特性，生成针对该问题的高效且可扩展的定制切割平面。我们提出了一种名为BICCOS（分支定界推断切割与约束强化）的新方法，该方法利用分支定界搜索树中已验证子问题内神经元的逻辑关联，并引入能阻止其他子问题中这些关联的切割平面。我们开发了一种机制，为每条路径中的神经元分配影响分数以强化这些切割平面。此外，我们设计了多树搜索技术来识别更多切割平面，有效缩小搜索空间并加速分支定界算法。实验表明，BICCOS能在分支定界过程中生成数百个有效切割平面，并在广泛基准测试中（包括先前切割平面方法无法扩展的大型网络）一致提高可验证实例数量。BICCOS是VNN-COMP 2024冠军α,β-CROWN验证器的组成部分。代码开源于http://github.com/Lemutisme/BICCOS。