Title: EFFICIENT BI-DIRECTIONAL VERIFICATION OF RELU NETWORKS VIA QUADRATIC PROGRAMMING

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.
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 x 0 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 x 0 and an > 0, the task is to verify whether an adversarial point exists within the neighborhood of x 0 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 x 0 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 l 2 -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.

2. NOTATION AND IDEA:

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 n l for l = 0, . . . , L, meaning that the data has n 0 features and n L classes. Furthermore, we present our analysis for the l 2 -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 x 0 ∈ R n0 , weight matrices W l ∈ R n l ×n l-1 , and bias vectors b l ∈ R n l , we define the output of the i-th neuron in the l-th layer after the ReLU activation as

x l i = W l i x l-1 + b l i + and

(1)

f i (x 0 ) = x L i = W L i x L-1 + b L i

where [x] + is the positive part of x and f (x 0 ) = x L 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.

EQUATION

3 OPTIMIZATION PROBLEM

3.1. FORMULATION OF DTDB:

For a given sample x0 , pre-trained neural net f , predicted label ỹ and target label y we aim to find the closest point to x0 in R n0 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.

EQUATION

where e i is the i-th unit vector in R n L and x denotes the Euclidean norm of x. Note that we explore the boundary between classes y and ỹ around x0 . To compute the distance from x0 to the (full) decision boundary, one needs t compute the solution for all target labels y = 1, . . . , n L except ỹ.

We can "unfold" the above optimization problem using (1), where x denotes a container with all variables x 0 , . . . , x L .

min x∈R n x 0 -x0 2 , s.t. (e ỹ -e y ) T x L ≤ 0, x L = W L x L-1 + b L x l = ReLU(W l x l-1 + b l ) for l = 1, . . . , L -1

We apply (2) to reformulate the problem and eliminate x L , such that from now on x contains only the remaining variables x 0 , . . . , x L-1 and n = n 0 + . . . + n L-1 .

min x∈R n x 0 -x0 2 , s.t. (e ỹ -e y ) T W L x L-1 + b L ≤ 0 (DtDB) x l T x l -W l x l-1 + b l = 0 for l = 1, . . . , L -1 (3) x l -W l x l-1 + b l ≥ 0, x l ≥ 0 for l = 1, . . . , L -1 (4) 3.2 QP RELAXATION

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∈R n x 0 -x0 2 + L-1 l=1 λ l x l T x l -W l x l-1 + b l , s.t. (QPRel) (e ỹ -e y ) T W L x L-1 + b L ≤ 0 (5) x l -W l x l-1 + b l ≥ 0, x l ≥ 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

x 0 ∈ R n0 , . . . , x L-1 ∈ R n L-1 and λ ∈ R L-1 + c(x, λ) := L-1 l=1 λ l x l T x l -W l x l-1 + b l (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 x 0 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 x 0 as an input and the value of x l 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 ỹ). Lemma 1. Denote the solution of QPRel by x qp and the square root of its optimal objective value by d qp , let d be the square root of the optimal objective value of DtDB. The following holds:

1. d qp ≤ d and when c(x qp , λ) = 0 we have d qp = d and x qp is optimal for DtDB.

2. For two non-negative λ 1 , λ 2 with λ 1 ≤ λ 2 elementwise it holds that d qp (λ 1 ) ≤ d qp (λ 2 ). The first result from Lemma 1 ensures that d qp 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 E l ∈ R n l ×n l be the identity matrix of the corresponding dimension. We define M λ ∈ R n×n as the following symmetric block tridiagonal matrix

M λ :=       D 0 M T 1 M 1 D 1 M T 2 M 2 . . . . . . . . . D L-1       with M l := - 1 2 λ l W l , D l := λ l E l and λ 0 := 1.

Using this matrix we can rewrite the objective function from QPRel as (see Appendix C, Lemma 2): 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 W l 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 , . . . , W L-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.

