Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Neural Network Robustness Verification
Authors: Shiqi Wang
Huan Zhang
Kaidi Xu
Xue Lin
Suman Jana
Cho-Jui Hsieh
J Zico Kolter
Venue: NeurIPS 2021 Poster (2021)
Keywords: neural network verification
branch and bound
adversarial robustness
adversarial examples
certified robustness

Abstract: Bound propagation based incomplete neural network verifiers such as CROWN are very efficient and can significantly accelerate branch-and-bound (BaB) based complete verification of neural networks. However, bound propagation cannot fully handle the neuron split constraints introduced by BaB commonly handled by expensive linear programming (LP) solvers, leading to loose bounds and hurting verification efficiency. In this work, we develop $\beta$-CROWN, a new bound propagation based method that can fully encode neuron splits via optimizable parameters $\beta$ constructed from either primal or dual space. When jointly optimized in intermediate layers, $\beta$-CROWN generally produces better bounds than typical LP verifiers with neuron split constraints, while being as efficient and parallelizable as CROWN on GPUs. Applied to complete robustness verification benchmarks, $\beta$-CROWN with BaB is up to three orders of magnitude faster than LP-based BaB methods, and is notably faster than all existing approaches while producing lower timeout rates. By terminating BaB early, our method can also be used for efficient incomplete verification.  We consistently achieve higher verified accuracy in many settings compared to powerful incomplete verifiers, including those based on convex barrier breaking techniques. Compared to the typically tightest but very costly semidefinite programming (SDP) based incomplete verifiers, we obtain higher verified accuracy with three orders of magnitudes less verification time. Our algorithm empowered the $\alpha,\!\beta$-CROWN (alpha-beta-CROWN) verifier, the winning tool in VNN-COMP 2021. Our code is available at http://PaperCode.cc/BetaCROWN.

Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Neural Network Robustness Verification
Shiqi Wang"*
Huan Zhang
Kaidi Xu
Xue Lin'
Suman Jana"
Cho-Jui Hsich Zico Kolter²
CColubii University
CMU NNotheasttern University
4UCLA
Sua3215@cor wttp///owmbaaa..mmmmm wublll edu edu
huanChuan-zhang com
xu. ww..aadnooothhaaternnnmmm edu sumanêcs. columbia. edu chohsieh@cs ucla.edu
xue mue.iin@ee weeetnorrtthattee.eedde
zkolterθcs cmu. edu
Equal Contribution
Abstract
Bound propagation based incomplete neural network verifiers such CROWN are very efficient and can significantly accelerate branch-and-bourt (BaB) based complete verification of neural networks. However, bound propagation cannot fully handle the neuron split constraints introduced by BaB commonly handled by expensive linear programming (LP) solvers, leading to loose bounds and hurting verification efficiency. In this work, we develop B-CROWN, a new bound propaga- tion based method that can fully encode neuron splits via optimizable parameters I constructed from either primal or dual space. When jointly optimized in interme- diate layers, 8 3-CROWN generally produces better bounds than typical LP verifiers with neuron split constraints, while being as efficient and parallelizable CROWN on GPUs. Applied to complete robustness verification benchmarks, 3-CROWN with BaB is up three orders of magnitude faster than LP-based BaB methods, and is notably faster than all existing approaches while producing lower timeout rates. By terminating BaB early, method can also be used for efficient incomplete verification. We consistently achieve higher verified accuracy in many settings compared powerful incomplete verifiers, including those based convex barrier breaking techniques. Compared to the typically tightest but very costly semidefinite programming (SDP) based incomplete verifiers, obtain higher verified accuracy with three orders of magnitudes less verification time. Our algorithm empowered the 3.CB-COONN (alpha- beta-CROw)) verifier, the winning tool in VNN-COMP cc/BetacRBene
2021. Our code is available at
1 Introduction
As neural networks (NNs) are being deployed in safety-critical applications, it becomes increasingly important to formally verify their behaviors under potentially malicious inputs. Broadly speaking, the neural network verification problem involves proving certain desired relationships between inputs and outputs (often referred to as specifications), such as safety or robustness guarantees, for all inputs inside some domain. Canonically, the problem can be cast as finding the global minima of some functions on the network's 's outputs (e.g., the difference between the predictions of the true label and another target label), within bounded input set constraints. This is challenging problem due to the non-convyxity and high dimensionality of neural networks.
35th Conference on Neural Information Processing Systems (NcurIPS 2021).

---

