Fast and Complete: Enabling Complete Neural Network Verification with Rapid and Massively Parallel Incomplete Verifiers
Authors: Kaidi Xu
Huan Zhang
Shiqi Wang
Yihan Wang
Suman Jana
Xue Lin
Cho-Jui Hsieh
Venue: ICLR 2021 Poster (2021)
Keywords: neural network verification
branch and bound

Abstract: Formal verification of neural networks (NNs) is a challenging and important problem. Existing efficient complete solvers typically require the branch-and-bound (BaB) process, which splits the problem domain into sub-domains and solves each sub-domain using faster but weaker incomplete verifiers, such as Linear Programming (LP) on linearly relaxed sub-domains.  In this paper, we propose to use the backward mode linear relaxation based perturbation analysis (LiRPA) to replace LP during the BaB process, which can be efficiently implemented on the typical machine learning accelerators such as GPUs and TPUs.  However, unlike LP, LiRPA when applied naively can produce much weaker bounds and even cannot check certain conflicts of sub-domains during splitting, making the entire procedure incomplete after BaB. To address these challenges, we apply a fast gradient based bound tightening procedure combined with batch splits and the design of minimal usage of LP bound procedure, enabling us to effectively use LiRPA on the accelerator hardware for the challenging complete NN verification problem and significantly outperform LP-based approaches. On a single GPU, we demonstrate an order of magnitude speedup compared to existing LP-based approaches.

Published as a conference paper at ICLR 2021
FAST AND COMPLETE: ENABLING COMPLETE NEU- RAL NETWORK VERIFICATION WITH RAPID AND MASSIVELY PARALLEL INCOMPLETE VERIFIERS
Kaidi Xu 111
Huan Zhang :2
Shiqi Wang
Yihan Wang
Suman Jana
Xue Lin'
Cho-Jui Hsieh
NNrtheasterrn University PUCLA
CColubbia University
xu.
w..kaie@enttthesteem.coo edu, huan@huan-zhang com, towangshiigiecs.cooumm
langylhan6117@gaal com, sumanêcs, cowumbia......omomooo.oo........ cambii..ddi edd,, xue wwe.In@ehorthhastern..ciii
chchsiehêcs. acla
ABSTRACT
Formal verification of neural networks (NNs) a challenging and important prob- lem. Existing efficient complete solvers typically require the aarch-and-bound (BaB) process, which splits the problem domain into sub-domains and solves each sub-domain using faster but weaker incomplete verifiers, such Linear Program- ming (LP) on linearly relaxed sub-domains. this paper, we propose to use the backward mode linear relaxation based perturbation analysis (LiRPA) to replace LP during the BaB process, which can be efficiently implemented on the typi- cal machine learning accelerators such GPUs and TPUs. However, unlike LP,, LiRPA when applied naively can produce much weaker bounds and even cannot check certain conflicts of sub-domains during splitting, making the entire proce- dure incomplete after BaB. To address these challenges, we apply a fast gradient based bound tightening procedure combined with batch splits and the design of minimal usage of LP bound procedure, enabling us to effectively use LiRPA on the accelerator hardware for the challenging complete NN verification problem and significantly outperform LP-based approaches. On single GPU, we demon- strate an order of magnitude speedup compared to existing L.-based approaches.
INTRODUCTION
Although neural networks (NNs) have achieved great success on various complicated tasks, they remain susceptible to adversarial examples (Szegedy et al.) 2013): imperceptible perturbations of test samples might unexpectedly change the NN predictions. Therefore, it is crucial to conduct formal verification for NNs such that they can be adopted in safety security-critical settings.
Formally, the neural network verification problem can be cast into the following decision problem:
Given neural network f-), input domain C, and property P. Vz E C, does f(x) satisfy P?
The property P is typically set of desirable outputs of the NN conditioned on the inputs. Typically, consider a binary classifier f(x) and a positive example &o (f(z) 2 0), we can set P to be non- negative numbers R+ and bounded within an Too norm ball
{x|1a Fulloc S c). The success of verification guarantees that the label of zu cannot flip for any perturbed inputs within C.
In this paper we study the complete verification setting, where given sufficient time, the verifier should give definite "yes/no" answer for property under verification. In the above setting, it must solve the non-convex optimization problem mingec f(x) to global minimum. Complete NN verification is generally challenging NP-Hard problem (Katz et al. 2017) which usually requires expensive formal verification methods such as SMT (Katz et al. 2017) or MILP solvers (Tjeng et al. 2019b). On the other hand, incomplete solvers such convex relaxations of NNs (Salman et al. 2019) can only provide a sound analysis, i.e., they can only approximate the lower bound of minzec C f(z) if and verify the property when 0. No conclusion can be drawn when 0.
Recently, a Branch and Bound (BaB) style framework (Bunel et al. 2018 20206) has been adopted for efficient complete verification. BaB solves the optimization problem mingec ((x) global

---

Published as a conference paper at ICLR 2021
minimum by branching into multiple sub-domains recursively and bounding the solution for each sub-domain using incomplete verifiers. BaB typically uses a Linear Programming (LP) bounding procedure incomplete verifier to provide feasibility checking and relatively tight bounds for each sub-domain. However, the relatively high solving cost of LPs and incapability of paralleliza- tion (especially on massively parallel hardware accelerators like GPUs TPUs) greatly limit the performance and scalability of the existing complete BaB based verifiers.
In this paper, aim to use fast and typically weak incomplete verifiers for complete verification. Specifically, we focus on a class of incomplete verifiers using efficient bound propagation oper- ations, referred as linear relaxation based perturbation analysis (LiRPA) algorithms (Xu et al., 2020). Representative algorithms in this class include convex outer adversarial polytope (Wong) Kolter, 2018), CROWN (Zhang et al., 2018) and DeepPoly (Singh et al., 2019b). LiRPA algo- rithms exhibit high parallelism as the bound propagation process is similar to forward or backward propagation of NNs, which can fully exploit machine learning accelerators (e.g., GPUs and TPUs).
Although LiRPA bounds are very efficient for incomplete verification, especially in training certified adversarial defenses (Wong et al. 2018: Mirman et al. [2018] Wang et al. 201 Sa Zhang et al. 2020), they are generally considered too loose to be useful compared to LPs in the complete verification settings with BaB. As we will demonstrate later, using LiRPA bounds naively in BaB cannot even guarantee the completeness when splitting ReLU nodes, and thus we need additional measures to make them useful for complete verification. In fact, LiRPA methods have been used to get upper and lower bounds for each ReLU neuron in constructing tighter LPs (Bunel al.. 2018 Lu & Kumar 2020). It was also used in (Wang et al. 2018c) for verifying small-scale problems with relatively low dimensional input domains using input splits, but splitting the input space can be quite ineffective (Bunel et al. 2018) and is unable to scale to high dimensional input case like CIFAR-10. Except one concurrent work (Bunel et al., 2020a), most complete verifiers are based on relatively expensive solvers like LP and cannot fully take benefit from massively parallel hardware (e.g., GPUs) to obtain tight bounds for accelerating large-scale complete verification problems. Our main contributions are:
We show that LiRPA bounds, when improved with fast gradient optimizers, can potentially out- perform bounds obtained by LP verifiers. This is because LiRPA allows joint optimization of both intermediate layer bounds of ReLU neurons (which determine the tightness of relaxation) and output bounds, while I. can only optimize output bounds with fixed relaxations on ReI.U neurons.
We show that BaB purely using LiRPA bounds is insufficient for complete verification due to the lack of feasibility checking for ReLU node splits. To address this issue, we design our algorithm to only invoke LP when absolutely necessary and exploits hardware parallelism when possible.
To fully exploit the hardware parallelism on the machine learning accelerators, we use a batch splitting approach that splits on multiple neurons simultancously, further improving our efficiency. proposed NN verification framework
On few standard and representative benchmarks, can outperform previous baselines significantly, with a speedup of around 30X compared to basic BaB+LP baselines, and up 3X compared to recent state-of-the-art complete verifiers.
2
BACKGROUND
2.1 FORMAL DEFINITION OF NEURAL NETWORK (NN) VERIFICATION
Notations of NN. For illustration, we define an L-layer feedforward NN f g + R with L weights w (i {1,.... .L)) recursively as (x) = g( hidden layer (() = ReI.U((((x)) input layer (xx())) ) = x. and final output [(x) = (x). For simplicity we ignore biases. We sometimes omit x and use h, represent the pre-activation of the j-th ReLU neuron
in i-th layer for x E C, and we use 9 to represent the post-activation value. We focus on verifying ReLU based NNs, but our method is generalizable to other activation functions supported by LiRPA.
NN Verification Problem. Given input v, its bounded input domain C, and feedforward NN f(.). the aim of formal verification is to prove or disprove certain properties P of NN outputs. Since most properties studied in previous works can be expressed as a Boolean expression over linear equation of network output, where the linear property can be merged into the last layer weights of a NN, the ultimate goal of complete verification reduces to prove or disprove:
Ya C, f(x) 2
2

---

Published as a conference paper at ICLR 2021
One way to prove Eq. is to solve mingee f(z). Due to the non-convexity of NNs, finding the exact minimum of f(z) over I E C is challenging as the optimization process is generally NP- complete (Katz al. 2017). However, in practice, sound approximation of the lower bound for f()), denoted as J, can be more easily obtained and is sufficient to verify the property. Thus, good verification strategy to get a tight approximation f can save significant time cost. Note that f must
be sound, i.e. Vx E C S f(x), proving f z 0 is sufficient prove the property fx) 2 0.
2.2 THE BRANCH AND BOUND (BAB) FRAMEWORK FOR NEURAL NETWORK VERIFICATION
Branch and Bound (BaB), an effective strategy in solving traditional combinatorial optimization problems, has been customized and widely adopted for NN verification (Bunel et al. 2018 2020b). Specifically, BaB based verification framework is recursive process, consisting of two main steps: branching and bounding. For branching. BaB based methods will divide the bounded input domain C into sub-domains {C.]C U, C, each defined as new independent verification problem. For instance, it can split a ReLU unit 9j = ReLU(h) (k)) to be negative and positive cases as Co-
cn 2 2) and C1 C n hy <0 for ReLU-based network; for each sub-domain Ci, BaB based methods perform bounding to obtain a relaxed but sound lower bound Le. A tightened global lower bound over C can then be obtained by taking the minimum values of the sub-domain lower bounds from all the sub-domains: f min; Le:- Branching and bounding will be performed recursively to tighten the approximated global lower bound over C until either (1) the global lower bound / becomes larger than 0 and prove the property or (2) a violation (e.g.. adversarial example) is located in a sub-domain to disprove the property. Essentially, we build a search tree where each leaf is a sub-domain, and the property P can be proven only when it is valid on all leaves.
Soundness of BaB We say the verification process is sound if we can always trust the "yes" (P is verified) answer given by the verifier. It is straightforward to see that the whole BaB based verification process is sound as long as the bounding method used for each sub-domain C, is sound.
Completeness of BaB The completeness of the BaB-based NN verification process, which was usually assumed true in some previous works (Bunel et al. 2020b 2018), in fact, is not always true even if all possible sub-domains are considered with a sound bounding method. Additional requirements for the bounding method required point that key factor for completeness involves feasibility checking in the bounding method which we will discuss in Section 3.2
Branching in BaB Since branching step determines the shape of the search tree, the main chal- lenge is to efficiently choose a good leaf to split, which can significantly reduce the total number of branches and running time. In this work we focus on branching on activation (ReLU) nodes. BaBSR (Bunel et al.) 2018) includes simple branching heuristic which assigns each ReLU node a score to estimate the improvement for tightening f by splitting it, and splits the node with the highest score.
Bounding with Linear Programming (LP) A typical bounding method used in BaB based veri- fication is the Linear Programming bounding procedure (sometimes simply referred to as "LP" or "LP verifier" in our paper). Specifically, we transform the original verification problem into linear programming problem by relaxing every activation unit as convex (linear) domain (Ehlers) 2017) and then get the lower bound Le, with linear solver given domain C. For instance, as shown in
Figure
1. 9 (1) = ReLUU())) (1) can be linearly relaxed with the following constraints: (1) (1),,) 2 n,";
( (h 1(")). Note that the lower bound 15/ and upper bound u (i) for
(2)g)
0: (3) 96
each activation node h are required in the LP construction given C, They are typically computed by the existing cheap bounding methods like LiRPA variants (Wong & Kolter, 2018) with low cost. The tighter the intermediate bounds (1))) uj (0) are, the tighter f approximated by LP is.
2.3 LINEAR RELAXATION BASED PERTURBATION ANALYSIS (LiRPA)
Bound propagation in LiRPA We used Linear Relaxation based Perturbation Analysis (LiRPA TT] as bound procedure in BaB get linear upper and lower bounds of NN output w.r.t input x E C:
Ax + b < f(x)= < Az + b, x C
We only use the backward mode LiRPA bounds (e.g., CROWN and DeepPoly) in this paper.
3

