Year: 2019

Abstract:
Neural networks are known to be sensitive to adversarial perturbations. To investigate this undesired behavior we consider the problem of computing the distance to the decision boundary (DtDB) from a given sample for a deep neural net classifier. In this work we present an iterative procedure where in each step we solve a convex quadratic programming (QP) task. Solving the single initial QP already results in a lower bound on the DtDB and can be used as a robustness certificate of the classifier around a given sample. In contrast to currently known approaches our method also provides upper bounds used as a measure of quality for the certificate. We show that our approach provides better or competitive results in comparison with a wide range of existing techniques.

heading: 1 INTRODUTION
text: The high predictive power of neural network classifiers makes them the method of choice to tackle challenging classification problems in many areas. However, questions regarding the robustness of their performance under slight input perturbations still remain open, severely limiting the applicability of deep neural net classifiers to sensitive tasks that require certification of the obtained results.
In recent years this issue gained a lot of attention, resulting in a large variety of methods tackling tasks ranging from adversarial attacks and defenses against these to robustness verification and robust training. In this work we focus on robustness verification of deep classifiers. That is, computing the distance from a given anchor point x0 in the input space to its closest adversarial, i.e. a point that is assigned a different class label by the network. This problem plays a fundamental role in understanding the behavior of deep classifiers and essentially provides the only reliable way to assess classifier robustness. Unfortunately, its complexity class does not allow a polynomial time algorithm. For deep classifiers with ReLU activation the verification problem can equivalently be reformulated as a mixed integer programming (MIP) task and was shown to be NP-complete by Katz et al. (2017). Even worse, Weng et al. (2018) showed that an approximation of the minimum adversarial perturbation of a certain (high) quality cannot be found within polynomial time.
Related work There exist three streams of related work on robustness verification of deep ReLU classifiers. This categorization is based on whether they are solving the verification problem exactly or verifying a bound on the distance to the decision boundary (DtDB).
The first group of methods are exact verification approaches. As mentioned above, the verification task can be modeled using MIP techniques. Katz et al. (2017) present a modification of the simplex algorithm that can be used to solve the verification task exactly for smaller ReLU networks based on satisfiable modulo theory (SMT). Other approaches (see Ehlers (2017)) rely on SMT solvers when solving the described task. Bunel et al. (2018) provide an overview and comparison of those. Other exact methods (Dutta et al. (2018); Lomuscio and Maganti (2017); Tjeng et al. (2017)) deploy MIP solvers together with presolving to find a tight formulation of the MIP problem or (Jordan et al. (2018)) use an algorithm to find the largest ball around the anchor point that touches the decision boundary.
The second popular class of methods for verifying classifier robustness deals with verification of an -neighborhood: given an anchor point x0 and an > 0, the task is to verify whether an adversarial point exists within the neighborhood of x0 which is defined with respect to a certain norm in the
input space. All existing methods relax the initial problem and require bounds on activation inputs in each layer. These bounds should be as tight as possible to ensure good final results. Raghunathan et al. (2018a;b); Dvijotham et al. (2018; 2019) consider semidefinite (SDP) and linear (LP) problems as relaxations of the -verification problem. Wong and Kolter (2018) replace ReLU constraints by linear constraints and consider the dual formulation of the obtained LP relaxation. Weng et al. (2018) present an approach that also uses linear functions (later extended to quadratic functions by Zhang et al. (2018)) to deal with nonlinear activation functions and propagate the layer-wise output bounds until the final layer. Finally Hein and Andriushchenko (2017); Tsuzuku et al. (2018) use the Lipschitz constant of the transformations within classifier’s architecture.
Our approach belongs to the third group of approaches dealing with constructing lower bounds on DtDB without restricting admissible adversarial points to a given neighborhood. The -verification task is closely related to the problem of constructing lower bounds on DtDB: each -neighborhood that can be certified as adversarial-free immediately provides a lower bound on the minimal adversarial perturbation magnitude. It is also a common strategy for the methods from the previous group to use a binary search or a Newton method on top of their algorithm to find the largest such that the -neighborhood around x0 can still be verified as robust. Croce et al. (2019) leverage the piecewise affine nature of the outputs of a ReLU classifier and compute lower bounds on DtDB by assuming that the classifier behaves globally the same way it does in the linear region around the given anchor point.
Adversarial attacks Constructing misclassified examples that are close to the anchor point can be considered as a complementary research direction to robustness verification since each adversarial example by definition provides an upper bound on the DtDB. Many methods were proposed to construct such points (Szegedy et al. (2014); Goodfellow et al. (2015); Kurakin et al. (2016); Papernot et al. (2016); Madry et al. (2017); Carlini and Wagner (2017).
Robust training The question of how to actually train a robust classifier is closely related to robustness verification since the latter might allow us to construct some type of robust loss based on the insights from the verification procedure (see Hein and Andriushchenko (2017); Madry et al. (2017); Wong and Kolter (2018); Raghunathan et al. (2018a); Tsuzuku et al. (2018); Wang et al. (2018); Croce et al. (2019)). We leave this direction for future work.
Contributions
1. We propose a novel relaxation of the DtDB problem in form of a QP task allowing efficient computation of high quality lower bounds on the DtDB in l2-norm with an extension to l∞-norm. For networks with up to two hidden layers we reach state-of-the-art performance with an improvement of over 50% when compared to the bounds obtained from methods based on LP relaxations (CROWN by Zhang et al. (2018) and ConvAdv by Wong and Kolter (2018)). Furthermore, our method performs much faster than methods based on SDP relaxations (Raghunathan et al., 2018b), while providing smaller lower bounds. This is a fundamental property due to the difference in computational complexity between SDP and QP tasks.
2. Unlike -verification techniques, we provide a lower bound on DtDB without an initial guess and without computing bounds for the neuron activation values in each layer. Such bounds have to be tight enough to verify non-trivial neighborhoods and play an important role in other relaxation techniques such as the SDP based approaches by Raghunathan et al. (2018b); Dvijotham et al. (2019).
3. In addition to computing the lower bounds after solving a single QP, our approach allows to construct adversarial examples by repeatedly choosing a new anchor on the boundary of the verified region and solving its associated QP. One of the main limitations of competing inexact approaches is the fact that the situation around the given anchor point outside of the certified radius remains unclear. Since these approaches rely on relaxations of the initial problem, failed certification does not indicate the presence of an adversarial example. Instead, when using these methods, one must rely on externally constructed adversarial examples to obtain an upper bound. We present a bi-directional robustness verification technique that uses the verification mechanism itself to construct upper bounds and assess the quality of the lower bounds.

heading: 2 NOTATION AND IDEA
text: We consider a neural network consisting of L linear transformations representing dense, convolutional, skip or average pooling layers and L− 1 ReLU activations (no activation after the last hidden layer). The number of neurons in layer l is denoted as nl for l = 0, . . . , L, meaning that the data has n0 features and nL classes. Furthermore, we present our analysis for the l2-norm as perturbation magnitude measure since only few available methods are applicable to this setting. To make our method comparable with Raghunathan et al. (2018b) a generalization to l∞-perturbations is addressed in Appendix A.
Given sample x0 ∈ Rn0 , weight matrices W l ∈ Rnl×nl−1 , and bias vectors bl ∈ Rnl , we define the output of the i-th neuron in the l-th layer after the ReLU activation as
xli = [ W lix l−1 + bli ] + and (1)
fi(x 0) = xLi = W L i x L−1 + bLi
where [x]+ is the positive part of x and f(x 0) = xL denotes the output of the complete forward pass through the network. We start with the observation that the ReLU activation function acts as one of two linear functions depending on its input’s sign. That allows us to reformulate it (see Section 3.1) and obtain an optimization problem with so called linear complementarity constraints (also used by Raghunathan et al. (2018b); Dvijotham et al. (2019) for -verification). Note that for each pair of scalars a and b the following holds.
b = [a]+ ⇐⇒ b ≥ 0, b− a ≥ 0, b(b− a) = 0 (2)

heading: 3 OPTIMIZATION PROBLEM

heading: 3.1 FORMULATION OF DTDB
text: For a given sample x̃0, pre-trained neural net f , predicted label ỹ and target label y we aim to find the closest point to x̃0 in Rn0 that has a larger or equal probability of being classified as y compared to the initial label. This can be done by solving the following optimization problem.
min x0∈Rn0
‖x0 − x̃0‖2, s.t. (eỹ − ey)T f(x0) ≤ 0, (DtDB)
where ei is the i-th unit vector in RnL and ‖x‖ denotes the Euclidean norm of x. Note that we explore the boundary between classes y and ỹ around x̃0. To compute the distance from x̃0 to the (full) decision boundary, one needs t compute the solution for all target labels y = 1, . . . , nL except ỹ.
We can “unfold” the above optimization problem using (1), where x denotes a container with all variables x0, . . . , xL.
min x∈Rn
‖x0 − x̃0‖2, s.t. (eỹ − ey)TxL ≤ 0, xL = WLxL−1 + bL
xl = ReLU(W lxl−1 + bl) for l = 1, . . . , L− 1
We apply (2) to reformulate the problem and eliminate xL, such that from now on x contains only the remaining variables x0, . . . , xL−1 and n = n0 + . . .+ nL−1.
min x∈Rn
‖x0 − x̃0‖2, s.t. (eỹ − ey)T ( WLxL−1 + bL ) ≤ 0 (DtDB)
( xl )T ( xl − ( W lxl−1 + bl )) = 0 for l = 1, . . . , L− 1 (3) xl − ( W lxl−1 + bl ) ≥ 0, xl ≥ 0 for l = 1, . . . , L− 1 (4)

heading: 3.2 QP RELAXATION
text: Next we consider a Lagrangian relaxation of DtDB without constraints (3). We will refer to the resulting problem as QPRel(λ), when the explicit dependency on the multipliers is required.
min x∈Rn ‖x0 − x̃0‖2 +
L−1∑
l=1
λl ( xl )T ( xl − ( W lxl−1 + bl )) , s.t. (QPRel)
(eỹ − ey)T ( WLxL−1 + bL ) ≤ 0 (5) xl − ( W lxl−1 + bl ) ≥ 0, xl ≥ 0 for l = 1, . . . , L− 1 (6)
The obtained problem is indeed a QP with linear constraints. We need to clarify two questions. How does the problem QPRel help us with solving DtDB and how can this problem itself be solved efficiently?
QPRel vs. DtDB First, we describe properties of the solution of QPRel providing information about DtDB. To do so, we define for arbitrary vectors x0 ∈ Rn0 , . . . , xL−1 ∈ RnL−1 and λ ∈ RL−1+
c(x, λ) :=
L−1∑
l=1
λl ( xl )T ( xl − ( W lxl−1 + bl )) (7)
as the corresponding propagation gap. It follows directly from the definition that for arbitrary non-negative λ it holds that:
• if x is feasible for DtDB we have c(x, λ) = 0, meaning that x equals the vector obtained by propagating x0 through the neural net as defined in (1), • if x is feasible for QPRel we have c(x, λ) ≥ 0, meaning that there might be a slack between
the true output of layer l when getting x0 as an input and the value of xl obtained by QPRel.
In general the following holds for the relation between the solution of QPRel and DtDB (see also Figure 1, every point in the hatched area is certified to be classified as belonging to the class ỹ). Lemma 1. Denote the solution of QPRel by xqp and the square root of its optimal objective value by dqp, let d be the square root of the optimal objective value of DtDB. The following holds:
1. dqp ≤ d and when c(xqp, λ) = 0 we have dqp = d and xqp is optimal for DtDB.
2. For two non-negative λ1, λ2 with λ1 ≤ λ2 elementwise it holds that dqp(λ1) ≤ dqp(λ2).
The first result from Lemma 1 ensures that dqp provides a radius of a certified neighborhood around the anchor point. Whereas the second part indicates that we should choose λ as large as possible to get our lower bound closer to DtDB. Unfortunately, as we show below, the problem QPRel becomes non-convex for large values of λ. While one could try to tackle a non-convex QP with proper optimization methods, we will address necessary conditions such that QPRel is guaranteed to be convex and can be solved efficiently next.
Convexity of QPRel To look into the problem QPRel in more detail we introduce the Hessian Mλ (which is a constant matrix) of its objective function.
Definition 1. Let El ∈ Rnl×nl be the identity matrix of the corresponding dimension. We define Mλ ∈ Rn×n as the following symmetric block tridiagonal matrix
Mλ :=   D0 M T 1 M1 D1 M T 2
M2 . . . . . . . . . DL−1
  with Ml := − 1 2 λlW l, Dl := λlEl and λ0 := 1.
Using this matrix we can rewrite the objective function from QPRel as (see Appendix C, Lemma 2):
min x∈Rn
xTMλx+ xT b̄(λ, x̃0) + c̄(x̃0), s.t. (5), (6)
where b̄ and c̄ influence only the linear and constant terms and are therefore not relevant in this section. From this reformulation we can clearly see that the matrix Mλ determines the (non-)convexity of the objective function. The following theorem provides sufficient and necessary conditions on λ depending on the weights Wl assuring that Mλ is positive semi-definite. This allows us to use off-the-shelf QP-solvers with excellent convergence properties. Theorem 1. Let W 1, . . . ,WL−1 be the weights of an arbitrary pre-trained neural net and ‖W‖ the spectral norm of an arbitrary matrix. Then the following two conditions for λ provide correspondingly a sufficient and a necessary criterion for the matrix Mλ to be positive semi-definite.
(suf. condition) λ1 ≤ 2λ0 ‖W 1‖2 and λl ≤ λl−1 ‖W l‖2 for l = 2, . . . , L− 1 (8)
(nec. condition) λl ≤ 4λl−1 ‖W l‖2 for l = 1, . . . , L− 1 (9)
Furthermore, we define ¯ λ and λ̄ that correspondingly satisfy conditions (8) and (9) with equality:
¯ λl = 2
l∏
k=1
1
‖W k‖2 , λ̄l = 4 l
l∏
k=1
1
‖W k‖2 .
In case with a single hidden layer choosing λ = λ̄ from (9) guarantees Mλ to be positive-semi definite.
We use (8), (9) and our previous results as guidelines for the choice of λ. Since QPRel(λ) is monotonous in the sense of Lemma 1 we perform a binary search between
¯ λ and λ̄ from Theorem 1
to find the point closest to λ̄ such that the QP remains convex. This preprocessing step does not considerably affect the runtime since checking whether a matrix is positive semi-definite is done efficiently by Cholesky decomposition. However, it improves the final bounds by up to a factor two compared to the bounds obtained when using λ =
¯ λ without binary search.
Note that this procedure has to be done once for a given classifier. The obtained λ can subsequently be used to solve QPRel for all anchor points and target labels. This is a significant computational advantage compared to SDP based -verification procedures. For example, the method by Dvijotham et al. (2019) includes the dual multipliers as variables in the SDP problem that has to be solved for each combination of the anchor point, target label and verified epsilon.

heading: 4 UPPER BOUNDS
text: Now we describe an iterative procedure generating a sequence of points in Rn0 that converges to a point on the decision boundary. This procedure provides an upper bound on the distance to DtDB and thus allows for bi-directional verification of a classifier.
Algorithm 1: Algorithm to construct an adversarial example by iteratively solving QPRel. Data: x̃0, trained neural net and λ such that Mλ is positive semi-definite, ctol, δ. Result: dub, x0adv
1 begin 2 x0 ←− x̃0; c←− +∞ 3 while c > ctol, pred(x̃0) = pred(x0) do 4 Solve QPRel(λ) from the anchor point x0: 5 xqp, dqp ←− optimal solution and square root of the objective function value 6 c←− c(xqp, λ) 7 Choose the next anchor point on the boundary of the current certified region: 8 if c > ctol then x0 ←− x0 + dqp x 0 qp−x 0
‖x0qp−x0‖ else x0 ←− x0 + dqp(1 + δ) x
0 qp−x 0
‖x0qp−x0‖ 9 end
10 x0adv ←− x0; dub ←− ‖x̃0 − x0adv‖ 11 end
Idea In each step we verify a certain neighborhood around the current anchor point x0 and then expand the verified region further. For that we choose the next anchor point as follows. 1) Choice of direction: we go from x0 towards the solution of QPRel since, if the QP relaxation is tight, its solution should be close to an optimal solution of DtDB which is the closest adversarial point to x0. 2) Choice of step size: we know that there are no adversarial points within the ball of the verified radius d around the anchor, so every step size smaller than d would be unnecessary small. On the other hand, if we proceed with a new anchor point that is strictly farther away than d, we might miss an adversarial point lying close to the boundary of the d-ball around x0. Therefore, we choose the next anchor point to be on the boundary of the currently verified region, so that every -ball that we manage to verify around the new point would add to the overall robust set. Algorithm 1 provides a pseudo-code for this procedure.
Termination The algorithm terminates as soon as the propagation gap c(x, λ) (see (7)) becomes small enough or the anchor point gets misclassified. Note that c(x, λ) = 0 means that the solution x provides the optimal objective function value of the DtDB problem (see Lemma 1) and, thus, an adversarial example. However, the termination condition c ≤ ctol from Algorithm 1, line 3 cannot ensure that the optimal point x0qp from the last iteration belongs to a different class. Therefore, if we stop with c ≤ ctol and the second termination condition is not satisfied, we take an additional step on the boundary of the ball of radius dqp(1 + δ), where dqp is the verified radius and δ is a tiny offset.
Additionally, we check in each step whether the next anchor point is already misclassified before the condition c ≤ ctol is reached (this can happen in a multi-class setting; and is indeed observed frequently). We empirically verified that all points obtained this way are indeed true adversarials. This means that the sequence of anchor points converges towards the boundary and then, if no adversarial point was found yet, makes a step across the boundary using a positive, small δ. Note, while the most powerful attacks as proposed by Carlini and Wagner (2017) were empirically shown to succeed for every considered sample, their success in not guaranteed and might require tuning of hyper-parameters. In contrast, we provide a formal proof of our method’s convergence below.
Figure 2 illustrates how the constructed sequence of anchor points and solutions of QPRel might look like for the setting of Figure 1. Here only the first three steps are shown assuming that we would reach either a small value for the propagation gap or an adversarial point in the last step. Blue arrows show how we proceed from the solution of QPRel to the next anchor point in each iteration (compare to the update formula from Algorithm 1, line 8).
Convergence The following result holds for the convergence rate of Algorithm 1 under the assumption that the propagation gap c(x, λ) is not too large with respect to the optimal objective function value for the QPRel problem solved in each step.
Theorem 2. For k = 0, 1, . . . let ck be the propagation gap as defined in (7) and d2k the optimal objective function value we obtain after solving QPRel in the k’th iteration of Algorithm 1. Assume that there exists α ∈ [0, 1] such that for all k the following holds.
ck d2k ≤ 1− α2 or equivalently ‖x0 − x0qp‖ dk ≥ α (10)
where x0 is the anchor point and xqp is the optimal solution of QPRel in iteration k (we omit the iteration index k on x’s). Then for all k
d2k+1 ≤ 2(1− α)d2k, ck ≤ (2(1− α))k+1d20. (11)
Furthermore, if α > 12 then the number of iterations k̄ such that Algorithm 1 terminates with ck̄ ≤ ctol is bounded by
k̄ ≤ log ctol − 2 log d0 log 2(1− α) − 1. (12)
First of all, this result ensures that Algorithm 1 terminates after a final number of steps if (10) holds for some α ∈ ( 12 , 1]. Moreover, it provides a hint about how many iterations we would have to do if we decreased the threshold ctol by a factor of 10. In this case the upper bound (12) on the number of iterations would increase by ∆kα = −(log 2(1−α))−1 with ∆kα →∞ when α→ 12 and ∆kα → 0 when α→ 1. Note that α being almost 1 means that ck is close to 0. In this regime the relaxation is exact, as discussed in Lemma 1, part 1. Therefore, considering α as a measure of tightness of the relaxation QPRel we can conclude that, when the relaxation is tight (i.e. α ≈ 1), decreasing ctol by an order of magnitude will not be as costly as when α is smaller.
Related work In relation to the methodology proposed in this section we consider the work on exact DtDB computation by Jordan et al. (2018). The proposed algorithm GeoCert iteratively computes the radius of the largest lp-ball that stays within a certain polyhedral complex. The latter is incrementally updated in each step until the decision boundary is reached. This way one get a sequence of lower bounds on DtDB until the true distance is found. GeoCert is significantly different to our method: 1.) It does not employ a relaxation of (DtDB). 2.) It does not change the anchor point, but rather expands the considered polyhedral complices by analyzing the linear regions of a ReLU classifier. 3.) While it can use an upper bound to speed up the algorithm, the complexity of computing its own exact distance is comparable to MIP-based approaches as shown in Jordan et al. (2018).

