DeepSplit: Scalable Verification of Deep Neural Networks via Operator Splitting
Authors: Shaoru Chen
Eric Wong
J Zico Kolter
Mahyar Fazlyab
Venue: ICLR 2022 Submitted (2022)
Keywords: neural network verification
operator splitting
ADMM

Abstract: Analyzing the worst-case performance of deep neural networks against input perturbations amounts to solving a large-scale non-convex optimization problem, for which several past works have proposed convex relaxations as a promising alternative. However, even for reasonably-sized neural networks, these relaxations are not tractable, and so must be replaced by even weaker relaxations in practice.  In this work, we propose a novel operator splitting method that can directly solve a convex relaxation of the problem to high accuracy, by splitting it into smaller sub-problems that often have analytical solutions. The method is modular, scales to very large problem instances, and compromises of operations that are amenable to fast parallelization with GPU acceleration. We demonstrate our method in obtaining tighter bounds on the worst-case performance of large convolutional networks in image classification and reinforcement learning settings. 

Under review as a conference paper at ICLR 2022
DEEPSPLIT: SCALABLE VERIFICATION OF DEEP NEURAL NETWORKS VIA OPERATOR SPLITTING
Anonymous authors Paper under double-blind review
A ABSTRACT
Analyzing the worst-case performance of doep neural networks against input perturbations amounts to solving a large-scale non-convex optimization problem, for which several past works have proposed convex relaxations as a promising alternative. However, even for reasonably-sized neural networks, these relaxations are not tractable, and so must be replaced by even weaker relaxations in practice. In this work, propose a novel operator splitting method that can directly solve a convex relaxation of the problem to high accuracy, by splitting it into smaller sub-problems that often have analytical solutions. The method is modular, scales to very large problem instances, and compromises of operations that are amenable fast parallelization with GPU acceleration. We demonstrate our method in obtaining tighter bounds on the worst-case performance of large convolutional networks in image classification and reinforcement learning settings.
1 INTRODUCTION
Despite their superior performance, neural networks lack formal guarantees, raising serious concerns about their adoption in safety-critiaal applications such as autonomous vehicles (Cao et al. 2019) and medical machine learning (Finlayson et al. 2019). Motivated by this drawback, there has been an increasing interest. developing tools verily desirable properties for neural networks, such robustness to adversarial attacks. Neural network verification refers to the problem of verifying whether the output of neural network satisfies certain properties for bounded set of input perturbations. This problem can be framed as optimization problems of the form
minimize
J(f(x) subject to x xE
(1)
where f is given by a deep neural network, J is real-valued function representing performance measure (or a specification), and X' is a set inputs to be verified. In this formulation, verifying the neural network amounts to certifying whether the optimal value of [ is bounded below by a certain threshold. This problem is large-scale and non-convex, making it extremely difficult to solve efficiently-both in terms of time and memory. For ReLU activation functions and linear objectives, the problem in ( can be cast as a. Mixed- Integer Linear Program (MILP) (Lomuscio & Maganti 2017 Cheng al. 2017 Dutta al., 2018 F'schhetti & Jo 2018), which can be solved for the global solution via, for example, Branch-and-Bound (BaB) methods. While we do not expect these approaches to scale to large problems, for small neural networks they can still be practical.
Instead of solving [1] for its global minimum, one can instead find guaranteed lower bounds on the optimal value via convex relaxations, such as Linear Programming (LP) (Wong & Kolter 2017 and Semidefinite Programming (SDP) (Raghunathan et al. 2018 Fazlyab al. 2019 2020). Verification methods based on convex relaxations are sound but incomplete, i.c., they are guaranteed to detect all false negatives but also produce false positives, whose rate depends on the tightness of the relaxation. Although convex relaxations are polynomial-time solvable (in terms number of decision variables), in practice they are not computationally tractable for large-scale neural networks. To improve scalability, these relaxations must typically be further relaxed (Wong & Kolter 2017 Weng et al.) 2018 Zhang et al. 2018
Dvijotham et al. 2018 Bunel al. 2020a).

---

Under review as a conference paper at ICLR 2022
Contributions In this work, we propose algorithm for solving convex relaxations exactly for large-scale neural networks. Our starting point is to express (I) as a constrained optimization problem whose constraints are imposed by the forward passes in the network. We then introduce additional decision variables and consensus constraints that naturally split the corresponding problem into independent subproblems, which often have closed-form solutions. Finally, we employ an operator splitting technique based on the Alternating Direction Method of Multipliers (ADMM) (Boyd et al.) 2011), ,, to solve the corresponding Lagrangian relaxation of the problem. This approach has several favorable properties. First, the method requires minimal parameter tuning and relies on simple operations, which scale to very large problems and can achieve a good trade-off between runtime and solution accuracy. Second, all the solver operations are amenable to fast parallelization with GPU acceleration. Third, our method is fully modular and applies to standard network architectures.
We employ our method to compute exact solutions to LP relaxations on the worst-case performance of adversarially trained deep networks, with a focus networks whose convex relaxations were previously impossible to solve exactly due to their size. Specifically, we perform extensive experiments in the loo perturbation setting, where verify robustness properties of image classifiers for CIFAR10 and deep Q-networks (DQNs) in Atari games (Zhang al.] 2020 Our method is able to quickly solve LP relaxations at scales that are Loo large for exact BaB verifiers, SDP relaxations, or commercial LP solvers such as Gurobi.
1.1 RELATED WORK
Convex relaxations LP relaxations are relatively the most scalable form of convex relax- ations (Ehlers 2017). However, even solving L.ss can become computationally prohibitive for small convolutional networks (Salman et al. 2019). One line of work studies computationally cheaper but looser bounds of the LP relaxation (Wong & Kolter 2017 which have been extended to larger and more general networks and settings (Wong et al. 2018 Weng et al. 2018: Zhang et al.] [2018] Xu et al. 2020). These bounds tend to be loose unless optimizod during training, which typically comes at significant cost. to slandard performance. Further work has aimed to tighten these bounds (Singh et al., 2019 (Tjandraatmadjja el al., 2020 de2), however these works focus primarily small convolutional networks and struggle to scale to more typical deep networks. Other work has studied the limits of these convex relaxations on these small networks using vast amounts of CPU-compute (Salman et al. 2019). Recent SDP-based approaches (Dathathri et al. 2020 can produce much tighter bounds these small networks.
Lagrangian-based bounds Related to our work is that which solves the Lagrangian of the LP relaxation (Dviotham et al. 2018 Bunel et al. 2020a), which can tighten the bound but do not aim to solve the LP exactly due to relatively slow convergence. However, these works primarily study small networks whose LP relaxation can still be solved exactly with Gurobi. Although these works could in theory be used on larger networks, only the faster, linear-based bounds (Xu et al.] 2020) have demonstrated applicability to standard deep learning architectures. In our work, we solve the LP relaxation exactly in large network settings that previously have only been studied with loose bounds of the LP relaxation such as LiRPA (Xu et al. 2020).
Complete verification methods These methods verify properties of deep networks exactly (without false positives or false negalives) using methods such as SMT solvers
(Scheibler et al. 2015; Ehlers 2017 Katz et al. (017) and MILP solvers (Lomuscio &
2018 Fischetti & Jo 2018]. Complete Maganti 2017 Cheng et al. 2017 Dutta et al.]
verification moth typically rely on BaB algorithms [Bunel et al.) (017). 7), in which the
verification problem is divided into subproblems (branching) that can be verified using incomplete verification methods (bounding) (Bunel et al. 2020b). However, these methods have a worst-case exponential runtime and have difficulty scaling beyond relatively small convolutional networks. Motivated by this, several recent works have improved the practical rumning time of BaB methods with custom solvers for medium-sized networks (Bunel et al. 2020a; De Palma et al. 2021. Xu et al. 2021 Wang et al. 2021), but have yet to scale to larger deep networks.
2

---

