General Cutting Planes for Bound-Propagation-Based Neural Network Verification
Authors: Huan Zhang
Shiqi Wang
Kaidi Xu
Linyi Li
Bo Li
Suman Jana
Cho-Jui Hsieh
J Zico Kolter
Venue: NeurIPS 2022 Accept (2022)
Keywords: neural network
formal verification
adversarial robustness

Abstract: 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 $\alpha,\beta$-CROWN verifier, the VNN-COMP 2022 winner. Code is available at http://PaperCode.cc/GCP-CROWN.

General Cutting Planes for Bound-rropagatinnBaseed Neural Network Verification
Huan Zhang
Shiqi Wang
Kaidi Xu -3
Linyi Li
Bo Li
Suman Jana?
Cho-Jui Hsich J. Zico Kolter
CMU
PColumbia University
*Drexel University "IICC SUCLA "Bosch Center for Al
huan@huan-zhen zhang. com
sx32158colubbaa edu kx46edrexel.
Linyi2@illinois
edu edu
1bo@illinois edu sumanØcs. cowumbia. edu
chohsieh@cs ucla. edu zkolterêcs. cmu.edu
Equal Contribution
Abstract
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. this paper, generalize the bound propagation procedure to allow the addition 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 apply general cutling plane methods for neural network verification while ben- efiting 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-pre propagation-basee verifiers using our new formulation. Since the branching- focused bound propagation proce- dure and the 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 benchmarks. GCP-CROW is part of
focused MIP solver can run parallel utilizing different
verifier, the VNN-COMP 2022 winner. Code available at htttt::/PapperCode CC/GCP-CROWN
Introduction
Neural network (NN) verification aims to formally prove or disprove certain properties (e.g., cor- rectness and safety properties) of a NN under a certain set of inputs. These methods can provide worst-case performance guarantees a NN, and have been applied mission-critical applications that involve neural networks, such as automatic aircraft control 31 4), learning sarning-enabled eyber-
systems [54], and NN based algorithms in an operating system 511
The NN verification problem is generally NP-complete 30
For piece-wise linear networks, it can be encoded as mixed integer programming (MIP) 53 problem with the non-linear ReLU neurons
36th Conference on Neural Information Processing Systems (NcurIPS 2022).

---

