Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Duo Zhou, Christopher Brix, Grani A Hanasusanto, Huan Zhang

TL;DR

The paper tackles the scalability bottleneck in neural network verification by introducing BICCOS, a Branch-and-bound Inferred Cuts with Constraint Strengthening approach. BICCOS generates cutting planes on the fly from verified BaB subproblems, strengthens them by selectively removing unused ReLU indicators, and proactively discovers additional cuts through a multi-tree presolve, all while extending GCP-CROWN to handle fixed z variables. Empirical results show that BICCOS significantly increases the number of verifiable instances on challenging benchmarks (VNN-COMP and SDP-FO), including very large networks that MIP-based cuts struggle to scale to, demonstrating improved verification performance with manageable overhead. The method offers a scalable, cutting-plane–driven alternative to generic MIP solvers for NN verification, with practical impact on safety-critical applications and open pathways for further integration with existing verifiers.

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 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 .

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

TL;DR

The paper tackles the scalability bottleneck in neural network verification by introducing BICCOS, a Branch-and-bound Inferred Cuts with Constraint Strengthening approach. BICCOS generates cutting planes on the fly from verified BaB subproblems, strengthens them by selectively removing unused ReLU indicators, and proactively discovers additional cuts through a multi-tree presolve, all while extending GCP-CROWN to handle fixed z variables. Empirical results show that BICCOS significantly increases the number of verifiable instances on challenging benchmarks (VNN-COMP and SDP-FO), including very large networks that MIP-based cuts struggle to scale to, demonstrating improved verification performance with manageable overhead. The method offers a scalable, cutting-plane–driven alternative to generic MIP solvers for NN verification, with practical impact on safety-critical applications and open pathways for further integration with existing verifiers.

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 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 .
Paper Structure (37 sections, 4 theorems, 25 equations, 4 figures, 4 tables, 2 algorithms)

This paper contains 37 sections, 4 theorems, 25 equations, 4 figures, 4 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Background
  3. Notations
  4. The NN Verification Problem
  5. MIP Formulation and LP Relaxation
  6. Branch-and-bound
  7. General Cutting Planes (GCP) in NN verification
  8. Branch-and-bound Inferred Cuts with Constraint Strengthening (BICCOS)
  9. Branch-and-bound Inferred Cuts
  10. Extension of GCP-CROWN
  11. Improving BaB Inferred Cuts via Constraint Strengthening and Multi-Tree Search
  12. Neuron Elimination Heuristic for Constraint Strengthening
  13. Multi-Tree Search
  14. BaB Tree Searching Strategy
  15. BICCOS Summary
  16. ...and 22 more sections

Key Result

Proposition 3.1

For a verified, or UNSAT, subproblem in a BaB search tree, let $\mathcal{Z}_{+}$ and $\mathcal{Z}_{-}$ be the set of neurons restricted to the positive and negative regimes respectively. These restrictions were introduced by the BaB process. Then, the BaB inferred cut can be formulated as:

Figures (4)

  • Figure 1: Each node represents a subproblem in the BaB process by splitting unstable ReLU neurons. Green nodes indicate paths that have been verified and pruned, while blue nodes represent domains that are still unknown and require further branching.
  • Figure 2: (\ref{['fig:infer']}): Inferred cut from UNSAT paths during BaB and why it fails in regular BaB. (\ref{['fig:refine']}): Constraint strengthening with Neuron Elimination Heuristic. (\ref{['fig:shallow']}): Multi-tree search.
  • Figure 3: Comparison of Venus2 and MILP with BICCOS. For a fair comparison, we do not use GPU-accelerated bound propagation but use a MILP solver (same as in Venus2) to solve the verification problem with our BICCOS cuts. In all 4 benchmarks, MILP with BICCOS cuts is faster than Venus (MILP with their proposed cuts), illustrating the effectiveness. Note that Venus2 can hardly scale to larger models presented in our paper, such as those on cifar100 and tinyimagenet datasets.
  • Figure 4: Slow down comparison on easier properties on BICCOS (base), BICCOS (MTS), GCP-CROWN with MIP cuts and BICCOS (auto) . We plot the number of solved instances versus verification time for BICCOS and $\beta$-CROWN (baseline). For easy instances that can be verified within a few seconds (bottom parts of the figures), the increase of verification time with BICCOS is negligible.

Theorems & Definitions (5)

  • Proposition 3.1
  • Theorem 3.2
  • Corollary 3.3
  • Lemma A.1
  • proof