min x∈R n x T M λ x + x T b(λ, x0 ) + c(x 0 ), s.t. (

(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.

4. UPPER BOUNDS:

Now we describe an iterative procedure generating a sequence of points in R n0 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: x0 , trained neural net and λ such that M λ is positive semi-definite, c tol , δ. Result: d ub , x 0 adv begin x 0 ←-x0 ; c ←-+∞ while c > c tol , pred(x 0 ) = pred(x 0 ) do

Solve QPRel(λ) from the anchor point x 0 :

x qp , d qp ←optimal solution and square root of the objective function value

c ←-c(x qp , λ)

Choose the next anchor point on the boundary of the current certified region:

if c > c tol then x 0 ←-x 0 + d qp x 0 qp -x 0 x 0 qp -x 0 else x 0 ←-x 0 + d qp (1 + δ) x 0 qp -x 0 x 0 qp -x 0 end x 0 adv ←-x 0 ; d ub ←-x0 -x 0 adv end

Idea In each step we verify a certain neighborhood around the current anchor point x 0 and then expand the verified region further. For that we choose the next anchor point as follows. 1) Choice of direction: we go from x 0 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 x 0 .

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 x 0 . 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 ≤ c tol from Algorithm 1, line 3 cannot ensure that the optimal point x 0 qp from the last iteration belongs to a different class. Therefore, if we stop with c ≤ c tol and the second termination condition is not satisfied, we take an additional step on the boundary of the ball of radius d qp (1 + δ), where d qp 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 ≤ c tol 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. 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 c k be the propagation gap as defined in (7) and d 2 k 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.

c k d 2 k ≤ 1 -α 2 or equivalently x 0 -x 0 qp d k ≥ α (10)

where x 0 is the anchor point and x qp is the optimal solution of QPRel in iteration k (we omit the iteration index k on x's). Then for all k

EQUATION

Furthermore, if α > 1 2 then the number of iterations k such that Algorithm 1 terminates with ck ≤ c tol is bounded by

EQUATION

)

First of all, this result ensures that Algorithm 1 terminates after a final number of steps if (10) holds for some α ∈ ( 1 2 , 1]. Moreover, it provides a hint about how many iterations we would have to do if we decreased the threshold c tol 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 α → 1 2 and ∆k α → 0 when α → 1. Note that α being almost 1 means that c k 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 c tol 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 l p -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) .

5. EXPERIMENTS:



5.1. SETUP:

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 l 2 -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) 

5.2. RESULTS:

Results on MNIST in l 2 -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. 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 l 2 -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 d qp computed by QPRel-LB and d max = 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.

6. CONCLUSION:

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 l 2 -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.

A GENERALIZATION TO l ∞ For comparison with Raghunathan et al. (2018b) we show how our method can be applied to compute bounds on the distance to the closest adversarial measured using the l ∞ norm. A straight forward way would be to modify the objective function accordingly. By introducing a new variable m representing

x 0 -x0 2 ∞ = max i |x 0 i -x0 i | 2

and n 0 new quadratic constraints we get the following versions of QPRel. Note that the quadratic constraints do not harm the complexity since they describe a convex cone and can be handled by the QP-solvers including gurobi.

min x∈R n , m∈R m + c(x, λ), s.t. (x 0 i -x0 i ) 2 ≤ m, i = 1, . . . , n 0 (e ỹ -e y ) T W L x L-1 + b L ≤ 0 x l -W l x l-1 + b l ≥ 0, x l ≥ 0

While this formulation is of a similar structure as the QPRel (quadratic objective and linear plus quadratic constraints), the Hessian of the objective function is not positive semi-definite for any value of λ. Since c(x, λ) is the only source of quadratic terms now (squared distance to the anchor point is now replaced by m), the new M λ is of the same form as in Lemma 2, but with λ 0 = 0. To see that we cannot affect the convexity of the objective function by the parameter λ anymore consider vector x with an arbitrary x 0 ∈ R n0 , x 1 = αW 1 x 0 with 0 < α < 1 and x l = 0 for l > 1. Then

x T M λ x = λ 1 x 1 2 -x 1 T W 1 x 0 = λ 1 (α 2 -α) W 1 x 0 2 < 0 meaning that M λ cannot be positive semi-definite.

To overcome this issue we utilize the new quadratic constraints. We return back to a convex QP by considering the following problem with a positive µ.

min x∈R n , m∈R m + c(x, λ) + µ n0 i=1 (x 0 i -x0 i ) 2 -m , with (x 0 i -x0 i ) 2 ≤ m, i = 1, . . . , n 0 (e ỹ -e y ) T W L x L-1 + b L ≤ 0 x l -W l x l-1 + b l ≥ 0, x l ≥ 0 Clearly, for 0 < µ ≤ n -1

0 the solution of this problem is a finite lower bound on DtDB with the l ∞ -norm. On the other side we are back in the setting of Theorem 1 with λ 0 = µ allowing us to use the same framework as before. Results in the l ∞ -setting were obtained by solving this problem with µ = (2n 0 ) -1 .

B EXPERIMENTS SETUP AND RUNTIME:

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 c tol = 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).