heading: 5 EXPERIMENTS

heading: 5.1 SETUP
text: The values of the parameters we used as well as the runtime of the compared algorithms is shown in Appendix B.1 and B.2. To solve the QP tasks we use Gurobi Optimization (2018).
Datasets and classifiers The experiments are performed using the MNIST and Fashion-MNIST datasets scaled such that the feature values lie in [0, 1] interval. For each of the datasets we use the correctly classified samples from 1200 train points (label distribution preserved) to evaluate the verification approaches. The exact number of used samples is reported for each experiment in Appendix D.
For classification we take ReLU networks consisting of dense linear layers. The architectures we used are named by the number of hidden layers and the number of neurons per hidden layer: L1N50, L2N50, L3N50, L4N50, L5N50 and L1N300 with the same number of neurons in each hidden layer. For each architecture we use normally trained classifiers as well as robustly trained ones (indicated by suffix R, e.g. L1N50R) using the method by Wong and Kolter (2018) with = 1.58 in l2-setting. The weights will be available in the project repository.
Competitors We compare our approach QPRel with the following -verification methods: ConvAdv by Wong and Kolter (2018) based on the LP relaxation of ReLU constraints (we use its implementation supporting the l2-norm by Croce et al. (2019)), CROWN by Zhang et al. (2018) which is a layerwise bound propagation technique including performance boosting quadratic approximations and warm start (for each setting we report only the best result from these two competitors), and SDPRel by Raghunathan et al. (2018b) based on a SDP relaxation solved by MOSEK. Finally, we take the iterative PGD attack with 200 steps and a step size of 2.5 /200 (in accordance with Madry et al. (2017)) as a competitor for QPRel-UB. We use the notation QPRel-LB or QPRel-UB, when we want to emphasize what bounds are meant.

