Beta-CROWN: Efficient Bound Propagation with Per-neuron Split Constraints for Neural Network Robustness Verification
Year: 2022

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 -CROWN, a new bound propagation based method that can fully encode neuron splits via optimizable parameters constructed from either primal or dual space. When jointly optimized in intermediate layers, -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, -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 ↵, -CROWN (alpha-beta-CROWN) verifier, the winning tool in VNN-COMP 2021. Our code is available at http://PaperCode.cc/BetaCROWN.

heading: 1 Introduction
text: 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 outputs (e.g., the difference between the predictions of the true label and another target label), within a bounded input set as constraints. This is a challenging problem due to the non-convexity and high dimensionality of neural networks.
35th Conference on Neural Information Processing Systems (NeurIPS 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 [8] involving (1) branching by recursively splitting the original verification problem into subdomains (e.g., splitting a ReLU neuron into positive/negative linear regions by adding split constraints) and (2) bounding each subdomain with specialized incomplete verifiers. Traditional BaB-based verifiers use expensive linear programming (LP) solvers [15, 23, 7] as incomplete verifiers which can fully encode neuron split constraints. Meanwhile, a recent verifier, Fast-and-Complete [45], demonstrates that cheap incomplete verifiers can significantly 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, 41, 13, 17, 36, 44], i.e., maintaining and propagating tractable and sound bounds through networks, and CROWN [46] is a 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 x, y 2 [ 1, 1], they can bound a ReLU’s input x + y as [ 2, 2] but they have no means to consider neuron split constraints such as x y 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 [45], leading to incompleteness unless costly checking is performed.
In our work, we develop a new, fast bound propagation based incomplete verifier, -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. -CROWN contains optimizable parameters which come from propagation of Lagrangian multipliers, and any valid settings of these parameters yield sound bounds for verification. These parameters are optimized using a 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 , allowing - CROWN to tighten relaxations and outperform typical LP verifiers with fixed intermediate layer bounds. Unlike traditional LP-based BaB methods, -CROWN can be efficiently implemented with an automatic differentiation framework on GPUs to fully exploit the power of modern accelerators. The combination of -CROWN and BaB ( -CROWN BaB) produces a complete verifier with GPU acceleration, reducing the verification time of traditional LP based BaB verifiers [8] by up to three orders of magnitudes on a commonly used benchmark suite on CIFAR-10 [6, 10]. Compared to all state-of-the-art GPU-based complete verifiers [7, 45, 10, 23, 6, 11], our approach is noticeably faster with lower timeout rates. Our algorithm empowered the tool ↵, -CROWN (alpha-beta-CROWN), which won the 2nd International Verification of Neural Networks Competition [3] (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 -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 on a few benchmarking models 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 [9] based on the semidefinite programming (SDP) relaxations [28, 14], our method obtains consistently higher verified accuracy while reducing verification time by three orders of magnitudes.

heading: 2 Background

heading: 2.1 The neural network verification problem and its LP relaxation
text: We define the input of a neural network as x 2 Rd0 , and define the weights and biases of an L-layer neural network as W(i) 2 Rdi⇥di 1 and b(i) 2 Rdi (i 2 {1, · · · , L}) respectively. For simplicity we assume that dL = 1 so W(L) is a vector and b(L) is a scalar. The neural network function f : Rd0 ! R is defined as f(x) = z(L)(x), where z(i)(x) = W(i)ẑ(i 1)(x) + b(i), ẑ (i)(x) = (z(i)(x)) and ẑ(0)(x) = x. is the activation function and we use ReLU throughout this paper. When the context is clear, we omit ·(x) and use z(i)j and ẑ (i) j 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. 1:
min f(x) := z(L)(x) s.t. z(i) = W(i)ẑ(i 1)+b(i), ẑ(i) = (z(i)), x 2 C, i 2 {1, · · · , L 1} (1)
The set C defines the allowed input region and our aim is to find the minimum of f(x) for x 2 C, and throughout this paper we consider C as an `1 ball around a data example x0: C = {x | kx x0k1 ✏} but other `p 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: if we can prove that f(x) > 0, 8x 2 C, we say f(x) is verified.
When C is a convex set, Eq. 1 is still a non-convex problem because the constraints ẑ(i) = (z(i)) are non-convex. Given unlimited time, complete verifiers can solve Eq. 1 exactly: f⇤ = min f(x), 8x 2 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 a tractable lower bound of the solution f  f⇤. If f 0, then f⇤ > 0 so f(x) can be verified; when f < 0, we are not able to infer the sign of f⇤ so cannot conclude if the specification holds or not.
A commonly used incomplete verification technique is to 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 to it as the “LP verifier” in this paper. Specifically, given ReLU(z(i)j ) := max(0, z (i) j ) and its intermediate layer bounds l (i) j  z (i) j  u (i) j , each ReLU can be categorized into three cases: (1) if l(i)j 0 (ReLU in linear region) then ẑ (i) j = z (i) j ; (2) if u(i)j  0 (ReLU in inactive region) then ẑ (i) j = 0; (3) if l (i) j  0  u (i) j (ReLU is unstable) then
three linear bounds are used: ẑ(i)j 0, ẑ (i) j z (i) j , and ẑ (i) j 
u (i) j u (i) j l (i) j
⇣ z(i)j l (i) j ⌘ ; they are often
referred to as the “triangle” relaxation [15, 42]. The intermediate layer bounds l(i) and u(i) are usually obtained from a 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 -CROWN, they have to use fixed intermediate bounds and cannot use the joint optimization of intermediate layer bounds (Section 3.3) to tighten relaxation.

heading: 2.2 CROWN: efficient incomplete verification by propagating linear bounds
text: Another cheaper way to give a lower bound for the objective in Eq. 1 is through sound bound propagation. CROWN [46] is a representative method that propagates a linear bound of f(x) w.r.t. every intermediate layer in a backward manner until reaching the input x. CROWN uses two linear constraints to relax unstable ReLU neurons: a linear upper bound ẑ(i)j  u (i) j
u (i) j l (i) j
⇣ z(i)j l (i) j ⌘ and a
linear lower bound ẑ(i)j ↵ (i) j z (i) j (0  ↵ (i) j  1). We can then bound the output of a ReLU layer:
Lemma 2.1 (ReLU relaxation in CROWN). Given w, v 2 Rd, l  v  u (element-wise), we have w
>ReLU(v) w>Dv + b0, where D is a diagonal matrix containing free variables 0  ↵j  1 only when uj > 0 > lj and wj 0, while its rest values as well as constant b0 are determined by l,u, w.
Detailed forms of each term are listed in Appendix A. Lemma 2.1 can be repeatedly applied, resulting in an efficient back-substitution procedure to derive a linear lower bound of NN output w.r.t. x: Lemma 2.2 (CROWN bound [46]). Given an L-layer ReLU NN f(x) : Rd0 ! R with weights W(i), biases b(i), pre-ReLU bounds l(i)  z(i)  u(i) (1  i  L) and input constraint x 2 C. We have
min x2C f(x) min x2C
a> CROWN x+ cCROWN
where aCROWN and cCROWN can be computed using W(i),b(i), l(i),u(i) in polynomial time.
When C is an `p 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 as GPUs [44] and TPUs [47], and it can be a few magnitudes faster than an LP verifier which is hard to parallelize on GPUs. CROWN was generalized to general architectures [44, 31] while we only demonstrate it for feedforward ReLU networks for simplicity. Additionally, Xu et al. [45] showed that it is possible to optimize the slope of the lower bound, ↵, using gradient ascent, to further tighten the bound (sometimes referred to as ↵-CROWN).

heading: 2.3 Branch and Bound and Neuron Split Constraints
text: Branch and bound (BaB) method is widely adopted in complete verifiers [8]: we divide the domain of the verification problem C into two subdomains C1 = {x 2 C, z(i)j 0} and C2 = {x 2 C, z (i) j < 0} where z(i)j is an unstable ReLU 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 Ci (denoted by fCi) is greater than 0, Ci is verified; otherwise, we further branch over domain Ci 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 ReLU in layer i, we can simply add z(i)j 0 or z (i) j < 0 to Eq. 1 and get a linearly relaxed lower bound to each subdomain. We denote the Z+(i) and Z (i) as the set of neuron indices with positive and negative split constraints in layer i. We define the split constraints at layer i as Z(i) := {z(i) | z(i)j1 0, z (i) j2
< 0, 8j1 2 Z+(i), 8j2 2 Z (i)}. We denote the vector of all pre-ReLU neurons as z, and we define a set Z to represent the split constraints on z: Z = Z(1)\Z(2)\· · ·\Z(L 1). For convenience, we also use the shorthand Z̃(i) := Z(1)\· · ·\Z(i) and z̃(i) := {z(1), z(2), · · · , z(i)}. 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.
Branching strategy. Branching strategies (selecting which ReLU neuron to split) are generally agnostic to the incomplete verifier used in BaB but do affect the overall BaB performance. BaBSR [7] is a widely used strategy in complete verifiers, which is based on an fast estimates on objective improvements after splitting each neuron. The neuron with highest estimated improvement is selected for branching. Recently, Filtered Smart Branching (FSB) [11] 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 -CROWN BaB is a general complete verification framework fit for any potential branching strategy, and we evaluate both BaBSR and FSB in experiments.

heading: 3 -CROWN for Complete and Incomplete Verification
text: In this section, we first give intuitions on how -CROWN handles neuron split constraints without costly LP solvers. Then we formally state the main theorem of -CROWN from both primal and dual spaces, and discuss how to tighten the bounds using free parameters ↵, . Lastly, we propose -CROWN BaB, a complete verifier that is also a strong incomplete verifier when stopped early.

heading: 3.1 -CROWN: Linear Bound Propagation with Neuron Split Constraints
text: The NN verification problem under neuron split constraints can be seen as an optimization problem:
min x2C,z2Z f(x). (2)
Bound propagation methods like CROWN can give a relatively tight lower bound for minx2C f(x) but they cannot handle the neuron split constraints z 2 Z . Before we present our 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 S(i) 2 Rdi⇥di in Eq. 3 where i 2 [1, · · ·L 1], j 2 [1, · · · , di] are indices of layers and neurons, respectively:
S(i)j,j = 1(if split z (i) j 0); S (i) j,j = +1(if split z (i) j < 0); S (i) j,j = 0(if no split z (i) j ) (3)
We start from the last layer and derive linear bounds for each intermediate layer z(i) and ẑ(i) with both constraints x 2 C and z 2 Z . We also assume that pre-ReLU bounds l(i)  z(i)  u(i) for each layer i are available (see discussions in Sec. 3.3 on these intermediate layer bounds). We initially have:
min x2C,z2Z f(x) = min x2C,z2Z
W(L)ẑ(L 1) + b(L). (4)
Since ẑ(L 1) = ReLU(z(L 1)), we can apply Lemma 2.1 to relax the ReLU neuron at layer L 1, and obtain a linear lower bound for f(x) w.r.t. z(L 1) (we omit all constant terms to avoid clutter):
min x2C,z2Z f(x) min x2C,z2Z
W(L)D(L 1)z(L 1) + const.
To enforce the split neurons at layer L 1, we use a Lagrange function with (L 1)>S(L 1) multiplied on z(L 1):
min x2C,z2Z f(x) min x2C
z̃(L 2)2Z̃(L 2)
max (L 1) 0
W(L)D(L 1)z(L 1) + (L 1) > S(L 1)z(L 1) + const
max (L 1) 0
min x2C
z̃(L 2)2Z̃(L 2)
⇣ W(L)D(L 1) + (L 1) > S(L 1) ⌘ z(L 1) + const
(5)
The first inequality is due to the definition of the Lagrange function: we remove the constraint z (L 1) 2 Z(L 1) and use a multiplier to replace this constraint. The second inequality is due to weak duality. Due to the design of S(L 1), neuron split z(L 1)j 0 has a negative multiplier (L 1) j and split z(L 1)j < 0 has a positive multiplier (L 1) j . Any
(L 1) 0 yields a lower bound for the constrained optimization problem. Then we substitute z(L 1) with W(L 1)ẑ(L 2) + b(L 1) for next layer:
min x2C,z2Z f(x) max (L 1) 0
min x2C
z̃(L 2)2Z̃(L 2)
⇣ W(L)D(L 1) + (L 1) > S(L 1) ⌘ W(L 1)ẑ(L 2) + const (6)
We define a matrix A(i) to represent the linear relationship between f(x) and ẑ(i), where A(L 1) = W(L) according to Eq. 4 and A(L 2) = (A(L 1)D(L 1) + (L 1) > S(L 1))W(L 1) by Eq. 6. Considering 1-dimension output f(x), A(i) has only 1 row. With A(L 2), Eq. 6 becomes:
min x2C,z2Z f(x) max (L 1) 0
min x2C
z̃(L 2)2Z̃(L 2)
A(L 2)ẑ(L 2) + const,
which is in a form similar to Eq. 4 except for the outer maximization over (L 1). This allows the back-substitution process (Eq. 4, Eq. 5, and Eq. 6) to continue. In each step, we swap max and min as in Eq. 5, so every maximization over (i) is outside of minx2C . Eventually, we have:
min x2C,z2Z f(x) max 0 min x2C
A(0)x+ const,
where := ⇥ (1)> (2)> · · · (L 1)> ⇤> concatenates all (i) vectors. Following the above idea, we present the main theorem in Theorem 3.1 (proof is given in Appendix A). Theorem 3.1 ( -CROWN bound). Given an L-layer NN f(x) : Rd0 ! R with weights W(i), biases b(i), pre-ReLU bounds l(i)  z(i)  u(i) (1  i  L), input bounds C, split constraints Z . We have:
min x2C,z2Z f(x) max 0 min x2C
(a+P )>x+ q> + c, (7)
where a 2 Rd0 ,P 2 Rd0⇥( PL 1 i=1 di),q 2 R PL 1 i=1 di and c 2 R are functions of W(i), b(i), l(i), u(i).
Detailed formulations for a, P, q and c are given in Appendix A. Theorem 3.1 shows that when neuron split constraints exist, f(x) can still be bounded by a linear equation containing optimizable multipliers . Observing Eq. 5, the main difference between CROWN and -CROWN lies in the relaxation of each ReLU layer, where we need an extra term (i)>S(i) in the linear relationship matrix (for example, W(L)D(L 1) in Eq. 5) between f(x) and z(i) to enforce neuron split constraints. This extra term in every ReLU layer yields P and q in Eq. 7 after bound propagations.
To solve the optimization problem in Eq. 7, we note that in the `p norm robustness setting (C = {x | kx x0kp ✏}), the inner minimization has a closed solution:
min x2C,z2Z f(x) max 0 ka+P kq✏+ (P>x0 + q)> + a>x0 + c := max 0 g( ) (8)
where 1p + 1 q = 1. The maximization is concave in (q 1), so we can simply optimize it using projected (super)gradient ascent with gradients from an automatic differentiation library. Since any
0 yields a valid lower bound for minx2C,z2Z f(x), convergence is not necessary to guarantee soundness. -CROWN is efficient - it has the same asymptotic complexity as CROWN when is fixed. When = 0, -CROWN yields the same results as CROWN; however the additional optimizable allows us to maximize and tighten the lower bound due to neuron split constraints.
We define ↵(i) 2 Rdi for free variables associated with unstable ReLU neurons in Lemma 2.1 for layer i and define all free variables ↵ = {↵(1) · · ·↵(L 1)}. Since any 0  ↵(i)j  1 yields a valid bound, we can optimize it to tighten the bound, similarly as done in [45]. Formally, we rewrite Eq. 8 with ↵ explicitly:
min x2C,z2Z f(x) max 0↵1, 0 g(↵, ). (9)

heading: 3.2 Connections to the Dual Problem
text: In this subsection, we show that -CROWN can also be derived from a dual LP problem. Based on Eq. 1 and linear relaxations in Section 2, we first construct an LP problem for `1 robustness verification in Eq. 10 where i 2 {1, · · · , L 1}.
min f(x) := z(L)(x) s.t.
Network and Input Bounds: z(i) = W(i)ẑ(i 1) + b(i); ẑ(0) x0 ✏; ẑ(0)  x0 + ✏;
Stable ReLUs: ẑ(i)j = z (i) j (if l (i) j 0); ẑ (i) j = 0 (if u (i) j  0);
Unstable: ẑ(i)j 0, ẑ (i) j z (i) j , ẑ (i) j 
u(i)j
u(i)j l (i) j
⇣ z (i) j l (i) j ⌘ (if l(i)j < 0 < u (i) j , j /2 Z+(i) [ Z (i))
Neuron Split Constraints: ẑ(i)j = z (i) j , z (i) j 0 (if j 2 Z +(i)); ẑ(i)j = 0, z (i) j < 0 (if j 2 Z (i)) (10)
Compared to the formulation in [42], we have neuron split constraints. Many BaB based complete verifiers [8, 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 dLP for the dual problem of Eq. 10 can be represented as
dLP = ka+P k1·✏+ (P>x0 + q)> + a>x0 + c,
where a, P, q and c are defined in the same way as in Theorem 3.1, and 0 corresponds to the dual variables of neuron split constraints in Eq. 10.
A similar connection between CROWN and dual LP based verifier [42] was shown in [30], and their results can be seen as a special case of ours when = 0 (none of the split constraints are active). An immediate consequence is that -CROWN can potentially solve Eq. 10 as well as using an LP solver: Corollary 3.2.1. When ↵ and are optimally set and intermediate bounds l,u are fixed, -CROWN produces p
⇤ LP , the optimal objective of LP with split constraints in Eq. 10:
max 0↵1, 0
g(↵, ) = p⇤ LP ,
In Appendix A, we give detailed formulations for conversions between the variables ↵, in - CROWN and their corresponding dual variables in the LP problem.

heading: 3.3 Joint Optimization of Free Variables in -CROWN
text: In Eq. 9, g is also a function of l(i)j and u (i) j , the intermediate layer bounds for each neuron z (i) j . They are also computed using -CROWN. To obtain l(i)j , we set f(x) := z (i) j (x) and apply Theorem 3.1:
min x2C,z̃(i 1)2Z̃(i 1)
z (i) j (x) max 0↵01, 0 0 g 0(↵0, 0) := l(i)j (11)
For computing u(i)j we simply set f(x) := z (i) j (x). Importantly, during solving these intermediate layer bounds, the ↵0 and 0 are independent sets of variables, not the same ones for the objective f(x) := z(L). Since g is a function of l(i)j , it is also a function of ↵ 0 and 0. In fact, there are a total
of PL 1
i=1 di intermediate layer neurons, and each neuron is associated with a set of independent ↵ 0
and 0 variables. Optimizing these variables allowing us to tighten the relaxations on unstable ReLU neurons (which depend on l(i)j and u (i) j ) and produce tight final bounds, which is impossible in LP. In
other words, we need to optimize ↵̂ and ̂, which are two vectors concatenating ↵, as well as a large number of ↵0 and 0 used to compute each intermediate layer bound:
min x2C,z2Z f(x) max 0↵̂1, ̂ 0 g(↵̂, ̂). (12)
This formulation is non-convex and has a large number of variables. Since any 0  ↵̂  1, ̂ 0 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 [8, 23, 6], 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 i as si := Tr(|S(i)|). Each neuron in layer i is associated with 2⇥ Pi 1 k=1 sk variables ↵
0. Suppose each hidden layer has d neurons (si = O(d)), then ↵̂ has 2⇥ PL 1 i=1 di Pi 1 k=1 sk = O(L 2 d 2) variables in total. This can be too large for efficient optimization, so we share ↵0 and 0 among the intermediate neurons of the same layer, leading to a total number of O(L2d) variables to optimize. Note that a weaker form of joint optimization was also discussed in [45] without , and a detailed analysis can be found in Appendix B.2.

heading: 3.4 -CROWN with Branch and Bound ( -CROWN BaB)
text: We perform complete verification following BaB framework [8] using -CROWN as the incomplete solver, and we use simple branching heuristics like BaBSR [7] or FSB [11]. To efficiently utilize GPU, we also use batch splits to evaluate multiple subdomains in the same batch as in [44, 10]. We list our full algorithm -CROWN BaB in Appendix B and we show it is sound and complete here: Theorem 3.3. -CROWN with Branch and Bound on splitting ReLUs is sound and complete.
Soundness is trivial because -CROWN is a sound verifier. For completeness, it suffices to show that when all unstable ReLU neurons are split, -CROWN gives the global minimum for Eq. 10. In contrast, combining CROWN [46] with BaB does not yield a complete verifier, as it cannot detect infeasible splits and a slow LP solver is still needed to guarantee completeness [45]. Instead, -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. 1 by splitting the problem into multiple subdomains, and more subdomains give a tighter lower bound for Eq. 1. Unlike traditional complete verifiers, -CROWN is efficient to explore a large number of subdomains during a very short time, making -CROWN BaB an attractive solution for efficient incomplete verification.

heading: 4 Experimental Results

heading: 4.1 Comparison to Complete Verifiers
text: We evaluate complete verification performance on dataset provided in [23, 10] and used in VNNCOMP 2020 [22]. The benchmark contains three CIFAR-10 models (Base, Wide, and Deep) with 100 examples each. Each data example is associated with an `1 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 baselines for complete verification: (1) BaBSR [7], 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, 33, 36, 34], an abstract interpretation based verifier which performs well on this benchmark in VNN-COMP 2020; (4) GNN-Online [23], a BaB and LP based verifiers using a learned Graph Neural Network (GNN) to guide the ReLU splits; (5) BDD+ BaBSR [6], a verification framework based on Lagrangian decomposition on GPUs (BDD+) with BaBSR branching strategy; (6) OVAL (BDD+ GNN) [6, 23], a strong verifier in VNN-COMP 2020 using BDD+ with GNN guiding the ReLU splits; (7) A.set BaBSR and (8) Big-M+A.set BaBSR [10], very recent dual-space verifiers on GPUs with a tighter linear relaxation than triangle LP relaxations; (9) Fast-and-Complete [45],
which uses CROWN (LiRPA) on GPUs as the incomplete verifier in BaB without neuron split constraints; (10) BaDNB (BDD+ FSB) [11], a concurrent state-of-the-art complete verifier, using BDD+ on GPUs with FSB branching strategy. -CROWN BaB can use either BaBSR or FSB branching heuristic, and we include both in evaluation. All methods use a 1 hour timeout threshold.
We report the average verification time and branch numbers in Table 1 and plot the percentage of solved properties over time in Figure 1. -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, -CROWN BaBSR still outperforms all literature baselines, including very recent ones such as A.set BaBSR [10], Fast-and-Complete [45] and BaDNB [11]. Our benefits are more clearly shown in Figure 1, 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 1 compared to CPU based verifiers such as MIPplanet and BaBSR.