C PROOFS:

Lemma 1. Denote the solution of QPRel by x qp and the square root of its optimal objective value by d qp , let d be the square root of the optimal objective value of DtDB. The following holds:

1. d qp ≤ d and when c(x, λ) = 0 we have d qp = d and x is optimal for DtDB.

2. For two non-negative λ 1 , λ 2 with λ 1 ≤ λ 2 elementwise it holds that d qp (λ 1 ) ≤ d qp (λ 2 ).

Proof. Assume x adv is the optimal solution of DtDB. Then it is an admissible point of QPRel as well and c(x adv , λ) = 0 since x l adv = W l x l-1 adv for l = 1, . . . , L -1. Since x qp is optimal for QPRel and x adv is just its admissible point we get that

d 2 = x 0 adv -x0 2 = x 0 adv -x0 2 + c(x adv , λ) ≥ x 0 qp -x0 2 + c(x qp , λ) = d 2 qp

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, e 1 ) . . . c(x, e L-1 )   

where each c(x, e l ) = x l T x l -W l x l-1 + b l is non-negative for admissible x because of the non-negativity constraints (4). Therefore the claim follows immediately from the assumption that

λ 1 l ≤ λ 2 l for all l c(x, λ 1 ) = L-1 l=1 λ 1 l c(x, e l ) ≤ L-1 l=1 λ 2 l c(x, e l ) = c(x, λ 2 ).

Lemma 2. Objective function of QPRel can be reformulated as

d qp (λ, x) = x T M λ x + x T b(λ, x0 ) + 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.

d qp (λ, x) = x 0 -x0 2 + L-1 l=1 λ l x l T x l -W l x l-1 + b l = x 0 T x 0 -2 x 0 T x0 + x0 2 + L-1 l=1 λ l x l T x l -x l T W l x l-1 -x l T b l = L-1 l=0 λ l x l T x l - L-1 l=1 λ l x l T W l x l-1 quadratic term -2 x 0 T x0 - L-1 l=1 λ l x l T b l + x0 2

linear and constant terms

From the quadratic term we can identify now the blocks of M λ diagonal:

M λ l,l = λ l E l l = 0, . . . , L -1, sub-diagonal: M λ l+1,l = M λ l,l+1 T = - 1 2 λ l W l l = 0, . . . , L -2.

Theorem 1. Let W 1 , . . . , W L-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 R n . First we prove the sufficient condition by deriving a lower bound on x T M λ x that is non-negative if (8) holds.

x

T M λ x = L-1 l=0 λ l x l 2 - L-1 l=1 λ l x l T W l x l-1 = λ 0 2 x 0 2 + λ L-1 2 x L-1 2 + L-1 l=1 λ l 2 x l 2 -λ l x l T W l x l-1 + λ l-1 2 x l-1 2 = λ 0 2 x 0 2 + λ L-1 2 x L-1 2 + L-1 l=1 λ l 2 x l 2 -λ l x l T W l x l-1 + λ l 2 W l x l-1 2 + L-1 l=1 λ l-1 2 x l-1 2 - λ l 2 W l x l-1 2 = λ 0 2 x 0 2 + λ L-1 2 x L-1 2 + L-1 l=1 λ l 2 x l -W l x l-1 2 + L-1 l=1 λ l-1 2 x l-1 2 - λ l 2 W l x l-1 2 = λ L-1 2 x L-1 2 + L-1 l=1 λ l 2 x l -W l x l-1 2 + + λ 0 x 0 2 - λ 1 2 W 1 x 0 2 + L-1 l=2 λ l-1 2 x l-1 2 - λ l 2 W l x l-1 2 ≥ λ L-1 2 x L-1 2 + L-1 l=1 λ l 2 x l -W l x l-1 2 + + 1 2 2λ 0 -λ 1 W 1 2 x 0 2 + 1 2 L-1 l=2 λ l-1 -λ l W l 2 x l-1 2

where we applied the sub-multiplicativity property of the spectral norm, i.e. W l x l-1 ≤ W l x l-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 x T M λ x in the last line is a sum of non-negative terms meaning that x T M λ x ≥ 0 for all x ∈ R n .

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 xl-1 := arg max

x∈R n l-1 W l x x and xl := 1 2 W l x l-1 .

For M λ in order to be positive semi-definite it has to satisfy