We first focus on complete verification: the verifier should give a definite "yes/no" answer given sufficient time. Many complete verifiers rely on the branch and bound (BaB) method [ involving (1) branching by recursively splitting the original verification problem into subdomains (e.g., splitting a ReL.U neuron into positive/negative linear regions by adding split constraints) and (2) bounding each subdomain with specialized incomplete verifiers. Traditional BaB- verifiers use expensive linear programming (LP) solvers [S 23 r as incomplete verifiers which can fully encode neuron split constraints. Meanwhile, a recent verifier, Fast-and-Complet A5I. demonstrates that cheap incomplete verifiers can significantyy accelerate complete verification on GPUs over LP-based ones thanks to their efficiency. Many cheap incomplete verifiers are based on bound propagation methods 46 42 13 BC,
44 i.c., maintaining and propagating tractable and sound bounds through networks, and CROWN 46 is representative which propagates a linear or quadratic bound.
However, unlike LP based verifiers, existing bound propagation methods lack the power to handle neuron split constraints introduced by BaB. For instance, given inputs z y E [-1, 1.. they can bound a ReL.Us input x + y as |-2, 2] but they have no means to consider neuron split constraints such as x y 2 0 introduced by splitting another ReLU to the positive linear region. Such a problem causes looser bounds and unnecessary branching. hurting the verification efficiency. Even worse, without considering these split constraints, bound propagation methods cannot detect many infeasible subdomains in BaB [5). leading to incompleteness unless costly checking is performed.
In our work, we develop a new, fast bound propagation based incomplete verifier, 3 3-CROWN. It solves an optimization problem equivalent to the expensive LP based methods with neuron split constraints while still enjoying the efficiency of bound propagation methods. 3-CROWN contains optimizable parameters ,3 which come from propagation of Lagrangian multipliers, and any valid settings of these parameters yield sound bounds for verification. These parameters are optimized using few steps of (super)gradient ascent to achieve bounds as tight as possible. Optimizing & can also eliminate many infeasible subdomains and avoid further useless branching. Furthermore, we can jointly optimize intermediate layer bounds similar to 44 but also with the additional parameters G, allowing 3- CROWN to tighten relaxations and outperform typical LP verifiers with fixed intermediate layer bounds. Unlike traditional LP-based BaB methods, 3-CROWN can be efficiently implemented with an automatic differentiation framework on GPUs to fully exploit the power of modern accelerators. The combination of 3-CROWN and BaB (3-CROWN BaB) produces a complete verifier with GPU acceleration, reducing the verification time of traditional LP based BaB verifiers
[ by up to three G 10] Compared to all O [1) our approach is noticeably faster with lower timeout rates. Our algorithm empowered the tool a, 3-3-CROWN aalpha-beta-CRown which won the 2nd International Verification of Neural Networks Competition
orders of magnitudes on a commonly used benchmark suite on CIFAR-10 10
state-of-the -hrt-----t---tttt- art GPU-based complete verifiers 7 55
HC
23
G (VNN-COMP
2021) with the highest total score and verified the most number of problem instances in 8 benchmarks.
Finally, by terminating our complete verifier 3-CROWN BaB early, our approach can also function as a more accurate incomplete verifier by returning an incomplete but sound lower bound of all subdomains explored so far. We achieve better verified accuracy over powerful incomplete verifiers including those based on tight linear relaxations 35 37 26 and semidefinite relaxations [9]. Compared to the typically tightest but very costly incomplete verifier SDP-FO ( based on the semidefinite programming (SDP) relaxations (2 [4], our method obtains consistently higher verified accuracy while reducing verification time by three orders of magnitudes.
few benchmarking models
2
Background
2.1 The neural network verification problem and its LP relaxation
We define the input of neural network as x Rd and define the weights and biases of an L-layer neural network as (t)) Rd xd.-1 and b(t Rd (i E {1...., L)) respectively. For simplicity we assume that d2 = 1 so W(L) is vector and b(L) is a scalar. The neural network function d + R is defined as f(x)
W() ((())(t-)(a)) (xx) + b(, (1:) and (x)) = x. is the activation function and we ReI.U throughout this
(z), where 20)(2)
(x) = (=((
paper. When the context is clear, we omit -(z) and use (() and 2 to represent the pre-activation and post-activation values of the j-th neuron in the i-th layer. Neural network verification seeks the solution of the optimization problem in Eq.
min f(z)= ;= (x) s.t. 2 g0 +b(0 2000 oo=)) ZE CiiE
(1)
2

---

The set C defines the allowed input region and our aim is to find the minimum of fz) for x E C. and throughout this paper we consider C as an &x ball around a data example Tp: C= f2 | c) but other Ep norms can also be supported. In practical settings, we typically have "specifications" to verify, which are (usually linear) functions of neural network outputs describing the desired behavior of neural networks. For example, to guarantee robustness we typically investigate the margin between logits. Because the specification can also be seen as an output layer of NN and merged into f(x) under verification, we do not discuss it in detail in this work. We consider the canonical specification f(x)= > 0: we can prove that (x) > O, Va E C, we say f() is verified.
When is a convex set, Eq. D is still non-convex problem because the constraints g(() oz((1) are non-convex. Given unlimited time, complete verifiers can solve Eq. I exactly: f = min f(z), Vr e C, so we can always conclude if the specification holds or not for any problem instance. On the other hand, incomplete verifiers usually relax the non-convexity of neural networks to obtain tractable lower bound of the solution f S f If f Z O, then f > 0 so f(x) can be verified; when [ < O, we are not able to infer the sign of f so cannot conclude if the specification holds or not.
commonly used incomplete verification technique is relax non-convex ReLU constraints with linear constraints and turn the verification problem into a linear programming (LP) problem. which can then be solved with linear solvers. We refer it the "L.P verifier" in this paper. Specifically,
(4) I u each ReLU given RcLU(x))) == max(0, 2 and its intermediate layer bounds 15 I =)
can be categorized into three cases: (1) if ( 2 (ReLU in linear region) then 2) = ; (2) if
< 0 (ReLU in inactive region) then ( = 0: (3)
(6)
< < (() (ReLU is unstable) then S
three linear bounds are used: 2) 2 0,
and
- (3) -1 they are often
(6)
referred to as the "triangle" relaxation 113 The intermediate layer bounds [(s) and u are usually obtained from cheaper bound propagation method (see next subsection). LP verifiers can provide relatively tight bounds but linear solvers are still expensive especially when the network is large. Also, unlike our 3-CROWN, they have to use fixed intermediate bounds and cannot the joint optimization of intermediate layer bounds (Section 3.3 to tighten relaxation.
2.2 CROWN: efficient incomplete verification by propagating linear bounds
Another cheaper way to give a lower bound for the objective in Eq. D is through sound bound propagation. CROWN 46 is representative method that propagates linear bound of [xr w.r.t. every intermediate layer in a backward manner until reaching the input x. CROWN uses two linear
constraints to relax unstable ReL.U neurons: linear upper bound 2/0 - (2) -
11)) and
linear lower bound =(()
(0 S a.) 1). We can then bound the output of ReLU layer: Lemma 2.1 (ReLU relaxation in CROWN). Given w, v R u (element-wise), we have w ReLLUU)) 2 w Dv + B',
where D is a diagonal matrix containing free variables 0 S aa < 1 only when uj 0 1 and wy 2 O, while its rest values as well as constant b' are determined by 1, u, W.
Lemma 2.1 can be repeatedly applied, resulting in an efficient mack-substitution procedure to derive linear lower bound of NN output w.r.t. æ:
Detailed forms of each term are listed in Appendix A
Lemma 2.2 (CROWN bound 46) ). Given an L-layer ReLU f(x): do + R with weights W(i,
biases (6), pre-ReLU bounds 1(() < z00 < u i < L) and input constraint E C. We have
min f(x) min a.nowx= x + CeROWN
aec
aEC
where acnows and CenowN can be computed using W() ((),, 100) n( in polynomial time.
When C is an bp norm ball, minimization over the linear function can be easily solved using Hölder's inequality. The main benefit of CROWN is its efficiency: CROWN can be efficiently implemented on machine learning accelerators such GPUs 44 and TPUs faster than an LP verifier which is hard to parallelize on GPUs CROWN was generalized to general architectures 44 3T] while we only demonstrate it for feedforward ReLUU networks for simplicity. Additionally, Xu et al. [5 showed that it is possible to optimize the slope of the lower bound, a. using gradient ascent, further tighten the bound (sometimes referred as c-CROWN).
44 I, and it can be few magnitudes
3

---

2.3 Branch and Bound and Neuron Split Constraints
Branch and bound (BaB) method is widely adopted in complete verifiers X we divide the domain of the verification problem C into two subdomains C₁ = fx C, 2 0} and C2 fz E C, 2) < 0}
where (0) is an unstable ReL.U neuron in C but now becomes linear for each subdomain. Incomplete verifiers can then estimate the lower bound of each subdomain with relaxations. If the lower bound produced for subdomain C; (denoted by Le? ) is greater than O, C2 is verified; otherwise, we further branch over domain C; by splitting another unstable ReLU neuron. The process terminates when all subdomains are verified. The completeness is guaranteed when all unstable ReLU neurons are split.
LP verifier with neuron split constraints. A popular incomplete verifier used in BaB is the LP
verifier. Essentially, when we split the j-th ReI.U in layer i, we can simply add =, 2 0 or 2j (1) < 0 to Eq. and get a linearly relaxed lower bound to each subdomain. We denote the Z+(1) and 2-
as the set of neuron indices with positive and negative split constraints in layer i. We define the split (0,,,,
Vj E Z+)+), Vj2 E 2-- We denote the vector of all Pre-ReLU neurons as z, and we define a set Z represent the split constraints on z: Z z (1) 2z n.... n-..nZ((-1) For convenience, we also use the shorthand 2 := z n- and z(0) ==
constraints at layer i as ( == (2(9) (0 2 0,
}. LP verifiers can easily handle these neuron split constraints but are more expensive than bound propagation methods like CROWN and cannot be accelerated on GPUs.
=00).
Branching strategy. Branching strategies (selecting which ReLU neuron split) are generally agnostic to the incomplete verifier used in BaB but do affect the overall BaB performance. BaBSR M is widely used strategy in complete verifiers, which is based
fast estimates on objective improvements after splitting each neuron. The neuron with highest estimated improvement is selected for branching. Recently, Filtered Smart Branching (FSB) | improves BaBSR by mimicking strong branching- it utilizes bound propagation methods to evaluate the best a few candidates proposed by BaBSR and chooses the one with largest improvement. Graph neural network (GNN) based branching was also proposed [23]. Our 3-CROWN BaB is general complete verification framework fit for any potential branching strategy, and we evaluate both BaBSR and FSB in experiments.
3 B-CROWN for Complete and Incomplete Verification
In this section, we first give intuitions on how 3-CROWN handles neuron split constraints without costly LP solvers. Then we formally state the main theorem of 3-CROWN from both primal and dual spaces, and discuss how to tighten the bounds using free parameters B. Lastly, we propose 3-CROWN BaB, a complete verifier that is also a strong incomplete verifier when stopped early.
3.1 8-CROWN: Linear Bound Propagation with Neuron Split Constraints
The NN verification problem under neuron split constraints can be seen as an optimization problem:
min fx)
Bound propagation methods like CROWN can give a relatively tight lower bound for minzec f() but they cannot handle the neuron split constraints z E Z. Before we present main theorem, we first show the intuition on how to apply split constraints to the bound propagation process.
To encode the neuron splits, we first define diagonal matrix ((1) Rd,xd, in Eq. 3 where
[1, ..... L - 11,j E [I,... ...,
di) are indices of layers and neurons, respectively:
S/t 1(if split 2fth 2 0); $/9 = (if split 2 < <);; $ = Off no split 20))
(3)
We start from the last layer and derive linear bounds for each intermediate layer 200) and 200) with
both constraints x E C and 2 E Z. We also assume that pre-ReLU bounds (()) < 20) < ( for each
layer are available (see discussions in Sec. 3.3 on these intermediate layer bounds). We initially have:
min f(x) ZEC,1E2
min (LL))(L-1) + +b())
(4)
=EC,2E2