heading: 4.2 Comparison to Incomplete Verifiers
text: 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 ✏ as reported in [35, 37, 26]. Among the baselines, kPoly [35], OptC2V [37] and PRIMA [26] utilize state-of-the-art multi-neuron linear relaxation for ReLUs and can bypass the single-neuron convex relaxation barrier [30], and are among the strongest incomplete verifiers. -CROWN FSB achieves better verified accuracy on all models using a similar or less amount of time. Some models, such as MNIST ConvBig and CIFAR ConvBig, are quite challenging - the verified accuracy obtained by -CROWN FSB is close to the upper bound found via PGD attack.
To make more comprehensive evaluations, in Table 3 we further compare against a state-of-the-art semidefinite programming (SDP) based verifier, SDP-FO [9], on one MNIST and six CIFAR-10 models reported in their paper. The models were trained using adversarial training, which posed a 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 one GPU for verifying a single property, resulting 5,400 GPU hours to verify 200 testing images with 10 labels each. Due to resource limitations, we directly quote SDP-FO results from [9] on the same set of models. We 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 2, 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. 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
* CROWN/DeepPoly evaluated on CPU. † PRIMA is a concurrent work and its results are from [26] (Oct 26, 2021 version), except that ResNet results are from personal communications with the authors due to a different input normalization used. ‡ Because these MLP models are fairly small, some of their intermediate layer bounds are computed by mixed integer programming (MIP) using 80% time budget before branch and bound starts and -CROWN FSB is used during the branch and bound process. We find that tighter intermediate bounds by MIP is beneficial for these small MLP models.
f(x) := z(L)y (x) z(L)y0 (x), where z(L) is the logit layer output, y and y0 are the true label and the runner-up label. For each test image, a 200-step PGD attack [24] provides an adversarial upper bound f of the optimal objective: f⇤  f . Verifiers, on the other hand, can provide a verified lower bound f  f⇤. Bounds from tighter verification methods lie closer to line y = x in Figure 2. Figure 2 shows that on both PGD adversarially trained networks, -CROWN FSB consistently outperforms SDP-FO for all 100 random test images. Importantly, for each point on the plots, -CROWN FSB needs 3 minutes while SDP-FO needs 178 minutes on average. LP verifier with triangle relaxations produces much looser bounds than -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 International 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 ↵, -CROWN is based on the -CROWN algorithm in this work and uses the same codebase.