0 ≤ xT M λ x = xl-1 xl T λ l-1 E l-1 -1 2 λ l W l T -1 2 λ l W l λ l E l xl-1 xl = λ l-1 xl-1 2 -λ l xl T W l xl-1 + λ l xl 2 = λ l-1 xl-1 2 - 1 4 λ l W l xl-1 2 = λ l-1 - 1 4 λ l W l 2 xl-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 ∈ R n that

x T M λx = λ 0 x 0 2 -λ 1 x 1 T W 1 x 0 + λ 1 x 1 2 = λ 0 x 0 2 - 1 4 λ 1 W 1 x 0 2 + λ 1 1 2 W 1 x 0 -x 1 2 ≥ λ 0 - 1 4 λ 1 W 1 2 x 0 2 + λ 1 1 2 W 1 x 0 -x 1 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 c k be the propagation gap as defined in (7) and d 2 k 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.

c k d 2 k ≤ 1 -α 2 or equivalently x 0 -x 0 qp d k ≥ α (10)

where x 0 is the anchor point and x qp is the optimal solution of QPRel in k's iteration (we omit the iteration index k on x's). Then for all k

EQUATION

Furthermore, if α > 1 2 then the number of iterations k such that Algorithm 1 terminates with ck ≤ c tol is bounded by

EQUATION

Proof. First, we prove that given (10) it holds that d 2 k+1 ≤ 2(1α)d 2 k . We denote the anchor point in iteration k as x 0 and the optimal solution for QPRel with that anchor point as x qp . The corresponding objects in the next iteration k + 1 are denoted by y 0 and y qp . Then according to the choice of the next anchor point (see Algorithm 1, line 8)

EQUATION

)

and it follows that d 2 k+1 = min

x:(5),( 6)

y 0 -x 0 2 + c(x, λ) ≤ y 0 -x 0 qp 2 + c(x qp , λ) = (13) d k -x 0 -x 0 qp 2 + c k ≤ (10) (1 -α) 2 d 2 k + (1 -α 2 )d 2 k = 2(1 -α)d 2 k .

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) c k ≤ (10) (1 -α 2 )d 2 k ≤ (1 -α 2 )(2(1 -α)) k d 2 0 ≤ (2(1 -α)) k+1 d 2 0 .

It remains to prove the last inequality (12). Note that for 1 ≥ α >1 2 the derived upper bound on c k 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 c k becomes smaller or equal c tol we have to solve the equation c tol = (2(1α)) k+1 d 2 0 for k resulting in the upper bound on k as claimed in (12). 

D TABLES:



https://docs.mosek.com/9.0/pythonapi/parameters.html contains the full list of parameters including their description.

Figures and Tables:

Figure 1: Setting of the optimal solutions for DtDB x adv and QPRel x qp .

Figure 2: Three steps of Algorithm 1.

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).

based on the LP relaxation of ReLU constraints (we use its implementation supporting the l 2 -norm byCroce et al. (2019)), CROWN byZhang 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 byRaghunathan 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 withMadry 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.

Better bounds and verification ratio for the compact networks (l 2 -perturbations)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 Table1, 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 byWong 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 Table1, 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.