Under review as a conference paper at ICLR 2022
Operator splitting methods Operator splitting, and in particular the ADMM method, is a powerful technique in solving structured convex optimization problems and has applications in numerous settings ranging from optimal control (O (O'Donoghue et al. 2013) to training neural networks (Taylor et. al. 2016). These methods scale well with the problem dimensions, can exploit sparsity in the problem data efficiently (Zheng et al. 2017).
amenable to parallelization on GPU (Schubiger et al. (2020), and have well-understood convergence properties under minimal regularity assumptions (Boyd al. 2011.. The benefit of ADMM as an alternative to interior-point solvers has been shown in various classes of optimization problems (O'oonoguue et al. 2016). Our operator splitting method is specifically tailored for neural nelwork verilication in order to fully exploit the problem structure.
Notation. We denote the set of real numbers by R. the set of nonnegative real numbers by RG, the set of real n-dimensional vectors by R", the set of m n-dimensional matrices by Rmxx, and the n-dimensional identity matrix by In- The p-norm (p 2 1) is denoted by
||- lp: 1² + 14. For set S, define the indicator function [s(x)) of S as lls(x) 0 if x S and [l(()) = +o0 otherwise. Given a function f: X' + Y, the graph of f the set Gy [(x,f(x)) [x E
2 SCALABLE NEURAL NETWORK VERIFICATION VIA OPERATOR SPLITTING
We consider an l-layer ford-forward neural network f(x): R Rh described by the following recursive equations,
(2) where 20 E Roo is the input to the neural network, IA E Ras is the imput to the k-th layer, and Φ&: Th - Me is the operator of the k-th layer, which can represent any commonly-used operator in deep networks, such as linear (convolutional) layers, MaxPooling units, and activation functions.
Io I, Tk+1 = Ōx(xx)) -......,66-
f(z)=
Given the neural network f, a specification function J: Rd + R, and an input set X' R"o, we say that f satisfies the specification J if (+)))) > 0 for all x E X. This is equivalent to verifying that the optimal value of [1 is non neggnegaieee We assume X' C I is a closed convex set and J: RT + R [+ } is convex function, defining a performance measure on the output of the network. Note that our formulation generalizes to arbitrary computational graphs (e.g. residual blocks) and general objective functions (see Appendix B
Using the sequential representation of the neural network in 2 we may rewrite the optimization problem in [ as the following constrained optimization problem,
J' + minimize
((x) subject to Tk+1 = (x(),),
,- 1,
To E X
(3)
with n = Eo decision variables. We can rewrite 33 equivalently as
Do E XX (4) J minimize J(z)) subject (Ix, 2x+1) E Go. k= -......,.11.
Fn} is the graph of dx. Here Ta and Ty are a priori known bounds on dh when xo E X. The problem in (1) is non-convex due to presence of nonlinear operators in the network, such activation layers. By over- approximating Gor by convex set (or ideally by its convex hull), we arrive at a direct layer-wise convex relaxation of the problem. However, solving this relaxation directly cannot scale to even medium-sized neural networks Salman et al. (2019). In this section, by exploiting the sequential structure of the constraints, we proposc a reformulation of whose convex relaxation can be solved efficiently and in a scalable manner.
where Go. {(Ix, Fx41) Zx+1 (xx),, Fx I 24
2.1 VARIABLE SPLITTING
By introducing the intermediate variables yk and zk, we can rewrite 13 as
J minimize subject to
(
(5)
V/ = Fk. 2x = ox(U)), Ik+1 = 2x, k: k= 0, ...
Zo E X
3

---

Under review as a conference paper at ICLR 2022
Ø0
22
Φ
ADMM module for layer k
6
Id
423 425
Avp
JAk
second update
first update
third update
Figure 1: Left: Illustration the network structure (top) and DeepSplit computation module for generic layer (bottom). Adding identity layers in between the neural network layers decouples the variables Is and allows processing them independently. Right: Over- approximation of the graph of lanh (top) and ReLU (boltom) function by convex hull.
which has now 3n no nr decision variables. Intuitively, we have introduced additional "ddentity layers" between consocutive layers (see Figure 1 By overapproximating Go. by a convex set Sox, obtain the convex relaxation
relaxxed miniiiize subject to
J (xx)
(6)
yk Jk. (yk, E Sour Ik+1 En. k= 0, ,--,,
xo E X,
for which Jelaxed S J This form known consensus yk and ø are just copies of the variable TA. As shown below, this "overparameterizatior" allows us to split the optimization problem into smaller sub-problems that can be solved parallel and often in closed form.
2.2 LAGRANGIAN RELAXATION AND OPERATOR SPLITTING
We x (....... ,2), y = (vu..... 1e and z (zo. (zo.... ... 21-1 to denote the concate- nated variables. By relaxing the equality constraints with Lagrangian multipliers, we define the augmented Lagrangian for (6) as follows,
((x,y,2, A, ()) (Ix)
Isa, (Mkr 2x) +1x(20) + (0/2)
Σ k=0
(1
yk + Ax 1Ax
k=
+ (p/2)
(1xx+1 - 13l13 1122 || 12)
(7)
k=
1e-1) and /a (wo,.... (e-1) the scaled dual variables (by 1/p) and > 0 is the augmentation constant. Note that we have only relaxed the equality constraints in (6). and the constraints describing the Sa, as well as X' are kept intact. Furthermore, the inclusion of augmentation will render the dual function differentiable (see the Appendix for more details), and hence, casier to optimize. For the Lagrangian in 7 the dual function, which provides a lower bound to Jreaaedd is given by g(,, p1) = inf (x.y.2) L(x, 2, 2, μt).
where A= (Ao..... ,e-
The best lower bound can then be found by maximizing the dual function.
Solving the inner problem jointly over (x, to find the dual function is as difficult as solving direct convex relaxation of (3). Instead, split the primal variables yx y. z) into x and (y, z) and apply the classical ADMM algorithm to obtain the following iterations
If strong duality holds, then this best lower bound would match Jielaeed- As shown in Salman al. 2019), strong duality holds under mild conditions.
4

---

Under review as a conference paper at ICLR 2022
Algorithm 1: DeepSplit. Algorithm
Data: neural network f (Eq. 2, bounded convex input set X, convex function J.
Result:
lower bound J relaxed
Problem [
Initializatio:: Iо E X, Ik+1 = (x(xx), yi = Tk. 24 = 2841, Av= = 0, pi = 0,
k = ,--,, 1, augmentation constant 0.
repeat
Step 1: x-update 9
Step 2: (y, z--ddalee
10
Step 3: dual updale
until stopping criterion is met; Output: (zz)
(shown in Figure
! for updating the primal and dual variables,
xt argminy C(x, y, 2, X, 14)
(8a)
(y+ z²) E argmin(y L(x* y, 2, X, pt)
(8b)
(X / )= (X, 11) + (A. [(x* yy xz k.).
(8c)
As we show below, the Lagrangian has a separable structure by construction that can be exploited in order to efficiently implement each step of
2.3 THE X-UPDATE
The Lagrangian in is separable across the Fy variables; hence, the minimization in 8a can be done independently for each rt. Specifically, for k = O, we obtain the following update rule for Zo:
T0 = Projx - Ao)-
(9a)
Projections onto the fo and l balls can be done in closed-form. For the & ball, can use the efficient projection scheme proposed in (Duchi et al. 2008). which has O(no) complexity in expectation. For subsequent layers k = I,... we obtain the updates
1 2 2 (yk- Au + z4-1 1k-11)
(9b)
27 arg min J(xx) L f11,,
- -100--0-11 +
(9c)
For convex and p > O, the optimization problem for updating 2e is strongly convex with a unique optimal solution. Indeed, its solution is the proximal operator of J/p evaluated at ze-1- 14-1- For the special case of linear objectives, J(zz) = Ie, we obtain the closed-form
solution o = -epp + (ze-1 - 1e-1).
2.4 THE (y, 2)-UPAATE
Similarly, the Lagrangian is also separable across the (Jk. 21) variables. Updating these variables in (bb) corresponds to the following projection operations per layer,
(vt 2x)) Prois,, (zt + #x41 + pk),
(10)
for - 0....... 1-1 Depending on the type of the layer (linear, activation, convolution, etc.), we obtain different projections, which we describe below.
Affine Layers. Suppose (vx) Weyn + +b is affine layer representing fully-comnectdd, convolutional, or average pooling layer. Then the graph of oe is already convex set given by Goz {yr, 2x) z4 wayk bu). Choosing So. = Gou. the projection in [10
takes the form
y = (nn + W
+ + W + bb))
(11)
2t Whie + bk-

---

Under review as a conference paper at ICLR 2022
The matrix (In, + W Wx) can be pre-computed and cached for subsequent iterations. We can do this efficiently for convolutional layers using the fast Fourier transform, which we discuss later in Section D3
Activation Layers. For an activation layer of the form 6(z) := (p)(())) ... Pn (z,,)²; the convex relaxation of G3 is given by the Cartesian product of individual convex relaxations i.c,, Sg = Sp x .... x S...- For a generic activation function yo: R - I, suppose we have a concave upper bound & and convex lower bound & on & over an interval [], i.e.,
((()) s (p())= s (fxx) A [). A convex overapproximation of Gp is
--=((x,y) ( g(z) S V ((z),
(12)
which turns out to be the convex hull of ((p)) when & and of are concave and convex envelopes of 9, respectively. As an example, when < ह. the ReLU activation function
admits the envelopes (fxx) = max(0, x), ((x) +
-- i-g
(x 2) on [ J
where y = max(0, and y= max(0, σ) (Ehlers 2017 Wong & Kolter 2017 (see Figure
The assumed pre-activation bounds g. and o used to relax the actival rnn Tunctions can be
obtained priori via a variely of existing techniques (Wong Kolter 2017 Zhang et al.
2018 2019 We present projection operators of additional layers in Appendix
2.5
THE CCPDAAE
Finally, we update the scaled dual variables follows,
v ) p = ur (* =t)
x Aa (xt
1 0,
l
1,
(13)
k 0,
The DeepSplit Algorithm is summarized in Algorithm 1 We provide further details such as parameter selection and efficient implementations for convolutional layers in Appendix
CONNECTION TO LAGRANGIAN-BASED METHODS
In this section, draw connections two related methods relying on Lagrangian relaxation. Specifically, we relate our approach to an earlier dual method (Dvijolham et al. 2018 (Section 3.1 as well as a recent Lagrangian decomposition method (Bunel et al. 2020a)
(Section 3.2) Overall, these approaches use a similar Lagrangian formulation, but the
specific choices in splitting and augmentation of the Lagrangian result in poorer theoretical convergence guarantecs when solving the convex relaxation to optimality.
3.1 DUAL METHOD VIA LAGRANGIAN RELAXATION OF THE NONCONVEX PROBLEM
Instead of splitting the neural network equations with auxiliary variables, an alternative strategy is to directly relax (3) with Lagrangian multipliers (aaieersssviiii (Dvijotham et al. 2018):
C(x. A) = J(re)
( du (xx)) (zx))
(14)
k=0
where x (Io. ... x1) and A (Ao...., Ae-1). This results in the dual problem g" maximize gA)), where the dual function is
o(A)= = inf (J(zz) + + T + SBr
En inf (T- - [x(()))) inf { {-> (o()))) ZoERo
E k= SuLSE
By weak duality, 9" < J The inner minimization problems in g()) compute the dual function for given X can often be solved efficiently or even in closed-form (Dvijotham et al. 2018p. The resulting dual problem unconstrained but non-differentiable; hence is solved using dual subgradient method (Dvijohha et al. 2018). However, subgradient methods are known to be very slow with convergence rate O(1/VN) where N is the number of updates [Nesterov] 2003). making it inefficient to find exact solutions to the convex relaxation. On the other hand, this method can be stopped at any time to obtain valid lower bound.

---

Under review as a conference paper at ICLR 2022
3.2 LAGRANGIAN METHOD VIA NON-SEPARABLE SPLITTING
Another related approach the Lagrangian decomposition method from Bunel et al. (020aa..
To decouple the constraints for the convex relaxation of (3), this approach can viewed as introducing one set of intermediate variables yk as copies of zq lo obtain
Felaxed f minimize
[yv)
(15)
subject to
(yk, Fk+1) SΦx
k= = , 1-1
yk = Ikk Tu X
== 0.......
This splitting is in the spirit of the splitting introduced in Bunel et al. (2020a by and differs from our splitting which uses two sets of variables in 55. By relaxing the consensus constraints yk = zk, the Lagrangian is
8-1 Σ Iso, Tx+1) + (x())).
C(x.y, (1) = (yve +
Σ Me M (yk xb) +
(16)
Again the Lagrangian is separable and its minimization results in the following dual function
((w) inf (J( +ue ye) + Su
inf (ye (ee
{ur yk
I M + inf { Mo zo).
Since the dual function is not differentiable, it must be maximized by subgradient method, which again has O(1/v N) rale. To induce differentiability in the dual function and improve speed, Bunel et al.
2020a) uses Augmented Lagrangian (AL). Since only one set of
variables was introduced in Therefore, for each update the dual variable, the AL must be minimized iteratively. To this end, [Bunel ct al. (2020a) an iterative subroutine. However, this slows down overall convergence and suffers from compounding errors when the sub-problems primal minimization must be solved to convergence in order to compute the dual function and produce valid bound.
15 the AL is longer separable across the primal variables.
the Frank- Wolfe Algorithm in block-coordinate as
not fully solved. When stopping early, the
In contrast to the approach described above, in this paper we used a different variable splitting scheme in 5) that allows us fully separate layers in neural network. This subtle difference has significant impact: we can efficiently minimize the corresponding AL in closed form, without resorting to any iterative subroutine. Specifically, we use the ADMM algorithu,, which is known to converge at an O(1/N) rate (He & Yuan 2012). In summary, our method enjoys an order of magnitude faster theoretical convergence, is more robust to numerical errors, and has minimal requirements for parameter tuning. To stop early, can use a similar strategy as the Frank- Wolfe approach from Bunel et al. (2020a) and run the primal iteration to convergence with fixed dual variables get valid bound.
EXPERIMENTS
The strengths of our method are (a) its ability to exactly solve LP relaxations and (b) do so at scales that were previously impossible. To evaluate this, we first demonstrate how solving the LP to optimality leads to tighter certified robustness guarantoes in image classification and reinforcement learning tasks (Section 4.1h. We then stress test our method in both speed and scalability against a commercial LP solver and in the large network setting (Section 4.2)
Setup In all the experiments, we focus on the setting of verification-agnossii networks, similar Dathathri al. (020). However, we focus on significantly larger networks that
If we define du (I=) (xx) + bx+1, where We+1, bx+1 are the parameters of the affine layer and a is layer of activation functions, this splitting coincides with the one proposed in Bunel al. (2020a
7

---

Under review as a conference paper at ICLR 2022
Table Certified test accuracy (%) of PGDDtrained models on CIFAR1O through ADMM, the Lagrangian dccomposition methods (Dvijotham et al.) 2018 Bunel et al. 2020b). and fast dual/ linear (Wong al., 2018: Xu al. 2020 or interval bounds [Gowal al. 2018
All the methods are given the same time budget.
Exact ADMM
Lagrangian methods
Fast bounds
Adam
Prox
Dual Adam
Dual Decomp Adam
Linear
IBP
1/255
64.0
17.4
61.1
47.6
47.8
59.8
42.8
1.5 /255
45.7 7
28.4
41.8
28.5
28.8
36.8
16.8
2/255
19.5
10.9
17.4
11.0
11.1
13.2
3.6
2.5/ 255
5.5
2.6
4.5
2.7
2.7
3.3
0.7
have previously only been feasibly bounded with fast. linear-based bounds the LP relaxation WWog et al. 2018 Xu et al.) 2020). All the networks have been trained adversarially with the PGD attack (Madry et al. 2017]. Full details about the network architecture, network training, and the parameters for our splitting method can be found in Appendix
4.1 IMPROVED BOUNDS FROM EXACT LP SOLUTIONS WITH ADMM
We first demonstrate how solving the LP exactly with our method results in tighter bounds than prior work. We consider two main settings: certifying the robust ness of classifiers for CIFAR10 and deep Q-networks (DQNs) in Atari games. We defer additional analogous results in the smaller MNIST setting to Appendix F.3
CIFAR10 Much work studying verification in CIFAR10 has focused primarily on a small CNN with only 6k hidden units smaller than the classic LeNet from MNIST (LeCun et al., In this regime, tighter approaches such as SDP and branch-and-boung are applicable.
2015
Instead, we consider an order of magnitude larger model, which cannot be feasibly solved by these alternatives. Up until this point, the only solutions for large networks were sincarbbased bounds to the LP relaxation (Wong ct al. 2018 Xu et al.] 2020). However, these bounds are known to be quite loose. How much better can do if solve the LP exactly?
In Table we find that solving the LP exactly leads to siguificant gains in certified robust ness for large networks, with up to 4% additional certified robustness over the best-performing alternative. All the methods in Table [ are given the same time budget. Indeed, the better theoretical convergence guarantees of ADMM translate to better results in practice: when given a similar budget, the Lagrangian basclines have worse convergence and cannot verify many examples. A complete description of these baselines is in Appendix F.3 with implementation details for the Lagrangian methods in Appendix
State-robust RL We demonstrate our approach on a non-classification benchmark from reinforcement learning: verifying the robustness of deep Q-networks (DQNs) to adversarial state perturbations (Zhang et al. 2020). Specifically, we verify whether a learned DQN policy outputs stable actions in the discrete space when given perturbed states. Similar to the large network considered in the CIFAR10 setting, this benchmark has only been demonstrably verified with fast but loose linear-based bounds (Xu et al. 2020).
Similar to the CIFARIO setting, we observe consistent improvement in certified robustness of the DQN when solving the LP exactly with ADMM across multiple RL scttings. We summarize the results using our method and the lincar-based bounds on LP relaxations (Wong ct al.] 2018 Xu al.) 2020) in Table 2 Further details regarding the datasct, the DQN architect uree, and this lask can be found in Appendix
4.2 SPEED AND SCALABILITY
In this section, stress test several aspects of DeepSplit for solving LP relaxations. We first compare solving speeds of our ADMM-based LP solver to a commercial-grade LP solver. We then push the limits of architecture size and solve the LP relaxation for standard ResNet 18.
8

---

Under review as a conference paper at ICLR 2022
Table 2: The percentage of actions from a deep Q-network that are certifiably robust to changes in the state space for three RL tasks: Bankheist, Roadrunner, and Pong. We compare fast linear bounds (Lincar) (Wong et al.
2018 Xu al. 2020 and ADMM.
Bankheist
Roadrummer
Pong
ADMM
ADMM
Linear
ADMM
0.0016
0.0012
36.6
96.1
97.4
0.0020
39.7
49.5
0.0016
26.3
27.5
0.0008
93.4
95.6
0.0024
25.9
0.0020
19.6
22.8
0.0012
92.1
94.3
0.0027
1.4
7.3
0.0024
1.1
3.7
0,0016
82.1
81.0
250-
500
200
relative improvement of bounds
relative improvement upper bounds
total of 1000 ResNet18 outpul lower and upper bounds are computed from ADMM and LiRPA for comparison in CIFAR10. Histograms of the relative improvement percentage of ADMM over LiRPA are shown for the lower (left) and upper (right) bounds, which have an average relative improvement of 31.61% and 2.32%, respectively.
Figure 2:
Speed comparison We first compare the solving speeds of our method with state-of- the- art solvers for convex relaxations: a commercial-gres
LP solver, Gurobi. Since Gurobi cannot handle large networks, we benehmark the approaches on a fully connected network that Gurobi can handle (see Appendix H for further details on experimental setup, as well as additional speed comparisons to alternative approaches).
We find that our method provides nearly 7x speedup over Gurobi. On average, it takes ADMM 38 seconds per example to calculate these intermediate bounds using a single GePorce GTX 1080, in comparison to 258 seconds per example for Gurobi Intel Core i7-6700K.
Scalability Finally, to test the scalability and generality of our approach, consider solving the LP relaxation for a ResNet18, which up to this point has simply not been possible. The only applicable method here is LiRPA (Xu et al.) 2020)- highly scalable implementation of the linear-based bounds that works for arbitrary networks but can be quite loose in practice. We defer specific experimental details to Appendix [
We find that exact LP solutions with our ADMM solver can also produce substantial improvements in the bound at ResNet.18 scales, as shown in Figure 2 For substantial number of examples, we find that ADMM can find significantly tighter bounds (especially for lower bounds). tabular presentation of the results is Table 5 of Appendix
5 CONCLUSION
In this paper, we proposed DeepSplit, a scalable and modular operator splitting technique for solving convex relaxation-baus verification problems for neural networks. The method can exactly solve large-scale LP relaxations with GPU acceleration with favorable convergence rates. Our approach leads to significantly tighter bounds across a range of classification and reinforcement learning benchmarks, and can scale to standard ResNet18. We leave as future work a further investigation variations ADMM that can improve convergence rates in deep learning-sized problem instances, well extensions beyond the IPP setting.

---

Under review as a conference paper at ICLR 2022
REFERENCES
Dimitri P Bertsekas. Nonlinear programming, Journal of the Operalional Reseorch Sociely, 48(3):334 334, 1997.
Stephen Boyd, Neal Parikh, and Eric Chu. Distributed optimization and statistical learning via the alternating direction method of multipliers. Now Publishers Inc, 2011.
Rudy Bunel, Tkker Turkaslan, Philip HS Torr, Pushmeet Kohli, and M Pawan Kumar. A unified view of piecewise linear neural network verification. ar preprint 1x1:1711.000 2017.
Rudy Bunel, Alessandro De Palma, Alban Desmaison, Krishnamurthy Dvijotham, Pushmeet Kohli, Philip Torr, and M Pawan Kumar. Lagrangian decomposition for neural network verification. In Conference on Uncertainty in Artificial Intelligence, pp. 370 379.. PMLR, 2020a.
Rudy Bunel, Jingyue Lu, Tkker Turkaslan, Pushmeet Kohli, P Torr, and Mudigonda. Branch and bound for piecewise linear neural network verification. Journal of Machine Learning Research, 21 (2020), 2020b.
Yulong Cao, Chaowei Xiao, Benjamin Cyr, Yimeng Zhou, Won Park, Sara Rampazzi, Qi Alfred Chen, Kevin Fu, and Z Morley Mao. Adversarial sensor attack on lidar- based perception in autonomous driving. Tn Proceedings of the 2019 ACM SIGSAC conference on computer and communications security, pp. 1267-2281, 2019.
Chib-Hong Cheng, Georg Nührenberg, and Harald Ruess. Maximum resilience of artificial neural networks. In International Symposium on Automated Technology for Verification and Analysis, pp. 251.268. Springer, 2017.
Sumanth Dathathri, Krishnamurthy Dvijotham, Alexey Kurakin, Aditi Raghunathan, Jonathan Uesato, Rudy Bunel, Shreya Shankar, Jacob Steinhardt, Ian Goodfellow, Percy Liang, et al. Enabling certification of verification-agnostii ic networks via memory-effiiient semidefinite programming. arXiv preprint. arXivv2010.1 11645, 2020.
Alessandro De Palma, Rudy Bunel, Alban Desmaison, Krishnamurthy Dvijotham, Pushmeet Kohli, Philip HS Torr, and M Pawan Kumar. Improved branch and bound for neural network verification via lagrangian decomposition. Xr preprint arXiv:2104.06714 2021.
John Duchi, Shai Shalev-Shwartz, Yoram Singer, and Tushar Chandra. Efficient projections outo the 1 1-ball for learning in high dimensions. In Proceedings of the 25th international conference on Machine learning, pp. 272 279, 2008.
Souradeep Dutta, Susmit Jha, Sriram Sankaranarayanan, and Ashish Tiwari, Output range analysis for deep feodforward neural networks. In NASA Formal Methods Symposium, pp. 121-138. Springer, 2018.
Krishnamurthy Dvijotham, Robert Stanforth, Sven Gowal, Timothy Mann, and Push- meet Kohli. A dual approach to scalable verification of deep networks. arXiv preprint arxie:1803 06567, 2018
Ruediger Ehlers. Formal verification of piece-wise linear feed-forward neural networks. In International Symposium on Automated Technology for Verification and Analysis, pp. 269-286. Springer, 2017.
Mahyar Fazlyab, Alexander Robey, Hamed Hassani, Manfred Morari, and George J Pappas. Efficient and accurate estimation of lipschitz constants for deep neural networks. arXiv preprint arXiv:1906. 04893, 2019.
Mahyar Fazlyab, Manfred Morari, and George J Pappas. Safety verification and robustness analysis of neural networks via quadratic constraints and semidefinite programming. IEEE Transactions Automatic Control, 2020.
10

---

Under review as a conference paper at ICLR 2022
Samuel G Finlayson, John D Bowers, Joichi Ito, Jonathan L Zittrain, Andrew L Beam, and Isaac S Kohane. Adversarial attacks on medical machine learning. Science, (63(3) 1287-1289, 2019.
Matteo Fischetti and Jason Jo. Deep neural networks and mixed integer linear optimization. Constraints, 23(3):296 309, 2018.
Sven Gowal, Krishnamurthy Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Uesato, Timothy Mann, and Pushmeet Kohli. On the effectiveness of interval bound propagation for training verifiably robust models. arXiv preprint Xrx 12715, 2018.
Bingsheng He and Xiaoming Yuan. On the o(1/n) convergence rate of the douglas- rachs-racoorrt alternating direction method. STAM Journal on Numerical Analysis, 50(2):700-77) 700, 2012.
BS He, Hai Yang, and SL Wang. Alternating direction method with self-adaptive penalty parameters for monotone variational incqualities. Journal of Optimization Theory and applications, 106(2):337 356, 2000.
Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel Kochenderfer. Reluplex: An efficient smi solver for verifying deep neural networks. In International Conference on Computer Aided Verification, pp. 97-117. Springer, 2017.
Yann LeCun et al. Lenet-5, convolutional neural networks. URL: http://yann. lecun. hmm/ezdb/leened 20(3):14, 2015.
Alessio Lomuscio and Lalit Maganti, An approach to reachability analysis for leed-forward relu neural networks. orXiv preprinl arXiv:1706.070 2017.
Aleksander Madry, Aleksandar Makelov, Ludwig Schmidt, Dimitris Tsipras, and Adrian Vladu. Towards deep learning models resistant to adversarial attacks. arXiv preprint arxiv: 200.000600000 066.,,083, 2017.
Yurii Nesterov.
Introductory lectures convez optimization: A basic course, volume 87.
Springer Science & Business Media, 2003.
Brendan O'Donoghue, Giorgos Stathopoulos, and Stephen Boyd. A splitting method for optimal control. IEEE Transactions Control Systems Technology, 21(6):2432 2442, 2013.
Brendan O'donoghuc, Eric Chu, Neal Parikh, and Stephen Boyd. Conic optimization via operator splitting and homogeneous self-dual embedding. Journal of Oplimization Theory and Applications, 169(3):1042 1068, 2016.
Aditi Raghunathan, Jacob Steinhardt, and Percy S Liang. Semidefinite relaxations for cortifying robustness to adversarial examples. In Advances in Neural Information Processing Systems, pp. 10900 10910, 2018.
Hadi Salman, Greg Yang. Huan Zhang, Cho-Jui Hsieh, and Pengchuan Zhang, convex relaxation barrier to tight robustness verification of neural networks. arXiv preprint Xr:: 08722, 2019.
Karsten Scheibler, Leonore Winterer, Ralf Wimmer, and Bernd Becker. Towards verification of artificial neural networks. In MBMV, pp. 30-40, 2015.
Michel Schubiger, Goran Banjac, and John Lygeros. Gpu acceleration of admm for large-scale quadratic programming. Journal of Parallel and Distributed Computing, 144:55 67, 2020.
Gagandeep Singh, Rupanshu Ganvir, Markus Püishel, and Martin Vechev. Beyond the single neuron convex barrier for neural network certification. Advonces in Neural Information Processing Systems, 32:15098-15109 2019.
Gavin Taylor, Ryan Burmeister, Zheng Xu, Bharat Singh, Ankit Patel, and Tom Goldstein. Training neural networks without gradients: scalable admm approach. In International conference on machine learning, pp. 2722 2731. PMLR, 2016.
11

---

Under review as a conference paper at ICLR 2022
Christian Tjandraatmadja, Ross Anderson, Joey Huchette, Will Ma, Krunal Patel, and Juan Pablo Vielma. The convex relaxation barrier, revisited: Tightened angle-neuron relaxations for neural network verification. orXiv preprint arXiv:2006. 14076, 2020.
Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. Beta-crown: Efficient bound propagation with per-neuron split. constraints for complete and incomplete neural network verification. arXiv preprint orXiv:2103.00
2021.
Tsui-Wei Weng, Huan Zhang, Hongge Chen, Zhao Song, Cho-Jui Hsich, Duane Boning, Inderjit S Dhillon, and Luca Daniel. Towards fast computation of certified robustness for relu networks. Xie preprint urxiv:1804. 09699, 2018.
Eric Wong and J Zico Kolter. Provable defenses against adversarial examples via the convex outer adversarial polytope. arXw preprint arXiv:1711.00851, 1 2017.
Eric Wong, Frank R Schmidt, Jan Hendrik Metzen, and J Zico Kolter. Scaling provable adversarial defenses. arXiv preprint ar 12514, 2018.
Eric Wong, Leslie Rice, and J Zico Kolter. Fast is better than free: Revisiting adversarial training. ai preprint ar X00: 003994, 2020.
Kaidi Xu, Zhouxing Shi, Huan Zhang, Yihan Wang, Kai- Wei Chang, Minlic Huang, Bhavya Kailkhura, Xue Lin, and Cho-Jui Hsich. Automatic perturbation analysis for scalable certified robustness and beyond. Advances in Neurul Information Processing Systems, 33, 2020.
Kaidi Xu, Huan Zhang, Shiqi Wang, Yihan Wang, Suman Jana, Xue Lin, and Cho-Jui Hsich. Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. In International Conference on Learning Represenlations, 2021. URL https://openrewierr ott./
Huan Zhang, Tsui- Wei Weng, Pin- Yun-Yu Chen, Cho-Jui Hsich, and Luca Daniel. Efficient neural network robustness certification with general activation functions. arXie preprint or Xin: 1.:::8111000000 800006 2018.
Huan Zhang, Hongge Chen, Chaowei Xiao, Sven Gowal, Robert Stanforth, Bo Li, Duane Boning, and Cho-Jui Hsieh. Towards stable and efficient training of verifiably robust neural networks. arXiv preprint arXiv:1906. 06316, 2019.
Huan Zhang, Hongge Chen, Chaowei Xiao, Bo Li, Duane Boning, and Cho-Jui Hsieh. Robust deep reinforcement learning against adversarial perturbations on observations. Advances in Neural Information Processing Systems, 2020.
Yang Zheng, Giovanni Fantuzzi, Antonis Papachristodoulou, Paul Goulart, and Andrew Wynn. Fast admm for semidefinite programs with chordal sparsity. In 2017 American Control Conference (ACC), pp. 3335 3340. IEEE, 2017.
12

---

Under review as a conference paper at ICLR 2022
Demonstration of our codes are anonymously available in the attachment.
A CONVERGENCE ANALYSIS OF DEEPSPLIT
By defining X = x, X2 = 2) (the primal variables) and v = (A, 1)) (the scaled dual variables), we can write the split convex relaxation in 6
minimize fi(x1) + fx
(17)
subject to A|x + A2x2 =0
with the corresponding Augmented Lagrangian
L(xI, X2, v) = fi(x) + fx(x) 2 (1IAAx) + A2xa + +11 11(13
(18)
where fI: R - R RUU and f2: R2n > R [uf+o0} are extended real-valued functions
defined as [1(x (xxx)= == ( (To), 12(x2) = Ex=o Ss (yk, zw). Moreover, A1x + Agx2 = 0
represents the set oquality constraints yk = 2hk and xx+1 = 21 for = 0,,.. ,,, The dual
function is given by
g(v) inf L(x1, v). X1.32
(19)
By Danskin's theorem
(ertsekaa 1997), the sub-differential of the dual function is given by Ög(v) {A,x1 + A2X2: (X1, E arg min X(x1,x2,11)
(20)
Here X1, X2 are minimizers of the Lagrangian (not. necessarily unique), which satisfy the optimality conditions
E p4 A28, +v)
-
(21)
E (f2 - pAd (A1 + A2x2 +)
First, we show that the sub-differential is a singleton, i.e., g is continuously differentiable. Sup- pose (X1, E argmin min ((E, v) and (W1, W2) E arg min L(E, v) are two distinct minimizers of the Lagrangian, hence satisfying
0 E (w1) + pAd (Ai W1 + A2 + +v)
(22)
0 0 + PA? (A w + A2w2 + +v) By monotonicity of the sub-differentials, we can write
(0,) (w1)) (x) -w1) 2
20
(23)
(8f)(x,) - Of2 (w2(w))) (X2 W2) 20
By substituting [21 and [22 in 23 we obtain
(pA) (A₂x; + Agx₂ =) pAe (At + A2 + +V)) T (X1 W1) 2 0
(24)
(pA (A1x1 + A, +v pAd (A1 W1 + A2 + +))) (x22 W2) 2
By adding the preceding incqualities, obtain
-p||Ai + A2x; (A| + A
(25)
This implies that A₁ + A,X, A, + Azw, and hence, the sub-differential 0g is singleton.
Convergence. When X' is a closed nonempty convex set, (x(2)) is a convex closed proper (CCP) function. Assuming that J is also CCP, then we can conclude that fi is CCP. Furthermore, since the sets So, are nonempty convex sets, Under these assumptions, the augmented Lagrangian has a minimizer (not necessarily unique) for each value of the dual variables. Finally, under the assumption that the Augmented Lagrangian has a saddle point (which produces a solution to (17)), the ADMM algorithm we have primal convergence ||rp1| + 0 (scc (31)), ), dual residual convergence ||ral - 0, well as objective convergence J(Zz) + J (Boyd et al. 2011).
conclude that. /2 is CCP.
We remark that the convergence guarantees of ADMM holds even if f1 and fa assume the value +oo, This is the case for indicator functions resulting in projections in the first two updates of ADMM.
13

---

Under review as a conference paper at ICLR 2022
B ADMM FOR GENERAL COMPUTATIONAL GRAPHS
To handle general computational graphs, we follow the approach used in (Wong et al. 2018). Specifically, consider a generalized & 2-"layer" neural network given by the equations
& 1k+1 Σ da (I:) = (x((11)) k = 0....... . ,
(26)
where 21.6 denotes the concatenated vector of variables (x1,--. xR). Note that this view of a network reduces to the feedforward equations in 2 when (xx(2;) = 0 for all i < Furthermore, this view subsumes arbitrary skip connections, such as residual conncctions. Then, the graph form of the verification problem in (4] can be rewritten for the generalized neural network as
minimize subject to (21:k, Ix+1) E (or()n)) 0= 1-11
((xe)
(27)
E X.
Similar to before, let Sae be a sound convex approximation of Gos. Then, our convex relaxation introduces additional intermediate variables yısk and 24 to get the following convex relaxation (analogous to (
Prelaxed minimize
(xx)
(28)
subject to
Vi.k Ti:k
A 0, .6-
(y1:k: 21. E Sax
0, 1...,---
Ik+1 2k
.6-
xp X.
Thus, producing an ADMM layer for network with arbitrary skip connections reduces to deriving the corresponding projection operator onto Spc- Since most residual connections simply add an affine transformation of a previous layer, these projections are straightforward and have a closed form (an example of a typical residual ADMM block in Appendix C
C ADMM LAYERS
C.1 RELU PROJECTION
Consider the ReLU function y = (xx) = max(0, on the interval x E [2, The projection of a point (I()), ()) onto the convex hull of G(p) has a closed-form solution. We consider three cases.
Active neuron (g 2 0). In this case, the convex hull is given by
S = {(I,y) y == x, I S x $ a}. and the projection of (a( ()) onto S, is given by x' v min +0)
..)
2. Inactive neuron (# < 0). In this case, the convex hull is
S {(z,v)) v) y 0, z S < æ).
and the projection of (x(0),(()) ()) onto Sp is given by x' = (in(max(z:"),,))) y' 0.
Unknown neuron (I < 0 5 Ø). The convex hull is given by O, x, v x)} where = 8-ル = max(0, 2), 7 = ma 2). We first project (1) (0)) onto each facet of Ø-2'
S, = (xx v)
the triangle and then select. the point with the minimal distance.
(0) (0)
(1) min(max
0), y = (1))
x
+ sy )) + s(ST - y) x), y(2) s(z x) + s2 2
(2) min(max(
52
(3) min(max(00, (0))), ((3) =
14

---

Under review as a conference paper at ICLR 2022
20
20
c 9
03
03
6x111
03
80
22
(x1111
-20
-15
-10
-85
3.0
-20
-1.
-1.0
8.5
20
-20
-15
-18
-35
90
10
Figure 3: Projection of point (Io, yo) onto the convex hull of the ReLU function y/ = m0) over the interval [z, Ø]. We first project (wo. vo) onto all facets of the convex hull and then select the point with minimal distance to (zo. 30).
The projected point is arg minisia v(x(0) - 2())22 + (1(0) - y(
(d',8')
(x(1),
where
C.2 CONVOLUTIONS
Although convolution is technically linear operator, it is impractical to directly form the inverse matrix from the projection step of the DeepSplit algorithm. Instead, we represent typical convolutional layer fcoav with stride, padding and bias as
Seanv = fbins o fas o Serop o feire o Spad = Spost fcire o Spad,
(29)
where fpad is a padding step, foire is a circular convolution step, Scrop is cropping step, Sas is downsampling step to handle stride greater than one, and Jbias is a step that adds the bias. Then, the last three steps are combined into one post-processing step fpost to reduce the number of concensus constraints in the DeepSplit algorithm. The projection steps for all of these operators are presented next in Sections C.3 through C.6 and an efficient implementation of the projection step for the affine layer Jeire in Appendix b
C.3 PADDING
The padding layer Jpad takes an image as input and adds padding to it. Denote the input image by yi and the padded image by zk. We can decompose the output z into two vectors, zl which is copy of the imput ykk, and z which represents the padded zeros on the edges of image, Equivalently, the padding layer 25 dx(Hk) can be written in an affine form
!
2
0
yk Wayke
for which the projection operator reduces to the affine case.
C.4 CROPPING
The cropping layer fcrop crops the output of the circular convolution fere to the original size of the input image before padding. Denote yk the input image and 2 the output image of the cropping layer. By decomposing the input image into the uncropped pixels ve and the cropped pixels vl. the cropping layer z (v())) has an affine formulation
2*
v
0]
Wayk
V
whose projection operator is given in Section 2.4
C.5 DOWN-SAMPLING AND BIAS
the typical convolutional layer from has stride greater than one, a down-sampling layer is added in the DeepSplit algorithm, which essentially has the same affine form as the
15

---

Under review as a conference paper at ICLR 2022
cropping layer with different values of vi and yk- Therefore, the projection operator for the down-sampling layer reduces to the affine case as well.
The bias layer in the DeepSplit algorithm handles the case when the convolutional layer feany has a bias by and is implemented by 2 = Ø (Vk) = yk + by. This an affine expression and its projection operator is given in Section 2.4
C.6 CONVOLUTIONAL POST-PROCESSING LAYER
We combine the cropping, down-sampling and bias layers into one post-processing layer, ie., fpost = fsius @ fas fcrops as shown in 29).. This reduces the total number concensus constraints in the DeepSplit algorithm. Since all the three layers are in fact affine, the post-processing layer is also affine and its projection operator can obtained correspondingly.
C.7 MAXPOOLING
Consider Maxpooling layer d(x)) maxk Tk, k =, , over 2020b Appendix B.2) shows that the Maxpooling layer can be equivalently decomposed as combination of linear and ReLU layers. This is motivated by the following fact that max( F3. 24) max max,max(E1, (Ta) and max(r1, = max( 22, 0) max(#2 - I2, 0) + Z2. Therefore, we can represent the Maxpooling layer by composition of pairwise maximum functions which can themselves be decomposed into a combination of linear and ReLU layers. The projection operations onto the convex hull of the ReLU and
T. BBnell et al.
linear layers are closed-form shown in Appendix C.1 and Section 2.4 respectively.
C.8 RESIDUAL CONNECTION
We consider a typical residual connection Φ4 (yk, v.) = yı. + Way +6; for i < k, where is an arbitrary layer before yi and W,, b; is any affine transformation (i.e. I I convolution for upsampling or downsampling layer frequently used in residual connections with differently sized feature maps). Then, we can write this as
(x(u)) WEitkK + bi.
(30)
where yka = and Wki = [I Wi.. Then, the projection operator reduces to the affine
V/
case but with weights Wks b; for input yks-
C.9 BATCH NORMALIZATION AND AVERAGE POOLING
The batch normalization and average pooling layers that appear in the architecture of the residual networks, c.g., ResNet18 applied in this paper, are essentially affine mapping layers whose weights and biases can be extracted accordingly. Therefore, the projection onto the graph of these two layers has a closed-form solution as shown in Eq. (11).
D IMPLEMENTATION DETAILS
D.1 CONVERGENCE AND STOPPING CRITERION
The DeepSplit algorithm converges to the optimal solution of the convex problem 6 under mild conditions. Specifically, when J is closed, proper and convex, and when the sets Sk (convex outer approximations the graph of the layers) along with X' are closed and convex, resort. to the convergence results of ADMM (Boyd et. al. 2011
16

---

Under review as a conference paper at ICLR 2022
For the LP relaxation 6 of feed-forward neural network, the primal and dual residuals are defined as
Pp (lvi 11 + || 113
(31)
E-1 rd _ (1 yk) + (2 2x-1) (llb0 - 3oll2 + | - 22-1118)
These are the residuals of the optimality conditions for 6 and converge to zero as the algorithm proceeds. A reasonable termination criterion is that the primal and dual residuals must be small, L.e. Tp S Ep and S Ed, where Ep > 0 and > 0 are tolerance levels (Boyd jtt al. 2011 Chapter 3). These tolerances can be chosen using an absolute and relative criterion, such as
cp = vp Cabs Cre max [ +2
1 [xelBB)
(lua 11x1)))
6d = v cabs + Grat Ao 1 1111e-1113)
where no + 2 + ne, n Eizo fi, cabs > 0 and frel > are absolute and relative tolerances. Here n the dimension of x, the vector of primal variables that are updated in the first step of the algorithm, and is the total number of consensus constraints.
For neural networks with general computational graphs such as residual networks, the primal and dual residuals as well as the stopping criteria have different representations from what's shown above. But with our proposed splitting method, these representations are easy to derive from (Boyd et al. 2011 Chapter 3).
D.2 PARAMETER SELECTION
proper selection of the augmentation constant p has a dramatic effect on the convergence of the method. Large values of p enforces consensus residuals but larger dual ones. Conversely, smaller values of p leads to larger primal and smaller dual residuals. commonly used heuristic make this trade-off residual balancing He et al. (2000), in which the penalty parameter varies adaptively based on the following rule:
quickly, yielding smaller primal
TP rf pra if pr, otherwise,
pt
P/T
where 14, 7 > are parameters. In our experiments, we found this rule to be effective in speeding up the practical convergence.
D.3 CONVOLUTIONAL LAYERS
The projection step for affine layers from requires multiplication by the matrix (Iny + W. Wx)-1 for that layer, where is the number of neurons in the layer. When handling networks with convolutional layers on image data, ni can easily exceed tens of thousands, so the resulting matrix and its inversion exceed reasonable memory and computational constraints.
To make the update step practical and in line with typical computational costs of deep convolutional networks, we replace the typical deep learning convolution with an equivalent circular convolution. Specifically, let feenv be typical strided convolution with padding. We can rewrite from as three sequential updates using a circular convolution as foomv = fpost feire fpad, where fpad is padding step, feire is circular convolution, and f fpost is
17

---

Under review as a conference paper at ICLR 2022
post-processing step that performs cropping, downsampling, and adds any bias term from Sconv.
We can now treat these three updates separate, individual layers in our ADMM algorithm. The key observation is that we can use the convolution theorem to implement the ADMM update for the circular convolution feire efficiently. Specifically, for input of size ng nks the projection step from [11] for a circular convolution can be calculated in O(n log ny) using the fast Fourier transtorm. We provide the specific details of this procedure in Appendix
E FFT IMPLEMENTATION FOR CIRCULAR CONVOLUTIONS
In order to efficiently implement convolutional layers, recall that we decompose a convolution into the following three sleps:
Sconv = Spost o feire o Spad
(32)
We now discuss in detail how to efficiently perform the (y,z) update for multi-channel, circular convolutions feire using Fourier transforms. We begin with the single-channel setting, and then extend our procedure to the multi-channel setting. See Appendix C for details regarding the ADMM projection step for Spad and Spost.
E.1 SINGLE-CHANNEL CIRCULAR CONVOLUTIONS
Let U represent the discrete Fourier transform (DFT) as linear operator, and let W be the weight matrix for the circular convolution feire (2) = W x. Then, using matrix notation, the convolution theorem stales that
(cir( W= Un) U DUx
(33)
where D = diag(UW) is a diagonal matrix containing the Fourier transform of W and U is the conjugate transpose U. Then, we can represent the inverse operator from 11
as
(I+ f UT+ DD)
(34)
Since (I + DD) is diagonal matrix, its inverse can be computed quickly by simply inverting the diagonal elements, and requires storage space no larger than the original kernel matrix. Thus, multiplication by the inverse matrix for circular convolution reduces to two DFTs and an element-wise product. For an input of size n x n, this step has an overall complexity of (n² log n) when using fast Fourier transforms.
E.2 MULTT-CHANNEL CIRCULAR CONVOLUTIONS
We now exlend the operation for single-channel circular convolutions to multi-channel, which typically used in convolutional layers found in deep vision classifiers. Specifically, for circular convolution with imput channels and m output channels, we have
Scire (cire(x)) = =-we Wij 24
(35)
where [z)) is the jth output channel output of the circular convolution, Wi is the kernel of the ith input channel for the jth output channel, and x; is the ith channel of the input x. The convolutional theorem again tells us that
farc(z), = UU'DUU.
(36)
where Dig = (aag(UWW))) This can be re-written more compactly using matrices as
(cire = DU
(37)
where
18

---

is a block diagonal matrix with m copies of along the Under review as a conference paper at ICLR 2022
Ü
a block diagonal matrix with n copies of along the diagonal
0
U
U
0
0-=
U
diagonal
Di1
Dn1
=
:
is block matrix with diagonal blocks where the ijth
Dim
D Dam
block
Dij
21
x :
vertical stacking of all the input channels.
Zn
Then, we can represent the inverse operator from
11 as
(I + fdacfane)==
Ü* (1
(38)
where I + DD is block matrix, where each block is diagonal matrix. The inverse can then be calculated by the inverting sub-matrices formed from sub-indexing the diagonal components. Specifically, let Dj:p be slice of D containing elements spaced m clements apart in both column and row directions, starting with the jth item. For example, Do:p is the matrix obtained by taking the top-left most element along the diagonal of every block. Then, for j = .....m m, we have
(I+ DD) - ((I+DD);))
(39)
Thus, calculating this matrix amounts to inverting a batch of p matrices of size m x m. For typical convolutional networks, is typically well below 1, 000, and so this can be calculated quickly. Further note that this only needs to be calculated once as a pro-computation step, and can be reused across different inputs and objectives for the network.
Memory and runtime requirements In practice we do not store the fully-expanded block diagonal matrices; instead, we omit the zero entries and directly store the the diagonal entries themselves. Consequently, for an input of size p, the diagonal matrices require storage of size (mmp), and the inverse matrix requires storage of size O(m²p). Since the discrete Fourier transform can be done in Opplog p) time with fast Fourier transforms, the overall runtime of the precomputation slep to form the matrix inverse the cost of the initial DFT and the batch matrix inverse, or Ommp log + m²²)). Finally, the runtime of the projection step is ((n + mlgloog +ogp+n"mpp) n²mp), which is the respective costs of the DFT transformations Ú and U* as well as the multiplication by D. Since the number of channels in deep network are typically much smaller than the size of the input to a convolutionn (i.c. n < p and m < p), the costs of doing the cyclic convolution with Fourier transforms are in line with typical deep learning architectures.
F EXPERIMENTAL DETAILS
F.1 ARCUITECTURES, DATASETS, AND TRAINING SPECIFICS
MNIST
We consider two ReLU based architectures. The first one is fully connected
network with layer sizes 784-600 600 400 1000-200 2000000-1100 100- 10 which we denote MNIST-A. more than triple the size of that considered by (Dathathri et al.] 2020) with one additional layer. It is, however, still small enough such that Gurobi is able to solve the LP relaxation, and allows
us to compare running time against Gurobi. The second is a convolutional network
19

---

Under review as a conference paper at ICLR 2022
Table 3:
Approximate verification time for solving the LP relaxation through ADMM. Epsilons are evenly spaced within the range.
Model
# of epsilon
Epsilon range
Time (hrs)
MNIST-A
10
[0.01, 0.1]
13.12
MNIST-B
[0.01, 0.1]
19.92
CIFAR10
8
00.5/555, 4/255
50.69
Bankheist
10
0..1/255, 1/255
4.96
Roadrunner
10
0..1/555, 1/255
52.33
Pong
00.1/255,
1/255
31.06
which uses the small convolutional architecture from (Wong et al. 2018 and consists of two
convolutional layers of size 16 32 with kernel sizes 4- 4, strides 2 2- and padding 1 We denote this network by MNIST-B. This architecture is comparable to the convolutional architecture considered by (Dathathri et al. 2020), and allows us to compare rumning time against the gradient-based SDP solver.
We train both models with foo. PGD adversary at radius 0.1, using 7 steps of size = 0.02, with batch size 100 for 100 epochs. We use the Adam optimizer with a cyclic learning rate (maximum learning rate of 0.005), and both models achieve a clean accuracy of 99%.
CIFAR10 For CIFARIO, we use the large convolutional architectures from (Wong et al. 2018). which consists of four convolutional layers with 32 - 32 64 - 64 channels, with strides 1
4, and padding 1 1 1. This is followed by three linear layers of size 512 - 512 - 10. This is significantly larger than the CIFAR10 architectures considered by (Dathathri et al. 2020), and has sufficient capacity to reach 43% adversarial accuracy against an too PGD adversary at = 8/255.
2, kernel sizes
4
The model is trained against a PGD adversary with 7 steps of size a = 2/255 at a maximum radius of 8.8/255, with batch size 128 for 200 epochs. We used the SGD optimizer with a cyclic learning rate (maximum learning rate of 0.23), momentum 0.9, and weight decay 0.0005, The model achieves clean test accuracy of 71.8%.
State-robust RL et al. 2020 from
We use the pretrained, adversarially trained, DQNs released by Zhang
https::/gituub..cm//chhhboprgpp
which has not included any license information up the date of submission of this paper. These models were trained to be robust at 1/2555 with PGD adversary for the Atari games Pong, Roadrunner, Freeway, and BankHeist. Each input to the DQN of size 1 x 84 x 84, which is more than double the size of CIFAR10. The DQN architectures are convolutional networks, with three convolutional layers with 32 - 64 64 channels, with kernel sizes 8 -4 4 3, strides 4 2 - 1, and no padding. This is followed by two lincar layers of size 512 - K, where is the number of discrete actions available in cach game.
F.2 TIMING EXPERIMENTS
Runtime summary: We certify the robustness of classifiers for MNIST and CIFAR10 and DQNs in Atari games to &oo perturbations setups can be found in Appendix F.3 and F.4 We report the approximate runtime for all experiments in Table
range of radii. The specific verification
Effects of ADMM paramcters: In this subsection, we demonstrate the effects of the algorithm parameters the convergence of ADMM through two networks: MNIST-A (fully-connected) and MNIST-B (convolutional). Specifically, we focus on the choice and the application of residual balancing.
20

---

Under review as a conference paper at ICLR 2022
20
objertive velue
dbal
Renation
Beration
Iteation
Figure 4: The objective values (left), primal residuals (middle), and dual residuals (right) of ADMM under different augmentation parameters p on the MNIST-A (fully-connected) network.
LC talaniin
peimmal rech stuu
objective
dual
N1. S0l
iteration
iteration
iteration
Figure 5: The objective values (left), primal residuals (middle), and dual residuals (right) of ADMM under different augmentation parameters p the MNIST-B (convolutional) network.
We conduct our experiment on the 1938-th example which is randomly chosen from the MNIST test data set. For this example, both MNIST-A and MNIST-B predicts its class (number 4) correctly. We add an for perturbation of radius c 0.02 to the input image and verify if the network outputs are robust with respect to class number 3. The maximum number of iterations is restricted 3000. The objective values, primal and dual residuals of ADMM for MNIST-A and MNIST-B under different augmentation parameters are plotted in Figure| and 5 respectively. The residual balancing in this experiment. applied with initial p 10.0,
2, and μ 10 as described in Section D.2
The update rule of ADMM suggests that a large value p tends to produce small primal residuals since it puts large penalty the violation of the primal feasibility. However, the dual residuals for such tends to be larger. Conversely, a small tends to reduce the dual residuals at the cost of larger primal residuals. This phenomenon is illustrated empirically with the fully-connected network MNIST-A in Figure and the convolutional network MNIST-B in Figure]
Since ADMM terminates when both the primal and dual residuals are small enough, in practice we prefer to choose the augmentation parameter p not too large or too small in order to balance the reduction in the primal and dual residuals. An effective way to choose a good p is residual balancing, which tries keep the primal and dual residuals close during the ADMM updates by adjusting P online. In both Figure 4 and Figure 5 ADMM with residual balancing is initialized with p= 10.0 and shows significant improvement in convergence rate compared with the case of constant & 10.0. As observed in our other experiments, with residual balancing, ADMM becomes insensitive to the initialization p and usually achieves good convergence rate.
In all of the test accuracy certification results reported in this paper, we initialize p = 1.0 and apply residual balancing when running ADMM. In different experiments, the stopping criterion parameters cabs; frel of ADMM are chosen by trial-and-crror to achieve a balance between the accuracy and the running time of the algorithm. Although ADMM has convergence guarantees for its objective values, primal and dual residuals, may take too many iterations for ADMM to achieve solution of high accuracy (Boyd et al. 2011
21

---

Under review as a conference paper at ICLR 2022
MNISTA
MNISTAA
6000
differnnce
3300
MNIST-B
MNIST-B
30000
140
2300
8300
2330
0.58
0.59
0.52
5.04 3.55
Figure 6: The numbers of certified examples (left column) of ADMM and the lincar-based bounds (Wong et al., 2018: Xu et al. 2020) for the MNIST-A (upper row) and MNIST-B (lower row) nelworks and their differences (right column) for each E (0.01, 0.02, ,0010)),
F.3 IMAGE CLASSIFICATION
In this section, report the details of certified test accuracy of our proposed method (ADMM) and the scalable linear- based bounds on LP relaxations (Linear) (Wong et al. 2018 Xu et al. 2020) in the image classification lasks of MNIST and CIFAR10.
MNIST: For both the fully-connected network MNIST-A and the convolutional network MNIST-B, we apply LP-ADMM with Cabs 10-33 Gre 10-3 as the stopping criterion, and residual balancing with the initial p p= 1.0. For cach classificr network, we go through the 10000 examples in the MNIST test data set and a range of foo perturbation radii count the number of certified examples. To make the counting more efficient, we (i) search over in a descending order since examples that are robust for larger are also robust for a smaller and (ii) only apply ADMM on examples that cannot be verified by Linear (Wong) al. 2018 Xu al., 2020) since Linear (Wong et al., 2018 Xu et al. 2020) gives more relaxed bound than the I.P-relxattion For each batch of test examples, ADMM solves ten
optimization problems of the form 5 with the linear objective function given with respect
to each prediction class.
For a range E (0.01, 0.02. ... 0.10). the numbers of verified examples of ADMM and
Linear (Wong al. 2018 Xu al. 2020 and their differences shown in Figure for MNIST-A and MNIS TTB, respectively. Exact certified accuracy is reported in Table for a range of
CIFAR10: On the CIFAR1O data set, we compare ADMM and Linear (Wong et al. 2018
Xu ct al.] 2020 following the same process
the MNIST data set. The stopping critcrion for LP-DDMM is set as cabs = 10-4, Grel = 10-4 and the range of e set as /2.5/255,1 1.0/255. 4.0/255). The numbers of certified examples of ADMM and Lin-
ear Wong el. al., 2018 Xu el al. 2020 and their differences are shown in Figure 7
Further details for baselines in Table In Table I report the certified accuracy of
solving the LP exactly with ADMM in comparison to a range of baselines. We compare with methods that have previously demonstrated the ability to bound networks of this size: fast
22

---

1.0/255] on Under review as a conference paper at ICLR 2022
CIFRROO
GFAR10
$300
4000
difference
20.0
0.30
0.500
Figure 7: The number of certified examples (left) of ADMM and the linear-based bounds (Wong et al.] 2018 Xu et al. 2020) for the CIFAR10 nelwork and their differ- ences (right) for each {0.5/255, 1.0 20/255, 4.0/255)..
Table 4: Certified accuracy of PGD-trained models on MNIST when using computationally cheap bound (linear-based bounds [Wong et al. 2018 Xu et al. 2020 vs. our method (ADMM)
Certified test accuracy (%)
Model
Epsilon
Linear
ADMM
Diff
MNIST-A
0.02
67.8
77.1
9.3
0.03
7.8
14.2
6.5
MNIST-B
0.07
88.8
91.5
2.7
0.08
74.5
82.2
7.7
0.09
43.0
58.9
15.9
0.10
2.6
8.8
6.2
bounds of the LP (Lincar) (Wong et al. 2018 Xu et al. 2020 and interval bounds (IBP) Gowal el. al. 2018). We additionally compare lo a suile of Lagrangian-based baselines, whose elfectiveness this scale was previously unknown. These methods include supergradient
ascent (Adam) (Bunel et al.) (200b)), dual supergradient ascent (Dual Adam) (Dvijotham ett al. 2018) and variant thereof (Dual Decomp Adam) (Bunel et al. (2220b). and proximal method (Prox) (Bunel et al. (020aa). Lagrangian-base basclines were given the same computational budget as the ADMM solver, with further details Appondix
F.4 REINFORCEMENT LEARNING
We compare the tightness of ADMM and Linear (Wong el al. 2018 Xu el. al. 2020 by verifying the robustness of DQNs on three Atari game benchmarks: BenkHeist, Roadrunner, and Pong The DQNs applied in these experiments
introduced in Appendix F.1
For each benchmark, we collect 10, 000 frames (each with dimension 1 x 84 x 84) across 100 episodes using the natural policy with 100 frames sampled randomly from each episode as the test data set. Note that the imput images to the DQNs are already pro-processod such that the pixel values normalized to [0, 1] with single channel.
In each game, for each frame in the sampled data set, we verify the DQN does not change its actions when loo perturbation of various radii is added to the frame which is the state observation of the agent. The number of actions in BankHeist, Roadrunner and Pong are 6, 4, respectively. Essentially, we reduce the verification of the DQN with finite discrete action space to the same setting as verifying classifiers. Therefore, we apply the same verification process as descried in Appendix F.3 with c E (0.1/255.0.2/255,
Zhang et al. 2020) consider one additional RL setting (Freeway). However, the released PGD-trained DQQ completely unverifiable for nearly all epsilons that considered.
23

---

Under review as a conference paper at ICLR 2022
Bankffeist
Bank
1290
oertiee number
393
6000
atfference
800
60.0
2aks sodis sodis colos calis cado rodis cabs
3aks aalas solis calas calas coloe codis cobo
Readrunner
Boadrunner
400-
Cortiee rumber
aifference
250
100
30-
1926 2920
695n tain sasn sicn 1160
4.00 anin anin sain rain sode sotn 5i66
Pong
Pung
10000
JASPM
3200
3990
4000
6
aain rain
Figure 8: The numbers of certified examples (left column) of ADMM and the linear-based bounds (Wong et al.) 2018 Xu et al., 2020) and their differences (right column) in the verification of DQNs from the BankHeist (first row), Roadrunner (sccond row) and Pong (third row) benchmarks. The range of is given by (0.1/255, 0.2/255, ... 1.0/255).
all three tasks. The numbers of certified examples of ADMM and Linear (Wong et al. 2018 Xu et al. 2020 and their differences on each task are plotted Figure
G ADDITIONAL DETAILS ON COMPARISON TO LAGRANGIAN-BASED METHODS
In Section 4.1 we compared the certified test accuracy of ADMM with suite of Lagrangian- based methods (Bunel al.) (2020ab on CIFAR10. These Lagrangian- barsang based baselines were implemented using the codes at
com hoalooollllga http:///w...oo/o/aaooooooaoooaa.
under the MIT license. As mentioned in Section 3.2 these baselines require solving inner optimization problem through iterative algorithms. In the experiments of Table [ the number of iterations of different iterative algorithms are bounded separately such that each Lagrangian-
based based method listed in Section 4.1 has runtime of 9 seconds to finish verifying one example.
24

---

Under review as a conference paper at ICLR 2022
Our ADMM solver averages 9 seconds runtime per example in this verification task, which the same as the average runtime of the Lagrangian-base methods, with the stopping criterion of Eabs 10 Grel 10 and p 1.0.
Architecture size. We note that the architecture verify in this paper is 10x larger than considered by (Bunel et al. 2020b). However, the released framework could not handle this model size due to their implementation of intermediate bounds. In order to handle this model size, we externally calculated the intermediate bounds (using (Wong et al., 2018) and loaded these into the framework for the Lagrangian-based baselines.
H SPEED COMPARISON
Comparison with LP solver: To demonstrate the effectiveness of GPU-acceleration in the DeepSplit algorithm, we compare the runtime of DeepSplit and Gurobi in solving LP relaxations that bound the output range of MNIST-A network (the fully connected network defined in Appendix F.1p with foo perturbations in the input. Specifically, for given example in the MNIST test data set, we apply DecpSplit Gurobi layer-by-layee to find the tightest pre-activation bounds under the LP-relaxation.
Recall that the MNIST-A A network is fully-connected netowrk with architecture 784 184-600 400 - 200 100 10. With the Gurobi solver, need to solve 2 x 600 LPs sequentially to obtain the lower and upper bounds for the first activation layer, 2 x 400 LPs for the second activation layer, and forth. With DeepSplit, the pre-activation bounds can be computed in batch and allows GPU-acceleration.
In our experiment, we fix the radius of the lo perturbation at the input image as 0.02. For the Gurobi solver, we randomly choose 10 samples from the test data set and compute the pro-activation bounds solved by Gurobi v9.1 on an Intel Core 17-6700K CPU, which has 4 cores and 8 threads. For each example, the total solver time of Gurobi is recorded with the average solver time being 275.9 seconds. For the DeepSplit. method, we compute the pre-activation bounds layer-by-layer on 19 randomly chosen examples. The algorithm applies residual balancing with the initial 1.0 and the stopping criterion is given by 6abs 10-4, -1e_,, 10-3 The total running time of DeepSplit is 717.9 seconds, with 37.8 seconds per example on average. With the GPU-acccleration, out method achieves 7x speedup in verifying NN properties compared with the commercial-grade Gurobi solver.
by-layer.. The LP relaxation is formulated in CVXPY and
Comparison with SDP solver: Our method is significantly faster than solving the convex relaxation through other approaches. For example, it took our method approximately 20 hours to verify all MNIST test set images for the convolutional architecture at 10 different epsilon values (See Table 3). taking on average 2 hours per epsilon to verify all 10,000 examples. See F.2 for the running time summary of each experiment. In contrast, the SDP relaxation (Raghunathan et al., 2018) takes 3 hours to verify 500 examples at one epsilon value for similarly sized CNN. This highlights the difference in speed and scalability of solving the LP relaxation over the SDP one, albeit at the cost of looser verification guarantees.
Comparison with branch-and-bound solver: Branch-and-bound methods have expo- nential runtime as opposed to the polynomial runtime LP-solvers. In practice, this leads to significantly longer solve times that has largely limited these methods to the small network regime. For example, the fastest branch-and-bomee average 6 minutes per example to verify small convolutional network, whereas our solver takes on average seconds per example (40x faster) to verify an order-of offerr----aanttude larger network.
mothod from Bunel et al. (2020a) takes
25

---

Under review as a conference paper at ICLR 2022
ADHIN Lintss ba
JCHS
LS3% Uts
-100
200
140
bound Index
bound index
Figure 9: ResNet18 output lower (left) and upper (right) bounds obtained using either ADMM (blue dots) and LiRPA (orange triangles) from the first 100 CTFAR10 test examples. Higher lower bounds and lower upper bounds are better. For ease of visualization, bounds are sorted in ascending order according to the ADMM bound.
Table 5: Comparison of computed bounds using LiRPA Xu et al. (ADMM) on a ResNet18 for CIFARIO.
2020 vs. our method
Linear
ADMM
Diff
Upper bounds
39.87 + 66.42
38.02 + 62.21
2.32% + 2.35%
Lower bounds
0.04 + 17.02
4.76 + 7.56
31.61% + 43.38%
I SCALABILITY
To highlight the scalability of our approach, we consider a ResNet18 network trained on CIFAR10 whose max pooling laver is replaced by down-sampling convolutional layer for comparison with LiRPA (Xu et al. 2020 (codes available at
under the BSD 3-Clause "New" or "Revised" license), which is capable of computing provable linear bounds for the outputs of general neural networks and is the only method available so far that can handle ResNet18. The ResNet18 is adversarially trained using the fast adversarial training code from (Wong al. 2020).
In our experiments, for the first 100 examples CIFAR1O, we use LiRPA to compute the preactivation bounds for each ReLU layer in ResNet18 and then apply ADMM to compute the lower and upper bounds ResNet18 outputs (there are 10 outputs corresponding 10 classes of the dataset). The ADMM run with stopping criterion Eabs 10 Erel 10 and augmentation parameter = 1.0. With c 1/255, the lower /upeer bounds of ADMM from these 100 examples arranged in ascending order in Figure 9 and are compared with those obtained by LiRPA. We observe that the bounds from ADMM are consistently lighter than those from LiRPA. The average running time of ADMM across the 100 examples
the
is 2312 seconds. Overall bound statistics are shown in Table 5
4The max pooling layer has not been considered in the implementation of LiRPA by the submission of this paper.
26


Reviews:
[{"review_id": "vOYP_K0beJm", "reviewer": "Reviewer_ZCXL", "summary": "", "questions": "", "limitations": "", "rating": 5, "confidence": 3, "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": "While this paper is well-written and has proposed quite an interesting idea to improve the scalability of the neural network verification problem, the idea of applying operator or variable splitting to neural networks is definitely not novel, although neural network training and verification might be differet tasks. However, due to their highly similar problem formulations, I woule expect the authors to discuss the similarities and difference between the proposed method and such related papers, e.g., Taylor et al. (2016), Cui et al. (2019), Zeng et al. (2019, 2021). I would raise my score if the authors can explain the above in their response and include such details in the revision of the paper. \n\n---\nCui, Y., He, Z., & Pang, J. S. (2020). MultiComposite nonconvex optimization for training deep neural networks. SIAM Journal on Optimization, 30(2), 1693--1723. \n\nZeng, J., Lau, T. T. K., Lin, S., & Yao, Y. (2019). Global convergence of block coordinate descent in deep learning. In ICML. \n\nZeng, J., Lin, S. B., Yao, Y., & Zhou, D. X. (2021). On ADMM in deep learning: Convergence and saturation-avoidance. Journal of Machine Learning Research, 22(199), 1--67.\n", "summary_of_the_paper": "This paper proposes an operator splitting method which solves a convex relaxation of a learge-scale nonconvex optimization problem for analyzing the worst-case performance of deep neural networks against input perturbations. The proposed method is modular, scalable and parallelizable. Experimentally, the authors demonstrate that the proposed method has tighter bounds on the worst-case performance of large CNNs in image classification and RL settings. ", "summary_of_the_review": "This paper has proposed an interesting idea (i.e., operator splitting) to improve the scalability of neural network verification, but this idea is not novel for its applications to neural networks (e.g., neural network training). The paper will better position itself if more detailed comparisons are made with such methods in the existing literature. ", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "3: Some of the paper’s claims have minor issues. A few statements are not well-supported, or require small changes to be made correct.", "technical_novelty_and_significance": "2: The contributions are only marginally significant or novel.", "empirical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work."}, "extra_text": {}}, {"review_id": "KMivMNnCSw1", "reviewer": "Reviewer_aJXo", "summary": "", "questions": "", "limitations": "", "rating": 3, "confidence": 5, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "---- Pros ----\n\nAs implied in section 3, DeepSplit is an improvement on two closely-related dual solvers for the same relaxation (the convex hull of element-wise activation functions):\n- (Dvijotham et al. 2018) presented a dual solver based on the Lagrangian relaxation of problem (3), which converges to the same bounds as DeepSplit, with a rate of O(1/sqrt(T)).\n- (Bunel et al. 2020a) first employed variable splitting and an Augmented Lagrangian on the same relaxation, improving upon the dual solver from (Dvijotham et al. 2018). While the Augmented Lagrangian is differentiable, the inner problems require the use of an iterative optimisation algorithm.\n- DeepSplit adds a second variable split to the formulation from (Bunel et al. 2020a) so that the inner problems enjoy a closed-form solution. This results in faster empirical convergence, and attains the O(1/T) rate.\n\nSuggestion: perhaps inverting the ordering of sections 3 and 2 could improve the paper's readability.\n\n---- Cons ----\n\nThe paper repeatedly claims that DeepSplit solves the considered relaxation *exactly*, seemingly contrasting this with other approaches. However, the methods from (Dvijotham et al. 2018) and (Bunel et al. 2020a) enjoy the same property, the only difference being a slower empirical convergence rate. As a consequence, I believe the authors should tone down claims such as that they compute bounds for \"networks whose convex relaxations were previously impossible to solve exactly due to their size\".\n\nFurthermore, in neural network verification, one is typically concerned with verifying the largest number of properties in the smallest possible time, rather than solving a given relaxation exactly. Suboptimal yet inexpensive bounds are then potentially preferable to solving a given relaxation to optimality, especially considering that running a fixed small number of branch and bound steps will significantly tighten the bounds (see for instance (Wang et al. 2021)). In other words, methods based on branch and bound can be employed as incomplete verifiers, if they are terminated early. The cost of running recent branch-and-bound methods to termination is nevertheless significantly smaller than what the authors claim: BaDNB from (De Palma et al. 2021) verifies a large number of properties in under 10s for a network of 50k activations. Similar (or better) results were obtained by the participants of VNN COMP 2020, or VNN COMP 2021. I believe this is in the same order of magnitude as the network size employed for Table 1, for which the reported runtime of DeepSplit (in the appendix) is around 10s as well.\n\nIn addition, recent works such as (Xu et al. 2021), and [Bunel et al. non-convex 2020] have shown that non-convex reformulations (lacking convergence guarantees to the exact solution of the relaxation, for ReLUs) obtain significantly better speed-accuracy trade-offs (on the same relaxation) than (Dvijotham et al. 2018) and (Bunel et al. 2020a). These newer works seemingly scale quite well with network sizes: I hence doubt that the only applicable method to a ResNet18 is non-optimized LiRPA, as claimed by the authors.\n\nI am willing to significantly increase my score if the authors address the following points:\n- Table 1 should report the average runtime in addition to the certified test accuracy. Preferably, different speed-accuracy trade-offs should be reported for iterative algorithms.\n- The certified accuracy for \"Dual Decomp Adam\" should not be lower than the one for \"Linear\", as the latter can be used an initializer to the dual problem in (Bunel et al. 2020a). Are the authors taking this into account? Could DeepSplit enjoy the same initialization?\n- Compare against the more recent bounding algorithms from [Bunel et al. non-convex 2020] and (Xu et al. 2021). While introduced in the context of branch and bound, the \"alpha-CROWN\" method, or LiRPA with optimized slopes, is a valid incomplete verifier, and the global optimum of its optimization problem coincides with DeepSplit's. Furthermore, it might yield tigther bounds than DeepSplit in case of joint optimization over intermediate bounds. The code of both algorithms is available online.\n- Compare speed-accuracy trade-offs against works operating on tighter relaxations, such as [Active Set].\n- Considering that the memory footprint of alpha-CROWN with fixed intermediate bounds is only marginally larger than the one for LiRPA, the authors should add this to the ResNet18 experiments.\n- Complete verification performance is tightly linked to the quality of the speed-accuracy trade-offs of an incomplete verifier. It would be quite informative if the authors could provide complete verification experiments on the model from Table 1.\n\n---- Minor comments ----\n- End of page 1 \"these relaxations must typically be further relaxed\": this statement does not apply to (Dvijotham et al. 2018) and (Bunel et al. 2020a)\n- section 1.1, typo in reference, \"de2\"\n- Sec 3.2 \"When stopping early, the primal minimization must be solved to convergence in order to compute the dual function and produce a valid bound.\": this is incorrect, as a valid bound can be obtained in closed-form by minimising the Lagrangian, rather than Augmented Lagrangian.\n\nReferences:\n[Bunel et al. non-convex 2020] - An efficient nonconvex reformulation of stagewise convex optimization problems, NeurIPS 2020\n[Active Set] - Scaling the Convex Barrier with Active Sets, ICLR 2021", "summary_of_the_paper": "The authors present DeepSplit, a novel solver for a popular neural network convex relaxation. Relying on ADMM and on a careful problem re-formulation, the authors achieve both a O(1/T) converge rate and closed-form solutions for the inner problems, differently from previously presented solvers for the same relaxation. Computational results are presented for incomplete neural network verification, showing that DeeSplit scales to a ResNet18 and achieves better bounds in the same time compared to relevant baselines.", "summary_of_the_review": "DeepSplit is an improvement upon two closely-related solvers for the same convex relaxation: (Dvijotham et al. 2018) and (Bunel et al. 2020a).  The work focuses on solving the relaxation exactly. However, as shown in a variety of recent papers (Xu et al. 2021), [Active Set],  [Bunel et al. non-convex 2020], (Wang et al. 2021), heuristics and switching to tighter relaxations (possibly considering branching) might verify more properties in the same time (both in incomplete and complete verification). These developments have been somewhat ignored by the authors.\n\nThe authors should put their work in perspective with more recent and scalable optimizers for the same relaxation: (Xu et al. 2021), [Bunel et al. non-convex 2020]; and with works on tighter relaxations [Active Set]. Furthermore, as commonly done for solvers of the considered relaxation, complete verification experiments are needed to fully assess the quality of DeepSplit's speed-accuracy trade-offs.", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "2: Several of the paper’s claims are incorrect or not well-supported.", "technical_novelty_and_significance": "2: The contributions are only marginally significant or novel.", "empirical_novelty_and_significance": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}, {"review_id": "DZEJrmcFuWd", "reviewer": "Reviewer_LjMA", "summary": "", "questions": "", "limitations": "", "rating": 3, "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": "Strengths\n1. The method uses variable splitting and Lagrangian relaxation which have been used in previous verification works. However, the proposed variable splitting is novel as it allows closed-form updates for the primal variables. Thus enjoying faster convergence than Bunel et al. 2020a. \n\n2. The authors have done a good job at discussing the differences with previous related works like Dvijotham et al. and Bunel et al. in section 3.\n\nConcerns\n1. Incomplete verification experiments not thorough:\n* Are the different methods using the same intermediate bounds? I found in the supplementary that you computed intermediate bounds for Bunel et al, using KW. How are intermediate bounds computed for your method?\n* The table and details are not very clear. Do the different rows correspond to the same network tested with different epsilon values?\n\n2. Missing baselines in incomplete verification experiments:\n* The paper is using weaker baselines. The authors should compare with [A] (which is a published work at ICLR21). They use a tighter relaxation (Tjandraatmadja et al., 2020) and solve it using a Lagrangian relaxation and active set based approach. Furthermore, they are outperforming solvers from Bunel et al. 2020 which has been used as a baseline in this paper.\n* This also brings into question the relevance of this work. Because [A] outperforms Bunel et al. 2020. Can your method be extended to the relaxation from Tjandraatmadja et al., 2020? It is not clear that this work can outperform [A] or work with tighter relaxations. \n* The authors should also compare with Fast-and-complete (Xu et al., 2021), Beta-CROWN(Wang et al. 2021) as they use the same LP relaxation as this paper, and are very effective. This should be done in both Table 1 and the scalability section, as these methods can scale to such networks.\n\n3. Missing complete verification experiments:\n* Complete verification experiments are missing. This has been done in works that have been used by the authors as a baseline (Bunel et al. 2020). Even the recent propagation-based solvers provide results on complete verification (see Xu et al., 2021 and Wang et al. 2021). \n* They are quite important to judge the practical relevance of the algorithm. Branch-and-bound takes memory, speed and accuracy all into account, thus is crucial to see the relevance of the work.\n* See VNN-comp [B] for recent developments in this space. The authors should use a branch-and-bound framework from the open-sourced codes from VNN-comp and plug DeepSplit into them.\n* You should also add these b&b baselines in the speed-comparison experiment. b&b solvers can be used as incomplete verifiers, and that should be possible here since the network size is small.\n\n4. Scalability experiments representation:\n* Can you provide verified accuracy here? This will help in checking if the method can in fact verify this size networks or if the bounds are too large to be relevant.\n\n5. Overclaiming\n* 'focus on networks whose convex relaxations were previously impossible to solve exactly due to their size.' in Introduction seems to be an overclaim, since LirPA seems to be not doing that bad. And LirPA is not even the state-of-the-art baseline. Is this statement corresponding to experiments in Table 1 or the scalability experiment?\n\nI am willing to update my rating depending on the authors' response to these concerns.\n\n[A] Scaling the Convex Barrier with Active Sets Alessandro De Palma, Harkirat Behl, Rudy R Bunel, Philip Torr, M. Pawan Kumar, ICLR 2021\n\n[B] https://sites.google.com/view/vnn20/vnncomp", "summary_of_the_paper": "The paper proposes a novel method for the neural network verification problem. The authors use variable splitting and Lagrangian relaxation to relax the verification problem, which is then solved with ADMM. The method is GPU friendly (similar to previous work like Dvijotham et al. 2018 and Bunel et al. 2020a), and claims to solve the relaxation to optimality.", "summary_of_the_review": "The authors have proposed a novel method for the neural network verification problem. It is better than Bunel et al 2020. However, authors have not compared against recent state-of-the-art published baselines. Also, complete verification experiments are missing.", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "3: Some of the paper’s claims have minor issues. A few statements are not well-supported, or require small changes to be made correct.", "technical_novelty_and_significance": "2: The contributions are only marginally significant or novel.", "empirical_novelty_and_significance": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}, {"review_id": "C8TUrdt2Kt", "reviewer": "Reviewer_Km1h", "summary": "", "questions": "", "limitations": "", "rating": 5, "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": "This paper proposes an operator splitting method (i.e. ADMM) to deal with neural network verification problems. This is because the ADMM is scalable to large datasets. Specifically, they solve the convex relaxations of problems analytically. Extensive experiments on network verifications demonstrate outstanding performance as well as excellent scalability.  This paper has several limitations, which are discussed as follows:\n1.\tSome statements in the paper are unclear. For example, in the introduction, the authors state that neural networks lack formal guarantees. However, the meaning of formal guarantees is unclear, and how does it relate to safety-critical applications should be explained better. As another example,  the background of the neural network verification problem is missing. It is unclear what are potential applications of this problem, and examples should be provided to better understand required properties.  \n2.\tThe novelty of this paper should be justified better. The authors just utilize an existing optimization framework ADMM to relax nonconvex problems into convex ones, which lead to analytic solutions. As they mentioned, several papers consider similar ideas, but the difference seems subtle. it is unclear how ADMM resolves the incomplete problem (i.e. methods are guaranteed to detect all false negatives but also produce false positives). Moreover, the ADMM usually converges slowly to the solution, how do authors address this issue?\n3.\tExperimental details are missing.  Even though the authors show many experimental results,  the background of problems in the experiments is missing, and little information such as architectures and hyperparameter settings is provided.  So it is difficult to reproducible experimental results.\n", "summary_of_the_paper": "This paper proposes ADMM for neural network verification problems. Experiments are demonstrated to show its effectiveness and scalability.", "summary_of_the_review": " This paper addresses an important problem. However, the unclear presentation, the lack of novelty justification, and missing experimental details should be improved to make it an acceptable paper in ICLR.", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "3: Some of the paper’s claims have minor issues. A few statements are not well-supported, or require small changes to be made correct.", "technical_novelty_and_significance": "2: The contributions are only marginally significant or novel.", "empirical_novelty_and_significance": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}, {"review_id": "4rk6FL4RTw5", "reviewer": "Reviewer_JVyx", "summary": "", "questions": "", "limitations": "", "rating": 8, "confidence": 5, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "# Strengths\n* The paper is very clearly written, with a clear narrative explaining how the algorithm is derived (Equation 3 to 13) with a helpful summary in Algorithm 1 on how things tie together. The appendix is very detailed and provide clear explanations for how to implement each component of the algorithm efficiently.\n* The contribution is clearly framed with regards to previous work. The Introduction and Related work are a good summary of the current state of neural network verification, and Section 3 does a great job at highlighting the differences between the proposed methods and the most closely related published work, highlighting why this results in significant improvements.\n* The significance of the contribution is also quite important. The authors give convergence guarantees and show good convergence empirically with the optimization curves in the appendix, which previous methods could not offer. They even show that this results in improved certified accuracy (for a given time budget),\n* The evaluation is done quite rigorously, on several domains (Vision / RL) and at different scales (comparison to Gurobi on small models, evaluation against related methods on Cifar10 network of a standard size, and evaluation of scalability against fast linear bound on ResNet models).\n\n# Weaknesses\nA potential improvement that this paper could benefit from is a comparison to methods such as the OptimizedLirpa bounds from the Fast and Complete paper, which the authors cite. This would not need to include comparison to the branch and bound aspect of it, but simply to the bound computation, which rely on fast linear bounds, but iteratively optimizes the slope of the relaxation. This is equivalent to solving the same problem and has been empirically shown to be quite efficient. \nA comparison of the tightness / speed tradeoff that would result would be extremely useful. (The method described in this paper are valuable even if they are slower, as they provide convergence guarantees, which OptimizedLirpa bounds do not.)", "summary_of_the_paper": "This paper proposes an efficient solver for computing the convex relaxation of Neural Networks, which is an important component of verification methods. The method is based on ADMM, with the authors proposing a novel decomposition of the optimization problem, which allows them to get closed form solutions of all the intermediate steps of the algorithm, The proposed method also improves on the guaranteed convergence rate and is shown to scale to larger networks than the ones considered in other works.\n\nEvaluation is performed on robustness verification on Cifar10 and on Reinforcement learning models.", "summary_of_the_review": "Very well written paper, with interesting and significant contributions, and which provide a great summary of the state of the field.", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "4: All of the claims and statements are well-supported and correct.", "technical_novelty_and_significance": "4: The contributions are significant, and do not exist in prior works.", "empirical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work."}, "extra_text": {}}]

Author rebuttal:

Meta-review: The authors propose a novel operator splitting method for solving convex relaxations of neural network verification problems, and develop and validate an optimized implementation of the same on large scale networks, focusing on the problem of verifying robustness to norm bounded adversarial perturbations.

The reviewers agree that the paper contains interesting ideas that are worthy of further development and that these ideas may prove useful eventually in pushing the envelope of what is possible in neural network verification. However, in its current form, the paper misses some key experimental evidence to rigorously evaluate the value of the contributions made:
1) Comparison against SOTA incomplete verifiers: The authors do not provide detailed and rigorous comparisons against well-known baselines (for example the incomplete verifiers from Fast-and-complete (Xu et al., 2021), Beta-CROWN(Wang et al. 2021)) 
2) Incorporating tighter relaxations: It would be valuable for the community to understand whether the proposed algorithm is compatible with tighter relaxations like those of (Tjandraatmadja et al., 2020). Even if they are not, it would be interesting to understand the comparison against standard solvers for these tighter relaxations compared against the advanced solver developed by the authors applied to the weaker relaxation.
3) Showing performance in the context of complete verification: While this is not a requirement, it would be great to see how the method performs in the conjunction with a branch and bound search, as this sometimes reveals surprising tradeoffs or weaknesses of incomplete verifiers (as observed in the results of Beta-CROWN(Wang et al. 2021)).

I encourage the authors to strengthen the paper adding these experiments and resubmit to a future venue.
Decision: Reject