PaperlayerView exact revision on arXiv

Source-linked AI summary

General Cutting Planes for Bound-Propagation-Based Neural Network Verification

Huan Zhang, Shiqi Wang, Kaidi Xu, Linyi Li, Bo Li, Suman Jana, Cho-Jui Hsieh, J. Zico Kolter

arXiv:2208.05740v2cs.LGcs.CRcs.CVmath.OCstat.ML

TL;DR

Existing bound-propagation verifiers cannot efficiently handle general cutting planes, limiting convex-relaxation strengthening. The paper introduces GCP-CROWN, which supports arbitrary cuts and combines GPU-based bound propagation with MIP-generated cuts. It completely solves oval20 and verifies twice as many oval21 instances as the VNN-COMP 2021 winner.

  • Problem

    Existing bound-propagation frameworks cannot efficiently solve general cutting-plane constraints, including those involving cross-layer variables and relaxed ReLU indicators.

  • Method

    GCP-CROWN generalizes bound propagation to arbitrary cutting planes and combines GPU-accelerated branching with high-quality cuts generated by an off-the-shelf MIP solver.

  • Results

    GCP-CROWN completely solves all oval20 instances and verifies twice as many oval21 instances as the VNN-COMP 2021 winner.

  • Takeaways & Limitations

    Combining fast bound propagation with strong general cutting planes yields state-of-the-art verification performance across multiple benchmarks.

  • Takeaways & Limitations

    The method is developed for ReLU networks, and stronger or faster neural-network-specific cutting-plane methods may exist beyond the generic MIP cuts used here.

Abstract

from arXiv · show

Bound propagation methods, when combined with branch and bound, are among the most effective methods to formally verify properties of deep neural networks such as correctness, robustness, and safety. However, existing works cannot handle the general form of cutting plane constraints widely accepted in traditional solvers, which are crucial for strengthening verifiers with tightened convex relaxations. In this paper, we generalize the bound propagation procedure to allow the addition of arbitrary cutting plane constraints, including those involving relaxed integer variables that do not appear in existing bound propagation formulations. Our generalized bound propagation method, GCP-CROWN, opens up the opportunity to apply general cutting plane methods for neural network verification while benefiting from the efficiency and GPU acceleration of bound propagation methods. As a case study, we investigate the use of cutting planes generated by off-the-shelf mixed integer programming (MIP) solver. We find that MIP solvers can generate high-quality cutting planes for strengthening bound-propagation-based verifiers using our new formulation. Since the branching-focused bound propagation procedure and the cutting-plane-focused MIP solver can run in parallel utilizing different types of hardware (GPUs and CPUs), their combination can quickly explore a large number of branches with strong cutting planes, leading to strong verification performance. Experiments demonstrate that our method is the first verifier that can completely solve the oval20 benchmark and verify twice as many instances on the oval21 benchmark compared to the best tool in VNN-COMP 2021, and also noticeably outperforms state-of-the-art verifiers on a wide range of benchmarks. GCP-CROWN is part of the $α,\!β$-CROWN verifier, the VNN-COMP 2022 winner. Code is available at http://PaperCode.cc/GCP-CROWN

1 Introduction

NN verification formally checks properties such as correctness and safety, but scalable verifiers lack efficient support for general cutting planes. GCP-CROWN generalizes bound propagation to arbitrary cuts and combines it with MIP-generated cuts, achieving strong benchmark results.

  • 1 Introduction: NN verification formally proves or disproves properties such as correctness and safety under specified input sets, providing worst-case guarantees.The problem is generally NP-complete and can be encoded as mixed integer programming for piece-wise linear networks.
  • 1 Introduction: General cutting planes strengthen convex relaxations by capturing inter-neuron dependencies that single-neuron relaxations miss.Existing scalable verifiers generally cannot handle cuts involving variables from different layers or relaxed integer variables.
  • 1 Introduction: GCP-CROWN generalizes bound propagation to constraints spanning any network layers and ReLU indicator variables, enabling arbitrary cutting planes.The formulation avoids relying on a slow LP solver and combines GPU-accelerated propagation with MIP-generated cuts.
  • 1 Introduction: The proposed verifier completely solves oval20 and verifies twice as many oval21 instances as the VNN-COMP 2021 winner.The oval20 result is achieved with an average time of less than 5 seconds per instance.

2 Background