heading: 5.2 RESULTS
text: Results on MNIST in l2-setting are shown in Table 1. We include the complete results in Appendix D. We run all methods for each of the considered samples and report the following metrics.
AvgBound: The average value of the bounds obtained from QPRel and the corresponding competitor. Both lower and upper bounds are reported separately.
MedRelDiff to QPRel: The median of the relative difference between the bounds (e.g. QPRel-LB minus CROWN and then divided by CROWN). Positive values for the lower bounds mean our bounds are better in average over the samples; negative values are better for the upper bounds.
to hit 50% LB-verified: The number of samples with an adversarial-free radius of is monotonically decreasing in . Therefore, to assess the performance of a verification procedure like QPRel-LB or CROWN we report the smallest such that exactly 50% of the samples can be verified. The larger this value, the better.
VerRatio worst: While the previous metric only considers the lower bound, we can consider both bounds (LB, UB) jointly by evaluation the verification ratio: For a given , it corresponds to the fraction of samples for which we can either prove that the -neighborhood is adversarial-free or contains a misclassified point in it. In short: either the lower bound is larger then or the upper bound is smaller then . Note, that for very small values almost all samples will be verified as -robust by any algorithm providing non-trivial lower bounds. On the other side, when is large, attacks will be able to find an adversarial that is even closer to the anchor and verify almost every sample as -non-robust. Between these two extremes, the verification ratio drops to its minimum for a certain value of 0. In this setting, the considered algorithm is able to verify the smallest fraction of samples – that is, it corresponds to the worst case performance of the bi-directional verification method. We report this smallest fraction in the table, denoted with VerRatio worst. The larger, the better.
MedRelDiff UB-LB: Lastly, we report the median of the relative difference between the different bounds for each approach (QPRel-UB vs. QPRel-LB or PGD vs. CROWN/ConvAdv). It shows the tightness of the certificates when compared to the upper bounds. The smaller, the better.
State-of-the-art bounds For the normally trained networks with a smaller number of hidden layers the lower bounds computed by QPRel are tighter in comparison to the competitors in average and for most individual images (see Table 1, AvgBound and MedRelDiff ). This results in larger values of to hit 50% VerRatio as well. It seems that the competitors tend to underestimate robustness of these networks. For example, for 50% of the MNIST images classified with L1N300 we have improved the lower bound from CROWN by over 149%. This discrepancy in the quality of the lower bounds decreases with network’s depth and if it was trained using the robust training approach by Wong and Kolter (2018) so that the competitors outperform QPRel’s lower bound for robustly trained deep networks.
Noteworthy, the upper bounds derived via QPRel always outperform the one computed by the competing methods – independent of the neural network architecture and the training procedure. That is, the 200-step PGD attack was not able to construct adversarial examples that are closer to the anchor point then those found by QPRel-UB as described in Section 4 in all settings (see Table 1, columns AvgBound/UB and MedRelDiff to QPRel/UB). Therefore, in the settings where the bounds from QPRel-LB are also tighter as the competitors’ we get a much higher VerRatio worst value and smaller MedRelDiff UB-LB that ensure the good quality of QPRel-LB bounds without computing the DtDB exactly. For example, for L2N50 the gap between QPRel-LB and QPRel-UB vanishes resulting in VerRatio worst of over 99%. That means the computed lower bound is almost the exact DtDB for the majority of the samples. Note that no exact method computing DtDB via MIP techniques is used to achieve that. For larger networks we observe a decay of VerRatio worst and looser MedRelDiff UB-LB.
Comparison with SDP-relaxations in l∞-setting In order to compare our method with Raghunathan et al. (2018b) we generalize QPRel to the l∞-setting as described in Appendix A. Note, that the resulting relaxation is looser then the initial QPRel for the l2-setting since we introduce an additional penalty term to make the problem convex. That leads to worse results shown in Tables 9 and 10. To compute the largest such that the SDP verification succeeds we perform a binary search between the lower bounds dqp computed by QPRel-LB and dmax = 1.0 which is the maximal perturbation for the l∞-norm on images. Since this approach takes longer to run we test it only on the L1N50R net trained with = 0.1 (MNIST test data). Further, we speed up this approach by modifying MOSEK parameters (see Table 6 for details) such that the optimization procedure terminates earlier (approximately after a half of the usual number of iterations). We can still rely on the obtained results since we are not interested in the exact value of the SDP objective, but only whether it is positive or negative which was observed to be determined far sooner during the solution process then when the solver would reach a true optimum.
While QPRel-LB in this setting is able to provide tighter bounds then the LP-based approaches for larger computational cost, our bounds are about 1.54 times larger then the ones of SDPRel (see Table 10) – though computed three orders of magnitude faster (see Appendix B.2). This shows that the QP relaxation is less suited then SDPRel for obtaining tight bounds in l∞-setting as already indicated by the arguments above and in Appendix A but trades this off by much better efficiency.