---

Since 2(1-1) = ReLU ReLU(2((i-1)), we can apply Lemma 2.1 to relax the ReLU neuron at layer L 1, and obtain linear lower bound for f(r) w.r.t. 2(4-1) (we omit all constant terms to avoid clutter):
min f(z) 2 min ( ( ((--1) + const. =EC.2E2
=EC,3E2
To enforce the split neurons at layer L 1, we use a Lagrange functionn with g(4-1)T multiplied on 2(1--1);
min (())
min glL
max w( ((1-1) + (((-1)) (((-1))((-11 const
e2 2) ge 1220
(5)
(w"" (1.-)) gl1-1) g(i-))) g(1 = ((
max
min ZEC g 22
const
The first inequality is due to the definition of the Lagrange function: we remove the constraint ((111) g(L-1) and use a multiplier to replace this constraint. The second inequality due to weak duality. Due to the design of ((L-1), neuron split 2 2 0 has a negative multiplier -33/--1 and split 2j =/(-1) < 0 has positive multiplier ///"" Any (L(-11) 2 0 yields lower bound for the constrained optimization problem. Then we substitute (!.-1) with (1--)))(tt-- + b(.-1)) for
((+-1)
next layer:
((LL) + g(a s(c s((e-))((--)) w( + const (6)
min f(x) xEC,
max 22-0
min (LL-))
We define a matrix
(4) to represent the linear relationship between f(x) and 2(0), where (1-1)
WLL) according Eq. and A (L--2) ((LL-))D(L-1) + ((L-1) T S ((L-1) W(L-1) by Eq.
Considering 1-dimension output (x), A (i) has only I row. With (1-2) Eq. becomes:
min f(x) xEC.:E2
max 12-
min
A (1-2))((6-2) const,
which is a form similar to Eq. except for the outer maximization over g(L-1), This allows the
back-substinution process (Eq, Eq. 5 and Eq,
6 to continue. In each step, swap max and min as in Eq. 5 so every maximization over (3() is outside of minzec. Eventually, we have:
min f(x) =cC,aCZ
max min A (0) x + const,
B20 #EC
where 3 = [3()T ((2) 1
concatenates all ( vectors. Following the above idea,
we present the main theorem Theorem 3.1 (proof is given in Appendix A
Theorem 3.1 (3-CROWN bound). Given an L-layer NN f(x) : RRdo + with weights W(), biases
(1), Rre- bounds 10) S (+) S (() (1 S $ L). input bounds split constraints Z. We have:
min f(x) max min (a PP3) TT
=EC
#20 ZEC
where a E P de Els di and c R are functions of ( b(0 10), O
Detailed formulations for a. P. q and are given in Appendix A Theorem 3.1 shows that when neuron split constraints exist, f(x) can still be bounded by linear equation containing optimizable multipliers B. Observing Eq, 5 the main difference between CROWN and 3-CROWN lies in the relaxation of each ReLU layer, where
need extra term T (() in the linear relationship matrix (for example, (L) (L-1) in Eq. between f(r)) and ()) to enforce neuron split constraints.
This extra term in every ReLU layer yields P and q in Eq. after bound propagations.
To solve the optimization problem in Eq. 7 we note that in the Ep norm robustness setting (C fo || -xull c)), the inner minimization has a closed solution:
min =EC
f(x)= max -la + PBI,, (P To T B20
B + a zo c
c: max (
,200
where 1+ 1. The maximization is concave in B (g 2 1), so we can simply optimize it using
projected (super)gradiens ascent with gradients from automatic differentiation library. Since any
5

---

32 O yields valid lower bound for mingeC.sE2 f(z), convergence is not necessary to guarantee soundness. 3-CROWN efficient it has the same asymptotic complexity as CROWN when B is fixed. When 3 0, B-CROWN yields the same results as CROWN; however the additional optimizable 33 allows us to maximize and tighten the lower bound due to neuron split constraints.
We define ( E IR for free variables associated with unstable ReLU neurons in Lemma 2. for layer and define all free variables a = {a(()) ...a((-11).. Since any 0 S (M) < yields a valid
bound, we can optimize it tighten the bound, similarly as done in 45 Formally, we rewrite Eq. with a explicitly:
min =EC,:E2
f(x)
max
g),
05as1, 320
3.2 Connections to the Dual Problem
In this subsection, we show that 3-CROWN can also be derived from a dual LP problem. Based on Eq. D and linear relaxations in Section we first construct LP problem for &oo robustness verification in Eq. IC where E {1,...,L L 1}.
= min {= (z) s.t.
Network and Input Bounds:
200 g(1)
+ b,,; 2 20 222 S tE
Stable ReLUs: 2(
3j (if (1) 2 0); a/4 = 0 (if u <0;;
(t)
Unstable:
2 0,
(1) (6) (0
2 2
s - (4) 10 (ifl <0<ul) u0 2 2+0
.
Neuron Split Constraints: 2 2 2 (if 2 - ; = 0, < 0 (ifj E + (0)
(10)
Compared to the formulation in 42 we have neuron split constraints. Many BaB based complete verifiers E 23 use an LP solver for Eq. 10 as the incomplete verifier. We first show that it is possible
to derive Theorem 3.1 from the dual of this LP, leading to Theorem 3.2
Theorem 3.2. The objective dir for the dual problem of Eq. 10 can be represented as
dep = - + P3ll + (PT 2g + q) B aaaann xo +
where a, P, q and e are defined in the same way as Theorem 3.1 and [3 2 corresponds to the dual variables of neuron split constraints in Eq. 70
similar connection between CROWN and dual LP based verifier 42 was shown in B0, and their results can be seen as special case of ours when 3 = 0 (none of the split constraints are active), An immediate consequence that 3-CROWN can potentially solve Eq. [0 as well as using an LP solver:
Corollary 3.2.1. When and B are optimally set and intermediate bounds 1, u are fixed, B-CROWN produces pip, the optimal objective of LP with split constraints in Eq. 10
max 05a
g(a, 3) PîP:
In Appendix A
give detailed formulations for conversions between the variables a. 3 in 8- CROWN and their corresponding dual variables in the LP problem.
3.3 Joint Optimization of Free Variables in 3-CROWN
In Eq. g is also a function of 16)) and uj the intermediate layer bounds for each neuron z/00 They
(8)
are also computed using 3 3-CROWN, To obtain 168) we set f(x) = 22)(()) and apply Theorem 3.1
(z)
min 10
(1) (x) 2 max
g' d 10
(11)
05a š1, 8'20
For computing u, we simply set f(x) := -2 (x). Importantly, during solving these intermediate layer bounds, the a' and 3' are independent sets of variables, not the same ones for the objective f(x) := 2(),, Since g is function of 155) it is also function of a' and G In fact, there are total

---

of E di intermediate layer neurons, and each neuron is associated with a set of independent a' and / variables. Optimizing these variables allowing us to tighten the relaxations on unstable ReLU neurons (which depend on 1 and y ( and produce tight final bounds, which is impossible in LP. In other words, we need to optimize & and 3. which are two vectors concatenating a, ß as well as a large number of o' and B3' used to compute each intermediate layer bound:
min f f(x) 2 =EC.:EZ
max g(a.
(12)
05á51, $20
This formulation is non-convex and has a large number of variables. Since any 0 S á ك 11 leads to a valid lower bound, the non-convexity does not affect soundness. When intermediate layer bounds are also allowed to be tightened during optimization, we can outperform the LP verifier for Eq. 10 using fixed intermediate layer bounds. Typically, in many previous works S 23 [ when the LP formulation Eq, 10 is formed, intermediate layer bounds are pre-computed with bound propagation procedures 8 23 which are far from optimal. To estimate the dimension of this problem, we denote the number of unstable neurons at layer as (r((S())). Each neuron in layer i is associated with 2 x Σ E 8% variables a'. Suppose each hidden layer has d neurons (s; (d)), then & has 2 x ΣL-1 d; k= 8K = O(L2d)) variables in total. This can be too large for efficient optimization, so we share and 9' among the intermediate neurons of the same layer, leading to total number of ( variables to optimize. Note that a weaker form of joint optimization was
also discussed in 55 without B, and detailed analysis can be found in Appendix B.2
3.4 8-CROWN with Branch and Bound (3-CROWN BaB)
We perform complete verification following BaB framework X using 3- 3-CROWN as the incomplete solver, and we use simple branching heuristics like BaBSR 7 or FSB [I]. To efficiently utilize GPU, we also use batch splits to evaluate multiple subdomains in the same batch as in 44 IQ. We list our full algorithm B-CROWN BaB in Appendix B and we show it is sound and complete here:
Theorem 3.3. 3-CROWN with Branch and Bound on splitting ReLUs is sound and complete.
Soundness trivial because 3-CROWN a sound verifier. For completeness, suffices show that when all unstable ReLUU neurons are split, 3-CROWN gives the global minimum for Eq. 10 In contrast, combining CROWN
46 with BaB does not yield complete verifier, as it cannot detect infeasible splits and a slow LP solver is still needed to guarantee completeness 45 Instead,
3-CROWN can detect infeasible subdomains according to duality theory, an infeasible primal problem leads to an unbounded dual objective, which can be detected (see Sec. B.3 for more details).
Additionally, we show the potential of early stopping a complete verifier as an incomplete verifier. BaB approaches the exact solution of Eq. by splitting the problem into multiple subdomains, and more subdomains give tighter lower bound for Eq. I Unlike traditional complete verifiers, 3-CROWN is efficient to explore a large number of subdomains during very short time, making 3-CROWN BaB an attractive solution for efficient incomplete verification.
Experimental Results
4.1 Comparison to Complete Verifiers
We evaluate complete verification performance on dataset provided in Px I0 and used in VNN- COMP 2020 (22) The benchmark contains three CIFAR-10 models (Base, Wide, and Deep) with 100 examples each. Each data example is associated with Eoo norm and a target label for verification (referred to as a property to verify). The details of neural network structures and experimental setups can be found in Appendix C We compare against multiple basclines for complete verification: (I) BaBSR 77. a basic BaB and LP based verifier; (2) MIPplanet (15), a customized MIP solver for NN verification where unstable ReLU neurons are randomly selected for splitting; (3) ERAN 35
R an abstract interpretation based verifier which performs well on this benchmark VNN-COMP 2020; (4) GNN-Online (23] BaB and LP based verifiers using a learned Graph Neural Network (GNN) to guide the ReLU splits; (5) BDD+ BaBSR 16.. verification framework based on Lagrangian decomposition on GPUs (BDD+) with BaBSR branching strategy; (6)
3
3d
OVAL (BDD+ GNN) 6 23 strong verifier in VNN-COMP 2020 using BDD+ with GNN guiding the ReLU splits; (7) A.set BaBSR and (8) Big-M+A.se set BaBSR 10 very recent dual-space verifiers
on GPUs with tighter linear relaxation than triangle LP relaxations; (9) Fast-and- -Cmolleeeeeee (5).
7

---

Table 1: Average runtime and average number of branches three CIFAR-I0 models over 100 properties.
CIFAR-10 Base
CIFAR-10 Wide
CIFAR-10 Deep
Method
(ime(s)
brunches
%timeout
time(s)
brunches
%timeout
time(s)
branches
Xtimevut
BaBSR
2367.78
1020.55
36.00
2871.14
812.65
49,00
2750.75
401,28
39,00
MiPplanet
[5
2849.69
68.00
2417.53
46.00
2302.25
40.00
FRAN"
35
kT
805, 94
5.00
632.20
9.00
545.72
0.00
GNN-online
1794.85
565.
33.00
1367.35 338
372.74
15.00
1055.33
131.85
4,00
BDD+ BaBSR
(5
807 91
195480.14 14
20.00
505 655
74203.
10.00
266.28
12722.74
4,00
(BDD+ GNN)
662.17
67938.33 38
16.00
17895.94
6.00
94.69
1990,34
1.00
A.set BaBSR
[0]
381.78
12004.60
7.00
165.91
2253. 10
3.00
190.28
2491.55
2.00
BigM+A.set BaBSR
10
390.44
11938.75
7.00
172.65
4050.55
3.00
177.22
3275.25
2,00
Fast and Complete
45
695.01
119522.65
17.00
495 88
80519.85
9.00
105.66
2455.11
1,00
BaDNB (BDD+ FSR) DT
309.29
38239.04
7.00
165.53
112.14.44
4.00
10.50
368.16
0.00
88 CROWW BaBSR
226.06
509608.50
6.00
217691.24
3.00
6.12
3-CROWN FSB
118.23
208018.21
3,00
78.32
116912.57
2,00
5.69
41.12
0.00
OVAL (BDD+ GNN) and ERAN results are from VNN COMP 2020 report
Other results reported by their authors.
a-CROWN FSB
100%
100%
8-CROINN DaBse
OVAL DWWN-Comp
80%
00%
80%
60%
60%
60%
GEN Online
40%
40%
40%
B.CNBURDDS 1501
600+ booSA
20%
20%
20%
A.Set BaB5R
Big Mi- Set 3JB5R
TecheeddCarrglee
0%
10
100
10a
100
0%
10a
307
16
0%
107
10'
10a
CIFAR-10 Base: Running time lin s)
CIFAR-10 Wide: Running time lin
CIFAR-10 Deep: Running time (in
Figure 1: Percentage of solved properties with growing running time. 3-CROWN FSB (light green) and
8-CROWN BaBSR (dark green) clearly lead in all 3 settings and solve over 90% properties within 10 seconds.
which uses CROWN (LiRPA) on GPUs as the incomplete verifier in BaB without neuron split constraints; (10) BaDNB (BDD+ FSB) [... concurrent state-of-the-art complete verifier, using BDD+ on GPUs with FSB branching strategy. 3-CROWN BaB can use either BaBSR or FSB branching heuristic, and we include both in evaluation. All methods use I hour timcout threshold.
We report the average verification time and branch numbers in Table L and plot the percentage of solved properties over time in Figure ! 8-CROWN FSB achieves the fastest average running time compared to all other baselines with minimal timeouts, and also clearly leads on the cactus plot. When using a weaker branching heuristic, 3-CROWN BaBSR still outperforms all literature baselines, including very recent ones such as A.set BaBSR ITC, mest-and-Comple
451 and BaDNB []] Our benefits are more clearly shown in Figure μ where we solve over 90% examples under 10s and most other verifiers can verify much less or none of the properties within 10s. We see a 2 to 3 orders of magitudes speedup in Figure compared to CPU based verifiers such as MIPplanet and BaBSR.
4.2 Comparison to Incomplete Verifiers
Verified accuracy. In Table 2 we compare against a few representative and strong incomplete verifiers on 5 convolutional networks and 4 MLP networks for MNIST and CIFAR-10 under the same set of 1000 images and perturbation
reported in [35 3y 26 Among the baselines, kPoly (35 OptC2V B7 and PRIMA R utilize state-of-the-ee art multi neutrnn linear relaxation for ReLUs and can bypass the single-neuron convex relaxation barrier 30 and are among the strongest incomplete verifiers. 3-CROWN FSB achieves better verified accuracy on all models using a similar or less amount of time. Some models, such as MNIST Conv Big and CIFAR ConvBig, are quite challenging- the verified accuracy obtained by 3-CROWN FSB is close to the upper bound found via PGD attack.
To make more comprehensive evaluations, in Table 3 we further compare against state-of-the-art semidefinite programming (SDP) based verifier, SDP-FO (9) on one MNIST and six CIFAR-I0 10 models reported in their paper. The models were trained using adversarial training, which posed challenge for verification (28). The SDP formulation can be tighter than linear relaxation based ones, but it is computationally expensive- SDP-FO takes 2 to 3 hours to converge on GPU for verifying a single property, resulting 5,400 GPU hours to verify 200 testing images with 10 labels each. Due to resource limitations, evaluate verified accuracy on the same set of 200 test images for other baselines. We include a concurrent work PRIMA 26 the strongest multi-neuron linear relaxation baseline in Table which generally outperforms kPoly and OptC2V. Table 3 shows that overall we are 3 orders of magnitude faster than SDP-FO while still achieving consistently higher verified accuracy on average.
directly quote SDP-FO results from M on the same set of models. We
Tightness of verification. In Figure 2 we compare the tightness of verification bounds against SDP-FO on two adversarially trained networks from 9 Specifically, we use the verification objective
8

---

Table 2: Verified accuracy (%) and avg. time (8) of 1000 images evaluated the ERAN models in kPoly, OpIC2V and PRIMA are strong incomplete verifiers that can break the convex relaxation barrier 30 The average time reported by us excludes examples that are classified incorrectly.
35
26
Dataset
Model
CROWN/DeePPoly [66
kPoly
35
Og/C2V Ex Time(s)
PRIMA!
26
5-CROWN FSB
Upper bound
(Same settings as t5 k2 26
Venfied%
Time (4)
Ver:%
Time(s)
Ver: 56
Ver:%
Time(()
Ver.%
Time(s
MLP 100F
42.9
51.0
69.9
84.2
MNIST
MLPS.. 8 x 100
18.2
14
36.9
171
38.4
759
42.8
301
62.0
103
82.0
MLP 5 x 200
29.2
24
57.4
187
60.1
403
69.0
224
77.4
86
90.1
MI.P% x 200
25.9
50.6
464
52.8
3451
62.4
73.5
95
91.1
Con-Small
15.8
3
34.7
477
43.6
55
59.8
42
72.7
7.0
73.2
ConyBig
71.1
21
73.6
40
77.1
102
77.5
11
79.3
3.1
80.4
ConvSmail
35,9
105
44.6
13
46.3
45.
CIFAR
Con/Big
42.1
43
45.9
346
No public code
48.3
176
$1.6
15.3
$5.0
ResNer
24,1
1
24.5
91
cannot run
24.8
1.7
24.8
1.6
24.8
CROWNieepPoly evaluated on CPU. 1 PRIMA concurmet work
resultss are from
(Oet
version), except ResNet results Because these MLP models are fairly small, some
are from personal communications with the authors due a different input narmalization used. of their intermediate layer bounds computed by mixed integer programming (MIP) using 90% time budget before brunch and bound starts and A-CROWN FSD is used during the branch and hound process. find that righter intermediate bounds by
beneficial these small MLP models.
Table 3: Verified accuracy (%) and avg. per-example verification time (s) on 7 models from SDP-FO M
CROWNieeePPoly are fast but loose bound propagation based methods, and they cannot he improved with more running time. SDP-FO uses stronger semidefinite relaxations, which can be very slow and sometimes has convergence issues. PRIMA, concurrent work, is the sfate-of-the-arr relaxation barrier breaking method; we
did not include kPoly and OpIC2V because they are weaker than PRIMA (see Table 2
Dataset
Model
CROWN/DeePPoly
SDP-FO MJ'
PRIMA
X
3-CROWN FSB
Upper bound
= 0.3 and
2/255
Verified%
Time (8)
Ver.%
Time(s)
Ver%%
Time(s)
Ver
Time(s)
MNIST
CNN-A-Adv
1.0
0.1
43.4
>2hh
44.5
135.9
70.5
21.1
76.5
CNN-B-Adv
21.5
0.5
32.8
>25h
38.0
343.6
46.5
32.2
65.0
CNN-B-Adv-4
43.5
0.9
46.0
>25h
53.5
43.8
54.0
11.6
63.5
CNN-A-Adv
35.5
0.6
39.6
>25h
41.5
4.8
44.0
5.8
50.0
CIFAR
CNN-A-Ads-4
41.5
0.7
40.0
>25h
45.0
4.9
46.0
5.6
49,5
CNN-A-Mix
23.5
0.4
2-5hh
37.5
34.3
41.5
49.6
CNN-A-Mix-4
38.0
0.5
47.8
>25h
48.5
7.0
50.5
5.9
57.5
SDP-FO results are directly from their paper due to its very long running time (>20th per example). 1 PRIMA experiments were done using commit examples (first 200 examples of CIFAR-10 dataset) and we don't 't run verifiers on examples that are classified incorrectly or can be attacked 200-step PGD. B-CROWN
commit396de77a [396dc7a] released on June 4, 2021. PRIMA and 3-CROWN FSB results are on the same set of 200
GPU and I CPU; PRIMA uses GPU and 20 CPUs.
f(x) : 2y 21 (x) - zgy (z), where 2(4) is the logit layer output, y/ and y' are the true label and the runner-up label. For each test image, a 200-step PGD attack A provides an adversarial upper bound of the optimal objective: / < J. Verifiers, on the other hand, can provide a verified lower bound I -" Bounds from tighter verification methods lie closer to line y = x in Figure 2 Figure 2 shows that on both PGD adversarially trained networks, 3-CROWN FSB consistently outperforms SDP-FO for all 100 random test images. Importantly, for each point on the plots, 3-CROWN FSB needs 3 minutes while SDP-FO needs 178 minutes on average. LP verifier with triangle relaxations produces much looser bounds than 3-CROWN FSB and SDP-FO. Additional results are in Appendix C.2
VNN-COMP 2021 results. We encourage the readers to checkout the report of the Second Inter- national Verification of Neural Networks Competition (VNN-COMP 2021) 3 with 9 additional benchmarks and 12 competing methods evaluated in a standardized testing environment on AWS. Our entry R.B-CROWN is based on the 33CROWN algorithm in this work and uses the same codebase.
5 Related Work
Many early complete verifiers for neural networks relied on existing solvers such MILP or SMT
solvers 20 13
38 and were limited to very small problem instances. Branch and bound (BaB)
Verified lower bound
Wortfldd lower bound
A
é CROWN LP
1 2
BCRRWWN
A.
LP
5D0-10
PGD
PGD ly-xi
edversarial upper bound
PGD adverserial upper bound
()) MNIST CNN-A-Ady, runner up targets, 0.3
(b) CIFAR CNN B-Ady, runner up targets, 2/255
Figure 2: Verified lower bound v.s. PGD adversarial upper bound. A lower bound closer to the upper bound
(closer to the line y x) is better. 8-CROWN FSB uses 3mins while SDP-FO needs 2 to hours per point.

---

based method was proposed to better exploit the network structure using LP-based incomplete verifier for bounding and ReLU splits for branching E EC
23
[5. Besides branching on ReLU neurons,
input domain branching was also considered in 41 29
but limited by input dimensions [8].
Recently, few approaches have been proposed use efficient iterative solvers bound propagation methods on GPUs without relying on LP solvers. Bunel et al. [ decomposed the verification problem layer by layer, solved each layer a closed form on GPUs, and used Lagrangian to enforce consistency between layers. However, their formulation only has the same power as LP and needs many iterations to converge. De Palma al. [TO]] used a dual-space verifier with linear relaxation 2 3 tighter than triangle LP relaxation, but in most settings the extra computational costs and difficulties for an efficient implementation offset its benefits (more discussions in section B.2) A concureet work BaDNB (II] proposed a new branching strategy, filtered smart branching (FSB), combined with Lagrangian decomposition to get better verification performance. Xu et al. 44 used CROWN as a massively paralleled incomplete solver on GPUs for complete verification, but it cannot handle neuron split constraints, leading to suboptimal efficiency and high timeout rates.
For incomplete verification, Salman et al. B3 shows the inherent limitation of using per-neuron convex relaxations for verification problems. Singh et al. 35 and Müller et al. [26] broke this barrier by considering constraints involving multiple ReLU neurons; Tjandraatmadja et al. 37 proposed to relax linear layer with ReLU neuron together using strong mixed-integer programming formu- lation [.. SDP based relaxations 28
16 14] typically produce tight bounds but with significantly higher cost. The most recent GPU based SDP verifier [ is still relatively slow and can take hours to verify single image. In this work, we impose neuron split constraints using B-CROWN and combine with branch and bound done in parallel on GPUs. Although for each subdomain in BaB, 3-CROWN is still subject to the convex relaxation barrier, the efficiency of B- B-CROWN BaB allows it to quickly explore a very large number of subdomains and outperform existing convex barrier breaking incomplete verifiers under many scenarios in both runtime and tightness.
Additionally, another line of works train networks enhance verified accuracy, typically using cheap incomplete verifiers at training time 42 39
32). Traditionally only these intiecatiionusttmizzeee networks can have reasonable verified accuracy, while 8-CROWN BaB can also give non-trivial verified accuracy on relatively large networks agnostic to verification.
25
43
18
25
47
4
Conclusion
We proposed 3-CROWN, new bound propagation method that can fully encode the neuron split constraints introduced in BaB, which clearly leads in both complete and incomplete verification settings. The success of B-CROWN comes from few factors: (1) In Section 3.1 we show that 3- CROWN is an GPU-friendly bound propagation algorithm significantly faster than LP solvers. (2) In Section 3.2, we show that 3-CROWN is solving an equivalent problem of the LP verifier with neuron split constraints. (3) In Section 3.3 we show that 3-CROWN can jointly optimize intermediate layer bounds and achieve tighter bounds than rypical LP verifiers using fixed intermediate layer bounds.
Limitations. Our verifier has several limitations which are commonly shared by most existing BaB-based complete verifiers. First, we focused on ReLU which can be split into two lincar cases. For other non-piecewise linear activation functions, although it is still possible to conduct branch and bound, it is difficult to guarantee completeness. Second, we discussed only the norm perturbations for input domains. In practice, the threat model may involve complicated and nonconvex perturbation specifications. Third, although our GPU accelerated verifier outperforms existing ones, all BaB based verifiers, including ours, are still limited to relatively small models far from the ImageNet scale. Finally, we have only demonstrated robustness verification of image classification tasks, and generalizing it to give verification guarantees for other tasks such as robust deep reinforcement is an interesting direction for future work.
learning [2 48 40
Societal Impact
NNs have been used in an increasingly wide range of real-world applications and play an important role in artificial intelligence (AI). The trustworthiness and robustness of NNs have become crucial factors since Al plays an important role in modern society. 3 3-CCRWN is strong neural network verifier which can be used to check certain properties of neural networks, which can be helpful for guaranteeing the robustness, correctness, and fairness of NNs in applications that can directly or indirectly impact human life. We believe our work has overall positive societal impacts, although it may potentially be misused to identify the weakness of NNs and guide attacks.
10

---

Acknowledgement
This work supported by NSF grant CNS18-01426; an ARL Young Investigator (YIP) award; an NSF CAREER award; Google Faculty Fellowship; Capital One Research Grant; and a J.P. Morgan Faculty Award; Air Force Research Laboratory under FA8750-18-2200553 18-2-0058; NSF IIS-1901527, NSF IIS-2008 173 and NSF CAREER-2048288 and NSF CNS-193235I. Huan Zhang is supported by funding from the Bosch Center for Artificial Intelligence.
References
[1] G. Anderson, S. Pailoor, I. Dillig. and S. Chaudhuri. Optimization and abstraction: A synergistic approach for analyzing neural network robustness. In Proceedings of the 40th ACM SIGPLAN Conference on Progranmiing Language Design and Implementation (PLDI), 2019.
[2] R. Anderson, J. Huchette, Tjandraatmadjaa, and J. Vielma. Strong convex relaxations and mixed-integer programming formulations for trained neural networks. Mathematical Programming. 2020.
[3] S. Bak, C. Liu, and T. Johnson. The second international verification of neural networks competition (ynn-comp 2021): Summary and results. arXiv preprint arXiv:2109.0045 2021.
[4] M. Balunovic and M. Vechev. Adversarial training and provable defenses: Bridging the gap. In International Conference on Learning Representations (ICLR). 2020.
[5] E. Botoeva, P. Kouvaros, J. Kronqvist, A. Lomuscio, and R. Misener. Efficient verification of relu-based neural networks via dependency analysis. AAAI Conference on Artificial Intelligence (AAAI), 2020.
[6] R. Bunel, A. De Palma, A. Desmaison, K. Dvijotham, Kohli, H. S. Torr, and M. Kumar. Lagrangian decomposition for neural network verification. Conference Uncertainty in Artificial Intelligence (UAI), 2020.
[7] R. Bunel, J. Lu, I. Turkaslan, P. Kohli, P. Torr, and P. Mudigonda. Branch and bound for piecewise linear neural network verification. Journal of Machine Learning Research (JMLR), 2020.
[8] R. R. Bunel, I. Turkaslan, P. Torr, P. Kohli, and P. K. Mudigonda. unified view of piecewise linear neural network verification. In Advances in Neural Information Processing Systems (NeurIPS), 2018.
[9] S. Dathathri, K. Dvijotham, A. Kurakin, A. Raghunathan, Uesato, R. Bunel, S. Shankar, J. Steinhardt, I. Goodfellow, P. S. Liang, et al. Enabling certification of verification-agnssicc networks via memory-efficient semidefinite programming. Advances in Neural Information Processing Systems (NeurIPS), 2020.
[10] A. De Palma, H. Behl. R. Bunel, P. H. S. Torr, and M. P. Kumar. Scaling the convex barrier with active sets. International Conference on Learning Representations (ICLR). 2021.
[11] A. De Palma, Bunel, A. Desmaison, K. Dvijotham, Kohli, H. Torr, and M. P. Kumar. Improved branch and bound for neural network verification via lagrangian decomposition. arXiv preprint Ttl::2044.06111 2021.
[12] Dutta, S. Jha S. Sankaranarayanan, and A. Tiwari, Output range analysis for deep feedforward neural networks. NASA Formal Methods Symposium, 2018.
[13] K. Dvijotham, R. Stanforth, S. Gowal, T. Mann, and P. Kohli. A dual approach to scalable verification of deep networks. Conference on Uncertainty in Artificial Intelligence (UAI), 2018
[14] K. D. Dvijotham, R. Stanforth, S. Gowal, C. Qin, S. De, and P. Kohli. Efficient neural network verification with exactness characterization. Conference on Uncertainty in Artificial Intelligence ( (UAI), 2020.

---

[15] R. Ehlers. Formal verification of piece-wise linear feed-forward neural networks. In Interna- tional Symposium on Automated Technology for Verification and Analysis (ATVA), 2017.
[16] M. Fazlyab, M. Morari, and G. J. Pappas. Safety verification and robustness analysis of neural networks via quadratic constraints and semidefinite programming. IEEE Transactions Automatic Control, 2020.
[17] T. Gehr, M. Mirman, D. Drachsler-Cohen, P. Tsankov, S. Chaudhuri, and M. Vechev, Ai2: Safety and robustness certification of neural networks with abstract interpretation. In 2018 IEEE Symposium on Security and Privacy (SP). IEEE, 2018.
[18] S. Gowal, K. Dvijotham, R. Stanforth, R. Bunel, C. Qin, J. Uesato, T. Mann, and P. Kohli. On the effectiveness of interval bound propagation for training verifiably robust models. Proceedings of the IEEE International Conference on Computer Vision (ICCV), 2019.
[19] X. Huang, M. Kwiatkowska, S. Wang, and M. Wu. Safety verification of deep neural networks. In International Conference on Computer Aided Verification (CAV), 2017.
[20] G. Katz, C. Barrett, D. L.. Dill, K. Julian, and M. J. Kochenderfer. Reluplex: An efficient smi solver for verifying deep neural networks. In International Conference on Computer Aided Verification (CAV), 2017.
[21] D. P. Kingma and J. Ba. Adam: A method for stochastic optimization. International Conference on Learning Representations (ICLR), 2015.
[22] C. Liu and T. Johnson. Vnn comp 2020. URL httth://ssttsss... http:///tte..oogeee..o//////////
vnncomp
[23] Lu and M. P. Kumar. Neural network branching for neural network verification. International Conference Learning Representation (ICLR), 2020.
[24] A. Madry, A. Makelov, L. Schmidt, D. Tsipras, and A. Vladu. Towards deep learning models resistant to adversarial attacks. In International Conference on Learning Representations (ICLR), 2018.
[25] M. Mirman, T. Gehr, and M. Vechev. Differentiable abstract interpretation for provably robust neural networks. In International Conference on Machine Learning (ICML), 2018.
[26] M. N. Müller, G. Makarchuk, G. Singh, M. Püschel, and M. Vechev. Precise multi-neuron abstractions for neural network certification. arXiv preprint arXiv:2103.0366 2021.
[27] A. Pattanaik, Z. Tang, S. Liu, G. Bommannan, and G. Chowdhary. Robust deep reinforcement learning with adversarial attacks. arXiv preprint arXiv:1712.03632. 2017.
[28] A. Raghunathan, J. Steinhardt, and P. S. Liang. Semidefinite relaxations for certifying robustness to adversarial examples. In Advances in Neural Information Processing Systems (NeurIPS), 2018.
[29] V. R. Royo, R. Calandra, D. M. Stipanovic, and C. Tomlin. Fast neural network verification via shadow prices. arXiv preprini 19Xvv:192.007244 2019.
[30] H. Salman, G. Yang. H. Zhang, C.-J. Hsieh, and P. Zhang. A convex relaxation barrier to tight robustness verification of neural networks. In Advances in Neural Information Processing Systems (NeurIPS), 2019.
[31] Z. Shi, H. Zhang, K.-W. Chang, M. Huang, and C.-J. Hsich. Robustness verification for transformers. In International Conference on Learning Representations (ICLR), 2020.
[32] Z. Shi, Y. Wang. Zhang, Yi, and C.-J. Hsich. Fast certified robust training via better initial- ization and shorter warmup. Advances in Neural Information Processing Systems (NeurIPS), 2021.
[33] G. Singh, Gehr, M. Mirman, M. Püschel, and M. Vechev. Fast and effective robustness certification. In Advances in Neural Information Processing Systems (NeurIPS), 2018.
12

---

[34] G. Singh, T. Gehr, M. Püschel, and M. Vechev. Boosting robustness certification of neural networks. International Conference on Learning Representations, 2018.
[35] G. Singh, R. Ganvir, M. Püschel, and M. Vechev. Beyond the single neuron convex barrier for neural network certification. In Advances in Neural Information Processing Systems (NeurIPS), 2019.
[36] G. Singh, T. Gehr, M. Püschel, and M. Vechev. An abstract domain for certifying neural networks. Proceedings of the ACM on Programming Languages (POPL), 2019.
[37] C. Tjandraatmadja. R. Anderson, Huchette, W. Ma, K. Patel, and J. P. Vielma. The convex relaxation barrier, revisited: Tightened single-neuron relaxations for neural network verification. Advances in Neural Information Processing Systems (NeurIPS), 2020.
[38] V. Tjeng, K. Xiao, and R. Tedrake. Evaluating robustness of neural networks with mixed integer programming. International Conference on Learning Representations (ICIRR, 2019.
[39] S. Wang, Y. Chen, A. Abdou, and S. Jana. Mixtrain: Scalable training of formally robust neural networks. arXiv preprint
2018.
[40] S. Wang, K. Pei, J. Whitehouse, J. Yang, and S. Jana. Efficient formal safety analysis of neural networks. In Advances in Neural Information Processing Systems (NeurIPS), 2018.
[41] S. Wang, K. Pei, J. Whitehouse, J. Yang, and S. Jana. Formal security analysis of neural networks using symbolic intervals. In USENIX Security Symposium, 2018.
[42] E. Wong and 7. Kolter. Provable defenses against adversarial examples via the convex outer adversarial polytope. In International Conference on Machine Learning (ICMI.), 2018.
[43] E. Wong, F. Schmidt, H. Metzen, and J. Z. Kolter. Scaling provable adversarial defenses. In Advances in Neural Information Processing Systems (NeurIPS). 2018.
[44] K. Xu, Z. Shi, H. Zhang. Y. Wang, K.-W. Chang, M. Huang, B. Kailkhura, X. Lin, and C.-J. Hsieh. Automatic perturbation analysis for scalable certified robustness and beyond. Advances in Neural Information Processing Systems (NeurIPS). 2020.
[45] K. Xu, H. Zhang, S. Wang, Wang, Jana, X. Lin, and C.-J. Hsich. Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. International Conference on Learning Representations (ICLR), 2021.
[46] H. Zhang. T.-W. Weng, P.-Y. Chen, C.-J. Hsieh, and L. Daniel. Efficient neural network
robustness certification with general activation functions. In Advances in Neural Information Processing Systems (NeurIPS), 2018.
[47] H. Zhang, H. Chen, C. Xiao, B. Li, D. Boning, and C.-J. Hsich. Towards stable and effi- cient training of verifiably robust neural networks. In International Conference on Learning Representations (ICLR), 2020.
[48] H. Zhang, H. Chen, C. Xiao, B. Li, M. Liu, D. Boning, and C.-J. Hsieh. Robust deep rein- forcement learning against adversarial perturbations on state observations. Advances Neural Information Processing Systems (NeurIPS), 2020.
[49] H. Zhang, H. Chen, D. Boning, and C.-J. Hsieh. Robust reinforcement learning on state obser- vations with learned optimal adversary. International Conference on Learning Representations (ICLR), 2021.
13


Reviews:
[{"review_id": "rMhpFrBreus", "reviewer": "Reviewer_vGgK", "summary": "The paper develops a bound propagation method for neural network verification.\nDifferently from related work, the method adds support for ReLU split constraints \nthereby offering a more efficient way (than linear programming) to bound a\nverification problem under the constraints.\n", "questions": "", "limitations": "", "rating": 7, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "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": "Bound propagation methods were shown particularly effective in both incomplete\nand complete verification, where in the latter case they are commonly used to\nderive strong MILP formulations of the verification problem in question.\nHowever, in the case of customised BaB methods for neural network verification,\nwhere the verification sub-problems resulting from branching on the ReLU nodes\nneed to be bounded, propagation methods cannot handle the ReLU constraints\nintroduced from branching. I believe that the paper makes a significant\ncontribution towards overcoming this shortcoming, thus contributing to improved\nscalability in complete verification.  Indeed, the extensive experimental\nresults speak for themselves of the attractiveness of the approach.\n\nThe paper is very well written and easy to follow. Some typos that I found: \n\nLine 108: u \\leq \\upsilon \\leq l -> l \\leq \\upsilon \\leq u ?\nLine 135: intersection -> union ?\n\n", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "The authors adequately addressed the limitations of their work. There is no discussion on potential negative societal impact of their work.", "review_text": "", "extra_scores": {"needs_ethics_review": "No", "ethics_review_area": "", "time_spent_reviewing": "3"}, "extra_text": {}}, {"review_id": "db33Hmd_DuO", "reviewer": "Reviewer_pv7s", "summary": "The paper presents Beta-CROWN, a novel algorithm to compute bounds on the output of neural network activations.\nBeta-CROWN is designed to be employed within recent branch-and-bound frameworks [6, 10], resulting in an effective complete (or incomplete, when returning early) verification algorithm.\n\nThe authors build on the bounding algorithm presented in [43] (\"alpha-CROWN\"), which (with fixed intermediate bounds) is an effective solver for the popular triangle LP relaxation (Planet [14]) of ReLU neural networks.\nThe main contributions of the paper are the following:\n- differently from alpha-CROWN, beta-CROWN can represent the effect that a ReLU split at the i-th layer has on the activations preceding it, leading to tighter bounds within branch and bound;\n- when jointly optimizing over intermediate bounds and output bounds, beta-CROWN shares fewer parameters between the various sub-problems, resulting in tighter final bounds.", "questions": "", "limitations": "", "rating": 6, "confidence": 5, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "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": "**Strengths:**\nAlpha-CROWN [43] has shown the potential of optimized propagation-based methods within branch and bound for neural network verification, resulting in very fast complete verification on easier verification properties.\nBeta-CROWN successfully addresses the main weakness of alpha-CROWN (lack of split constraint support), enhancing performance on the harder properties and improving upon the considered baselines.\n\n**Concerns:**\nWhile the empirical results look good, I believe the presentation of the paper is rather confusing. Beta-CROWN is an incremental improvement over alpha-CROWN, the main difference being the addition of split constraints in the formulation (see equation (32) for a dual perspective).\nWhile this is not a problem per se, the connection seems to be systematically understated in the paper: for instance, alpha-CROWN should be properly described in section 2, whereas the presentation in section 3 rarely mentions alpha-CROWN [43] and does not cite it when introducing the optimization over the alpha variables (lines 197-200). As made clearer in the Appendix, the results in section 3.2 follow from results in alpha-CROWN with only minor modifications to include split constraints (yet this discussion is absent in the main paper).\nFurthermore, from a quick reading, it would appear like beta-CROWN is the first GPU-accelerated dual bounding algorithm (excluding LP solvers) that can incorporate split-constraints (lines 136,137,149), however they were naturally incorporated by some previous methods such as [5, 9, 12] (as mentioned by the authors in Appendix B.2).\n\nI feel like ablation studies are missing: the importance of the joint optimization of intermediate bounds is often stressed. However, how much improvement is due to the split constraints, and how much to the joint optimization? What would be the performance if tight intermediate bounds were computed only once, before any branching? In addition, it would be great if the authors could investigate the performance of the algorithm if the alpha variables from alpha-CROWN are not optimized over.  \n\nThe authors could perhaps tone down the claims on the relative performance of Beta-CROWN to other GPU-based verifiers (lines 59-60). For instance, Beta-CROWN on average does not appear to be \"2 to 7\" times faster than [10] (and [9]) on the Wide and Deep networks of Table 1. Moreover, the relative improvement over [10] further decreases when part of its contributions (the FSB branching strategy) are not integrated within Beta-CROWN.\n\nFinally, the incomplete verification results (verified accuracy) in the main paper should include more branch-and-bound-based incomplete verifiers such as alpha-CROWN [43] (and the experiments on [9] presented in the Appendix), which may be stronger baselines than the ones considered.", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "I could not find any detailed description of the limitations of the paper. While most of the limitations are shared with many works in the area of neural network verification, the authors could point out to the fact that proposed method only deals with ReLU activations, or state the assumptions on the input-output specifications of the networks to be verified (for instance, convexity of the input set).", "review_text": "", "extra_scores": {"needs_ethics_review": "No", "ethics_review_area": "", "time_spent_reviewing": "7"}, "extra_text": {}}, {"review_id": "Ys61TbYJp9d", "reviewer": "Reviewer_qX8M", "summary": "The paper deals with efficiently incorporating CROWN into the branch-and-bound framework for complete verification. The authors propose to relax the split constraints using Lagrangian relaxation, and show how this can be done within the bound propagation framework. They also jointly optimise the intermediate bounds to tighter verification.\n\nThe technical contribution is fairly simple.\n\nThe method gives good improvements over existing complete verification methods. Authors have done a very good experimental evaluation, on different datasets and compared with many baselines.\n\nThe writing is good overall. Sections 2 and 3 are very well written. I have some comments which I have added in the main review.\n\nThe related work section and conclusion section need some work.\n", "questions": "", "limitations": "", "rating": 6, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "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": "The paper proposes a new method for neural network verification (mainly complete verification), which gives state-of-the-art results on a wide range of datasets. The authors propose a technique to deal with neuron split constraints while using CROWN within branch-and-bound.  \n\nThe key idea is to use Lagrangian relaxation to relax the split constraints. This is done in a way such that linear bound propagation can still be used. The idea is fairly simple, and the method section is well written. The authors also jointly optimize the intermediate bounds. \n\nThis technique is very useful for the verification community. CROWN has been a state-of-the-art incomplete verifier but has not had much success in complete verification. This technique allows the use of efficient CROWN style algorithms to speed up complete verification.\n\nI have a few comments:\n1. Introduction\n- I don't see why the authors have not added the details about using Lagrangian relaxation to relax the split constraints in L46-48? It would help better understand what alpha and beta are in L48.\n\n2. Section 3\n- The layer constraints seem to be missing from Eq 2.\n- L186-188 are good. This intuition can be brought forward to the introduction too. It takes 4 pages before anything about the actual method is brought. Giving detail about the Lagrangian function in the introduction would help better capture the interest of the reader.\n\n3. Experimental Results\n- In section 4.1, are all these methods run on the same machine (GPU and CPU)?\n- The colours in Fig.1 are quite confusing. It takes many minutes to understand the figure, maybe remove some baselines to avoid confusion.\n\n4. Related Work\n- L334 discussion about [35] is factually incorrect. They do not relax a layer of neurons. They give a relaxation for composition of linear+ReLU. Please be careful when writing related work.\n- L336 I don't think you are breaking the convex barrier since you are still using the planet relaxation. From your definition, all bab methods will break the barrier. I don't think that is the point that the convex barrier paper is trying to make.\n- The main comparing baselines seem to be [9, 10 and 42]. So discuss these more thoroughly. The description about [9] is not clear.\n\n6. Conclusion\n- No future work is mentioned.\n- No limitations mentioned.\n- No broader impact discussed.\nPlease add these\n\n\n====================================\n\n***Updates after rebuttal***\n\nI would like to thank the authors for answering the questions. I hope that the authors will indeed add the limitations in the main paper. My initial questions were sufficiently answered by the authors.\nHowever, some points raised by other reviewers are valid. I also believe that the technical delta over alpha-crown is incremental.\nThe experimental results are good and I am still voting for acceptance.\n", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "The paper does not discuss limitations or societal impact. A potential negative societal impact is that since verification exposes potential flaws in networks, it can be misused too.", "review_text": "", "extra_scores": {"needs_ethics_review": "No", "ethics_review_area": "", "time_spent_reviewing": "5"}, "extra_text": {}}, {"review_id": "C-7RlQwWgn3", "reviewer": "Reviewer_kL3f", "summary": "The authors propose an augmentation to CROWN that leverages weak duality to enable neuron-split constraints. This approach is amenable to GPU acceleration and can theoretically attain (or even surpass) the bounds produced by the costlier LP based incomplete verification methods. ", "questions": "", "limitations": "", "rating": 7, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "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": "Originality: \nAt its heart, this approach is a small tweak to well-established techniques that introduces a new set of optimization variables (the beta variables) than can then be optimized in a similar fashion to the alpha's (i.e. in the Fast-and-complete paper). The notation is heavy, but the idea itself is quite simple. Similarly, the proofs are only minor modifications to existing results. The related work is clearly and fairly compared against, and it the exact contributions of this work are clearly delineated. \n\nClarity:\nThe paper is clearly written and easy to follow (for CROWN-style papers, which are notoriously heavy in their notation). The lengthy derivations are conveniently pushed to the appendices and only the relevant details are kept in the main paper. In some of the experiments, it is not \n\nQuality: \nThe experimentation section is very thorough and extremely convincing. The approach presented by the authors is the new state-of-the-art for both complete and incomplete neural network verification on a standard set of benchmark networks and properties. I have very little to complain about here: while the tweak to CROWN is fairly minor, the resulting method wins in both the verification% and time against the extensive set of benchmarks considered. Certainly it would be interesting to also consider cases outside of the VNN suite of metrics, such as i) ablating against a lack of GPU to demonstrate how much GPU acceleration helps here, ii) considering different domains outside of image classification or the standard benchmark models, iii) considering different threat models; but the lack of these results does not detract from the paper. From a theoretical standpoint, the comparisons to the dual form and arguments that Beta-CROWN can attain the same LP bounds with the same intermediate layer bounds (and improve when the intermediate layer bounds are adaptive), is a nice addition to the paper and increases the strength of this submission. \n\nSignificance: \nThe problem of verifying neural networks against adversarial inputs is very important, and this work extends SOTA in that domain. Bound propagation methods, or complete verification techniques, however, still do not show the promise of being able to provide meaningful guarantees against large SOTA image classifiers (such as Resnet50, etc). While this work certainly is better than existing works, I'm hesitant to highly praise a line of work that seems unlikely to ever be applicable to real-world networks, or even the standard threat-models for the small networks. Chipping away at faster and tighter bounds on small networks and small threat models seems like a great way to get papers published, but I require more convincing that this line of work has the potential to be applicable to the networks or threat models used in practice. \n\nOverall: \nThis paper clearly explains an approach that modifies existing techniques to extend the state of the art for a problem that is important and receives significant attention within the community. I am dubious of this approach for long-term success or impact, but for the stated problem, this is the best solution we have right now and I'd like to see this paper accepted. \n\nSome typos: \nline 108 and 506: inequalities should be flipped to show $l <= v <= u$ \n", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "The limitations of this approach were not addressed, nor were the societal impacts. For methods guaranteeing safety of neural networks, the societal impacts are mostly beneficial and can be read in many other papers. It would be nice to see the authors address the potential limitations of this work. ", "review_text": "", "extra_scores": {"needs_ethics_review": "No", "ethics_review_area": "", "time_spent_reviewing": "4"}, "extra_text": {}}]

Author rebuttal:

Meta-review: The paper was well-received. The main idea is fairly simple, but the problem is important and the writing and empirical evaluation are solid. Based on the reviewers' advice, I am recommending acceptance. Please make sure to add to the final version the new results and the text on limitations and societal impact that you described in your author response. 
Decision: Accept (Poster)