Table content: <table><tr><td/><td>MNIST, l2</td><td colspan="2">AvgBound</td><td colspan="2">MedRelDiff</td><td colspan="2">to hit 50% VerRatio</td><td>MedRelDiff</td></tr><tr><td/><td/><td/><td/><td colspan="2">to QPRel (%)</td><td>LB-verified</td><td>worst (%) UB-LB (%)</td></tr><tr><td>L/N/R</td><td>Method</td><td>LB</td><td>UB</td><td>LB</td><td>UB</td><td/></tr><tr><td>1/50</td><td>QPRel</td><td colspan="3">0.42 0.49 -</td><td>-</td><td>0.398</td><td>87.5</td><td>13.7</td></tr><tr><td>1/50</td><td>CROWN+PGD</td><td colspan="3">0.25 0.72 +63.0</td><td colspan="2">-30.8 0.239</td><td>31.4</td><td>168.7</td></tr><tr><td>1/50/R</td><td>QPRel</td><td colspan="3">1.69 1.84 -</td><td>-</td><td>1.698</td><td>90.3</td><td>5.3</td></tr><tr><td>1/50/R</td><td>CROWN+PGD</td><td colspan="3">1.52 2.68 +12.8</td><td colspan="2">-30.8 1.567</td><td>49.8</td><td>72.0</td></tr><tr><td>2/50</td><td>QPRel</td><td colspan="3">1.20 1.21 -</td><td>-</td><td>1.174</td><td>99.3</td><td>&lt;0.01</td></tr><tr><td>2/50</td><td colspan="4">ConvAdv+PGD 0.89 1.80 +30.1</td><td colspan="2">-25.0 0.891</td><td>51.2</td><td>89.8</td></tr><tr><td>2/50/R</td><td>QPRel</td><td colspan="3">1.39 1.81 -</td><td>-</td><td>1.388</td><td>74.8</td><td>25.3</td></tr><tr><td>2/50/R</td><td colspan="4">ConvAdv+PGD 1.47 2.62 -2.9</td><td colspan="2">-30.8 1.527</td><td>52.4</td><td>76.3</td></tr><tr><td>3/50</td><td>QPRel</td><td colspan="3">0.18 0.55 -</td><td>-</td><td>0.181</td><td>26.0</td><td>200.2</td></tr><tr><td>3/50</td><td colspan="4">ConvAdv+PGD 0.19 0.71 -9.3</td><td colspan="2">-18.2 0.199</td><td>19.9</td><td>246.4</td></tr><tr><td>3/50/R</td><td>QPRel</td><td colspan="3">1.10 1.78 -</td><td>-</td><td>1.091</td><td>59.5</td><td>57.7</td></tr><tr><td>3/50/R</td><td colspan="4">ConvAdv+PGD 1.43 2.55 -21.9</td><td colspan="2">-30.8 1.488</td><td>51.1</td><td>74.3</td></tr><tr><td>4/50</td><td>QPRel</td><td colspan="3">0.09 0.58 -</td><td>-</td><td>0.106</td><td>9.1</td><td>484.6</td></tr><tr><td>4/50</td><td colspan="4">ConvAdv+PGD 0.19 0.70 -50.4</td><td colspan="2">-18.2 0.191</td><td>19.5</td><td>255.4</td></tr><tr><td>4/50/R</td><td>QPRel</td><td colspan="3">0.69 1.76 -</td><td>-</td><td>0.698</td><td>35.7</td><td>142.5</td></tr><tr><td>4/50/R</td><td colspan="4">ConvAdv+PGD 1.41 2.51 -49.8</td><td colspan="2">-25.0 1.497</td><td>51.2</td><td>71.6</td></tr><tr><td>5/50</td><td>QPRel</td><td colspan="3">0.02 0.42 -</td><td>-</td><td>0.037</td><td>9.5</td><td>1370.6</td></tr><tr><td>5/50</td><td colspan="4">ConvAdv+PGD 0.16 0.63 -84.4</td><td colspan="2">-35.7 0.167</td><td>19.5</td><td>274.2</td></tr><tr><td>5/50/R</td><td>QPRel</td><td colspan="3">0.37 1.76 -</td><td>-</td><td>0.391</td><td>20.0</td><td>357.0</td></tr><tr><td>5/50/R</td><td colspan="4">ConvAdv+PGD 1.41 2.58 -73.1</td><td colspan="2">-30.8 1.466</td><td>49.3</td><td>79.9</td></tr><tr><td>1/300</td><td>QPRel</td><td colspan="3">0.26 0.28 -</td><td>-</td><td>0.243</td><td>94.0</td><td>5.5</td></tr><tr><td>1/300</td><td>CROWN+PGD</td><td colspan="5">0.10 0.53 +149.1 -43.8 0.101</td><td>17.2</td><td>385.2</td></tr><tr><td colspan="2">1/300/R QPRel</td><td colspan="3">0.78 1.81 -</td><td>-</td><td>0.782</td><td>42.8</td><td>120.4</td></tr><tr><td colspan="2">1/300/R CROWN+PGD</td><td colspan="3">1.43 2.76 -44.1</td><td colspan="2">-30.8 1.418</td><td>46.6</td><td>83.5</td></tr></table>

MOSEK parameters we use to run SDPRel and their default values

Table content: <table><tr><td>Parameter 1</td><td colspan="2">New value Default value</td></tr><tr><td>MSK_IPAR_NUM_THREADS</td><td>1</td><td>0</td></tr><tr><td colspan="2">MSK_DPAR_INTPNT_CO_TOL_MU_RED 10 -4</td><td>10 -8</td></tr><tr><td colspan="2">MSK_DPAR_INTPNT_CO_TOL_REL_GAP 10 -4</td><td>10 -8</td></tr><tr><td>MSK_DPAR_INTPNT_CO_TOL_INFEAS</td><td>10 -6</td><td>10 -12</td></tr><tr><td>MSK_DPAR_INTPNT_CO_TOL_DFEAS</td><td>10 -4</td><td>10 -8</td></tr><tr><td>MSK_DPAR_INTPNT_CO_TOL_PFEAS</td><td>10 -4</td><td>10 -8</td></tr></table>