heading: 6 CONCLUSION
text: In this work we present a novel approach to solve the problem of approximating the minimal adversarial perturbations for ReLU networks based in a convex QP relaxation of DtDB. We show that the lower bounds computed with QPRel improve the results of the available LP based methods and allow certification of larger neighborhoods. Since convexity of the underlying QP determines computational efficiency of our approach we derive the necessary and sufficient conditions on the Lagrangian multipliers for it. Additionally, a method that constructs a sequence of points converging to the point on the decision boundary provides us upper bounds on DtDB. Quality of the obtained bounds in the l2-setting is shown to be good enough to verify consistently over 80% of the considered samples for MNIST and FashionMNIST data and simple networks for all values of the perturbation magnitude, while competitors’ verification ratio might drop below 20%.
With our contribution we make a step towards robustness verification of deep ReLU-based classifiers. To be able to apply the approach on a wider class of networks it should be generalized to popular architectures beyond ReLU activations and linear layers. Moreover, for deeper networks the proposed
relaxation was shown to provide looser bounds than the other methods indicating an important direction of the future work. Furthermore, there are several points about Theorem 2 that will be addressed in our future work. It is an open question how to verify (10) a priori. Experiments show that for the current choice of λ (see the discussion after Theorem 1) this condition does hold for small networks, but not for the larger ones.