The paper formulates ReLU-network verification as MIP or LP optimization over bounded inputs and uses bound propagation to obtain sound lower bounds efficiently. Branch-and-bound improves completeness, while adding cutting planes strengthens the LP relaxation.

  • 2 Background: NN verification minimizes a scalar specification over a bounded input set, proving the property when the optimum f* is nonnegative.The paper uses an ℓ∞ perturbation ball around a predefined input and can append the specification as an output layer.
  • 2 Background: MIP encodes unstable ReLU neurons with binary variables, while active and inactive neurons remain linear under sound pre-activation bounds.The resulting formulation is relaxed to an LP by allowing ReLU indicators to take continuous values between 0 and 1.
  • 2 Background: The LP relaxation supplies a lower bound on the MIP optimum, but a nonnegative bound is sufficient for verification only when it proves the specification.Branch-and-bound can improve the lower bound, while this paper strengthens the relaxation in an orthogonal direction by adding cutting planes.
  • 2 Background: Bound propagation computes sound lower bounds by repeatedly propagating linear inequalities backward through affine and ReLU layers.The procedure reaches the input layer and can be implemented efficiently on GPUs without directly solving an LP.

3 Neural Network Verification with General Cutting Planes

GCP-CROWN generalizes bound propagation to incorporate arbitrary cutting-plane constraints, including cross-layer and relaxed ReLU-indicator variables. It combines GPU-based branching with CPU-based MIP cut generation in a parallel verifier.

  • 3.1 GCP-CROWN: General Cutting Planes in Bound Propagation: The generalized propagation rule derives a valid lower bound by propagating dual variables layer by layer and optimizing α and β with gradient ascent.The resulting procedure can run on a GPU for acceleration.
  • 3.1 GCP-CROWN: General Cutting Planes in Bound Propagation: GCP-CROWN supports cutting planes involving pre-activation, post-activation, and ReLU-indicator variables from any network layer.This extends bound propagation beyond constraints limited to neighboring layers and explicitly accommodates relaxed integer variables.
  • 3.1 GCP-CROWN: General Cutting Planes in Bound Propagation: With all β set to zero, GCP-CROWN recovers the existing bound-propagation equations, while optimizing β makes its objective at least as strong.This establishes the earlier formulation as a special case of the generalized method.
  • 3.2 Branch-and-bound with GCP-CROWN and MIP Solver Generated Cuts: The verifier uses GCP-CROWN as the bounding procedure within branch-and-bound and obtains cutting planes from an off-the-shelf MIP solver.The MIP solver focuses on generating cuts, while GCP-CROWN performs branching and bounding.
  • 3.2 Branch-and-bound with GCP-CROWN and MIP Solver Generated Cuts: GPU bound propagation and CPU MIP cut generation run in parallel, with newly generated cuts added during branch-and-bound.The verifier queries MIP processes during each iteration and incorporates returned cuts into GCP-CROWN.

4 Experiments

Experiments evaluate GCP-CROWN with MIP cuts across oval20, VNN-COMP 2021, VNN-COMP 2022, and SDP-FO benchmarks. The method consistently improves verification performance, including complete oval20 coverage and substantially more verified oval21 instances.

  • All three oval20 models were solved without timeout, with average runtime below five seconds per instance.The slowest instance took only a few minutes, while easy instances took a few seconds.
  • 22 out of 27 oval21 instances were verified, twice the 11 verified by the best competition participants.
  • GCP-CROWN with MIP cuts achieved the best performance on cifar10-resnet, solving the most instances with the lowest average time.The comparison includes VNN-COMP 2021 participants, α-CROWN+MIP, and MN-BaB.
  • The VNN-COMP 2022 α,β-CROWN tool, which includes GCP-CROWN, verified 25 of 30 oval21 instances versus 19 for MN-BaB.
  • Verified accuracy improved on all seven SDP-FO models compared with state-of-the-art verifiers.The results also narrowed the gap between verified accuracy and empirical robust accuracy from PGD attacks.

5 Related Work

The paper situates GCP-CROWN within convex-relaxation and cutting-plane approaches for neural-network verification. It emphasizes that general cutting planes strengthen relaxed formulations, while existing verification methods often use more restricted relaxations.

  • Cutting planes strengthen convex relaxations in integer programming, with generic and problem-specific variants used in branch-and-cut solvers.
  • GCP-CROWN specializes cutting-plane use for neural-network verification while retaining fast lower-bound computation through bound propagation.
  • Piecewise-linear neural-network verification can be formulated as MIP, but recent methods often use linear or semidefinite convex relaxations for efficiency.

6 Conclusion

The paper presents GCP-CROWN as a GPU-accelerated bound-propagation method that handles arbitrary cutting-plane constraints and achieves strong benchmark performance. Its current scope is limited to ReLU networks, while generic MIP-generated cuts may not be optimal.

  • GCP-CROWN handles arbitrary cutting-plane constraints while combining GPU-accelerated bound propagation with branch and bound.
  • The method achieves state-of-the-art verification performance across multiple benchmarks by combining fast bound propagation with strong MIP-generated cuts.
  • The branch-and-bound and bound-propagation procedures are developed for ReLU networks, making extension to non-piecewise-linear operations non-trivial.
  • The current method directly uses cuts from a generic MIP solver, although stronger and faster neural-network-specific cutting-plane methods may exist.
  • A complete verifier could also help identify neural-network weaknesses and guide adversarial attacks.

Appendix