Results for train data, l 2 -perturbations

Table content: <table><tr><td>Setting</td><td/><td/><td>MedRelDiff</td><td colspan="2">to hit 50% VerRatio</td><td>MedRelDiff</td></tr><tr><td colspan="2">Data L/N</td><td>NrPts Method</td><td colspan="4">to QPRel (%) LB-verified worst (%) UB-LB (%)</td></tr><tr><td/><td colspan="2">1/100 QPRel-LB</td><td>-</td><td>0.246</td><td>82.8</td><td>13.4</td></tr><tr><td/><td colspan="3">1/100 CROWN+FGSM +82.4</td><td>0.129</td><td>8.1</td><td>1033.7</td></tr><tr><td>MNIST</td><td colspan="3">2/100 2/100 1/300 QPRel-LB QPRel-LB ConvAdv+FGSM +30.1 --</td><td>1.174 0.891 0.243</td><td>99.3 23.3 94.0</td><td>&lt;0.01 277.9 5.5</td></tr><tr><td/><td colspan="3">1/300 CROWN+FGSM +149.1</td><td>0.101</td><td>10.9</td><td>627.8</td></tr><tr><td/><td>1/50</td><td>QPRel-LB</td><td>-</td><td>0.872</td><td>82.4</td><td>14.3</td></tr><tr><td/><td>1/50</td><td colspan="2">CROWN+FGSM +67.0</td><td>0.506</td><td>8.8</td><td>419.4</td></tr><tr><td/><td colspan="2">1/100 QPRel-LB</td><td>-</td><td>0.252</td><td>81.9</td><td>17.2</td></tr><tr><td>F-MNIST</td><td colspan="3">1/100 CROWN+FGSM +49.1 2/100 QPRel-LB -2/100 ConvAdv+FGSM +68.0</td><td>0.159 0.332 0.205</td><td>15.9 83.0 22.2</td><td>678.8 20.3 375.1</td></tr><tr><td/><td colspan="2">1/300 QPRel-LB</td><td>-</td><td>0.183</td><td>78.8</td><td>23.1</td></tr><tr><td/><td colspan="3">1/300 CROWN+FGSM +56.6</td><td>0.122</td><td>12.8</td><td>902.2</td></tr></table>

Results for test data, l 2 -perturbations

Table content: <table><tr><td>Setting</td><td/><td/><td>MedRelDiff</td><td colspan="2">to hit 50% VerRatio</td><td>MedRelDiff</td></tr><tr><td colspan="2">Data L/N</td><td>NrPts Method</td><td colspan="4">to QPRel (%) LB-verified worst (%) UB-LB (%)</td></tr><tr><td/><td colspan="2">1/100 QPRel-LB</td><td>-</td><td>0.268</td><td>81.9</td><td>14.6</td></tr><tr><td/><td colspan="3">1/100 CROWN+FGSM +84.6</td><td>0.146</td><td>6.7</td><td>1097.2</td></tr><tr><td>MNIST</td><td colspan="3">2/100 QPRel-LB 2/100 ConvAdv+FGSM +30.2 -1/300 QPRel-LB -</td><td>1.251 0.959 0.267</td><td>99.4 23.6 93.9</td><td>0.0 281.8 5.9</td></tr><tr><td/><td colspan="3">1/300 CROWN+FGSM +154.6</td><td>0.111</td><td>7.0</td><td>658.5</td></tr><tr><td/><td>1/50</td><td>QPRel-LB</td><td>-</td><td>0.937</td><td>80.0</td><td>15.2</td></tr><tr><td/><td>1/50</td><td colspan="2">CROWN+FGSM +68.5</td><td>0.562</td><td>7.4</td><td>421.8</td></tr><tr><td/><td colspan="2">1/100 QPRel-LB</td><td>-</td><td>0.258</td><td>79.8</td><td>19.2</td></tr><tr><td>F-MNIST</td><td colspan="3">1/100 CROWN+FGSM +50.3 2/100 QPRel-LB -2/100 ConvAdv+FGSM +71.6</td><td>0.164 0.355 0.213</td><td>13.7 79.9 19.3</td><td>703.0 21.3 375.2</td></tr><tr><td/><td colspan="2">1/300 QPRel-LB</td><td>-</td><td>0.194</td><td>77.0</td><td>24.7</td></tr><tr><td/><td colspan="3">1/300 CROWN+FGSM +59.3</td><td>0.122</td><td>10.6</td><td>890.9</td></tr></table>

