[2501.00200] Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes

Computer Science > Machine Learning arXiv:2501.00200 (cs) [Submitted on 31 Dec 2024 (v1), last revised 28 Mar 2026 (this version, v2)] Title:Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes Authors:Duo Zhou, Christopher Brix, Grani A Hanasusanto, Huan Zhang View a PDF of the paper titled Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes, by Duo Zhou and 3 other authors View PDF HTML (experimental) Abstract: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 ide...