The appendix provides derivations, background, and additional experimental details for GCP-CROWN and its MIP-cut case study.

  • The appendix derives GCP-CROWN bound propagation and proves Theorem 3.1.
  • It also adds branch-and-bound background and presents further experiments and a case study using MIP cuts.

A The dual problem with cutting planes

The paper derives a dual formulation for verification with arbitrary cutting planes while retaining ReLU integer variables, then converts it into the sound GCP-CROWN bound-propagation rule.

  • A The dual problem with cutting planes: The formulation keeps original ReLU binary variables in the linearly relaxed MIP, allowing cutting planes to involve integer variables and neurons from any layer.This extends beyond the usual triangle relaxation, which omits the binary variables.
  • A The dual problem with cutting planes: The derivation introduces dual variables for arbitrary added linear constraints and uses strong duality to obtain a bound-propagation objective.The resulting dual includes variables associated with the cutting planes and network constraints.
  • A The dual problem with cutting planes: A technical lemma provides a closed-form optimization over paired nonnegative dual variables under a fixed-sum constraint.Its piecewise objective depends on whether q lies below, within, or above the interval determined by the ReLU bounds.
  • A The dual problem with cutting planes: Theorem 3.1 defines GCP-CROWN by substituting valid dual settings parameterized by α and β into the dual objective.The parameter α can be optimized during bound propagation, while β represents cutting-plane-related terms.
  • A The dual problem with cutting planes: GCP-CROWN is sound because every valid setting with 0 ≤ α ≤ 1 and β ≥ 0 yields a valid lower bound of the cutting-plane relaxation.The theorem explicitly establishes soundness, although optimizing α and β does not necessarily recover the optimal primal value.

B More technical details and background of GCP-CROWN with MIP cuts

GCP-CROWN strengthens branch-and-bound verification by adding cutting planes during bounding, reducing the branching burden while preserving soundness and completeness under valid cuts.

  • B More technical details and background of GCP-CROWN with MIP cuts: Branch-and-bound splits unstable ReLU neurons into cases, tightens lower bounds in each subdomain, and verifies any subproblem whose lower bound is positive.If all unstable neurons are split but a domain remains negative, a counterexample can be constructed.
  • B More technical details and background of GCP-CROWN with MIP cuts: Tighter bounds from cutting planes reduce the number of branch-and-bound subproblems needed to verify neural-network properties.Branching on unstable ReLUs creates subproblems, while positive lower bounds certify them without further splitting.
  • B More technical details and background of GCP-CROWN with MIP cuts: GCP-CROWN is the first bound-propagation method described here to support general cutting planes, including constraints across layers and cuts generated by a MIP solver.This combines the scalability of bound propagation with general cuts used in mathematical programming.
  • B More technical details and background of GCP-CROWN with MIP cuts: The method remains sound when valid cutting planes are added and complete when combined with branch-and-bound because its bounding step strictly improves over existing approaches.The soundness claim relies on Theorem 3.1 and valid cuts.

C.1 Experimental Setup

Experiments use the α,β-CROWN implementation with MIP-related code, combining CPU cores and one GPU across neural-network benchmarks with specified model structures.

  • C.1 Experimental Setup: Experiments run on an AMD Ryzen 9 5950X, one NVIDIA RTX 3090 with 24GB memory, and 64GB CPU memory.The evaluated α-CROWN+MIP and GCP-CROWN configurations use all 16 CPU cores and one GPU.
  • C.1 Experimental Setup: The benchmark models include CIFAR-10 Base, Wide, and Deep architectures used in the oval20 and oval21 evaluations.These structures are summarized alongside convolutional, linear, residual, and ReLU-layer notation.
  • C.1 Experimental Setup: Table 4 defines Conv, Linear, and ResBlock by their channel or feature dimensions and kernel size, with ReLU activations between consecutive linear or convolutional layers.The table specifies the model structures used in the experiments.

C.2 A case study on cutting planes

The oval21 case study evaluates MIP-generated cuts on 39 hard properties and finds that they substantially strengthen GCP-CROWN’s verification bounds. The generated cuts predominantly involve variables across multiple network layers.

  • Case-study setup: The study focuses on oval21’s 39 hard properties after filtering out cases that α-CROWN can verify directly.The benchmark contains 30 instances with 9 target properties each, totaling 270 properties before filtering.
  • Number of cuts: 1,683 cuts were applied on average to solve each hard property, with 318 to 4,162 cuts used per property.
  • Improvements on lower bounds: 0.51 average lower-bound improvement enabled direct verification of 4 of 39 hard properties without branching.The improvement ranged from 0.04 to 1.54, relative to an average α-CROWN lower bound of -2.54 without branching or cuts.
  • Structure of Generated Cuts: 65,647 cuts were generated across the 39 hard properties, and 65,301 involved variables from multiple layers.This indicates that single-layer cuts commonly used in prior work are not generally optimal.
Loading 2208.05740v2…