Results for train data, l ∞ -perturbations

Table content: <table><tr><td>Setting</td><td/><td/><td>MedRelDiff</td><td colspan="2">to hit 50% VerRatio</td><td>MedRelDiff</td></tr><tr><td colspan="2">Data L/N</td><td>NrPts Method</td><td colspan="4">to QPRel (%) LB-verified worst (%) UB-LB (%)</td></tr><tr><td/><td colspan="2">1/100 QPRel-LB</td><td>-</td><td>0.010</td><td>5.8</td><td>1478.1</td></tr><tr><td/><td colspan="3">1/100 CROWN+FGSM +33.4</td><td>0.010</td><td>13.6</td><td>882.5</td></tr><tr><td>MNIST</td><td colspan="3">2/100 2/100 1/300 QPRel-LB QPRel-LB ConvAdv+FGSM +16.8 --</td><td>0.057 0.057 0.011</td><td>5.3 32.4 3.6</td><td>2484.0 220.4 1691.4</td></tr><tr><td/><td colspan="3">1/300 CROWN+FGSM +104.3</td><td>0.011</td><td>13.0</td><td>575.1</td></tr><tr><td/><td>1/50</td><td>QPRel-LB</td><td>-</td><td>0.033</td><td>1.6</td><td>3344.0</td></tr><tr><td/><td>1/50</td><td colspan="2">CROWN+FGSM +2.2</td><td>0.033</td><td>16.0</td><td>286.8</td></tr><tr><td/><td colspan="2">1/100 QPRel-LB</td><td>-</td><td>0.010</td><td>6.9</td><td>1520.8</td></tr><tr><td>F-MNIST</td><td colspan="3">1/100 CROWN+FGSM +5.5 2/100 QPRel-LB -2/100 ConvAdv+FGSM +17.1</td><td>0.010 0.013 0.013</td><td>17.8 3.6 33.1</td><td>599.5 1855.8 341.6</td></tr><tr><td/><td colspan="2">1/300 QPRel-LB</td><td>-</td><td>0.007</td><td>3.0</td><td>1579.8</td></tr><tr><td/><td colspan="3">1/300 CROWN+FGSM +11.0</td><td>0.007</td><td>14.2</td><td>741.8</td></tr></table>

Results for test data, l ∞ -perturbations

Table content: <table><tr><td>Setting</td><td/><td/><td>MedRelDiff</td><td colspan="2">to hit 50% VerRatio</td><td>MedRelDiff</td></tr><tr><td colspan="2">Data L/N</td><td>NrPts Method</td><td colspan="4">to QPRel (%) LB-verified worst (%) UB-LB (%)</td></tr><tr><td/><td colspan="2">1/100 QPRel-LB</td><td>-</td><td>0.011</td><td>7.2</td><td>1439.0</td></tr><tr><td/><td colspan="3">1/100 CROWN+FGSM +33.6</td><td>0.011</td><td>10.5</td><td>946.5</td></tr><tr><td>MNIST</td><td colspan="3">2/100 QPRel-LB 2/100 ConvAdv+FGSM +16.5 -1/300 QPRel-LB -</td><td>0.115 0.058 0.011</td><td>5.2 28.7 2.4</td><td>2480.9 218.6 1704.3</td></tr><tr><td/><td colspan="3">1/300 CROWN+FGSM +105.7</td><td>0.011</td><td>8.1</td><td>610.7</td></tr><tr><td/><td>1/50</td><td>QPRel-LB</td><td>-</td><td>0.037</td><td>1.8</td><td>3462.1</td></tr><tr><td/><td>1/50</td><td colspan="2">CROWN+FGSM +2.3</td><td>0.037</td><td>15.5</td><td>280.8</td></tr><tr><td/><td>1/50</td><td>SDPRel+FGSM</td><td>-54.5</td><td>0.074</td><td>51.1</td><td>68.1</td></tr><tr><td/><td colspan="2">1/100 QPRel-LB</td><td>-</td><td>0.011</td><td>6.8</td><td>1520.9</td></tr><tr><td>F-MNIST</td><td colspan="3">1/100 CROWN+FGSM +5.5 2/100 QPRel-LB -2/100 ConvAdv+FGSM +18.2</td><td>0.011 0.012 0.012</td><td>19.3 2.5 28.6</td><td>605.4 1938.1 344.7</td></tr><tr><td/><td colspan="2">1/300 QPRel-LB</td><td>-</td><td>0.007</td><td>3.9</td><td>1543.1</td></tr><tr><td/><td colspan="3">1/300 CROWN+FGSM +12.6</td><td>0.007</td><td>12.9</td><td>736.9</td></tr></table>

