Skip to yearly menu bar Skip to main content


Poster

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

Duo Zhou · Christopher Brix · Grani A. Hanasusanto · Huan Zhang

East Exhibit Hall A-C #2206
[ ]
Wed 11 Dec 11 a.m. PST — 2 p.m. PST

Abstract:

Recently, cutting-plane methods such as GCP-CROWN have been explored to enhance neural network verifiers and made significant advancements. However, GCP-CROWN requires 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 to this problem setting. We propose a novel approach, Branch-and-bound Inferred Cuts with COnstraint Strengthening (BICCOS), that leverages the logical relationships of neurons within verified subproblems in the branch-and-bound search tree, and we introduce cutting planes constraints 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 experimental results demonstrate that this approach can generate hundreds of high-quality 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.

Live content is unavailable. Log in and register to view live content