---

Published as a conference paper at ICLR 2021
101
10
9
gj
93
93
19
10
10
11
101
1
19
/
(b)
(c)
(d)
Figure I: Relaxations of ReLU: (a) "triangle" relaxation LP; (b)(c) No relaxation when uj S 0 (always
inactive) 1/5) 2 0 (always active): (d) linear relaxation in LiRPA when 1 <0, u
> 0 (unstable).
A lower bound can then be simply obtained by taking the lower bound of the linear equation Ar + b w.r.t input C, which can be obtained via Hölder's inequality when is a a norm ball.
To get the coefficients A, A, b, b, LiRPA propagates bounds of f(x) as a linear function to the output of each layer, in backward manner. At the output layer (x)) we simply have:
(x) & f(x) I (x), x ECC
(3)
Then, the next step is to backward propagate the identity linear relationship through a linear layer (x)) w()) (x) to get the linear bounds of f(x) w.r.t g(=tg((
w (11) (x))) S f(x) I w( (x),,, 2EC
(4)
To get the linear relationship of (L-1)) w.r.t f1)), need backward propagate through ReLU layer g (z) = ReLU(h (--10)((-1)()))) (x)). Since it is nonlinear, we perform linear relaxations. For illustration, considering the j-th ReLU neuron at i-th layer, 9j (x) (()
= ReLU (x)), we can
linearly upper and lower bound it by 2 (1)((())) (x) + 0 I 93 (x) s 1/ (x) by where
(4)
(i)
(0) ( are:
(
= 0,b/1 (6) 0
(always inactive for
(1] = 1,64 -b; =0
1 2 0 (always active for x C)
(5)
aj
p 1
0
= 0,5
100 0, u (unstable for E C)
Here 18 < 2h (z) u are intermediate pre-activation bounds for x E C, and oj is an arbitrary
value between O and 1. The pre-activation bounds 1(00 and (9) can be computed by treating h (x) as the output neuron with LiRPA. Figure [bc.d)) illustrate the relaxation for each state of ReLU
neuron. With these linear relaxations, we can get the linear equation of (I.-1) w.r.t output f(x):
W ( (2-1) (x) (b(4) < f(x) w(DD (1-1) ((--1) 1 Th)
JEC
(()) (.,
a
(
20 b bb T w( where (((4)
((4)
((()
2
(6)
w
<0'
(1)) <0
The diagonal matrices D(L-1),
D (1-1) and biases reflects the linear relaxations and also considers
the signs in (L) to maintain the lower and upper bounds. The definitions for j-th diagonal element ((())
Da.is)) and bias (T) are similar, with the conditions for checking the signs of w(( swapped. Importantly, (!.-1) has free variables a E [0, 1] which do not affect correctness of the bounds. We can continue backward propagating these bounds layer by layer (e.g., ((L-2)(z), h (z),, etc) until reaching (0) (I) x, getting the eventual linear equations of f(x) in terms of input æ: L(x, a)) & f(x) & U(2,
E where
L(x,a) D D. ( +b.. U(x, a) w(') D. w x (7)
Here a denotes o for all unstable ReLU neurons NN. The obtained bounds (L(x,, ar), U(x, ax)
of (xx are linear functions in terms of x. Beyond the simple feedforward NN presented here, LiRPA support more complicated NN architectures like DenseNet and Transformers by computing L and U automatically and efficiently on general computational graphs (Xu et al., (020).
Soundness of LiRPA The above backward bound propagation process guarantees that L(æ, a) and U(x, a) soundly bound fx) for all x E C. Detailed proofs can be found in (Zhang et al. 2018 Singh et al. 2019b) for feedforward NNs and eXu al. 2020) for general networks.
4

---

Published as a conference paper at ICLR 2021
Prove: /(x) 2 Vx
Unoortimized LaRPk: lower hound f -1994
Example: Optimized LIRPA for
ReLU
bound Optimaaod
Always Active: f
Ligher (20 and uq
make lighter melacation
Always Inactive: u
Optimined IRPA, lower bound f 0.83
Example: BaB to find tighter lower bound
0.17
Split a
Linear relacee Unstable nesuro:: f < 0,
Pick A
Pick AlD)
{
Split
0..5
f- 031
Figure 2: Illustration of our optimized LiRPA bounds and the BaB process. Given two-layer neural network, aim verify output f(x) 0. Optimized LiRPA chooses optimized slopes for ReLU lower bounds, allowing tightening the intermediate layer bounds 2/11 and (") and also the output layer lower bound f. BaB splits two unstable neurons 1.)") and ii to improve / and verify sub-domains (f 2 for cases).
PROPOSED ALGORITHM
Overview In this section, we will first introduce our proposed efficient optimization of LiRPA bounds on GPUs that can allow us achieve tight approximation on par with LP or even tighter for some cases but in much faster manner. In Fig. 2 we provide a two-layer NN example to illustrate how our optimized LiRPA can improve the performance of BaB verification. In Section 3.2 we then show that feasibility checking is important to guarantee the completeness of BaB, and BaB using LiRPA without feasibility checking will end up to be incomplete. To ensure completeness, design our algorithm with minimal usage of LP for checking feasibility of splits. Finally, propose a batch split design by solving a batch sub-domains in a massively parallel manner on GPUs to fully leverage the benefits of cheap and parallelizable LiRPA. We further improve BaBSR in parallel fashion for branching and we summarize the detailed proposed algorithm in Section 3.4
3.1
OPTIMIZED LiRPA FOR COMPLETE VERIFICATION
Concrete outer bounds with optimizable parameters We propose to use LiRPA as the bounding step in BaB. A pair of sound and concrete lower bound and upper bound (f.F) to f(x) can be obtained according to Eq. given fixed a an:
f(as) = min L(x, ac), J(am) = max U(x on) =ec
(8)
=Ec
Because L, U are linear functions w.r. when is fixed, it is casy to solve Eq. |using Hölder's inequality when C is a lp norm ball (Xu et al.) 2020). In incomplete verification settings, a can be set via certain heuristics (Zhang al. 2018). Salman al. (2019) showed that, the variable is equivalent to dual variables the LP relaxed verification problem [Wong & 20188. Thus, an
optimal selection of a given the same pre-activation bounds 1.)) and u,
(c) can in fact, lead to the the
same optimal solution for if and f as in LP.
Previous complete verifiers typically use LiRPA variants obtain intermediate layer bounds to construct an LP problem (Bunel et al. (018); Lu & Kumar (2020)) and solve the LP to obtain bounds at output layer. The main reason for using LP is that it typically produces much tighter bounds than LiRPA when a is not optimized. We use optimized LiRPA, which is fast, accelerator- friendly, and can produce tighter bounds, well outperforming LP for complete verification:
f= 1=min
min min L(x, a)), f max max U(x, ai), aj E 1] sEC
(9)
zEC
The inner minimization or maximization has closed form solutions Xu et al. 2020 based on aU
Hölder's inequality, so we only need to optimize on a. Since we use a differentiable framework (Xu et al., 2020 to compute the LiRPA bound functions L and U, the gradients da and de: can be obtaned easily. Optimization over a can be done via projected gradient descent (cach coordinate of is constrained in [0, 1)). Since the gradient computation and optimization are done GPUs, the bounding process is still very fast and can be one or two magnitudes faster than solving an LP.
aL
Optimized LiRPA bounds
be tighter than LP Solving Eq. Jusing gradient descent cannot guarantee to converge to the global optima, so it seems the bounds must be looser than LP. Counter- intuitively, by optimizing a, can potentially obtain lighter bounds than I.P. When "triangle"
5

---

Published as a conference paper at ICLR 2021
relaxation is constructed for LP, intermediate pre-activation bounds 1691 ( must be fixed for the 3 j-th ReLU in layer i. During the LP optimization process, only the outpui bounds are optimized; intermediate bounds stay unchanged. However, in the LiRPA formulation, L(x, a) and U(r, a)) are complex functions of o:: since intermediate bounds are also computed by LiRPA, they depend on all oy
(t') (0 < i) in previous layers. Thus, the gradients @L and @U 8cx 80 can tighten output layer bounds and / indirectly by tightening intermediate layer bounds, forming a tighter convex relaxation for the next iteration. An LP solver cannot achieve this because adding 154) and u as optimization variables makes the problem non-linear. This the key to our success of applying LiRPA based bounds for the complete verification setting, where tighter bounds are essential.
In Figure 3 we illustrate our optimized LiRPA bounds and the LP solution. Initially, we use LiRPA with a set via a fast heuristic to compute intermediate layer bounds 16) and !")
lower bound
and then use them to build relaxed LP problem. The solution to this initial IP problem (red line) is much tighter than the LiRPA solution with the heuristically set a (the left-most point of the blue line). Then, we optimize a with gradient decent, and LiRPA quickly outperforms this initial LP solution due to optimized tighter intermediate layer bounds. We can create a new LP with optimized intermediate bounds (light blue line), producing a slightly tighter bound than LiRPA with optimized a. The LP bounds in most existing complete verifiers all use intermediate layer bounds obtained from unoptimized LiRPA bounds or even weaker methods like interval arithmetic, ending up to the solution close to lower than the red line in Figure 3 In- stead, our optimized LiRPA bounds can produce tight bounds, and also exploit parallel acceleration from machine learning accelerators, leading to huge improvements verification time compared to existing baselines.
-10
LP inttaal bound optimized LiRPA bound
optimized bound
50
100
150
200
iteration
Figure 3: Optimized LiRPA bound (0 to 200 iterations) vs LP bounds.
ReLU Split Constraints In the BaB process, when ReLU h1g)) is split into two sub-domains (h > and ((()) < 0), we simply set (() 2 and ( < in bounding step. It tighten the LiRPA bounds by forcing the split ReLU linear, reducing relaxation errors. However, when splits
added, LiRPA and I.P not equivalent even under fixed 166) u and optimal After splits, LiRPA cannot check certain constraints where LP is capable to, as we will discuss in the next section.
3.2 COMPLETENESS WITH MINIMAL USAGE OF LP BOUNDING PROCEDURE
Even though our optimized LiRPA can bring us huge speed improvement over LP for BaB based verification, we observe that it may end up to be incomplete due to the lack of feasibility checking: cannot detect some conflicting settings of ReLU splits. We state such observation in Theorem 3.1
Theorem 3.1 (Incompleteness without feasibility checking) When using LiRPA variants de- scribed in Section 2.3 as the bounding procedure, BaB based verification is incomplete.
We prove the theorem by giving a counter example in Appendix A.I where all ReLU neurons are split and thus LiRPA runs linear network for each sub-domain. As result, LiRPA can still be indecisive for the verification problem. The main reason is that LiRPA variants will lose the feasibility information encoded by the sub-domain constraints. For illustration, consider sub- (61) 2 0), LiRPA will force 9j, (x) (inactive ReLU, a zero function) and 9/z (x) = 5 (6x) (z) (active ReLU, an identity function) respectively and propagate these bounds to get the approximated lower bound f.. However, the split feasibility constraint (12) (h (i)) 0) n (h ja
domain C, = Cn (h (b)) < 0) n (h ja
(f2)
(82)
2 0) is ignored, so two conflict splits may be conducted (e.g., when h( < O,
(22) cannot be 2 0). On the contrary. LP can fully preserve such feasibility information due to the linear solver involved and detect the infeasible sub-domains. Then, in Theorem 3.2 we show that the minimal usage of feasibility checking with IPP can guarantee the completeness of BaB with LiRPA.

---

Published as a conference paper at ICLR 2021
Algorithm Parallel BaB with optimized LiRPA bounding (we highlight the differences between our algorithm and regular BaB (Bunel et al.) 2018) in blue. Comments are in brown.)
1: Inputs: f.C. (batch size), o (threshold to switch to LP)
2: (f.)) <- www.piiiiee.LiPAA(.....
3: IP - [[]J[c)]
P IP is the set of all unverified sub-domains
4: while f < 0 and 2 do
5:
Pick sub-domains to split and removed them from 6: CI, CD batch split(C1,...... C.) Each C, splits into two sub-domains C2 and CT
(CI....,Cn) +- batchh.pcc..out
7:
Jep Jct -
< optimized
[c], CC..c......C C,,Ch) cx)) D
Compute lower and upper bounds using LiRPA for each sub nomado on GPUs in batch
8:
F P-PUP LDDamiiamnnniii Filter (LEop. Fct C11, Jcy, Cf)...., Lee Jet C, [fe Leggg
Jeg Cil)
Filter out verified sub-domains, insert the left domains back to P
9:
f +- min(fe, c, (Fa, (5,,CC) C.) E P) i
.. n I + min (T., C.) EP. I....,
D To ease notation, C, here indicates both CJ and C
10:
11:
if lengthh(P) > then
Fall back to LP for completeness Lej Jeq. Jep Jeq Ler Jeh, Jep + compute. [C|, CF .f............. cH))
12:
13:
P+ P-
Jct Cil. Jep, ..cglb.....Ly...... Jeg C.l, Ley Jey cx)
14:
Outputs:
/.J
Theorem 3.2 (Minimal feasibility checking for completenes)) When using LiRPA variants de- scribed in Section a.3 the bounding procedure, BaB based verification is complete all infeasible leaf sub-domains (i.e., sub-domains cannot be further split) are detected by linear programming.
We prove the theorem in Appendix A.2 where we show that by checking the feasibility of splits with LP, we can eliminate the cases where incompatible splits are chosen in the LiRPA BaB process. Since LP is slow while LiRPA is highly efficient, we propose to only use IPP when the LiRPA based bounding process is stuck, either (1) when partitioning and bounding new sub-domains with LiRPA cannot further improve the bounds, or (2) when all unstable neurons have been split. In this way, the infeasible sub-domains can be eventually detected by occasional usage of LP while the ad advantage of massive parallel LiRPA on GPUs is fully enjoyed. We will describe our full algorithm in Sec. 3.4
3.3 BATCH SPLITS
SOTA BaB methods (Bunel al. 2020b & Kumar 2020) only split one sub-domain during each branching step. Since we use cheap and GPU-friendly LiRPA bounds, we can select batch of sub-domains to split and propagate their LiRPA bounds in a batch. Such a batch splitting design can greatly improve hardware efficiency on GPUs. Given batch size n that allows us to fully use the GPU memory available, we can obtain n bounds simultaneously. It grows the search tree on single leaf by a depth of loga n,, or split n1/2 leaf nodes at the same time, accelerating by up to times.
3.4 OUR COMPLETE VERIFICATION FRAMEWORK
Our LiRPA based complete verification framework is presented in Alg. T The algorithm takes a target NN function and domain C as inputs. We run optimized LiRPA to get initial bounds (f for E C (Line 2). Then we utilize the power of GPUs to split in parallel and maintain a global set IP storing all the sub-domains which cannot be verified with optimized LiRPA (Line 5-10). Specifically, batch wwc.ppickk.oo pick_out improves BaBSR (Bunel et al. 2018) in parallel manner to select n sub-domains in P and determine the corresponding ReLU neuron to split for each of them. If the length of P is less than n, then we reduce C, to two sub-domains C/ and CH by forcing the selected unstable ReLU neuron to be positive and negative, respectively. optimize LiRPA runs optimized LiRPA in parallel as a batch and returns the lower and upper bounds for selected sub-domains simultancously. Domain Filter filters out verified sub-domains (proved with fe, 2 0) and we insert the remaining ones to P.. The loop breaks
the length of PP. batch split splits each selected
if the property is proved (f 2 0) or a counter-example is found in any sub-domain (f 0).
To avoid excessive splits, we set the maximum length of the sub-domains to v (Line 12). Once the canpute-bounde LP will be called. solves these 7 sub-domains
length of reaches this threshold, by LP (one by one in a loop, or in parallel if using multiple CPUs is allowed) with optimized LiRPA
7

---

Published as a conference paper at ICLR 2021
computed intermediate layer bounds. If sub-domain C, E P (which previously cannot be verified by LiRPA) is proved or detected to be infeasible by LP, as an effective heuristic, we will backtrack and prioritize to check its parent node with LP. If the parent sub-domain is also proved or infeasible, we can prune all its child nodes to greatly reduce the size of the search tree.
Completeness of our framework Our algorithm is complete, because follow Theorem 3.2 and check feasibility of all split sub-domains that have deep BaB search tree depth (length of P reaches threshold m) forming superset of the worst case where all ReLU neurons are split.
4 EXPERIMENTS
In this section, we compare our verifier against the state-of-the-an ones to illustrate the effectiveness of our proposed framework. Overall, our verifier is about 10X, 4X and 20X faster than the best LP-based verifier (Lu & Kumar (220) on the Base, Wide and Deep models, respectively.
Setup We follow the most challenging experimental setup used in the state-of-the-arr verifiers GNN-ONLINE (Lu & Kumar 2020) and BABSR (Bunel et al. 2020b). Specifically, we evalu- ate on CIFARIÓ dataset on three NNs: Base, Wide and Deep. The dataset is categorized into three difficulty levels: Easy, Medium, and Hard, which is generated according to the performance of BaBSR. The verification task is defined as given a Lo norm perturbation less than e, the clas- sifier will not predict specific (predefined) wrong label for each image (see Appendix [ We set batch size n = 400, 200, 200 for Base, Wide and Deep model respectively and threshold 7 12000. More details experimental setup provided in Appendix B Our code is available at httpp::/g tuub. com ka di xu / Sttp/LRPPAAVViiiS
Comparisons against state-of-the-at verifiers We include five different methods for comparison:
(1) BABSR (Bunel et al. 2020b). a BaB and I.P based verifier using simple ReLU split heuristic;
(2) MIPPLANET (Ehlers 2017), customized MIP solver for NN verification where unstable ReLU
neurons are randomly selected for split; (3) GNN (Lu & Kumar 2020) and (4) GNN-ONLINE (Lu
Kummar 2020) are BaB and LP based verifiers using learned graph neural network (GNN) to
guide the ReLU split. (5) PROXIMAL BABSR (Bunel et al. 2020a is very recently proposed verification framework based on Lagrangian decomposition which also supports GPU acceleration without solving LPs. All methods use 1 CPU with GPU. The timeout threshold is 3,600 seconds.
For the Base model different difficulty levels, Easy, Medium and Hard, Table T shows that we are around 5 ~ 40X faster than baseline BaBSR and around 2 ~ 20X faster than GNN split baselines. The accumulative solved properties with increasing runtime are shown in Figure 4 In all our exper- iments, use the basic heuristic in BaBSR for branching and do not GNNs, so speedup comes purely from the faster LiRPA based bounding procedure. We are also competitive against Lagrangian decomposition
GPUs.
Table 1: Performance of various methods on different models. We compare each method's 'ss avg. solving time, the avg. number of branches required, and the percentage of timed out (TO) properties.
Busc Easy
Bisc Modium
Rac- Had
Wide
Methed
cmecs)
branches
%30
brunches
%TT
branches
%6TO
cine6))
brunches
%TTO
branches
%30
BABSR
522.45
585
15
35.2
3325.65
455
50.3
2555. 19
365
54.0
1462.24
1912.25
2172.23
3068.40
2842.54
GNN
312.93
301
624.12
635
1465.75
15.6
1791.52
375
1870.63
GNN-ONLINE
45855
OURS
13,0
375.23
53481
Figure 4: Cactus plots for method and other baselines in Base (Easy, Medium and Hard ). Wide and Deep models, We plot the percentage of solved properties with growing running time.
Badgi
KiPsianet
CVN
Prox. Sussi
Ours
of
OF (c) Base-Hard
(a) Base-Easy
(b) Meddium
(d) Wide
(e) Deep
Performance Larger Models In Table I show that our verifier is more scalable larger
(wider or deeper) NNs compared to other state-of-the-an verifiers. Our method enjoys efficient GPU acceleration particularly Deep model and can achieve 30X speedup compared to BABSR,
8

---

Published as a conference paper at ICLR 2021
and we are also significantly faster than Lagrangian decomposition based GPU verifier (PROXIMAL BABSR). When compared to the state-of-the-are LP based BaB, GNN-ONLINE. our method can save 20X running time on Deep model. In Appendix C we analyze the effectiveness of optimized LiRPA and batch splits separately, and find that optimized LiRPA is crucial for NN verification. Performance comparisons of our proposed framework CPU cores without GPU acceleration included in Appendix D
5 RELATED WORK
Complete verifiers Early complete verifiers rely on satisfiability modulo theory (SMT) (Katz al.
2017 Huang et al. 2017 Ehlers 2017) and mixed integer linear programming (MILP) [Tjeng et al. 2019a Dutta et al. 2018), and they typically do not scale well. Higher order logic provers such as proof assistant (Bentkamp et al., 2018) can also be potentially used for NN verification, but their scalability to the NN setting has not been demonstrated. Recently, [Bunel et al. (2018) unified many approaches used in various complete verifiers into BaB framework. An I.P based bounding procedure is used in most of the existing BaB framework (Bunel et al., 2018 Wang et al., 2018c]
Royo et al. 2019 Lu & Kumar 2020). For branching. two categories of branching strategies were
proposed: (1) input node branching (Wang et al., 2018c| Bunel et al. 2020b Royo et al., 2019]
Anderson et al. 2019) where input features
divided into sub-domains, and (2) activation node
(especially, ReLU) branching (Katz et al. 2017 Bunel et al. 2018 Wang et al. 20188) Ehlers 2017
Lu & Kumar 2020 where hidden layer activations are split into sub-domains, Bunel al. (2018)
found that imput node branching cost is exponential to input dimension. Thus, many state-of-the-ee
verifiers use activation node branching instead, focusing on heuristics select good nodes to split. BaBSR (Bunel et al. 2018) prioritizes ReLUs for splitting based on their pre-activation bounds: Lu & Kumar (2020) used a graph neural network (GNN) to learn good splitting heuristics. Our work focuses on improving bounding and can use better branching heuristics to achieve further speedup.
Two mostly relevant concurrent works using GPUs for accelerating NN verification are: (1) GPUPoly (Müller et al. (020), an extension of DeepPoly on CUDA, is still an incomplete verifier. Also, it is implemented in CUDA C++, requiring manual effort for customization and gradient com- putation, so it is not easy to get the gradients for optimizing bounds
have done in Section 3.1 (2) Lagrangian Decomposition (Bunel et al. 2020a) is a -PU-acceleraeed BaB based complete ver- ifier that iteratively tightens the bounds based on Lagrangian decomposition optimization formu- lation and does not reply on LP. However, it solves a much more complicated optimization problem than LiRPA, and typically requires hundreds of iterations to converge for single sub-domain.
Many incomplete verification methods rely on convex relaxations of NN, replacing nonlinear activations like ReLUs with linear constraints (Wong & Kolter 2018: Wang et al. 20188] Zhang et al. 2018:; Weng et al.] 2018 Gehr et al. 20188] [Singh et al. |01 Sa bj 2019bb9 a) or semidefinite constraints (Raghunathan et al. 20118 Dvijoothm et al. (athattat Dathathri et al. 2020).
Incomplete verifiers
Tightening the relaxation for incomplete verification was discussed in (Dvijotham et al. [018 Singh jtt al., 2019a| Lyu et al., 2019; [jandraatmadja et al.] 2020). Typically, tight relaxations require more computation and memory in general. We refer the readers to (Salman et al., (0199) for a comprehensive survey. Recently, Xu et al. (2020) categorized the family of linear relaxation based incomplete verifiers into LiRPA framework. allowing efficient implementation on machine learning accelerators. Our work uses LiRPA as the bounding procedure for complete verification and exploits its computational efficiency to accelerate, and main contribution is to show that but weak incomplete verifiers as the main driver for complete verification when strategically applied.
use fast
CONCLUSION
We use LiRPA based incomplete NN verifier to accelerate the bounding procedure in branch and bound (BaB) for complete NN verification on massively parallel accelerators. We use a fast gradient based procedure to tighten LiRPA bounds. We study the completeness of BaB with LiRPA, and show up to 5X speedup compared to state-of-the-art verifiers across multiple models and properties.
ACKNOWLEDGMENTS
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. Mor-

---

Published as a conference paper at ICLR 2021
gan Faculty Award: Air Force Research Laboratory under FA8750-18-2-000 NSF IIS- and NSF IIS-2008173.
REFERENCES
Greg Anderson, Shankara Pailoor, Isil Dillig, and Swarat Chaudhuri. Optimization and abstraction: A synergistic approach for analyzing neural network robustness. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 731-
744, 2019.
Alexander Bentkamp, Jasmin Christian Blanchette, Simon Cruanes, and Uwe Waldmann. Super- position for lambda-free higher-order logic. International Joint Conference on Automated Reasoning, pp. 28-46 Springer, 2018.
Rudy Bunel, Alessandro De Palma, Alban Desmaison, Krishnamurthy Dvijotham, Pushmeet Kohli, Philip H. S. Torr, and M. Pawan Kumar. Lagrangian decomposition for neural network verifica- tion. Conference on Uncertainty in Artificial Intelligence (UAI) 2020, 2020a.
Rudy Bunel, Jingyue Lu, lIker Turkaslan, Kohli, P Torr, and P Mudigonda. Branch and bound for piecewise linear neural network verification. Journal of Machine Learning Research, 220200, 2020b.
Rudy R Bunel, Ilker Turkaslan, Philip Torr, Pushmeet Kohli, and Pawan K Mudigonda. A unified view of piecewise linear neural network verification. In Advances Neural Information Process- ing Systems, pp. 4790-4799, 2018.
Sumanth Dathathri, Krishnamurthy Dvijotham, Alexey Kurakin, Aditi Raghunathan, Jonathan Ue- sato, Rudy R Bunel, Shreya Shankar, Jacob Steinhardt, Ian Goodfellow, Percy S Liang, et al. Enabling certification of verification-agnosiie networks via memory-efficient semidefinite pro- gramming. Advances in Neural Information Processing Systems, 33, 2020.
Souradeep Dutta, Susmit Jha, Sriram Sankaranarayanan, and Ashish Tiwari. Output range analy- sis for deep feedforward neural networks. In NASA Formal Methods Symposium, pp. 121-138. Springer, 2018
Krishnamurthy
Dvijotham, Sven Gowal, Robert Stanforth, Relja Arandjelovic, Brendan O'Donoghue, Jonathan Uesato, and Pushmeet Kohli. Training verified learners with learned ver- ifiers. arXiv preprint arXiv:/805.1022 2018.
Krishnamurthy Dj Dvijotham, Robert Stanforth, Sven Gowal, Chongli Qin, Soham De, and Push- meet Kohli. Efficient neural network verification with exactness characterization. In Uncertainty in Artificial Intelligence, pp. 407-507. PMLR. 2020.
Ruediger Ehlers. Formal verification of piece-wise linear feed-forward neural networks. In Interna- tional Symposium on Automated Technology for Verification and Analysis, pp. 269-286. Springer, 2017.
Timon Gehr, Matthew Mirman, Dana Drachsler-Cohen, Petar Tsankov, Swarat Chaudhuri, and Mar- tin Vechev. Ai2: Safety and robustness certification of neural networks with abstract interpreta- tion. In 2018 IEEE Symposium on Security and Privacy (SP), pp. 3-18. IEEE, 2018.
Xiaowei Huang, Marta Kwiatkowska, Sen Wang, and Min Wu. Safety verification of deep neural networks. In International Conference on Computer Aided Verification, pp. 3-29. Springer, 2017.
Guy Katz, Clark Barrett, David I. Dill, Kyle Julian, and Mykel Kochenderfer. Reluplex: An efficient smt solver for verifying deep neural networks. In International Conference on Computer Aided Verification, pp. 97-117. Springer, 2017.
Jingyue Lu and M Pawan Kumar. Neural network branching for neural network verification. Inter- national Conference on Learning Representation (ICLR), 2020.
Zhaoyang Lyu, Ching Yun Ko, Zhifeng Kong, Ngai Wong, Dabua Lin, and Luca Daniel. Fastened crown: Tightened neural network robustness certificates. arXiv preprint arXiv:1912.0000 19/2000744 2019.
10

---

Published as a conference paper at ICLR 2021
Matthew Mirman, Timon Gehr, and Martin Vechev. Differentiable abstract interpretation for prov- ably robust neural networks. In International Conference on Machine Learning, pp. 3575-3583, 2018.
Christoph Mülllr, Gagandeep Singh, Markus Püschel, and Martin Vechev. Neural network robust- verification on gpus. arXiv preprint 17Xiv:2007.10866 2020.
Aditi Raghunathan, Jacob Steinhardt, and Percy S Liang. Semidefinite relaxations for certifying robustness adversarial examples. In Advances in Neural Information Processing Systems, pp- 10877-10887, 2018
Vicenc Rubies Royo, Roberto Calandra, Dusan M Stipanovic, and Claire Tomlin. Fast neural net- work verification via shadow prices. arXiv preprint arXiv: 190.007777 2019.
Hadi Salman, Greg Yang, Huan Zhang, Cho-Jui Hsieh, and Pengehuan Zhang. A convex relaxation barrier to tight robustness verification of neural networks. Advances in Neural Information Processing Systems 32, pp. 9832-9842, 2019.
Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin Vechev. Fast and effective robustness certification. Advances in Neural Information Processing Systems, pp. 10825-10836, 2018a.
Gagandeep Singh, Timon Gchr, Markus Püschel, and Martin Vechev. Boosting robustness certifica- tion of neural networks. In International Conference on Learning Representations, 2018b.
Gagandeep Singh, Rupanshu Ganvir, Markus Püschel, and Martin Vechev. Beyond the single neuron convex barrier for neural network certification. In Advances in Neural Information Processing Systems, pp. 15072-15083, 2019a.
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. An abstract domain for cer- tifying neural networks. Proceedings of the ACM on Programming Languages, 3(POPL):41, 2019b.
Christian Szegedy, Wojciech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian Goodfellow, and Rob Fergus. Intriguing properties of neural networks. In ICLR, 2013.
Christian Tjandraatmadja, Ross Anderson, Joey Huchette, Will Ma, Krunal Patel, and Juan Pablo Vielma. The convex relaxation barrier, revisited: Tightened single-neuron relaxations for neural network verification. arXiv preprint arXiv:2006. /4076, 2020.
Vincent Tjeng, Kai Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming. ICLR, 2019a.
Vincent Tjeng, Kai Y. Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net, 2019b. URL https:
//openreview. www/fforiii weeee/ooommid--yyyyooooe HyIddddddddyyyyyyyaddad
Shiqi Wang. Yizheng Chen, Ahmed Abdou, and Suman Jana. Mixtrain: Scalable training of formally robust neural networks. arXiv preprint arXiv: 1et.111166660 1.02225, 2018a
Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. Efficient formal safety analysis of neural networks. In Advances in Neural Information Processing Systems, pp. 6367- 6377, 2018b.
Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. Formal security analysis of neural networks using symbolic intervals. In 27th {USENIX) Security Symposium (UUSENIX) Security 18), pp. 1599-1614, 2018c.
Tsui-Wer Wei Weng, Huan Zhang, Hongge Chen, Zhao Song, Cho-Jui Hsieh, Luea Daniel, Duane Bon- ing, and Inderjit Dhillon. Towards fast computation of certified robustness for relu networks. In International Conference Machine Learning, pp. 5273-5282, 2018.

---

Published as a conference paper at ICLR 2021
Eric Wong and Zico Kolter. Provable defenses against adversarial examples via the convex outer adversarial polytope. In International Conference on Machine Learning, pp. 2283-5292, 2018.
Eric Wong, Frank Schmidt, Jan Hendrik Metzen, and J Zico Kolter. Scaling provable adversarial defenses. In NIPS, 2018.
Kaidi Xu, Zhouxing Shi, Huan Zhang, Yihan Wang, Kai-Wei Chang, Minlie Huang. Bhavya Kailkhura, Xue Lin, and Cho-Jui Hsieh. Automatic perturbation analysis for scalable certified robustness and beyond. Advances Neural Information Processing Systems, 33, 2020.
Huan Zhang, Tsui-War Weng, Pin- Yu Chen, Cho-Jui Hsich, and Luca Daniel. Efficient neural net-
work robustness certification with general activation functions. In Advances in neural information processing systems, pp. 4939-4948, 2018.
Huan Zhang, Hongge Chen, Chaowei Xiao, Bo Li, Duane Boning, and Cho-Jui Hsich. Towards stable and efficient training of verifiably robust neural networks. International Conference on Learning Representations, 2020.
12

---

Published as a conference paper at ICLR 2021
A PROOFS
A.1 PROOF OF THEOREM 3.1
We prove Theorem 3.1 by providing a simple counterexample, and we illustrate the necessity of feasibility checking for the completeness of BaB based verification. Consider an NN with only two ReLU units 91
(2) ReLU(h))) and (2) ReLU(h?) ( where they share the same one dimension The final output function of NN is defined as f of²) - As verification problem, we want to verify the property 2 0 where x = 1.. Since hidden nodes hn and hy are exactly the same, the ground-truth output range ['(x) E [0, 0). complete BaB based verifier is expected to obtain that optimal bound and prove the property after splitting h and he together while BaB with only LiPRA cannot guarantee that completeness. Specifically, BaB with only LiRPA will split the original domain E [-1, 1] into four sub-domains and approximate the bound with LiRPA respectively:
input ( 2
(1) (feasible) sub-domain x E h- (2) 2 0,
(2) 2 0 with output f [ar, a] [xr a] E [0,0] (2) (feasible) sub-domain x E {1-1,1], < <0,hg (2)
< 0 with output f [0, 0] - [0, 0] [0,0) 0]
(3) (infcasible) sub-domain I E [-,, //
< 0, 2
2 with output = [0, - [x, x] e [-1,1]]
(4) (infcasible) sub-domain x E 11,, k(
2 0, 0, with output f [z, x] 00 1-1.1]
Only the first two split sub-domains are feasible and therefore the ground- truth lower bound 0 can be obtained by taking the minimum of the estimated bounds from sub-domains (1) and (2). However, pure LiRPA is not able to tell the infeasibility of sub-domains (3) and (4) and thus BaB with pure LiRPA will report the minimum -1 got from all these four sub-domains as the global lower bound for the original input domain, ending up not being able to verify the property, i.e., incomplete.
A.2 PROOF OF THEOREM 3.2
We prove Theorem 3.2 by considering the worst case where all unstable ReL.U neurons split.
Given a neural network function f with input domain C, assume there are N unstable ReLU neurons {g. (h)li = 1, .N] .N} in total. In the worst case, have 2 leaf sub-domains S = [C = 1, 2º }. where each C; corresponds to one assignment of unstable ReLU neuron splits. For example, we can have
C1 = C n (h1 2 0) (h, 2 0) ... (hx 2 0)
C2 C (hı < 0) (he 2 0) 0.... (hN 2 0)
C3 = Cn (h, 2 n < 0) n.... (hN 2 0)
C4 = Cn (h 0) (h2 < 0) 0) n...n (hN (2220)
Note that by definition the original input domain C = UcresC"; in other words, all the 2 split sub-domains combined will be the same as the original input domain.
Not all of the sub-domains are actually feasible, due to the consistency requirements between neu- rons. For example, in our proof in Section A.1 (i(2) and h.(²) cannot be both 2 or both < 0. We can divide the sub-domains S into two mutually exclusive sub-sets, Sfeas for all the feasible sub-domains, and ginfeas for all the infeasible sub-domains. We have C = U since these infeasible sub-domains are empty sets.
We first show that linear programming (LP) can be used to effectively detect these infeasible sub- domains. For some C¹ ginfeas because all the ReLU neurons are fixed to be positive negative, no relaxation is needed and the network is essentially linear; thus, the input value of every hidden neuron h; can be written as a linear equation w.r.t. input x. We add all the Boolean predicates on h; to LP problem as linear constraints w.r.t x. If this LP is feasible, then we can find some input zo that assigns compatible values all h;; otherwise, the LP is infeasible.
Due to the lack of feasibility checking in LiRPA, the computed global lower (or upper) bounds from LiRPA is LLRAA = minc'ss te = min (mingresto for min Lc. With feasibility
13

---

Published as a conference paper at ICLR 2021
checking from LP, remove all infeasible sub-domains from this min such that they do not contribute to the global lower bound: f min fe
To prove the whole BaB verification is complete, it is sufficient to prove this lower bound f is the exact minimum of f bounded in C. Since any sub-domain C² E S is leaf sub-domain with no unstable ReLU neurons, the neural network bounded within C' a linear function. LiRPA can give an exact minimum of f within sub-domain C' Since C = UerestonC" (in other words, Steas covers all the feasible sub-domains within C), the minimal value for all of them f = mingre Le forms the exact minimum of f within the input domain C. Thus, BaB with LiRPA based bounding procedure is complete when feasibility checking is applied.
B EXPERIMENTAL SETUP
We use the same set of models and benchmark examples used in the state-of-the-art verifiers GNN- ONLINE (Lu & Kumar 2020) and BABSR (Bunel et al., (020b)) Specifically, we evaluate the most challenging CIFAR-10 10 dataset with the same standard robustly trained convolutional neural networks: Base, Wide, and Deep. These model structures are also used in (Lu & Kumar 2020 Bunel et al. 2020a). The Base model contains 2 convolution layers with 8 and 16 filters as well as two linear layers with 100 and 10 hidden units, respectively. In total, the Base model has 3,172 ReLU activation units. The Wide model contains 2 convolution layers with 16 and 32 filters and two linear layers with 100 and 10 hidden units, respectively, which contains 6,244 ReLU activation units in total. The Deep model contains 4 convolution layers and all of them have 8 filters and two linear layers with 100 and 10 hidden units, respectively, with 3,756 ReLU activation units in total. The source code of BABSR, MIPPLAANET, GNN and GNN- INLINE are available at afsttps: //githab. www.//owoll.oooooooooooooooowo.. http://oowao0rrp/////////aa wwwpwhhiaaaanannnnaaaaaa The source code of PROXIMAI. BABSR available at inttps://giitii wtw.:tttwb.ccom/eeettttaaaaaeeae //nn- by replacing the dataset to the same one we used here.
Given correctly classified image x with label you and another wrong label we + Me (pre-defined in this benchmark) and e, the verifier needs to prove:
(el=) - e (<') ((" f(x') > 0 V. ||0- =0'1=>>00 Se
(10)
where f(-) is the logit-layer output of a multi-class classifier, elr) and e(d)) are one-hot hot encoding vectors for labels Ye and ye' We want verify that for a given e, the trained classifier will not predict wrong label ye for image æ. All properties including 6, and c' are provided by (Lu & Kumar 2020). Specifically, they categorize verification properties solved by BABSR within 800s as easy, between 800s and 2400s as medium and more than 2400s as hard.
Our experiments are conducted on one Intel 17-7700K CPU and one Nvidia GTX 1080 Ti GPU. The parallel batch size is set to 400, 200 and 200 for base, wide and deep model respectively and the 7 is set to 12,000 due to GPU memory constraint. To make a fair comparison, we use one CPU core for all methods. Also, we one GPU for GNN, GNN-ONLINE, PROXIMAL-BABA method. When optimizing the LiRPA bounds, we apply 100 steps gradient decent for obtaining the initial f (Line 2 in Algorithm T.. After that, 10 steps gradient decent (Line 7) and early stop once >> 0 or of has no improvement.
and our
C ABLATION STUDY
Our efficient framework leverages two powerful components: (1) optimized LiRPA bounds and (2) batch splits on GPUs In this section, we conduct breakdown experiments to show how each individual technique can help with complete verification. As we can see in Table 2 using batched split with unoptimized LiRPA is not very successful and cannot beat BABSR. We observe that, without optimized LiRPA, the bounds are very loose and cannot quickly improve the global lower bound. In contrast, using optimized LiRPA bounds without batch splits (splitting single node at a time and running batch size of on GPU) can still significantly speed up complete verification, around 2 ~ 10X compared to BABSR. Finally, combining batch splits and optimized LiRPA allows us to gain up to 44X speedup compared to BABSR
14

---

Published as a conference paper at ICLR 2021
Table 2:
Ablation study for different components of our algorithm. The speedup rate is computed based on running time of BABSR baseline: speedup = Time of BaBSR/ Time of our method.
Easy
Medium
Hard
Wide
Deep
Method
time(s)
speedup
time(s)
speeclup
time(s)
speeduup
time(s)
speedup
time(s)
speedup
BABSR baseline
522.48
1335,40
2875.16
3325.65 65
2855.19
Batch Splits (unoptimized LiRPA)
587.
0.89
1470.02
0.91
3013.57
0.95
3457.30
0.96
2998.50
0.95
Optimized LiRPA batch splits)
5.58
361.53
3.70
1384.22
2.07
736.56
4.51
287.33
Optimized LiRPA & Batch Splits
11.86
44.05
42.04
31.80
633.85
4,53
375.23
8.86
81.55
35.01
D COMPLETE VERIFICATION WITH LiRPA ON CPU VS GPU
For a fair comparison, we only use one CPU core and one GPU (the same as GNN and GNN- ONLINE) in our experimental results in Section 4 In this section, we investigate the performance of our algorithm for the cases where one or multiple CPU cores are available without GPU accelera- tion. Note that existing baselines such as BABSR and MIPPLANET can only effectively utilize one CPU core subject to the Gurobi solver. GNN and GNN-ONLING can utilize one GPU to run the GNN during branching while the rest of the verification processes all perform one CPU core. In contrast, our method is much more flcxible, and we are not limited by the number of CPU cores or GPUs When running multi-core CPUs, LiRPA be automatically accelerated by the underly- ing linear algebra library (e.g., Intel MKL or OpenBLAS) since the main computation of LiRPA is just matrix multiplications.
In Figure 5. we show the performance of our algorithm on a single CPU core and multiple CPU cores (in blue), and compare it to our main results with one CPU core plus one GPU (in red). As we can see, the running time decreases when the number of CPU cores increases, but the speedup not linear due to the limitation of the underlying linear algebra library and hardware. There is a big gap between the running time on 8 CPU cores and the time on one CPU core + one GPU, and the performance gap more obvious on Wide and Deep models. Thus, the speedup of LiRPA computation on GPUs is significant. However, surprisingly, even when using only one CPU core, we are still significantly faster than baseline BABSR and also get very competitive performance when compared to GNN-ONLINE which needs one GPU additionally. This shows the efficiency of LiRPA based verification algorithms.
200
1600
1750
175
1400
corels)
1500
conels)
150
One CPU core one GPU
One care one
timels)
.GN Online
time(s)
1250
--.
GNN Online
1000
75-
n CPU coneist
800
50
GVN Online
Drw EPU curw one CPU
600
500
25
400
2
1
2
2
number of CPU core
number of CPU core
number of CPU core Deep Model (BABSR: 2855.19s)
Base Model (easy instances) (BABSR: 522.48s)
Wide Model (BABSR: 3325.65s)
Figure 5: Running time of our method on the Base, Wide, and Deep networks when using 1, 2, and 8 CPU cores without GPU (blue), and our method using 1 CPU core + GPU (red) and strong baseline method, GNN-ONLING (green). We report the baseline BABSR verification time in captions because they are out of range on the figures.
15


Reviews:
[{"review_id": "qIhmAxlCcGc", "reviewer": "AnonReviewer4", "summary": "", "questions": "", "limitations": "", "rating": 5, "confidence": 1, "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": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "### Summary\nThis paper describes a branch-and-bound (BaB) process for neural network verification that uses linear relaxation based perturbation analysis (LiRPA). It gives a way to tighten the bounds obtained via LiRPA. Overall, this results is a complete verification procedure, which is an order of magnitude faster than existing linear programming (LP) procedures.\n\n### Strengths\nThe biggest strength of the paper is the impressive experimental results in section 5: the method described in the paper is several times faster than previous methods.  \n\n### Concerns \nMy main concern is that the paper is very difficult to understand. It seems to require a lot of background knowledge about the problem and the related literature, which is not clearly provided in the paper. I had trouble understanding the problem, the setup, and the proposed algorithm. \n\nAnother concern is that the paper claims that the proposed verifier is complete, but there is no proof of that. It does not seem like that's something too difficult to prove (given that BaB + LP is complete), but it should still be clearly stated. \n\nFinally, the claim that the proposed framework outperforms previous methods by \"at least 10X and up to 50X\" is unsupported. Based on the results in section 5, a fairer statement regarding the speed would be \"at least 3X and up to 15X\" faster.\n\n### Reasons for score\nIt is very difficult to judge this contribution, as the paper is hard to understand. The two main reasons for the score I give are 1) some of the claims of the paper are unsupported (see above) and 2) I believe this paper will have a much better chance of conveying the idea and making a contribution, if more background knowledge and intuition is provided throughout.\n\n### Suggestions for improvement that have not affected the score I gave to the paper\n\nOne way to significantly improve the paper is to introduce more examples. An example consisting of a simple neural network to refer to throughout the explanation of LiRPA and BaB, and also in section 4, would make the paper much easier to read. \n\nAs a reader, I felt I couldn't appreciate the related work section so early in the paper. I encourage you to either move it later in the paper, or even better: introduce more background/examples in the introduction, as well as the notion of completeness, so that the related work is easier to understand.  \n\nSome typos:\n* Abstract: \"we demonstrate over a magnitude speedup ...\" -> \"we demonstrate speedup of an order of magnitude ...\" \n* First paragraph of section 2: \"guarantee to terminate either ...\" -> \"guarantee to terminate when either ...\"\n* First paragraph of page 3: \"used in state-of-the-art verifier (Lu & Kumar, 2020)\" -> \"used in the state-of-the-art verifier by Lu & Kumar (2020)\".\n* Second paragraph of page 3: \"Our paper firstly leverage ...\" -> \"Our paper firstly leverages ...\"\n* First paragraph of section 3.1: \"linear functions in the form of ...\" -> \"linear functions of the form ...\"\n* Start of section 4.1.: \"As we have introduced ...\" -> \"As we discussed ...\"\n* Mid page 5: \"greatly limited ...\" -> \"greatly limits ...\"\n* Bottom of page 5: \"We follow the most challenge experimental setup ...\" -> \"We follow the most challenging experimental setup ...\"\n* Mid page 6: \"we quickly reaches ...\" -> \"we quickly reach ...\"\n* Mid page 6: \"with only two hidden node ...\" -> \"with only two hidden nodes ...\"\n* Section 4.3: \"Benefited from our design ...\" -> \"Benefitting from our design ...\"\n* Conclusion: capitalisation of the first sentence\n\n### Post rebuttal \n\nThank you to the authors for their detailed response and their effort in improving the presentation of the paper. I was impressed with how much the paper improved in this second version. In particular, I very much appreciate that the introduction starts with a simple one sentence explanation of the problem of neural network verification. This can be further improved if it included (almost) no maths, which can be deferred to the Background section. The figures in the updated paper are very good and a huge improvement of presentation. Finally, the paper now includes two clearly stated theorems, which also make the presentation and contribution much clearer. \n\nI have increased the score I gave to the paper. Regardless of what the outcome for ICLR will be, I would like to encourage the authors to re-iterate on the presentation to really crystallize the problem, definitions and the suggested approach --- the paper is already so much better than the first version, and even just a little more work can make it even better. \n\n", "extra_scores": {}, "extra_text": {}}, {"review_id": "YEMYD0RJdN", "reviewer": "AnonReviewer2", "summary": "", "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": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "The authors demonstrate that using a modification of the LiRPA method during the branch-and-bound process for solving the neural network verification problem can lead to significant speed-ups. The experimental results are strong. The authors convincingly show that the their method outperforms the existing state-of-the-art method by Lu & Kumar (2020) on an experimental setup similar to that work. The application of LiRPA to branch-and-bound is straightforward (since any incomplete verifier can be used), as is the use of gradient descent to improve the bound given by LiRPA (a standard technique applied to improve the bounds of certain verifiers). \n\nDespite the fairly straightforward approach, the strength of the empirical results deserves attention. Overall, a solid contribution to the literature, and proof that research on incomplete verifiers leads to better complete verifiers. \n\nSome questions/requests:\n\n- The experimental setup details should be provided in the final version. \n\n- How dependent is the performance of LiRPA on GPUs? For example, if we do a CPU-only comparison between the different methods, would other methods now outperform LiRPA? And if so by how much? What if we use multiple cores? I would understand if a detailed comparison is too computationally intensive, but I would like some sense of this.\n\n---------------------------\nUpdate after author response:\nI thank the authors of the paper for significantly improving the prose of the paper, and I agree that the changes make the paper more self-contained and approachable. I have kept my ratings as my score was for primarily for the strong experiment results (and the score was also conditional on the paper being more polished). I am happy to support this paper for acceptance, but I am a little concerned about the degree of changes in the final version versus the initial submission, given the number of concerns the other reviewers had.", "extra_scores": {}, "extra_text": {}}, {"review_id": "X74S7dSa3EM", "reviewer": "AnonReviewer3", "summary": "", "questions": "", "limitations": "", "rating": 5, "confidence": 2, "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": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "The work proposes a new algorithm that can be used for the complete verification of neural networks (NNs). Unfortunately, the authors do not define the verification problem they study: Based on the second paragraph of the introduction, one is given a neural network (NN) on the input, and the task is to determine whether the NN has a specific formally defined property - but which kind of properties are verified is never explained. Intuitively, one would expect verification to focus on determining whether the NN gives a \"correct\" output for certain inputs, but that does not really match the general description given in the paper, and I did not find a place where the verification problem is formalized further. Without knowing what \"verification\" means in the context of this paper, it's difficult to follow the reasoning provided in the paper without having some rough idea of what kind of properties one wishes to verify (for instance, the discussion about using LP bounds assumes that the property that is being verified can be expressed using LP). I believe this issue could have been avoided by formalizing the precise task of verification (the verification problem).\n\nOn that note, many parts of the paper seemed rather confusing and hard to follow, either due to inconsistencies or due to language issues. For instance, the sentence \"Input domain split is shown effective in verifying the properties with low input dimensions while performs as poorly as incomplete verifiers on higher dimension properties\" on page 2 seems to contradict the definitions given for complete and incomplete verification. How can a complete verifier perform \"as poorly as incomplete verifiers\" if, by the definition given in the paper, complete verifiers must always correctly determine whether the NN has the given \"property\" or not? (Section 2: \"Complete verifiers guarantee to terminate either the property is proved or a violation is located.\")\n\nIn terms of presentation, the submission contains an incredibly large number of minor language issues (roughly 1 per 2-3 lines on average, ranging from minor article issues to malformed sentences; see also the quote in the previous paragraph), and I strongly encourage authors to fix these as they have a rather disruptive effect when trying to read and understand the paper. A very small number of examples is provided below:\nPage 1\n-\"cause the changes of NN predictions\" -> \"cause changes of NN predictions\"\n-\"Recently, a framework of Branch and Bound (BaB) (Bunel et al., 2018) is widely used for efficiently verifying NNs\" - cannot combine \"recently\" and \"is\".\n-\"adopts Linear Program (LP) bounding procedure\" -> \"adopts a Linear Program (LP) bounding procedure\"\nPage 2\n-\"for construct LPs\" -> \"for constructing LPs\"\n\nThe main contribution of the paper is the use of incomplete verifiers for complete verification, and the authors propose an algorithm for doing that using LIRPA bounds. However, I found no proof (or anything resembling a proof) showing that the resulting algorithm is correct, i.e., that it performs complete verification for neural networks. In fact, the problem is not even properly and formally defined in the paper. Hence, regardless of the experimental results, I do not think that the submission is ready for publication at this stage.\n\nPost-Rebuttal Comment:\nI thank the authors for responding to my comments. The updated version fixes most of the criticisms raised in the review, and I have raised the score accordingly. My new score is \"5\", partly because I believe that after performing such a large-scale and comprehensive overhaul of the paper (which was certainly necessary), the paper should go through a full new reviewing process. ", "extra_scores": {}, "extra_text": {}}, {"review_id": "5eA3cAre7mv", "reviewer": "AnonReviewer1", "summary": "", "questions": "", "limitations": "", "rating": 5, "confidence": 2, "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": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "The paper focuses on verifying simple properties of neural networks on\naccelerator hardware.  Instead of using linear programming, Lirpa is\nconsidered as an alternative and minimal amounts of LP is added around\nto allow to use the same class of properties. In the considered\nexamples the approach becomes much faster than the LP approach.\n\nMy main problem with the paper, is that is claims a complete\nverification procedure without proper proofs. Yes, the new algorithm\nis presented and some general discussion of things that are done with\nit and how they work is provided. However, to claim complete\nverification a general soundness of the procedure should be proved. In\nparticular I would like a theorem for the correctness of each of the\nvarious components and a combined theorem for the whole procedure.\n\nOn the other hand, the experiments show that the approach is fast and\nas such makes it more feasible for verification and the paper mostly\nreads well.\n\nAn interesting alternative to discuss in related work, could be proof\nassistants. See for example the work of Bentkamp, Blanchette JAR 2019.\nUsing proof assistants based on more complex logics, one can verify\nproperties much more efficiently.  The authors only mention Katz's\nwork on SMT, but if you consider higher order logic and the logics of\ninteractive theorem provers, the \"NP-hard properties\" can be checked\nwithout considering all the cases.\n\nMinor:\nConclusion starts with lowercase \"we\".\n\nBased on the problems found by the other reviews and having read the rebuttals I have modified my score.", "extra_scores": {}, "extra_text": {}}]

Author rebuttal:

Meta-review: Thank you for your submission to ICLR.  As noted, several of the reviewers had fairly low confidence in evaluating this submission.  However, based upon the reviewers and commenters who were familiar with this line of work, as well as my own evaluation of the paper, I believe it is clearly worth publishing at ICLR.  The proposed method pushes the boundary in methods for exact branch and bound-based verification of neural networks, using clever tricks from existing relaxations.  And while the method is still likely to be relegated to relatively small networks for the time being, pushing forward the state of the art in exact verification is still a worthy goal suitable for publication at ICLR.  I thus think that the paper is quite clearly above the bar, and should be accepted for publication.
Decision: Accept (Poster)