Peer review (iclr2020):
This paper proposed to use a convex QP relaxed formulation to solve the neural network verification problem, and demonstrated its effectiveness on a few small networks (1-2 hidden layers) on MNIST and Fashion-MNIST datasets. There are several benefits the proposed methods: they are technically tighter relaxations of ReLU neurons and empirically the authors show they perform well in L2 norm (but not L infinity norm, unfortunately); solving this formulation does not require to know pre-activation bounds of hidden neurons; also the convexity of the QP problem needs to be determined only once for a model, rather than once per example. Although the QP relaxation of ReLU neuron is not new and has been used in Raghunathan et al., 2018b, they solve the problem as a SDP rather than convex QP. SDP is tighter than the convex QP formulation used in this paper, however is much slower. Issues and Questions: 1. The concept of *bi-direction verification* is not new, since finding an upper bound is basically finding adversarial examples. Many previous papers have been using PGD based attacks to obtain the upper bound. Convex relaxation based verification methods like CROWN can also be used for generating adversarial examples, and it is called *Interval attack*, which is demonstrated in [1][2]. Claiming this is the first *bi-direction robustness verification technique* is not accurate. 2. The use of FGSM as an upper bound is inappropriate, as FGSM is known to be a very weak attack. Replacing it with a multi-step PGD attack is necessary. Using a stronger attack will also close the gap between upper and lower bound. Also, compare the upper bound found by PGD with QPRel-LB and update Figure 3(a). If a stronger attack like PGD is used, I think for larger norms CROWN+PGD in Figure 3(c) should be able to verify almost all examples. 3. The models used in Table 1 is trained using a L2 perturbation of epsilon=0.1. This epsilon value is too small for L2 norm. In page 22 (last page of appendix in arxiv version) of [3], you can find the they conduct L2 robustness training but at a much larger epsilon value (eps=1.58). Sine the authors did not use these standard epsilon setting, my concern is that does the proposed method works at larger L2 epsilon? 4. Some experiments on larger and deeper networks are necessary; especially, it is interesting to see how CROWN and the proposed method scale to deeper networks. The presented experiments only include networks with 1 and 2 hidden layers, which is insufficient. A new experiment with number of hidden neurons per layer kept (say 50) and increase the depth from 2 to 10 will be very helpful. 5. The main claim of the paper in Introduction needs to be made clearer, especially the primary strength of the proposed algorithm is in L2 norm, and it does not seem to outperform CROWN in L infinity norm setting. Further improvements and potential directions: 1. In the proposed method, the authors relaxed ReLU neurons using quadratic programming. This relaxation does not require to computing bounds for the neuron activation values. However, I think it is possible to include neuron activation upper and lower bounds as constraints of the QP problem (adding them as constraints like l <= x <= u in Eq. QPRel). This will make the bounds tighter. The per-neuron lower and upper bounds can be obtained using CROWN efficiently, so there is no too much computation cost. 2. Improving the scalability of QP relaxation is another challenge. CROWN can be implemented efficiently on GPUs [4]. For QP relaxations, this can possibly be done by transforming QP solving into a computation graph that can be executed efficiently on GPUs (this is a potential future work directions and I do not expect the authors to address them during the discussion period). Overall I am positive with this paper, however before accepting it I think the authors should at least make their claims clearer (the relaxation performs well mainly in L2 norm, and the concept of *bi-directional verification* is also not entirely new), replacing FGSM by a 200-step PGD and compare the upper bound found by PGD with QPRel, and test the proposed algorithm in models trained with a larger epsilon (eps=1.58 to align with previous works, if possible) and deeper models. [1] Wang, S., Chen, Y., Abdou, A., & Jana, S. (2019). Enhancing Gradient-based Attacks with Symbolic Intervals. arXiv preprint arXiv:1906.02282. [2] Wang, S., Chen, Y., Abdou, A., & Jana, S. (1811). MixTrain: Scalable Training of Verifiably Robust Neural Networks. [3] Wong, E., Schmidt, F., Metzen, J. H., & Kolter, J. Z. (2018). Scaling provable adversarial defenses. In Advances in Neural Information Processing Systems (pp. 8400-8409). [4] https://github.com/huanzhang12/RecurJac-and-CROWN