heading: B EXPERIMENTS SETUP AND RUNTIME
text: B.1 SETUP
λ is chosen for each classifier according to Theorem 1 and the discussion afterwards such that an accuracy level of 10−4 is achieved during the binary search in each λl. For the values of other parameters in Algorithm 1 we choose for all tests ctol = 10−4 and δ = 10−4. Other methods are tested with the default settings as provided in the corresponding repositories.
B.2 RUNTIME AND NUMBER OF ITERATIONS
Tables 2, 3, 4 and 5 show the average runtime and its standard deviation for networks L1N50R, L1N100, L1N300 and L2N100 as well as the number of iterations Algorithm 1 needs to terminate. During the binary search procedure we apply with SDPRel we always make 10 bisection steps. All tasks necessary for the computation of bounds on DtDB for one sample are run on a single CPU (including the solution of QPs and SDPs with Gurobi Optimization (2018) and MOSEK respectively).
Here, we do not consider ConvAdv as CROWN performs always faster. From the comparison of the time for the computation of our lower bounds (column Runtime-LB (s)) and the overall runtime (column Runtime (s)) we conclude that obtaining the upper bounds takes n − 1 times longer than solving the initial QP where n is approximately the overall number of the iterations in Algorithm 1. While in almost all considered settings n remains smaller than 4 it might become a limiting factor when applying QPRel-UB on larger networks. That means further investigation of the convergence properties of Algorithm 1 is necessary for generalizing the described method. From the comparison of QPRel-LB and CROWN we see the clear advantage of the latter since it doesn’t involve any optimization task. However, this advantage comes in cost of the verification properties as discussed above. On the other hand, SDPRel with a binary search provides better bounds, but is about 2000 times slower then QPRel-LB (see the last line in the MNIST section in Table 5).