described by binary variables. Thus, fundamentally, the NN verification problem can be solved using the branch and bound (BaB) [TO] method similar to generic MIP solvers, by branching some binary variables and relaxing the rest into a convex problem such as linear programming (LPP) to obtain bounds on the objective. Although early neural network verifiers relied on off-the-shelf CPU-based LP solvers [36] 9 for bounding in BaB, LP solvers do not scale well to large NNs. Thus, many recent verifiers are instead based on efficient and GPU-accelerated algorithms customized to NN
verification, such as bound propagation methods 160| 157. Lagrangian decomposition methods [8] 17
and others [66 IT.
Bound propagation methods, presented in a few different formulations [58
18
56
61
50
25 empower state-of- of-the-art NN verifiers such as a,B-CROWN [61 60 57 and
VeriNet B and can achieve two to three orders of magnitudes speedup compared to solving the NN verification problem using off-the-shell solver directly [57], especially on large networks.
Despite the success of existing NN verifiers, we experimentally find that state-of-the-art NN verifiers may timeout on certain hard instances which a generic MIP solver can solve relatively quickly, sometimes even without branching. Compared to an MIP solver, crucial factor missing in most scalable NN verifiers is the ability to efficiently generate and solve general cutting planes (or "cuts"). In generic MIP solvers, cutting planes are essential to strengthen the convex relaxation, so that much less branching is required. Advanced cutting planes are among the most important factors in modern MIP solvers [6]; they can strengthen the convex relaxation without removing any valid integer solution from the MIP formulation. In the setting of NN verification, cutting planes reflects complex intra-layer and inter-layer dependencies between multiple neurons, which cannot be easily captured by existing bound propagation methods with single neuron relaxations [5]. This motivates us to seek the combination of efficient bound propagation method with effective cutting planes to further increase the power of NN verifiers.
few key factors make the inclusion of general cutting planes in NN verifiers quite challenging. First, existing efficient bound propagation frameworks such as CROWN [6] and B-CROWN (57] cannot solve general cutting plane constraints that may involve variables across different layers in the MIP formulation. Particularly, these frameworks do not explicitly include the integer variables in the MIP formulation that are crucial when encoding many classical strong cutting planes, such as Gomory cuts and mixed integer rounding (MIR) cuts. Furthermore, although some existing works [47 52 40) enhanced the basic convex relaxation used in NN verification (such as the Planet relaxation [9] these enhanced relaxations involve only one few neurons in single layer two adjacent layers, and are not general enough. In addition, an LP solver is often required to handle these additional cutting plane constraints 400, for which the efficient and GPU-accelerated bound propagation cannot be used, so the use of these tighter relaxations may not always bring improvements.
In this paper, we achieve major progress in using general cutting planes in bound propagation based NN verifiers. To mitigate the challenge of efficiently solving general cuts, our first contribution is to generalize existing bound propagation methods to their most general form, enabling constraints involving variables from neurons of any layer as well as integer variables that encode the status of a ReLU neuron. This allows us to consider any cuts during bound propagation without relying slow LP solver, and opens up the opportunity for using advanced cutting plane techniques efficiently for the NN verification problem. Our second contribution involves combining off-the-shelf MIP solver with our aPU-accelerated, branching- focused bound propagation method capable of handling general cuts. We entirely disable branching in the MIP solver and use it only for generating high quality cutting planes not restricting to neurons within adjacent layers. Although an MIP solver often cannot verify large neural networks, we find that they can generate high quality cutting planes within a short time, significantly helping bound propagation to achieve better bounds.
Our experiments show that general cutting planes can bring significant improvements to NN verifiers: we are the first verifier that completely solves all instances in the oval20 benchmark, with an average time of less than 5 seconds per instance; on the even harder oval21 benchmark in VNN- COMP 2021 [] we can verify twice as many instances compared to the competition winner. We also outperform existing state-of-the-art bound- propagation- based methods including those using multi-neuron relaxations [20 (a limited form of cutting planes).
2 Background
The NN verification problem We consider the verification problem for an L-layer ReLU-based
Neural Network (NN) with inputs (0)) ;= E do, weights w e xRd.xd.-1, and biases
2

---

b(a) E Rd E f1,...,,I,, We can get the NN outputs f(x) x (T) E R by sequentially propagating the input a through affine layers with x(0) = ((-)) + b(3) and ReLU layer with a(+)) = (a))). We also let scalars f and z (5) denote the post-activation and pre-activation, respectively, of j-th ReL.U neuron in i-th layer. Throughout the paper, we use bold symbols to denote (() is the j-th element of x+)). We use the shorthand [V] to denote {1, .N). and w! is the j-th column of W
vectors (e.g., ()) and regular symbols to denote scalars (e.g., .r)
..j
Commonly. the imput a is bounded within a perturbation set C. (such as an Ep norm ball) and the verification specification defines a property of the output f(x) that should hold for any æ C. e.g., whether the true label's logit (a) will be always larger than another label's logit (a),, (i.e., checking if fz())) fa) is always positive). Since we can append the verification specification (such as linear function on neural network output) as an additional layer of the network, canonically, the
NN verification problem requires one to solve the following miedimensional (d, 1) optimization objective on (x)
I = min (a+), Va EC
(I)
x
with the relevant property defined to be proven if the optimal solution I* 2 0. Throughout this work, we consider the Loo norm ball C == fær ||æ sollos S e) where zo is predefined constant (e.g..
clean input image), although it is possible to extend to other norms or specifications 43 59
The MIP and LP formulation for NN verification The mixed integer programming (MIP) formulation is the root of many NN verification algorithms. This formulation uses binary variables z to encode the non-linear ReLU neurons to make the non-convex optimization problem (1) tractable.
Additionally, we assume that we know sound pre-activation bounds ((9) < x S (x() for æ E C
which can be obtained via cheap bound propagation methods such as IBP 23 or CROWN [6].
Then ReLU neurons for each layer can be classified into three classes (58) namely "active" (I (())), "inactive" (I (1) and "unstable" (I()) neurons, respectively:
I I+(0 = [j 1/0) 2 0); I- := {j: u5 00; It : (j: 1/" so u 2 0}
Based on the definition of ReLU, activate and inactive neurons are linear functions, so only unstable neurons require binary encoding. The MIP formulation of ① is:
f min f(x) 222,2
s.t. f(x) xz (4);
a
x E C:
(2)
z Wi +b(0; iE [E]
(3)
8 (0
2 0: jEZ 2 [L-1]
(4)
4 2 3j
JEI 1E [-
(5)
8 S Su 33 j jEI [L-1]
0
(6)
1 <0) ( (1-2)))))) JEI E [L-1]
(7)
2 (0.1) jEI",iE|L1
(8)
(
iE
(9)
(0) = 0; jEz-W,iEEL--
(10)
Since MIP problem is slow intractable to solve, it is commonly relaxed When the integer variables are relaxed to continuous ones, we obtain the LP relaxation of NN verification problem:
fip
min f(x)
2.P.
s.t.
0 05
<1; , [T-1]
(11)
The ReLU constraints involving is often projected out, leading to the well-known Planet relaxation used in many NN verifiers, replacing (6) and (8) with single constraint to get an equivalent LP:
f min f(x)
2,2
6
s.t.0
3
2
4
100
S
(x))) - -100) 1
(E(L-1) (12)
(1)
új
3

---

The minimization on linear layer can be solved easily when C is Ep norm ball to obtain a valid lower bound of f Since the bounds propagate layer-by-layer, this process can be implemented efficiently slow I.P solver, which greatly improves the scalability and solving Due to the relaxations, the objective of the LP formulation is always a lower bound of the MIP formulation: fip S fr. A verifier using this formulation is incomplete: if fir 2 O, then f 2 and the property is verified; otherwise, we cannot conclude the sign of f* so the verifier must return "unknown". Branch and bound can used improve the lower bound and achieve completeness [10 [57. However, in this paper, we work on an orthogonal direction of strengthening the LPP formulation by adding cutting planes to obtain larger bounds.
Bound propagation methods Instead of solving the LP formulation directly using a LP solver, bound propagation methods aims to quickly give a lower bound for fi.. For example, CROWN [6]] and B-CROWN [57] propagate a sound linear lower bound backwards for fL (a) with respect to each intermediate layer. For example, suppose we know
min fr.( 2 min a (1) c! sEe
(13)
With = L the above is trivially hold with a (1-1) = W(O), cll- = b In bound
propagation methods, a propagation rule propagates incquality (13) through a previous layer (()) = ReLUU((() ((-1) + b() to obtain a sound inequality with respect to (1-1))
min (x) 2 min a (1-1) (.(1-1) + (f-1))
#Ec
#EC
Here a clt-1) can be calculated in close-form via (1) cl)), W b 100 and ( such that the bound still holds (see Lemma in (57). Applying the procedure repeatedly will eventually reach the input layer:
min fz min a EEC
x + co0)
(14)
#EC
on GPUs (59 without relying
time. Additionally, it is often used to obtain intermediate layer bounds ((0) and and (+)) required for
the MIP formulation (6) by treating each .z.") the output neuron. The bound propagation rule can either be derived in primal space [61], dual space (58) or abstract interpretations [50). In S.c we will discuss the our bound propagation procedure with general cutting plane constraints.
3 Neural Network Verification with General Cutting Planes
3.1 GCP-CROWN: General Cutting Planes in Bound Propagation
In this section, we generalize existing bound propagation method to handle general cutting plane constraints. Our goal is to derive a bound propagation rule similar to CROWN and 3--CRON discussed in Section 2] however considering additional constraints among any variables within the LP relaxation. To achieve this, we first derive the dual problem of the LP; inspired by the dual formulation, derive the bound prorogation rule in a layer by layer manner that takes all cutting
plane constraints into consideration. The derivation process is inspired by [58 45 and (5].
LP relaxation with cutting planes. In this section, we derive the bound propagation procedure under the presence of general cutting plane constraints. A cutting plane a constraint involving any variables (1) (pre-activation), a(() apost-activation), (0)) (ReLU indicators) from any layer
Σ
( (0) + (() 2 - ((0) z
<d
Here h0, gl and 90)) coefficients for this cut constraint. The difference between valid cutting plane and an arbitrary constraint is that a valid cutting plane should not remove any valid integer solution from the MIP formulation. Our new bound propagation procedure can work for any constraints, although in this work we focus on studying the impacts of cutting planes. When there are N cutting planes, we write them in a matrix form:
H 0
( + GG G +Q())(0)) S d
(15)

---

where H GO
E RNdd The LP relaxation with all cutting planes is:
P min a.
(x)
0 O5 ( S1; j JE [L-1]
s.t.
Σ (H G Q (0)(1)) S d
(16)
Since an additional constraint is added, fir 2 fip and we get closer to f Unlike the original LP where each constraint only contains variables from two consecutive layers, our general cutting plane constraint may involve any variable from any layer in a single constraint.
The dual problem with cutting planes We first show the dual problem for the above LP. The dual problem we consider here different from existing works in two ways: first, we have constraints with integer variables to support potential cutting planes z. Additionally, we have cutting planes constraints that may involve variables in any layer, so the dual in previous works such as [58] cannot be directly reused. Our dual problem is given below (derivation details in Appendix A):
Sip-cu
max V.220,,300 20 7 220.m20,320
- -E|L ( voll1 - -3 d
Σ
1 ReLU (2 + 1, -
B 0
i=1 jEZO)
s.t. w (1) 1; and for each E [L 1]:
2/ (1) y (++I) ((+1) B (H + G jEZ(
(6) ST H (1) E (5)
and for each j E (())
the two equalities below hold:
50 = 10 3 H::
(T. + -1))-(1)) - + -1)"
((+1)) w(++1) 3 G
Instead of solving the dual problem exactly, we due to the definition of due problem, any valid setting of dual variables leads to a lower bound of für-cur- Informally, starting from (L) 11, by applying the constraints in this dual formulation, we can compute (1--1) pl.-2), ... until (1), The final objective is a function of (1) i e [NV and
obtain lower bound of f Intuitively,
other dual variables. Precisely, GCP-CROP CROWN bound propagation procedure with general cutting plane constraint is presented in the theorem below (proof in Appendix AA::
Theorem 3.1 (Bound propagation with general cutting planes). Given any optimizable parameters (1) 0 O < and B 2 fir is lower bounded by the following objective function, πj is function of !.
g(a, = -e]lp((1T ( w() Σ LOO d
d+
Σ Σ (8)
2=1 jEZO)
where variables (+) are obtained by propagating w(L) -1 throughout all i E [L-1]:
w1() (++1T w(++1) 33 (TH + Gb3), jEI(()
( -B H. jEI
u n -a 10
(0) (1)* (0
B T j E I(1)
Here of0) (*)
and h (1) (B) are defined for each unstable neuron j Ito.
o/01 ((++))T (++1)
(TG( 1 (1)
1.
1 + BT Q
(8) =
11/0 .0)
max
min
(6) 10
u
5

---

10)
if 1,00 10
SBQ S su,
h
0
if B
if
B
T isa IsafunctionofQ
Based on Theorem 3.1 to obtain an lower bound of fi we start with any valid setting of 0 S < 1 and / and p(L) -1. According to the bound propagation rule, we can compute each u(), i E [L [L-1], 11.
in a layer by layer manner. Then objective g(a, (3) can be evaluated based on all 216) to give an lower bound of [[ Since any valid setting of a and (3 lead to a valid lower bound, we can optimize a and B3 using gradient ascent a similar manner as in [60] [5) to tighten this lower bound. The entire procedure can also run on GPU for great acceleration.
Connection to Convex Outer Adversarial Polytope In convex outer adversarial polytope (58). bound propagation rule was developed in similar manner in the dual space without considering cutting plane constraints, and is special case of ours. We denote their bound propagation objective function as gwx which also contains optimizable parameters OwKK.
Proposition 3.2. Given the same input æ, perturbation set C, network weights, and N cutting plane constraints,
max ax Z max gwx (Oxwx) 0
1 and (3) = - -0''00
Proof. In Theorem 3.1. when all /3 are set to O, then
recover exactly the same bound propagation equations in addition of cutting plane methods and we can maximize over the additional parameter B, the objective given by our bound propagation always at least as good as gwK.
(58) However, since allow the
Connection to CROWN-like bound propagation methods CROWN 66 and a-CROWN [60] use the same bound propagation rule as [58] so Proposition 3.2 also applies, although they were derived from primal space without explicitly formulating the problem as a LP. Salman et al. 45
showed that many other bound propagation methods [50, (55) are equivalent to or weaker than 58
Recently, Wang et al. (57) extends CROWN to 3-CROWN to handle split constraints (c.g., zj 2 0). It can be seen a special case as GCP-CROWN where all H, G and Q matrices are zeros except:
1.j I (1)
(1) for zj < 0 split;
( / = - H
( for a
split
In addition, 20 encodes multi-neuron relaxations using sparse (+) and G1 and each cut contains small number of neurons involving (i) and (+) for the same layer i. Wang et al. [57] derived bound propagation rules from both the dual LP and the primal space with a Lagrangian without LP.
However, in our case, it is not intuitive to derive bound propagation without I.P due to the potential cutting planes on relaxed integer variables z, which do not appear without the explicit LP formulation. Furthermore, although we derived cutting planes for bound propagation methods, it is technically also possible to derive them using other bounding frameworks such as Lagrangian decomposition [8]
3.2 Branch-and-bound with GCP-CROWN and MIP Solver Generated Cuts
To build complete NN verifier, we follow the popular aanch-anddbound (BaB) procedure 10
9
in
state-of-the-art NN verifiers with GPU accelerated bound propagation method g 60
16
57 and
our GCP-CROWN is used as the bounding procedure in BaB. We refer the readers to Appendix for Having the efficient bound propagation procedure with general cutting plane constraints, we now need to find good set of general cutting planes H ( ((+) to accelerate NN verification. Since GCP-CROWN can adopt any cutting planes, to fully exploit its power, we propose to use off-the-shelf MIP solvers to generate cutting planes and create an NN verifier combining GPU-accelerated bound propagation with strong cuts generated by MIP solver. We make the bound propagation on GPU and the MIP solver on CPU run in parallel with cuts added on-the-fhy fly, so the original strong performance of bound- propagation-basee
a more detailed background on branch-and-bour

---

NN verifier will never be affected by potentially slow MIP solver. This allows us to make full use of available computing resource (GPU + CPU). The architecture of our verifier shown in Fig
MIP solvers for cutting plane generation Generic MIP solvers such as cplex (8 and gurobi [24] also apply branch-and-boun strategy, conceptually sim- ilar to state-of-the-art NN verifiers. They often tend to be slower than specialized NN verifiers because MIP solvers rely on slower bounding procedures (e.g.. Simplex or barrier method) and cannot apply an GPU-accelerated method such as bound propa- gation or Lagrangian decomposition. However, still find that MIP solvers are a strong baseline when combined with tight intermediate layer bounds. For example, in the oval21 benchmark in Table 2 a- CROWN+MIP (MIP solver combined with tight in- termediate layer bound computed by a-CROWN) is able to solve 4 more instances compared to all other tools in the competition. Our investigation found that a- a-CROWN+MII explores much less branches than other state-of-the-art branch-ane and-bound based NN verifiers, however before branching starts, the MIP solver produces very effective cutting planes that can often verify an instance with little branch- ing. MIP solvers is able to discover sophisticated cutting planes involving several NN layers reflecting complex correlations among neurons, while existing NN verifiers only exploit specific forms of constraints within same layer or between adjacent lay- ers [52 47 40). This motivates us to combine the strong cutting planes generated by MIP solvers soundd-ropggttionbbee based BaB.
Main Process
MIP Solver
Generic NN Parser
Coordination
Process
MIP Encoder
NN Verifier
Launch MIP Solver
Branching
solvers
Processes
Terminane
Loop
Parallelized MIP Solver
Fetching General
domain
remains
Cutting Planes
on CPU for Different
Pick domains
Real-time cutting planz
GPU-Accelerated GCP-CROWN
fesching upun
Labels
poneration
Terminate
Figure 1: Overview of our tutting-plane, enhanced, pallalppaalee NN verifier.
with GPU-accelerated
In this work, we use cplex as the MIP solver for cutting plane generation since gurobi cannot export cuts. We entirely disable all branching features in cplex and make focus on finding cutting planes only. These cutting planes are generated only for the root node of the BaB search tree so they are sound for any subdomains with neuron splits in BaB. We conduct branching using our generalized bound propagation procedure in Section 33.1 with the cutting planes generated by cplex.
Fully-parallelized NN verifier design We design our verifier as shown in Figure I After parsing the NN under verification, we launch separate process to encode the NN verification problem as MIP problem and start multiple MIP solvers, one for each target label to be verified. At the same time, the main NN verifier process executes branch-and bound without waiting for the MIP solver process. In each iteration of branch and bound, we query the MIP solving processes and fetch any newly generated cutting planes. If any cutting planes are produced, they are added (6), G6), Q!i in GCP-CROWN and tighten the bounds for subsequent branching and bounding. If no cutting planes are produced,
reduces to 3-CROWN [57]. Since our verifier based on strengthening the bounds in 3-CROWN with sound cutting planes, it is also sound and complete.
Adjustments to existing branch and bound method. We implement GCP-CROWN into the ORB-CROWN verifier [61] 59 (77. the winning verifier in VNN-COMP 2021 33 as the backbone for BaB with bound propagation. To better exploit the power of cutting planes under fully parallel and asynchronous design, we made a key changes to the BaB procedure. When the number of BaB subdomains are greater than batch size, we rank the subdomains by their lower bounds and choose the easiest domains with largest lower bounds first to verify with GCP-CROWN, unlike most existing verifiers which solve the worst domains first. We use such a order because the MIP solver generates cutting planes incrementally. Solving these easier subdomains tend to require no or fewer cutting planes, so we solve them earlier stages where cutting planes have not been generated or are relatively weak. On the other hand, if we split worst subdomains first, the number of subdomains will grow quickly, and can take a long time to verify these domains when stronger cuts become available later. Under similar rationale, when verifying a multi-class model and BaB needs to verify each
7

---

Table 1: Average runtime and average number of branches oval20 benchmarks with 100 properties per model. Timeout set to 3,600 seconds (consistent with other literature results). GCP-CROWN is the only method that can completely solve all instances (0% timeout) and the average time per-instance is less than seconds on all three networks.
CIFAR- 10 Base
CIFAR-10 Wide
CIFAR-10 Deep
Method
timo(s)
branches
XEtimeout
timo(s)
branches
Sttimeout
time(s)
branches
Atimoout
MiPplanct
2849.69
68.00
2417.53
46.00
2302.25
40.00
BaBSR
2367.78
1020.55
36.00
2871.14
812.65
2750.75
401.28
GNN online
56
1794.85
565.13
33.00
1367.38
372.74
15.00
1055.33
131,85
4,00
BDD+ RaBSR
807.91
195480.
20.00
505.65
74203.1
10.00
12722.74
Fast-and-Complite
(0
695.01
19522.665
17.00
495. 88
80519.85
9.00
105. 64
2455.11
1.00
(BDD+ GNN)
36
662.17
67938.38
16.00
280.38
17895.94
6.00
94.69
1990.34
1.00
A.set BaBSR
[66]
381.78
12004 60
7.00
165.91
2233. 10
3.00
190.28
2491.55
2,00
BigM+A.set set BaBSR
[T6]
190.44
11338.75
7.00
172.65
4050.50 59
3.00
177.22
3275.25
2.00
BaDNB (BDD+
17
38239.04
7,00
11214.44
10.50
368.16
ERAN" E7 48
49
805.94
5.00
632.20
9.00
545.72
0.00
8-CROWN
118.23
208018.21
3.00
78.32
116912.57
2.00
5.69
41.12
0.00
D-CROWN+MEL
335.50
8523.37
3.00
203.87
2029.60
0.00
76.90
1364,24
0.00
GCP-CROWN with MIP cuts
4.07
2580.53
0.00
3.02
2095. 18
0.00
3.87
110.92
0.00
Results from VNN COMP 2020 report
34
A new haseline progused and evaluated in this work, not presented in previous pupers.
100%
100%
100%
BDD+ Sabsn
80%
80%
80%
Fast Complete
ASc: budch
DWAi Comn-Comp 205
00%
60%
60%
DDDN 75th
Megieeee SABER
40%
40%
40%
20%
GCP-GROUN-NP..CM
100
100
1900
10
1000
1000
10
100
1000
CIFAR-10 Base: Running time (In s)
CIFAR-10 Wide Running time (In s]
CIFAR-10 Desp: Running tim a inn s)
Figure 2: Percentage of solved properties on the oval20 benchmark vs. running time (timeout hour).
target class label one by one, we start BaB from the easiest label first (a-CROW bound closest to 0), allowing the MIP solver run longer for harder labels, generating stronger cuts for harder labels.
4 Experiments
We now evaluate our verifier, GCP-CROWN with MIP cuts, on a few popular verification benchmarks. Since verifier uses MIP solver in pipeline, we also include new baseline, a-CROWN+MIP which uses gurobi as the MIP solver with the tightest possible intermediate layer bounds from a-CROWN [59]. We use the same branch and bound algorithm in 3-CROWN and we use filtered smart branching (FSB) [6] as the branching heuristic in all experiments. Without cutting planes, GCP-CROWN becomes vanilla 3-CROWN as we share the same code base as B-CROWN. We include model information and detailed setup for our experiments in Appendix C GCP-CROWN has been integrated into the Ne,8-CROWY (alpha-beta- bee--C verifier, and the instructions reproduce results in this paper are available at http::/PapprrCooe wateeecccccC/e.e cc/GCP-CROWI
Results on the oval20 benchmark in VNN-COMP 2020. oval20 popular benchmark consistently used in huge amount of NN verifiers and it perfectly reflects the progress of NN verifiers. We include literature results for many baselines in Table T We are the only verifier that can completely solve all three models without any timeout. Our average runtime is significantly lower compared to the time of baselines because we have no timeout (counted as 3600s), and our slowest instance only takes about a few minutes while easy ones only take few seconds, as shown in Figure Additionally, we often use less number of branches compared the state-of-the-ee verifier, 3-CROWN, since our strong cutting planes help us to eliminate many hard to solve subdomains in BaB. Furthermore, we highlight that a-CROWN+MIP also achieves a low timeout rate, although it is much slower than our bound propagation based approach combined with cuts from a MIP solver.
Results on VNN-COMP 2021 benchmarks. Among the eight scoring benchmarks VNN-COMP 2021 3. only two (oval21 and 1.far10-resnet, are most suitable for the evaluation of this work. Among other benchmarks, acasxu and nn4sys have low input dimensionality and require input space branching rather than ReLU branching; verivital, mnistfc, and eran benchmarks consist of
8

---

Table 2: VNN-COMP 2021 benchmarks: oval21 and cifari0- Results marked with VNN-COMP are from publicly available benchmark data on VNN-COME 2021 Github. "." indicates unsupported model.
ova121 (30 propenies PGD upper bound cifar10-reanet (72 properties)
Method
lime(s)
# verified
Stmeout
time(s)
verilled
Stimeout
nucnum
2
630.06
2
86.66
Marabou'
31
429.15 13
5
73.33
157.70
39
45.83
BRAN
233.84
70.00
129.48
40.28
OVAL.
Lk
16
393.14
II
53,33
VeriNet
2b
414.61
11
53.35
105.91
48
33,33
0.8-CROWN
61
60 57]
395.32
11
53.33
99.87
58
19.44
MN-BaB
20
435.46
10
56.66
Venus2t
386.71
17
33.33
CRIOWNMMPP
301.23
15
40.00
125.48
46
36, 11
GCP-CROWN with MIP cuts
145.26
23
13.33
53.49
63
12.5
Results from VNN-COMP 2021 report 3
We use the latest code of Venus2 in the vanconp branch, committed on 18, 2022. Older versions cannot run these convolutional networks.
Table 3: Verified accuracy (%) and avg. per-example verification time (s) on 7 models from SDP-FO 13
Dosset
Model 0.3.md
SDP PO
[5
PRIMA
(.CROWN
MIN Vtr.
BuB
CRRONNIMP
GCP GRWNN
Upper hnnrd
2/285
Veribat'
Time
Vor.s.
Timet))
Ver
Vor.5
Vaz.9i
Tinz(s)
Ver.7
Timets)
SINIST
A-d-A-Ade
43.4
520h
44.5
135.9
70.5
21.1
35.5
148.4
56.5
224
72,0
19,9
76,5
CRN Adr
123
0:55
35.5
343.5
46.5
32.2
27.3
10055
-6.5
51.8
[000
CNN-B-Add-4
46.0
3.25
$3.5
41.5
54.0
11.6
52.5
125.5
39.0
21.5
63.5
CHRAR
CNS.A-Adle4
UNN A-A
39.0
-250
0-25
41.5
4.5
46.0
46.0
5.8
5.6
42.5
46.0
68.3
47.5
26.0
13.1
46.0
63.3
48.5
9.8
50.0
CNN-A-Mic-4
40.0
We N-UM and MIN (Bll (405s sheedhold for models. *7 Indicaees that could model das model other We revulls Ocher reparted from
OCP-CROWN with MIP with aktrizr 200. timovur for modek and athizves better verileed thas other baadiino. Ocher
5r
small MLP networks that can be solved directly by MIP solvers; marabou contains mostly adversarial examples, making it a good benchmark for falsifiers rather than verifiers. We present our results 2021 participants, we also include two additional
in T Besides results from 6 VNN-COME baselines, a a-CROWN=MIP (same as in Table D. and MN-BaB [20]. recently proposed branch and bound framework with multi-neuron relaxations (39). which can be viewed as a restricted form of cutting planes. On the oval21 benchmark, OVAL, VeriNet and q,3-CROWN are the best performing tools, verified 11 out of 27 instances, while we can verify twice more instances (22 out of 27) on this benchmark. On the 1effar1-rresin instances and achieves the lowest average time. In fact, a-CROWN+MIP is also a strong baseline, solving more instances than all competition participants, showing the importance of strong cutting planes. Our GCP-CROWN with MIP cuts combines the benefits of fast bound propagation on GPU with the strong cutting planes generated by a MIP solver and achieves the best performance. We present a more detailed analysis on the cutting planes used in this benchmark in Appendix C.2
benchmark, our verifier also solves the most number of
The ova121 benchmark was also included as part of VNN-COMP 2022, concluded in July 2022, with a different sample of 30 instances. GCP-CROWN is part of the winning tool in VNN-COMP 2022, 9-CO-R, which verified 25 out of 30 instances in this benchmark, outperforming the second place tool (MN-BaB (20 with multi-neuron relaxations) with 19 verified instances by a large margin. More results on VNN-COMP 2022 can be found in these slide
Results on SDP-FO benchmarks. We further evaluate our method on the SDP-FO benchmarks
in [15] 57]. This benchmark contains 7 mostly adversarially trained MNIST and CIFAR models with
200 instances each, which are hard for many existing verifiers. Beyond the baselines reported in (57). we also include two additional baselines, a-CROWN N+ MIP (same as in Table and MN-BaB (20 (same as in Table 2). Table ( shows that our method improves the percentage of verified images ("verified accuracy") on all models compared to state-of-the-as verifiers, further closing the gap between verified accuracy and empirical robust accuracy obtained by PGD attack (reported as "upper bound" in Table
5 Related Work
Cutting plane method is a classic technique to strengthen the convex relaxation of an integer pro- gramming problem. Generic cutting planes such as Gomory's 's cut 21 22 Chvátal-Gomory cut [2].
AA formal competition report is under preparation by VNN-COMP organizers; scores were presented in FLoC 2022: //drive.././///e//e http://www.....oooooooooooooaaaa

---

implied bound cut (27). lift-and lift-and-project B3 reformulation-lineante
techniques [46] and mixed
integer rounding cuts [1 37 can be applied to almost any LP relaxed problems, and problem specific
cutting planes such as Knapsack cut [14] Flow-cover cut [2 and Clique cut [29] require specific problem structures. Modern MIP solvers typically uses a branch-and-cut strategy, which tends to generate large number of cuts before starting the next iteration of branching, and solve the LP relaxation of the MIP problem with cutting planes with an exact method such as the Simplex method. is specialized solver for the NN verification problem, which can quickly obtain a lower bound of the LP relaxation with cutting planes specially for the NN verification problem.
Our
The verification of diece-wise linear NNs can be formulated as MIP problem, so early works [30 [3 [53] solve an integer or combinatorial formulation directly. For efficiency reasons, most recent works use a convex relaxation such as linear relaxation 19 58 or semidefinite relaxation 44 [5]. Salman et al. [45] discussed the limitation of many convex relaxation based NN verification algorithms and coined the term "convex relaxation barrier", specifically for the popular single-neuron "Planet" relaxation [9]. Several works developed novel techniques to break this barrier. 47 added constraints that depends on the aggregation of multiple neurons, and these constraints were passed to LP solver. 40) enhanced the multi-neuron formulation of [47) to obtain tighter relaxations. M studied stronger convex relaxations for ReLU neuron after an affine layer, and [52] constructed efficient algorithms based on this relaxation for incomplete verification. [16] extended the formulation in [I to a dual form and combined it with branch and bound to achieve completeness. (7] proposed specialized cuts by considering neuron dependencies and solve them using a MIP solver. (20) combined the
multi-neuron relaxation [40] with branch and bound. Although these works can be seen as a special form of cutting planes, they mostly focused on enhancing the relaxation for several neurons within single layer two adjacent layers. GCP-CROWN can efficiently handle general cutting plane constraints with neurons from any layers in a bound propagation manner, and the cutting planes we find from MIP solver can be seen as tighter convex relaxations encoding multi-neuron and multi-layer correlations.
Conclusion
In this paper, we propose GCP- SCP-CROWN, an efficient and GPU-accelerated bound propagation method for NN verification capable of handling any cutting plane constraints. We combine GCP-CROW) with branch and bound and high quality cutting planes generated by a MIP solver to tighten the convex relaxation for NN verification. The combination of fast bound propagation and strong cutting planes lead to state-of-the-ar verification performance on multiple benchmarks. Our work opens up a great opportunity for studying more efficient and powerful cutting planes for NN verification.
Limitations of this work Our work generalizes existing bound propagation methods that can handle only simple constraints (such as neuron split constraints in 33-CROWN 57 to general constraints, and we share few common limitations as in previous works 10
60 16: the branch-and-bound
procces and bound propagation procedure are developed on ReLU networks, and can be non-trive non-trivial to extend it to neural networks with non-piecewise-lines operations. In addition, we currently directly use cutting planes generated by a generic MIP solver, and there might exist stronger and faster cutting plane methods that can exploit the structure of the neural network verification problem. We hope these limitations can be addressed in future works.
Potential Negative Societal Impact Our work focuses on formally proving desired properties of neural network under investigation such as safety and robustness, which is an important direction of trustworthy machine learning and has overall positive societal impact. Since our verifier is complete verifier, it might be possible to use it to find weakness of a neural network and guide adversarial attacks. However, we believe that formally characterizing model's behavior and potenti al weakness is important for building robust models and preventing real-world malicious attack.
Funding Disclosure This work is partially supported by the NSF grant No. 1910100, NSF CNS No. No.2046726, NSF IIS No.2008173 NSF IIS No. 2042008 and the Alfred P. Sloan Foundation. Huan Zhang supported by a grant from the Bosch Center for Artificial Intelligence. Suman Jana acknowledges the NSF CAREER award.
10

---

References
[1] Ross Anderson, Joey Huchette, Christian Tjandraatmadja, and Juan Pablo Vielma. Strong convex relaxations and mixed-integer programming formulations for trained neural networks. In Mathematical Programming, 2020.
[2] Stanley Bak. nnenum: Verification of relu neural networks with optimized abstraction refinement. In NASA Formal Methods Symposium, pages 19-36. Springer, 2021.
[3] Stanley Bak, Changliu Liu, and Taylor Johnson. The second international verification of neural networks competition (vnn-comp 2021): Summary and results. arXiv preprint arXiv:2109.00499, 2021.
[4] Stanley Bak, Hoang- Dung Tran, Kerianne Hobbs, and Taylor T. Johnson. Improved geometric path enumeration for verifying relu neural networks. In Proceedings of the 32nd International Conference on Computer Aided Verification. Springer, 2020.
[5] Dimitris Bertsimas and Robert Weismantel. Optimization over integers. Athena Scientific, 2005.
[6] Robert Bixby and Edward Rothberg. Progress in computational mixed integer programming look back from the other side of the tipping point. Annals of Operations Research, 149(1):37-41, 2007.
[7] Elena Botoeva, Panagiotis Kouvaros, Jan Kronqvist, Alessio Lomuscio, and Ruth Misener. Efficient verification of relu-based neural networks via dependency analysis. In AAAI Conference on Artificial Intelligence (AAAI), 2020.
[8] Rudy Bunel, Alessandro De Palma, Alban Desmaison, Krishnamurthy Dvijotham, Pushmeet Kohli, Philip H. S. Torr, and M. Pawan Kumar. Lagrangian decomposition for neural network verification. Conference on Uncertainty in Artificial Intelligence (UAI), 2020.
[9] Rudy Bunel, Jingyue Lu, llker Turkaslan, P Kohli, P Torr, and P Mudigonda. Branch and bound for piecewise linear neural network verification. Journal of Machine Learning Research (JMLR), 2020.
[10] Rudy R Bunel, I1ker Turkaslan, Philip Torr, Pushmeet Kohli, and Pawan K Mudigonda. A unified view of piecewise linear neural network verification. In Advances in Neural Information Processing Systems (NeurIPS), 2018
[11] Shaoru Chen, Eric Wong, J Zico Kolter, and Mahyar Fazlyab. Deepsplit: Scalable verification of deep neural networks via operator splitting. arXiv preprint arXiv:2106.09117, 2021.
[12] Vasek Chvátal. Edmonds polytopes and a hierarchy of combinatorial problems. Discrete mathematics, 4(4):305-33)) 1973.
[13] Michele Conforti, Gérard Cornuéjols, and Giacomo Zambelli. Integer programming / Michele Conforti, Gérard Cornuéjols, Giacomo Zambelli. Graduate texts in mathematics, 271. Springer, Cham, 2014.
[14] Harlan Crowder, Ellis L Johnson, and Manfred Padberg. Solving large-scale zero-one linear programming problems. Operations Research, 31(5):803-834 1983.
[15] Sumanth Dathathri, Krishnamurthy Dvijotham, Alexey Kurakin, Aditi Raghunathan, Jonathan Uesato, Rudy R Bunel, Shreya Shankar, Jacob Steinhardt, Ian Goodfellow, Percy S Liang, et al. Enabling certification of verification-agnostiic networks via memory-efficient semidefinite programming. Advances in Neural Information Processing Systems (NeurIPS), 2020.
[16) Alessandro De Palma, Harkirat Singh Behl, Rudy Bunel, Philip H. S. Torr, and M. Pawan Kumar. Scaling the convex barrier with active sets. International Conference on Learning Representations (ICLR), 2021.
[17] Alessandro De Palma, Rudy Bunel, Alban Desmaison, Krishnamurthy Dvijotham, Pushmeet Kohli, Philip HS Torr, and M Pawan Kumar. Improved branch and bound for neural network verification via lagrangian decomposition. arXiv preprint arXiv:2104.06711 067006.8. 2021.
11

---

[18] Krishnamurthy Dvijotham, Robert Stanforth, Sven Gowal, Timothy Mann, and Pushmeet Kohli. dual approach to scalable verification of deep networks. Conference on Uncertainty in Artificial Intelligence (UAT), 2018.
[19] Ruediger Ehlers. Formal verification of piece- wise linear forward neural networks. In International Symposium on Automated Technology for Verification and Analysis (ATVA), 2017.
[20] Claudio Ferrari, Mark Niklas Muller, Nikola Jovanovic, and Martin Vechev. Complete verifica- tion via multi-neuron relaxation guided 2022.
and-bound. arXiv preprint arXiv:2205.00265 000663
[21] Paul C Gilmore and Ralph E Gomory. A linear programming approach to the cutting-stock problem. Operations research, 9 1961.
[22] Paul C Gilmore and Ralph E Gomory. A linear programming approach to the cutting stock problem part ii Operations research, 1(6))863-888) 888, 1963.
[23] Sven Gowal, Krishnamurthy Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Uesato, Timothy Mann, and Pushmeet Kohli. On the effectiveness of interval bound propagation for training verifiably robust models. Proceedings of the IEEE International Conference on Computer Vision (ICCV), 2019.
[24] LLC Gurobi Optimization. Gurobi optimizer ggurobi, 2022.
[25] Patrick Henriksen and Alessio Lomuscio. Efficient neural network verification via adaptive refinement and adversarial search. In ECAI 2020, pages
IOS Press, 2020.
[26] Patrick Henriksen and Alessio Lomuscio. Deepsplit: An efficient splitting method for neural network verification via indirect effect analysis. In Proceedings of the 30th international joint conference on artificial intelligence (ICCA121), pages 2549-2555, 2021.
[27] Karla L Hoffman and Manfred Padberg. Solving airline crew scheduling problems by branch- and-cut. Management science, 39(6):657-682 1993.
[28] IBM. Ibm ilog cplex optimizer, 2022.
[29] Ellis L Johnson and Manfred W Padberg. Degree-two inequalities, clique facets, and biperfect graphs. In North-Holland Mathematics Studies, volume 66, pages 169-187. Elsevier, 1982.
[30] Guy Katz, Clark Barrett, David Dill, Kyle Julian, and Mykel J Kochenderfer. Reluplex: An efficient smt solver for verifying deep neural networks. In International Conference on Computer Aided Verification (CAV), 2017.
[31] Guy Katz, Derek A Huang, Duligur lbeling. Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zeljić, et al. The marabou framework for verification and analysis of deep neural networks. In International Conference on Computer Aided Verification (CAV), 2019.
[32] Diederik P Kingma and Jimmy Ba. Adam: A method for stochastic optimization. International Conference on Learning Representations (ICLR), 2015.
[33] Panagiotis Kouvaros and Alessio Lomuscio. Towards scalable complete verification of relu neural networks via dependency- -based branching. In IJCAI, pages 2643-2650, 2021.
[34] Changliu Liu and Taylor Johnson. Vnn comp 2020.
[35] László Lovász and Alexander Schrijver. Cones of matrices and set-functions and 0-1 optimiza- tion. SIAM journal on optimization, 1(2):166-19) 1991.
[36] Jingyue Lu and M Pawan Kumar. Neural network branching for neural network verification. International Conference on Learning Representation (ICLR), 2020.
[37] Hugues Marchand and Laurence Wolsey. Aggregation and mixed integer rounding to solve mips. Operations research, 49(3):363-37,, 2001.
12

---

[38] Christoph Müller, Francois Serre, Gagandeep Singh, Markus Püschel. and Martin Vechev. Scaling polyhedral neural network verification on gpus. Proceedings of Machine Learning and Systems, 3:733-746, 2021.
[39] Christoph Müller, Gagandeep Singh, Markus Püschel, and Martin Vechev. Neural network robustness verification on gpus. arXiv preprint arXiv:2007.10868 2020.
[40] Mark Niklas Müller, Gleb Makarchuk, Gagandeep Singh, Markus Püschel, and Martin Vechev. Precise multi-neuron abstractions for neural network certification. arXiv preprint arXiv:2/03.03638, 2021.
[41] George L Nemhauser and Laurence A Wolsey, A recursive procedure to generate all cuts for 0-1 mixed integer programs. Mathematical Programming, 46(1):379-390, 1990.
[42] Manfred W Padberg, Tony J Van Roy, and Laurence Wolsey. Valid linear inequalities for fixed charge problems. Operations Research, 33(4):842-88) 18442611,1111 1985.
[43] Chongli Qin, Brendan O'Donoguue, Rudy Bunel, Robert Stanforth, Sven Gowal, Jonathan Uesato, Grzegorz Swirszez, Pushmeet Kohli, et al. Verification of non-linear specifications for neural networks. arXiv preprint arXiv:1902.0900 09592, 2019.
[44] Aditi Raghunathan, Jacob Steinhardt, and Percy Liang. Semidefinite relaxations for certifying robustness to adversarial examples. In Advances in Neural Information Processing Systems (NeurIPS), 2018.
[45] Hadi Salman, Greg Yang, Huan Zhang, Cho-Jui Hsich, and Pengchuan Zhang. A convex relaxation barrier to tight robustness verification of neural networks. In Advances in Neural Information Processing Systems (NeurIPS), 2019.
[46] Hanif D Sherali and Warren P Adams. A reformulation--iinaatattoo technique for solving discrete and continuous nonconvex problems, volume 31. Springer Science & Business Media, 2013.
[47] Gagandeep Singh, Rupanshu Ganvir, Markus Püiscel,, and Martin Vechev. Beyond the single neuron convex barrier for neural network certification. In Advances in Neural Information Processing Systems (NeurIPS). 2019.
[48] Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin Vechev. Fast and effective robustness certification. In Advances in Neural Information Processing Systems (NeurIPS), 2018.
[49] Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. Boosting robustness certification neural networks. In International Conference on Learning Representations, 2018.
[50] Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. An abstract domain for certifying neural networks. Proceedings of the ACM on Programming Languages (POPL), 2019.
[51] Cheng Tan, Yibo Zhu, and Chuanxiong Guo. Building verified neural networks with specifica- tions for systems. In Proceedings of the 12th ACM SIGOPS Asia-Pacific Workshop on Systems, pages 42-47, 2021.
[52] Christian Tjandraatmadja, Ross Anderson, Joey Huchette, Will Ma, Krunal Patel, and Juan Pablo Vielma. The convex relaxation barrier, revisited: Tightened single-neuron relaxations for neural network verification. Advances in Neural Information Processing Systems (NeurIPS), 2020.
[53] Vincent Tjeng, Kai Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming. International Conference Learning Representations (ICLR), 2019.
[54] Hoang-Durg -unng Tran, Xiaodong Yang. Diego Manzanas Lopez, Patrick Musau, Luan Viet Nguyen, Weiming Xiang, Stanley Bak, and Taylor T Johnson. Nnv: The neural network verification tool for deep neural networks and learning-enabled cyber-physical systems. In International Conference Computer Aided Verification, pages 3-17. Springer, 2020.
13

---

[55] Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. Efficient formal safety analysis of neural networks. Advances Neural Information Processing Systems (NeurIPS), 2018.
[56] Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. Formal security analysis of neural networks using symbolic intervals. In USENIX Security Symposium, 2018.
[57] Shiqi Wang. Huan Zhang. Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification. Advances in Neural Information Processing Systems, 34, 2021.
[58] Eric Wong and Zico Kolter. Provable defenses against adversarial examples via the convex outer adversarial polytope. In International Conference on Machine Learning (ICML), 2018.
[59] Kaidi Xu, Zhouxing Shi, Huan Zhang, Yihan Wang, Kai-Wei Chang, Minlie Huang, Bhavya Kailkhura, Xue Lin, and Cho-Jui Hsieh. Automatic perturbation analysis for scalable certified robustness and beyond. Advances in Neural Information Processing Systems (NeurIPS), 2020.
[60] Kaidi Xu, Huan Zhang, Shiqi Wang, Yihan Wang, Suman Jana, Xue Lin, and Cho-Jui Hsieh. Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. International Conference on Learning Representations (ICLR), 2021.
[61] Huan Zhang. Tsui-War Weng. Pin- Yu Chen, Cho-Jui Hsieh, and Luca Daniel. Efficient neural network robustness certification with general activation functions. In Advances in Neural Information Processing Systems (NeurIPS), 2018.
Checklist
1. For all authors...
(a) Do the main claims made in the abstract and introduction accurately reflect the paper's
contributions and scope? [Yes]
(b) Did you describe the limitations of your work? [Yes]
(c) Did you discuss any potential negative societal impacts of your work? [Yes]
(d) Have you read the ethies review guidelines and ensured that your paper conforms them? [Yes]
2. If you are including theoretical results...
(a) Did you state the full set of assumptions of all theoretical results? [Yes]
(b) Did you include complete proofs of all theoretical results? [Yes]
3. If you ran experiments..
(a) Did you include the code, data, and instructions needed to reproduce the main experi- mental results (either in the supplemental material or URL)? [Yes]
(b) Did you specify all the training details (e.g., data splits, hyperparameters, how they were chosen)? [Yes]
(c) Did you report error bars (e.g., with respect the random seed after running experi- ments multiple times)? [N/A] Not applicable, our verification results typically do not change after running multi times.
(d) Did you include the total amount of compute and the type of resources used (e.g., type of GPUs, internal cluster, or cloud provider)? [Yes]
4. If you are using existing assets (e.g., code, data, models) or curating/releasing new assets...
(a) If your work uses existing assets, did you cite the creators? [Yes]
(b) Did you mention the license of the assets? [Yes]
(c) Did you include any new assets either in the supplemental material or as a URL? [Yes]
(d) Did you discuss whether and how consent was obtained from people whose data you're using/curating? [N/A] We use only public data.
14

---

(c) Did you discuss whether the data you are using/curating contains personally identifiable information or offensive content? [N/A] We use only public data.
5. If you used crowdsoureing conducted research with human subjects...
(a) Did you include the full text of instructions given to participants and screenshots, if applicable? [N/A]
(b) Did you describe any potential participant risks, with links to Institutional Review Board (IRB) approvals, applicable? [N/A]
(c) Did you include the estimated hourly wage paid to participants and the total amount spent on participant compensation? [N/A]
15


Reviews:
[{"review_id": "rhJ6qlRZe_A", "reviewer": "Reviewer_V4Wg", "summary": "The authors extend the popular and effective Beta-CROWN algorithm, a complete verifier that very efficiently operates on the triangle ReLU relaxation in the context of branch and bound, to support general cutting planes. \nThe presented algorithm, named GCP-CROWN, relies on cutting planes from off-the-shelf LP solvers, run on a CPU, in parallel to the GPU-based neural network verification procedure. \nGCP-CROWN is shown to outperform state-of-the-art baselines on relevant benchmarks.", "questions": "- I believe MN-BaB, which is closely related to GCP-CROWN, should be more accurately described and presented in the technical part of the paper;\n\n- the authors should explain and argue more on why one has to use these cutting planes in the context of bound propagation rather than lagrangian relaxation or decomposition, where doing so would be easier. It would be nice to see an experimental comparison on that, or theoretical arguments on why bound propagation is to be preferred. From the technical parts of the paper, it would seem like bound propagation methods are the only GPU-friendly alternative to off-the-shelf LP solvers. Many cited works [6, 13, 15] demonstrate otherwise, and that should be more carefully explained.\n\n- Theorem 3.1 shows that GCP-CROWN provides a lower bound to the LP with cutting planes. However, do the optimal values of alpha and beta lead to the optimal primal value? \n\n- what's the employed branching strategy in the experiments?\n\n- why does GCP-CROWN take more subproblems than beta-CROWN on the deep network of table 1? That's counter-intuitive.", "limitations": "The authors adequately address the limitations of their work, but should be more upfront with respect to their incremental improvements on beta-CROWN.", "rating": 6, "confidence": 5, "soundness": 3, "presentation": 1, "contribution": 3, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "While the idea behind GCP-CROWN is simple and somewhat incremental (it is a minor, yet powerful, extension of beta-CROWN), it is undeniably novel in the context of neural network verification. Furthermore, the experimental results clearly indicate that GCP-CROWN outperforms the state of the art on hard verification benchmarks.\n\nMy concerns mostly revolve around the sub-par quality of the presentation. Crucially, I believe that the authors should be more upfront with respect to their algorithm's incrementality with respect to beta-CROWN, which is not necessarily a bad thing. However, such incrementality might not be evident to someone outside the sub-field. In other words, the presentation should start from beta-CROWN, and then move on to include the relaxed integer variables, and the cutting planes.\nThe analysis of the cutting planes, presented in the appendix, is perhaps worth including in the main paper.\nFurthermore, it would be nice if the authors could include larger networks in the evaluations: for instance, the cifar2020 benchmark from VNN-COMP-21 includes networks with tens of thousands of activations. I would be curious to see whether cutting planes still pay off with respect to beta-CROWN at that scale.", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}, {"review_id": "CZ-UHI5x6Yq", "reviewer": "Reviewer_QMej", "summary": "These paper improve the general BaB method by integrateing any cutting cut method for formal complete evrifcation of adervarial robustness. This computation allows parallel comptation . they outperfom state of the art againstal several datset, methods, noise level for multilpes models for both verified accuracy and verification time.", "questions": "Can you compare the power ressources used compared to methods DP-FO [12]∗ PRIMA [35] β-CROWN [52] MN-BaB [17] α-CROWN+MIP ? (as you used parralel comptation: what if you did not use paralilsum)?\n\nYou did not discuss the limitations of your work\n\nYou did not dscuss the comprarsion of different cutting planes.", "limitations": "cf above", "rating": 7, "confidence": 4, "soundness": 3, "presentation": 2, "contribution": 3, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "Strengths: \n\nNovelty of the approach: complete verification of DNN specific family \n\nImportant topic \n\nSound proof of the Hessian bounds \n\nClarity of the paper \n\nFaster  verification and higher verified accuracy\n\nWeaknesses \n\nPoor experiments comparison according power resoureces", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}, {"review_id": "06P_sAczZsE", "reviewer": "Reviewer_Ygz6", "summary": "The paper considers the neural network verification problem where it builds on\nbound propagation methods to account for cutting planes generated by MILP\nsolvers. Experimental results on a number of benchmarks from VNN-COMP 20201\nshow improved performance over the SoA.", "questions": "Please see comments on Weaknesses.", "limitations": "These are sufficiently addressed.", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "Strengths.\n\n- First work that I am aware of that uses cutting planes from MILP solvers in a\n  bound propagation setting.\n\n- It is good to see that this works in practice.\n\nWeaknesses.\n\n- Highly incremental to previous work. The technical novelty is the addition of\n  cuts to a previously developed framework, which while is good to see that it\n  works, it presents limited originality and overall contribution.\n\n- There is no ablation study that compares GCP-CROWN with cuts and GCP-CROWN\n  without cuts. The authors should make precise the contribution of the cuts to\n  the overall performance (while there are comparisons with different variants\n  of crown, an ablation study on GCP-CROWN would make the actual contribution\n  more clear).\n\n- Related work on MILP-based verification which strengthens the MILP\n  formulation  with custom cuts is not discussed:  E. Botoeva et al., Efficient\n  Verification of ReLU-Based Neural Networks via Dependency Analysis, AAAI\n  2020.", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"ethics_review_area": ""}, "extra_text": {}}]

Author rebuttal:

Decision: Accept