heading: 5 Related Work
text: Many early complete verifiers for neural networks relied on existing solvers such as MILP or SMT solvers [20, 15, 19, 12, 38] and were limited to very small problem instances. Branch and bound (BaB)
based method was proposed to better exploit the network structure using LP-based incomplete verifier for bounding and ReLU splits for branching [8, 40, 23, 5]. Besides branching on ReLU neurons, input domain branching was also considered in [41, 29, 1] but limited by input dimensions [8].
Recently, a few approaches have been proposed to use efficient iterative solvers or bound propagation methods on GPUs without relying on LP solvers. Bunel et al. [6] decomposed the verification problem layer by layer, solved each layer in 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 et al. [10] used a dual-space verifier with a linear relaxation [2, 37] 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 concurrent work BaDNB [11] 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. [30] 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 a linear layer with a ReLU neuron together using a strong mixed-integer programming formulation [1]. SDP based relaxations [28, 16, 14] typically produce tight bounds but with significantly higher cost. The most recent GPU based SDP verifier [9] is still relatively slow and can take 2 hours to verify a single image. In this work, we impose neuron split constraints using -CROWN and combine it with branch and bound done in parallel on GPUs. Although for each subdomain in BaB, -CROWN is still subject to the convex relaxation barrier, the efficiency of -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 to enhance verified accuracy, typically using cheap incomplete verifiers at training time [42, 39, 25, 43, 18, 25, 47, 4, 32]. Traditionally only these verification-customized networks can have reasonable verified accuracy, while -CROWN BaB can also give non-trivial verified accuracy on relatively large networks agnostic to verification.