heading: C PROOFS
text: Lemma 1. Denote the solution of QPRel by xqp and the square root of its optimal objective value by dqp, let d be the square root of the optimal objective value of DtDB. The following holds:
1. dqp ≤ d and when c(x, λ) = 0 we have dqp = d and x is optimal for DtDB.
2. For two non-negative λ1, λ2 with λ1 ≤ λ2 elementwise it holds that dqp(λ1) ≤ dqp(λ2).
Proof. Assume xadv is the optimal solution of DtDB. Then it is an admissible point of QPRel as well and c(xadv, λ) = 0 since xladv = W
lxl−1adv for l = 1, . . . , L− 1. Since xqp is optimal for QPRel and xadv is just its admissible point we get that
d2 = ‖x0adv − x̃0‖2 = ‖x0adv − x̃0‖2 + c(xadv, λ) ≥ ‖x0qp − x̃0‖2 + c(xqp, λ) = d2qp proving the first claim. The second one follows from the fact that c(x, λ) for a given x is a linear function of λ:
c(x, λ) = λT   c(x, e1) ...
c(x, eL−1)
 
where each c(x, el) = ( xl )T ( xl − ( W lxl−1 + bl )) is non-negative for admissible x because of the non-negativity constraints (4). Therefore the claim follows immediately from the assumption that λ1l ≤ λ2l for all l
c(x, λ1) =
L−1∑
l=1
λ1l c(x, el) ≤ L−1∑
l=1
λ2l c(x, el) = c(x, λ 2).
Lemma 2. Objective function of QPRel can be reformulated as
dqp(λ, x) = x TMλx+ xT b̄(λ, x̃0) + c̄(x̃0)
where terms b̄ and c̄ don’t depend on x.
Proof. The proof is done by sorting the quadratic, linear and constant terms in the objective function of the initial formulation.
dqp(λ, x) = ‖x0 − x̃0‖2 + L−1∑
l=1
λl ( xl )T ( xl − ( W lxl−1 + bl ))
= ( x0 )T x0 − 2 ( x0 )T x̃0 + ‖x̃0‖2 + L−1∑
l=1
λl
( ( xl )T xl − ( xl )T W lxl−1 − ( xl )T bl )
=
L−1∑
l=0
λl ( xl )T xl − L−1∑
l=1
λl ( xl )T W lxl−1
︸ ︷︷ ︸ quadratic term
−2 ( x0 )T x̃0 − L−1∑
l=1
λl ( xl )T bl + ‖x̃0‖2
︸ ︷︷ ︸ linear and constant terms
From the quadratic term we can identify now the blocks of Mλ
diagonal: Mλl,l = λlEl l = 0, . . . , L− 1,
sub-diagonal: Mλl+1,l = ( Mλl,l+1 )T = −1
2 λlW
l l = 0, . . . , L− 2.
Theorem 1. Let W 1, . . . ,WL−1 be the weights of an arbitrary pre-trained neural net and ‖W‖ the spectral norm of an arbitrary matrix. Then the following two conditions for λ provide correspondingly a sufficient and a necessary criterion for the matrix Mλ to be positive semi-definite.
(suf. condition) λ1 ≤ 2λ0 ‖W 1‖2 and λl ≤ λl−1 ‖W l‖2 for l = 2, . . . , L− 1 (8)
(nec. condition) λl ≤ 4λl−1 ‖W l‖2 for l = 1, . . . , L− 1 (9)
Further, we define ¯ λ and λ̄ that correspondingly satisfy conditions (8) and (9) with equality:
¯ λl = 2
l∏
k=1
1
‖W k‖2 , λ̄l = 4 l
l∏
k=1
1
‖W k‖2 .
In case with a single hidden layer Mλ with λ = λ̄ from (9) is guaranteed to be positive-semi definite.
Proof. Let the assumptions hold and x be an arbitrary vector from Rn. First we prove the sufficient condition by deriving a lower bound on xTMλx that is non-negative if (8) holds.
xTMλx =
L−1∑
l=0
λl‖xl‖2 − L−1∑
l=1
λl ( xl )T W lxl−1
= λ0 2 ‖x0‖2 + λL−1 2 ‖xL−1‖2
+
L−1∑
l=1
λl 2 ‖xl‖2 − λl
( xl )T W lxl−1 +
λl−1 2 ‖xl−1‖2
= λ0 2 ‖x0‖2 + λL−1 2 ‖xL−1‖2
+
L−1∑
l=1
λl 2 ‖xl‖2 − λl
( xl )T W lxl−1 +
λl 2 ‖W lxl−1‖2
+
L−1∑
l=1
λl−1 2 ‖xl−1‖2 − λl 2 ‖W lxl−1‖2
= λ0 2 ‖x0‖2 + λL−1 2 ‖xL−1‖2 +
L−1∑
l=1
λl 2 ‖xl −W lxl−1‖2
+
L−1∑
l=1
λl−1 2 ‖xl−1‖2 − λl 2 ‖W lxl−1‖2
= λL−1
2 ‖xL−1‖2 +
L−1∑
l=1
λl 2 ‖xl −W lxl−1‖2+
+ ( λ0‖x0‖2 −
λ1 2 ‖W 1x0‖2
) + L−1∑
l=2
λl−1 2 ‖xl−1‖2 − λl 2 ‖W lxl−1‖2
≥ λL−1 2 ‖xL−1‖2 +
L−1∑
l=1
λl 2 ‖xl −W lxl−1‖2+
+ 1
2
( 2λ0 − λ1‖W 1‖2 ) ‖x0‖2 + 1
2
L−1∑
l=2
( λl−1 − λl‖W l‖2 ) ‖xl−1‖2
where we applied the sub-multiplicativity property of the spectral norm, i.e. ‖W lxl−1‖ ≤ ‖W l‖‖xl−1‖, to obtain the last inequality. We see that under the assumption (8) on λ and W ’s it holds that
λ1‖W 1‖2 ≤ 2λ0 and λl‖W l‖2 ≤ λl−1 for l = 2, . . . , L− 1
and the lower bound on xTMλx in the last line is a sum of non-negative terms meaning that xTMλx ≥ 0 for all x ∈ Rn. To prove the necessary condition consider for each l = 1, . . . , L − 1 a special vector x̃ (we don’t explicitly label it as dependent on l to avoid overloaded notation) which is everywhere zero except
x̃l−1 := arg max x∈Rnl−1 ‖W lx‖ ‖x‖ and x̃ l := 1 2 W lxl−1.
For Mλ in order to be positive semi-definite it has to satisfy
0 ≤ x̃TMλx̃ = ( x̃l−1
x̃l
)T ( λl−1El−1 − 12λl ( W l )T
− 12λlW l λlEl
)( x̃l−1
x̃l
)
= λl−1‖x̃l−1‖2 − λl ( x̃l )T W lx̃l−1 + λl‖x̃l‖2
= λl−1‖x̃l−1‖2 − 1
4 λl‖W lx̃l−1‖2 =
( λl−1 − 1
4 λl‖W l‖2
) ‖x̃l−1‖2
which results in the necessary condition (9) as stated above. It remains to prove the sufficiency of (9) if the considered network contains one hidden layer. For that we can reuse the last computation and obtain now for an arbitrary x ∈ Rn that
xTM λ̄x = λ0‖x0‖2 − λ1 ( x1 )T W 1x0 + λ1‖x1‖2
= λ0‖x0‖2 − 1
4 λ1‖W 1x0‖2 + λ1‖
1 2 W 1x0 − x1‖2
≥ ( λ0 − 1
4 λ1‖W 1‖2
) ‖x0‖2 + λ1‖ 1
2 W 1x0 − x1‖2.
We see that the last term remains non-negative in case of λ1 = 4λ0‖W 1‖2 for all x.
Theorem 2. For k = 0, 1, . . . let ck be the propagation gap as defined in (7) and d2k the optimal objective function value we obtain after solving QPRel in the k’th iteration of Algorithm 1. Assume that there exists α ∈ [0, 1] such that for all k the following holds.
ck d2k ≤ 1− α2 or equivalently ‖x0 − x0qp‖ dk ≥ α (10)
where x0 is the anchor point and xqp is the optimal solution of QPRel in k’s iteration (we omit the iteration index k on x’s). Then for all k
d2k+1 ≤ 2(1− α)d2k, ck ≤ (2(1− α))k+1d20. (11) Furthermore, if α > 12 then the number of iterations k̄ such that Algorithm 1 terminates with ck̄ ≤ ctol is bounded by
k̄ ≤ log ctol − 2 log d0 log 2(1− α) − 1. (12)
Proof. First, we prove that given (10) it holds that d2k+1 ≤ 2(1−α)d2k. We denote the anchor point in iteration k as x0 and the optimal solution for QPRel with that anchor point as xqp. The corresponding objects in the next iteration k+ 1 are denoted by y0 and yqp. Then according to the choice of the next anchor point (see Algorithm 1, line 8)
y0 = x0 + dk x0qp − x0 ‖x0qp − x0‖ ⇒ ‖y0 − x0qp‖ = dk − ‖x0 − x0qp‖ (compare to Figure 2) (13)
and it follows that
d2k+1 = min x:(5),(6) ‖y0 − x0‖2 + c(x, λ) ≤ ‖y0 − x0qp‖2 + c(xqp, λ)
= (13)
( dk − ‖x0 − x0qp‖ )2 + ck ≤
(10) (1− α)2d2k + (1− α2)d2k = 2(1− α)d2k.
Now, applying this relation on every two subsequent iterations up to the k’s we obtain (here we use 1− α2 = (1 + α)(1− α) ≤ 2(1− α) to get the last inequality)
ck ≤ (10) (1− α2)d2k ≤ (1− α2)(2(1− α))kd20 ≤ (2(1− α))k+1d20.
It remains to prove the last inequality (12). Note that for 1 ≥ α > 12 the derived upper bound on ck is monotonically decreasing and converges to 0 as k →∞ since 0 ≤ 2(1− α) < 1. Therefore, to find the first k such that the upper bound on ck becomes smaller or equal ctol we have to solve the equation ctol = (2(1− α))k+1d20 for k resulting in the upper bound on k as claimed in (12).

heading: D TABLES
text: 1https://docs.mosek.com/9.0/pythonapi/parameters.html contains the full list of parameters including their description.

Review summaries:
This paper proposes a method to compute the distance to the decision boundary for a given network, where the network is composed of linear layers followed by a RELU activation. The authors provide a lower bound and an upper bound for the distance of a sample from the decision boundary. The lower bound is obtained as the solution to a quadratic program, which in turn is obtained by relaxing the original optimization problem. The relaxation is obtained by decomposing the RELU condition to a set of 3 constraints (eqn 2). The authors also provide conditions under which the quadratic program stays convex.