heading: 6 Conclusion
text: We proposed -CROWN, a 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 -CROWN comes from a few factors: (1) In Section 3.1, we show that - CROWN is an GPU-friendly bound propagation algorithm significantly faster than LP solvers. (2) In Section 3.2, we show that -CROWN is solving an equivalent problem of the LP verifier with neuron split constraints. (3) In Section 3.3, we show that -CROWN can jointly optimize intermediate layer bounds and achieve tighter bounds than typical 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 linear 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 learning [27, 48, 49] is an interesting direction for future work.
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 AI plays an important role in modern society. -CROWN is a 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.

heading: Acknowledgement
text: This work is supported by NSF grant CNS18-01426; an ARL Young Investigator (YIP) award; an NSF CAREER award; a Google Faculty Fellowship; a Capital One Research Grant; and a J.P. Morgan Faculty Award; Air Force Research Laboratory under FA8750-18-2-0058; NSF IIS-1901527, NSF IIS-2008173 and NSF CAREER-2048280; and NSF CNS-1932351. Huan Zhang is supported by funding from the Bosch Center for Artificial Intelligence.

Review summaries:
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.  The technical contribution is fairly simple.  The 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.  The writing is good overall. Sections 2 and 3 are very well written. I have some comments which I have added in the main review.  The related work section and conclusion section need some work. 

The paper presents Beta-CROWN, a novel algorithm to compute bounds on the output of neural network activations. Beta-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.  The 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. The main contributions of the paper are the following: - 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; - when jointly optimizing over intermediate bounds and output bounds, beta-CROWN shares fewer parameters between the various sub-problems, resulting in tighter final bounds.