Title: TRAINING PROVABLY ROBUST MODELS BY POLYHEDRAL ENVELOPE REGULARIZATION

Abstract: Training certifiable neural networks enables one to obtain models with robustness guarantees against adversarial attacks. In this work, we use a linear approximation to bound model's output given an input adversarial budget. This allows us to bound the adversary-free region in the data neighborhood by a polyhedral envelope and yields finer-grained certified robustness than existing methods. We further exploit this certifier to introduce a framework called polyhedral envelope regularization (PER), which encourages larger polyhedral envelopes and thus improves the provable robustness of the models. We demonstrate the flexibility and effectiveness of our framework on standard benchmarks; it applies to networks with general activation functions and obtains comparable or better robustness guarantees than state-of-the-art methods, with very little cost in clean accuracy, i.e., without over-regularizing the model.

1. INTRODUCTION:

Despite their great success in many applications, modern deep learning models are vulnerable to adversarial attacks: small but well-designed perturbations can make the state-of-the-art models predict wrong labels with very high confidence (Goodfellow et al., 2014; Moosavi-Dezfooli et al., 2017; Szegedy et al., 2013) . The existence of such adversarial examples indicates unsatisfactory properties of the deep learning models' decision boundary (He et al., 2018) , and poses a threat to the reliability of modern machine learning systems.

As a consequence, studying the robustness of deep learning has attracted growing attention, from the perspective of both attack and defense strategies. Popular attack algorithms, such as the fast gradient method (FGM) (Goodfellow et al., 2014) , the CW attack (Carlini & Wagner, 2017) and the projected gradient descent (PGD) algorithm (Madry et al., 2017) , typically exploit the gradient of the loss w.r.t. the input to generate adversarial examples. To counteract such attacks, many defense algorithms have been proposed (Buckman et al., 2018; Dhillon et al., 2018; Guo et al., 2017; Ma et al., 2018; Samangouei et al., 2018; Song et al., 2017; Xie et al., 2017) . However, it was shown in Athalye et al. (2018) that most of them depend on obfuscated gradients for perceived robustness. In other words, these methods train models to fool gradient-based attacks but do not achieve true robustness. As a consequence, they become ineffective when subjected to stronger attacks. The only exception is adversarial training (Madry et al., 2017) , which augments the training data with adversarial examples. Nevertheless, while adversarial training yields good empirical performance, it still provides no guarantees of a model's robustness.

In this work, we focus on constructing certifiers to find certified regions of the input neighborhood where the model is guaranteed to give the correct prediction, and on using such certifiers to train a model to be provably robust against adversarial attacks. In this context, complete certifiers can either guarantee the absence of an adversary or construct an adversarial example given an adversarial budget. They are typically built on either Satisfiability Modulo Theories (SMT) (Katz et al., 2017) or mixed integer programming (MIP) (Tjeng et al., 2017; Xiao et al., 2018) . The major disadvantages of complete certifiers are their super-polynomial complexity and applicability to only piecewise linear activation functions, such as ReLU. By contrast, incomplete certifiers are faster, more widely applicable but more conservative in terms of certified regions because they rely on approximations. Techniques such as linear approximation (Kolter & Wong, 2017; Wong et al., 2018; Zhang et al., 2018; Weng et al., 2018) , symbolic interval analysis (Wang et al., 2018b) , abstract transformers (Gehr et al., 2018; Singh et al., 2018; 2019) , semidefinite programming (SDP) (Raghunathan et al., 2018a; b) and randomized smoothing (Cohen et al., 2019; Salman et al., 2019a) are exploited to offer better certified robustness. Some of these methods enable training provably robust models (Raghunathan et al., 2018a; Kolter & Wong, 2017; Wong et al., 2018; Cohen et al., 2019; Salman et al., 2019a) by optimizing the parameters so as to maximize the area of the certified regions.

While effective, all the above-mentioned methods, in their vanilla version, only provide binary results given a fixed adversarial budget. That is, if a data point is certified, it is guaranteed to be robust in the entire given adversarial budget; otherwise no guaranteed adversary-free region is estimated. To overcome this and search for the optimal adversarial budget that can be certified, Kolter & Wong (2017) ; Weng et al. (2018) ; Zhang et al. (2018) use either Newton's method or binary search. By contrast, Croce et al. (2018) take advantage of the geometric property of ReLU networks and gives finer-grained robustness guarantees. Given the piecewise linear ReLU function, any input is located in a polytope where the ReLU network can be considered linear. Based on geometry, robustness guarantees can thus be calculated using the input distance to the polytope boundary and the decision boundary constraints. Unfortunately, in practice, the resulting certified bounds are trivial because such polytopes are very small even for robust models. Nevertheless, Croce et al. (2018) introduce a regularization scheme based on these bounds to effectively train provably robust models.

In this paper, we construct a stronger certifier, as well as a regularization scheme to train provably robust models. To this end, building upon the geometry-inspired idea of Croce et al. (2018) , we estimate a linear bound of the model's output given a predefined adversarial budget. Then, the condition to guarantee robustness inside this budget is also linear and forms a polyhedral envelope of the model's decision boundary. Similar to Croce et al. (2018) , the region contained in the polyhedral envelope and the adversarial budget is certified to be adversary-free. We then further exploit this certifier to design a regularization framework to train provably robust neural network models.

In short, our contributions are twofold. First, we design a geometric-inspired certification method giving finer-grained one-shot bounds than its counterparts (Kolter & Wong, 2017; Weng et al., 2018; Zhang et al., 2018) with little overhead and applies to general activation functions. More importantly, we propose a regularization scheme to train provably robust models. Compared with existing provable training methods, which have been found to over-regularize the model (Zhang et al., 2019) , our training framework yields competitive robustness guarantees while maintaining good performance on clean inputs. In the remainder of the paper, we call our certification method Polyhedral Envelope Certifier (PEC) and regularization scheme Polyhedral Envelope Regularizer (PER).

2. PRELIMINARIES:



2.1. NOTATION AND TERMINOLOGY:

For simplicity, we discuss our approach using a standard N -layer fully-connected network. Note, however, that it straightforwardly extends to any network topology that can be represented by a directed acyclic graph (DAG) in the same way as in (Liu et al., 2019) . A fully-connected network parameterized by

{W (i) , b (i) } N -1

i=1 can be expressed as

z (i+1) = W (i) ẑ(i) + b (i) i = 1, 2, ..., N -1 ẑ(i) = σ(z (i) ) i = 2, 3, ..., N -1 (1)

where z (i) and ẑ(i) are the pre-& post-activations of the i-th layer, respectively, and ẑ(1) def == x is the input of the network. An l p norm-based adversarial budget S (p) (x) is defined as the set i) and ẑ (i) represent the adversarial input and the corresponding pre-& post-activations. For layer i having n i neurons, we have

EQUATION

W (i) ∈ R ni+1×ni and b (i) ∈ R ni+1 .

Throughout this paper, underlines and bars are used to present lower and upper bounds of adversarial activations, respectively, i.e., z (i) ≤ z (i) ≤ z(i) . A "+" or "-" subscript indicates the positive or negative part of a tensor. We use [K] as the abbreviation for the set {1, 2, ..., K}.

2.2. MODEL LINEARIZATION:

Given an adversarial budget S (p) (x), we study the linear bound of the output logits z (N ) , given by

EQUATION

The linear coefficients introduced above can be calculated by iteratively estimating the bounds of intermediate layers and linearizing the activation functions. In Appendix A.1, we discuss this for several activation functions, including ReLU, sigmoid, tanh and arctan. Note that our method differs from Zhang et al. (2018) because we need the analytical form of the linear coefficients for training, which removes numerical methods such as binary search. The bounding algorithm trades off computational complexity and bound tightness. In this work, we study two such algorithms. One is based on Fast-Lin / CROWN (Weng et al., 2018; Zhang et al., 2018) . It has tighter bounds but high computational complexity. Another is inspired by the interval bound propagation (IBP) (Gowal et al., 2018) , which is faster but leads to looser bounds. The details of both algorithms are provided in Appendices A.2 and A.3. We briefly discuss the complexity of both algorithms in Section 5.

3. ALGORITHMS:



3.1. ROBUSTNESS GUARANTEES BY POLYHEDRAL ENVELOPE:

For an input point x with label c ∈ [K], a sufficient condition to guarantee robustness is that the lower bounds of z

(N ) c -z (N ) i are positive for all i ∈ [K].

Here, we use a trick called elision of the last layer (Gowal et al., 2018) to merge the subtraction of z 

(N ) c -z (N ) i : z (N ) c -z (N ) i def == U i x + p i .

Then, the sufficient condition to ensure robustness within a budget S (p) (x) can be written as

EQUATION

The constraint is trivial when i = c, so there are K -1 such linear constraints, corresponding to K -1 hyperplanes in the input space. Within the adversarial budget, these hyperplanes provide a polyhedral envelope of the true decision boundary. In the remainder of the paper, we use the term d ic to represent the distance between the input and the hyperplane defined in (3) and define d c = min i∈[K],i =c d ic as the distance between the input and the polyhedral envelope boundary. The distance can be based on different l p norms, and d ic = 0 when the input itself does not satisfy the inequality (3). Since (3) is a sufficient condition for robustness given the adversarial budget S (p) (x), there is no adversarial examples in the intersection of S (p) (x) and the polytope defined in (3).

The theorem below formalizes our robustness certification. We defer its proof to Appendix C.1. Theorem 1 (PEC in Unconstrained Cases). Given a model f : R n1 → [K] and an input point x with label c, let U and p in (3) be calculated using a predefined adversarial budget S (p) (x). Then, there is no adversarial example inside an l p norm ball of radius d centered around x, with d = min { , d c } where d ic = max 0, Uix+pi Ui q . l q is the dual norm of the l p norm, i.e.,1 p + 1 q = 1.

Based on Theorem 1, when < d c , PEC has the same robustness guarantees as KW (Kolter & Wong, 2017) , Fast-Lin (Weng et al., 2018) and CROWN (Zhang et al., 2018) if we use the same model linearization method. When 0 < d c < , KW / Fast-Lin / CROWN cannot certify the data point at all, while PEC still gives non-trivial robustness guarantees thanks to the geometric interpretability of the polyhedral envelope. Figure 1 (a) compares the certified bounds of KW / Fast-Lin and PEC on a randomly picked input for different values of .

Figure 1 (b) shows a 2D sketch of the two cases mentioned above. If is too small, as in the left portion of the figure, the linear bounds in (3) are tight but only valid in a small region S (p) (x). Therefore, the certified robustness is at most. If is too large, the linear bounds are valid in a larger region but more pessimistic because of linear approximation. 1 This is depicted by the right portion of the figure, where the distances between the input and the hyperplanes are smaller and the certified robustness is then d c . The hyperplane segments inside the adversarial budget (green lines) never exceed the decision boundary (dark blue lines), by definition of the polyhedral envelope. To search for the optimal , i.e., the peak in Figure 1 (a), Kolter & Wong (2017) use Newton's method, which is an expensive second-order method. By contrast, Weng et al. (2018) ; Zhang et al. (2018) use binary search, and our PEC can accelerate their strategy. The acceleration comes from the partial credit when 0 < d c < , in which case we can rule out all values of below d c and obtain a better lower bound of the optimal . A more detailed discussion is provided in Appendix B.1. Under many circumstances, the input is constrained in a hypercube [r (min) , r (max) ] n1 . For example, for images with normalized pixel values, an attacker should not perturb the image out of the hypercube [0, 1] n1 . Because of this constraint for the attacker, the certified regions become larger.

To obtain robustness guarantees in this scenario, we need to recalculate d ic , which is now the distance between the input and the hyperplanes in (3) within the hypercube. The value of d ic then is the minimum of the optimization problem

min ∆ ∆ p s.t. a∆ + b ≤ 0, ∆ (min) ≤ ∆ ≤ ∆ (max) (4)

where, to simplify the notation, we define a = U i , b = U i x + p, ∆ (min) = r (min)x and ∆ (max) = r (max)x. When b ≤ 0, the minimum is obviously 0 as the optimal ∆ is an all-zero vector. In this case, either we cannot certify the input at all or even the clean input is misclassified. When b > 0, by Hölder's inequality, a∆ + b ≥ -∆ p a q + b, with equality reached when ∆ p and a q are collinear. Based on this, the optimal ∆ of minimum l p norm to satisfy a∆ + b ≤ 0 is

EQUATION

where sign(•) returns +1 for positive numbers and -1 for negative numbers.

To satisfy the constraint ∆ (min) ≤ ∆ ≤ ∆ (max) , we use a greedy algorithm that approaches this goal progressively. That is, we first calculate the optimal ∆ based on Equation ( 5) and check if the constraint ∆ (min) ≤ ∆ ≤ ∆ (max) is satisfied. For the elements where it is not, we clip their values within [∆ (min) , ∆ (max) ] and keep them fixed. We then optimize the remaining elements of ∆ in the next iteration and repeat this process until the constraint is satisfied for all elements. The pseudo-code is provided as Algorithm 2 in Appendix B.2. The output of Algorithm 2 is the optimum of Problem (4), i.e., d ic . We provide the proof in Appendix C.2. The certified bound in this constrained case is then min{ , d c } just as demonstrated by Theorem 1.

3.2. GEOMETRY-INSPIRED REGULARIZATION:

As in (Croce et al., 2018) , we can incorporate our certification bounds in the training process so as to obtain more robust models. To this end, we design a regularization term that encourages larger values of d c . We first introduce the signed distance dic : when d ic > 0, the clean input satisfies (3) and dic = d ic ; when d ic = 0, the clean input does not satisfy (3) and there is no certified region; dic in this case is a negative number whose absolute value is the distance between the input and the hyperplane defined in (3). If the input is unconstrained, we have dic = Uix+pi Ui q . Otherwise, following the notation of (4), dic = sign(b) ∆ p , where ∆ = arg min ∆ ∆ p , s.t. a∆ + b = 0, ∆ (min) ≤ ∆ ≤ ∆ (max) . This problem can be solved by a greedy algorithm similar to the one in Section 3.1.

Now, we sort { dic } K-1 i=0,i =c as dj0c ≤ dj1c ≤ ... ≤ dj K-3 c ≤ dj K-2 c

and then define the Polyhedral Envelope Regularization (PER) term, based on smallest T distances, as

EQUATION

Note that, following Croce et al. (2018) , to accelerate training, we take into account the smallest T distances. When djic ≥ α, the distance is considered big enough, so the corresponding term will not contribute to the gradient of the model parameters. This avoids over-regularization and allows us to maintain accuracy on clean inputs. In practice, we do not activate PER in the early training stages, when the model is not well trained and the corresponding polyhedral envelope is meaningless. Such 'warm up' trick is commonly used in the deep learning practice (Gotmare et al., 2018) .

Note that we can further incorporate PER with adversarial training in a similar way to Croce et al. (2018) . The only change w.r.t. the original PER consists of replacing djic with d jic , the distance between the polyhedral envelope and the adversarial example generated by PGD (Madry et al., 2017) instead of the clean input. We call the corresponding method PER+at.

Calculating the polyhedral envelope is expensive in terms of both computation and memory because of the need to obtain linear bounds of the output logits. To prevent a prohibitive computational and memory overhead, we use the stochastic robust approximation of Wang et al. (2018a) . For a mini-batch of size B, we only calculate the PER or PER+at regularization term for B < B instances sub-sampled from this mini-batch. Moosavi-Dezfooli et al. (2017) empirically points out the geometric correlation of high-dimensional decision boundaries near the data manifold. Thus, in practice, a B much smaller than B provides a good approximation of the full-batch regularization.

4. EXPERIMENTS:

To validate the theory and algorithms above, we conducted several experiments on two popular image classification benchmarks: MNIST and CIFAR10. Each of these experiments can be completed on a single GPU machine within hours. We will make the code and checkpoints publicly available.

4.1. TRAINING AND CERTIFYING RELU NETWORKS:

As the main experiment, we first demonstrate the benefits of our approach over the state-of-the-art training and certification methods. To this end, we use the same model architectures as in Croce et al. (2018) ; Kolter & Wong (2017) : FC1, which is a fully-connected network with one hidden layer of 1024 neurons; and CNN, which has two convolutional layers followed by two fully-connected layers. For this set of experiments, all activation functions are ReLU.

We focus on training and certification method based on model linearization and compare 7 different training schemes using 5 evaluation metrics under the same and fixed adversarial budgets. All the certification results here are one-shot results as the binary search for optimal is not used. The 7 training schemes are plain training (plain), adversarial training (at) (Madry et al., 2017) , KW (Kolter & Wong, 2017) , MMR (Croce et al., 2018) , MMR plus adversarial training (MMR+at) (Croce et al., 2018) , and our PER and PER+at of Section 3.2. For certification, we compare Fast-Lin (Weng et al., 2018) , KW (Kolter & Wong, 2017) and our PEC introduced in Section 3.1. KW is algorithmically equivalent to Fast-Lin with elision of the last layer (Salman et al., 2019b) , so we consider them as one certification method. Based on the discussions in Section 3.1, all three methods have the same certified robust error, which is the proportion of the inputs whose certified regions are smaller than the adversarial budget. Therefore, we report the clean test error (CTE), empirical robust error against PGD (PGD), the certified robust error (CRE Lin), the average certified bound by Fast-Lin / KW (ACB KW) and by PEC (ACB PEC) on the test set. We do not report the certified bound by MMR (Croce et al., 2018) , because, in practice, it only gives trivial results. As a matter of fact, Croce et al. (2018) emphasize their training method and report certification results using KW and MIP (Tjeng et al., 2017) . For methods that are not based on model linearization, such as IBP (Gowal et al., 2018) and CROWN-IBP (Zhang et al., 2019) , we put more results and discussions in Table 5 of Appendix D.2.1.

We downloaded the KW, MMR and MMR+at models from the checkpoints provided by Croce et al. (2018) . 2 To be fair, we use the same model linearization method for our method. For CNN models, we use the warm up trick consisting of performing adversarial training before adding our PER or PER+at regularization term. The running time overhead of pre-training is negligible compared with computing the regularization term. We train all models for 100 epochs and provide the detailed hyper-parameter settings in Appendix D.1.

We consider robustness in both the l ∞ and l 2 case, and the attackers are constrained to perturb the images within [0, 1] n1 . To demonstrate the trade-off between clean test error and certified robust error, we evaluate our approach with different regularizer strength γ in (6). Figure 2 shows the results of PER+at in the l 2 case for CIFAR10. When γ is small, PER+at becomes similar to adversarial training (at) and has low clean test error but high certified robust error. As γ grows, the model is increasingly regularized towards large polyhedral envelopes, which inevitably hurts the performance on the clean input. By contrast, the certified robust error first decreases and then increases. This is because training is numerically more difficult when γ is too large and the model is over-regularized. The results of KW are shown as horizontal dashed lines for comparison, which evidences that PER+at is less over-regularized in general than KW, with much lower clean test error for the same certified robust error. The experimental results of PER / PER+at in Table 1 rely on the same model linearization methods as Fast-Lin / KW. Since our framework is applicable to any linearization strategy, we present the results using IBP-inspired linearization in Table 6 of Appendix D.2.2. Compared with Table 1 , we find IBP-inspired linearization has competitive performance during training, although it leads to a looser polyhedral envelope. In addition, IBP-inspired linearization has less memory consumption and computational complexity, so it is suitable for machines of limited computational resources.

4.2. TRAINING AND CERTIFYING NON-RELU NETWORKS:

To validate our method's applicability to non-ReLU networks, we replace the ReLU function in FC1 with either sigmoid, or tanh, or arctan function. While Wong et al. (2018) claim that their methods apply to non-ReLU networks, their main contribution is rather the extension of KW to a broader set of network architectures, and their public code3 does not support non-ReLU activations. Instead, we thus compare the average certified bound of CROWN (Zhang et al., 2018 ) (ACB CRO), which generalizes Fast-Lin to non-ReLU functions, with our PEC (ACB PEC). Since any linearization of activation functions can be plugged in both methods4 , we use the method in Appendix A.1. Under review as a conference paper at ICLR 2020

4.3. FINDING THE OPTIMAL BUDGET:

To obtain the biggest certified bound, we need to search for the optimal value of , i.e., the peak in Figure 1 (a). While Kolter & Wong (2017) use Newton's method to solve a constrained optimization problem, which is expensive, Fast-Lin / CROWN (Weng et al., 2018; Zhang et al., 2018) apply a binary search strategy to find the optimal .

To validate the claim in Section 3.1 that PEC can find the optimal faster than Fast-Lin / CROWN, we compare the average number of iterations needed to find the optimal value given a required precision ∆ . Using and ¯ to define the initial lower and upper estimates of the optimal value, then we need log 2 ¯ -∆ steps of bound calculation to obtain the optimal value by binary search in Fast-Lin / CROWN. By contrast, the number of iterations needed by PEC depends on the model to certify. The pseudo-code of the search algorithm is provided in Appendix B.1.

We briefly discuss the experimental results here, and defer their details to Appendix D.2.3. Note that, because PEC has almost no computational overhead compared with Fast-Lin and CROWN, the number of iterations reflects the running time to obtain the optimal certified bounds. Altogether, our results show that PEC can save on average 25% of the running time for FC1 models with ReLU, 15% for FC1 models with non-ReLU activations and 10% for CNN models.

5. DISCUSSION:

Let us consider an N -layer neural network model with k-dimensional output and m-dimensional input. For simplicity, let each hidden layer have n neurons and n max{k, m}. In this context, the bounding algorithm based on Fast-Lin / CROWN need O(N 2 n 3 ) FLOPs to obtain linear bounds of output logits. However, the complexity can be reduced to O(N n 2 m) at the cost of bound tightness when we use the IBP-inspired algorithm. In MMR (Croce et al., 2018) , the complexity to calculate the expression of the input's linear region is also O(N n 2 m). On the training side, KW needs a back-propagation to calculate the bound, which costs O(N n 2 ). MMR needs to calculate the distance between the input and O(N n) hyper-planes, costing O(N nm) FLOPs, while PER only calculates O(k) hyperplanes, thus requiring O(km) FLOPs. Overall, we can see that the estimation of the output logits or decision boundary dominates the complexity of all training algorithms and is the main barrier towards scalable provably robust training. The complexity of PER is similar to Fast-Lin / CROWN if we use the same model linearization method as theirs. When we use an IBP-inspired algorithm instead, the complexity of PER is similar to MMR. Note that the FLOP complexity of PGD with h iterations is O(N n 2 h) and typically h min{m, n}, so the overhead of the warm up phase is negligible for PER training.

No matter which linearization method we use, the bounds of the output logits inevitably become looser for deeper networks, which can be a problem for large models. Furthermore, the linear approximation implicitly favors the l ∞ norm over other l p norms because the intermediate bounds are calculated in an elementwise manner (Liu et al., 2019) . As a result, our method performs better in l ∞ cases than in l 2 cases. Designing a training algorithm with scalable and tight certified robustness is highly non-trivial and worth further exploration.

6. CONCLUSION:

In this paper, we have studied the robustness of neural networks from a geometric perspective. In our framework, linear bounds are estimated for the model's output under an adversarial budget. Then, the polyhedral envelope resulting from the linear bounds allows us to obtain quantitative robustness guarantees. Our certification method can give non-trivial robustness guarantees to more data points than existing methods. Furthermore, we have shown that our certified bounds can be turned into a geometry-inspired regularization scheme that enables training provably robust models. Compared with existing methods, our proposed framework can be applied to neural networks with general activation functions. Unlike many over-regularized methods, it can achieve provable robustness at very little loss in clean accuracy. Extending this framework to larger networks will be the focus of our future research.

A MODEL LINEARIZATION A.1 LINEARIZATION OF ACTIVATION FUNCTIONS:

In this section, we discuss the choice of d, l and h in the linear approximation dx+l ≤ σ(x) ≤ dx+h for activation function σ when x ∈ [x, x]. Method used here is slightly different from Zhang et al. (2018) . First, the slope of the linear upper and lower bound is the same for simplicity. Second, all coefficients need to have analytical form because we need to calculate the gradient based on them during training. Note that Zhang et al. (2018) use binary search for optimal d, l, h.

A.1.1 RELU:

As Figure 3 shows, the linear approximation for ReLU σ(x) = max(0, x), which is convex, is: A.1.2 SIGMOID, TANH, ARCTAN Unlike ReLU function, Tanh function σ(x) = e 2x -1 e 2x +1 , Sigmoid function σ(x) = 1 1+e -x and Arctan function σ(x) = arctan(x) are not convex. However, these three functions are convex when x < 0 and concave when x > 0. (Left and right sub-figures of Figure 4 ) Therefore, when x ≤ x ≤ 0 or 0 ≤ x ≤ x, we can easily obtain the tight linear approximation. When x ≤ 0 ≤ x, we do not use the binary research to obtain the tight linear approximation like Zhang et al. (2018) , because the results would not have an analytical form in this way. Instead, we first calculate the slope between the two ends i.e. d = σ(x)-σ(x)

d =        0 x ≤ x ≤ 0 x x -x x < 0 < x 1 0 ≤ x ≤ x , l = 0, h =        0 x ≤ x ≤ 0 - xx x -x x < 0 < x 0 0 ≤ x ≤ x (7) -6 -3 0 3 6 -3 0 3 6 (a) x ≤ x ≤ 0 -6 -3 0 3 6 -3 0 3 6 (b) x < 0 < x -6 -3 0 3 6 -3 0 3 6 (c) 0 ≤ x ≤ x

x-x

. Then, we bound the function by two tangent lines of the same slope as d (middle sub-figure of Figure 4 ). For Tanh, Sigmoid and Arctan, we can calculate the coefficient of the linear approximation.

d = σ(x) -σ(x) x -x , l =    σ(t 1 ) -t 1 d x < 0 xσ(x) -xσ(x) x -x 0 ≤ x ≤ x , h =    xσ(x) -xσ(x) x -x x ≤ x ≤ 0 σ(t 2 ) -t 2 d 0 < x (8)

The coefficient t 1 < 0 < t 2 are the position of tangent points on both sides of origin. The definitions of t 1 and t 2 for different activation functions provided in Table 3 .

σ Tanh Sigmoid Arctan t 1 1 2 log -(d-2)-2 √ 1-d d -log -(2d-1)+ √ 1-4d 2d -1 d -1 t 2 1 2 log -(d-2)+2 √ 1-d d -log -(2d-1)- √ 1-4d 2d 1 d -1

Table 3 : Definition of t1 and t2 for different activation functions.

A.2 BOUNDS BASED ON FAST-LIN / CROWN:

Based on the linear approximation of activation functions above, we have i) where D (i) is a diagonal matrix and l (i) , u (i) are vectors. We can re-write this formulation as follows:

D (i) z (i) +l (i) ≤ σ(z (i) ) ≤ D (i) z (i) + u (

∃D (i) , l (i) , u (i) : ∀z (i) ∈ [z (i) , z(i) ], ∃m (i) ∈ [l (i) , u (i) ] s.t.σ(z (i) ) = D (i) z (i) + m (i) (9)

We plug ( 9) into (1) and the expression of z (i) can be rewritten as

z (i) = W (i-1) (σ(W (i-2) (...σ(W (1) ẑ (1) + b (1) )...) + b (i-2) )) + b (i-1) = W (i-1) (D (i-1) (W (i-2) (...D (2) (W (1) x + b (1) ) + m (2) ...) + b (i-2) ) + m (i-1) ) + b (i-1) = i-1 k=1 W (k) D (k) W (1) x + i-1 j=1   i-1 k=j+1 W (k) D (k)   b (j) + i-1 j=2   i-1 k=j+1 W (k) D (k)   W (j) m (j) .

(10) This is a linear function w.r.t x and {m (j) } i-1 j=2 . Once given the perturbation budget S (p) (x) and the bounds of {m (j) } i-1 j=2 , we can calculate the bounds of z (i) and the bias term in (10). This process can be repeated until we obtain the bound of output logits (2). The derivation here is the same as Weng et al. ( 2018 2018) is a simple and scalable method to estimate the bounds of each layer in neural networks. IBP is much faster than algorithm introduced in Appendix A.2 because the bounds of any intermediate layer are calculated only based on the information of its immediate previous layer. Therefore, the bounds are propagated just like the inference of network models, which cost only O(N ) matrix-vector multiplications for a N -layer network defined in (1).

In our work, we need linear bounds of output logits in addition to general numeric bounds, so the linearization of activation functions defined in ( 9) is necessary. We define linear bounds U (i) x + p (i) ≤ z (i) ≤ U (i) x + q (i) , U (i) x + p(i) ≤ ẑ (i) ≤ U (i) x + q(i) . According to Section A.1, we use the same slope to linearize activation functions, so the slopes of both bounds here are the same. Plug (9) into this formulation, we have:

U (i) = D (i) U (i) , p(i) = D (i) p (i) + l (i) , q(i) = D (i) q (i) + u (i) (11)

Here, we assume activation functions are monotonic increasing, so elements in D (i) are non-negative. Similarity, compare the linear bounds of ẑ (i) and z (i+1) , we have:

U (i+1) = W (i) U (i) , p (i+1) = W (i) + p(i) + W (i) - q(i) + b (i) , q (i+1) = W (i) + q(i) + W (i) - p(i) + b (i) (12)

By definition, we have U (1) = I and p(1) = q(1) = 0. Apply ( 11) and ( 12) iteratively, we can obtain the values of coefficients U (N ) , V (N ) , p (N ) and q (N ) in (2).

B ALGORITHMS B.1 ALGORITHMS FOR SEARCH OPTIMAL:

The pseudo code for finding optimal is demonstrated as Algorithm 1 below. M, x, ∆ , , ¯ represent the classification model, the input point, precision requirement, predefined estimate of lower bound and upper bound respectively. Typically, is set 0 and ¯ is set a large value to which degree the image perturbation is perceptible. f is a function mapping a model, an input point and a value of to a certified bound. f is a generalization form of algorithm Fast-Lin, CROWN, PEC etc.

During the search for optimal , the lower bound is updated by current certified bound, while the upper bound is updated only when current certified bound is smaller than the choice of . In Fast-Lin and CROWN, we update either lower or upper bound in one iteration since the certified bound is either 0 or current choice of . However, it is possible for PEC to update both lower and upper bound in one iteration, which leads to a faster convergence of .

Algorithm 1: Search for optimal value of Input: x, , ¯ , ∆ , f , M Set the bounds of : up = ¯ , low = ;

while up -low > ∆ do try = 1 2 ( low + up ); cert = f (M, x, try ); Update lower bound: low = max{ low , cert }; if try > cert then

Update upper bound: ¯ = try ; end end Output: 1 2 ( low + up )

B.2 GREEDY ALGORITHM IN CONSTRAINED CASES:

We provide the pseudo code of greedy algorithm to solve problem (4) as Algorithm 2 below.

To prevent prohibitive computational overhead, we set the maximum iteration number I (max) of the while-loop. If this maximum number is met and the iteration is broken, then the output is a lower bound of the solution in problem (4) and thus still a valid but suboptimal robustness guarantee. In practice, we set the maximum iteration number to be 20, although the while-loop breaks within 5 iterations in almost all cases.

C PROOFS C.1 PROOF OF THEOREM 1:

Proof. We let x = x + ∆ be a point to break the condition (3).

Algorithm 2: Greedy algorithm to solve Problem (4).

Input: x, a, b, ∆ (min) , ∆ (max) in (4) and maximum iteration I (max) Set of fixed elements S (f ) = ∅; Iteration number i = 0; Calculate ∆ according to (5); while ∆ (min) ≤ ∆ ≤ ∆ (max) not satisfied and i < I (max) do Set of violated elements

EQUATION

The =⇒ comes from the Hölder's inequality. ( 13) indicates a perturbation of l p norm over d ic = max 0, Uix+pi Ui q is needed to break the sufficient condition of z

(N ) c -z (N ) i ≥ 0.

Based on the assumption of adversarial budget S (p) (x) when linearizing the model, so the l p norm of a perturbation to produce an adversarial example is at least min { , d c }.

C.2 PROOF OF THE OPTIMALITY OF GEEDY ALGORITHM:

Proof. We use primal-dual method to solve the optimization problem (4), which is a convex optimization problem with linear constraints.

It is clear that there exists an image inside the allowable pixel space which makes the model predict wrong label. That is to say, the constrained problem (4) is strictly feasible:

EQUATION

Thus, this convex optimization problem satisfies Slater's Condition i.e. strong duality holds. We then rewrite the primal problem as:

EQUATION

We minimize ∆ p p instead of directly ∆ p in order to decouple all elements in vector ∆. In addition, we consider ∆ (min) ≤ ∆ ≤ ∆ (max) as the domain of ∆ instead of constraints for simplicity. We write the dual problem of (15) by introducing a coefficient of relaxation λ ∈ R + .

EQUATION

To solve the inner minimization problem, we let the gradient ∂g(∆,λ) ∂∆i = sign(∆ i )p|∆ i | p-1 + λa i to be zero and obtain

∆ i = -sign(a i ) λai p 1 p-1

. Based on the convexity of function g(∆, λ) w.r.t. ∆, we can obtain the optimal ∆i in the domain.

∆i = clip -sign(a i ) λa i p 1 p-1 , min = ∆ (min) i , max = ∆ (max) i (17)

Based on the strong duality, we can say the optimal ∆ is chosen by setting a proper value of λ. Fortunately, ∆ p increases monotonically with λ, so the smallest λ corresponds to the optimum.

As we can see, the expression of ∆ in ( 5) is consistent with ∆i in (17) if λ is set properly.5 Greedy algorithm in Algorithm 2 is the process to gradually increase λ to find the smallest value satisfying constraint a∆ + b ≤ 0. With the increase of λ, elements in vector ∆ remain unchanged when they reach either ∆ (min) or ∆ (max) , so we keep such elements fixed and optimize the others.

D ADDITIONAL EXPERIMENTS:

D.1 DETAILS OF EXPERIMENTS D.1.1 MODEL ARCHITECTURE FC1 and CNN network used in this paper is identical to ones used in Croce et al. (2018) . FC1 network is a fully-connected network with one hidden layer of 1024 neurons. CNN network has two convolutional layers and one additional hidden layer before the output layer. Both convolutional layers have a kernel size of 4, stride of 2 and padding of 1 on both sides, so the height and width of feature maps are halved after each convolutional layer. The first convolutional layer has 32 channels while the second one has 16. The hidden layer following convolutional layers has 100 neurons.

D.1.2 HYPER-PARAMETER SETTINGS:

In all experiments, we use Adam optimizer (Kingma & Ba, 2014) with the initial learning rate 10 -3 and train all models for 100 epochs with a mini-batch of 100 instances. For CNN models, we decrease the learning rate to 10 -4 for last 10 epochs. When we train CNN models on MNIST, we only calculate the polyhedral envelope of 20 instances subsampled from each mini-batch. When we train CNN models on CIFAR10, this subsampling number is 10. For PER and PER+at, the value of T is always 4. We search in the logarithmic scale for the value of γ and in the linear scale for the value of α. For the value of , we ensure its final values are close to the ones used in the adversarial budget S (p) (x). We compare the constant values with exponential growth scheme for but always use constant values for α and γ. The optimal value we find for different settings are provided as Table 4 below.

D.2 ADDITIONAL EXPERIMENTAL RESULTS:



D.2.1 ADDITIONAL RESULTS OF THE MAIN EXPERIMENT:

We show additional results including IBP (Gowal et al., 2018) and CROWN-IBP (C-IBP) (Zhang et al., 2019) in Table 5 . We also report the certified robust error obtained by IBP (CRE IBP) and the corresponding average certified bound (ACB IBP). Consistent with Zhang et al. (2019) , we find IBP has non-trivial certification results only on models that are trained by IBP or CROWN-IBP. For these models, IBP can have even better certification results than Fast-Lin / KW / PEC, whose complexity are significantly higher. As mentioned in Liu et al. (2019) The distribution of certified bounds of CIFAR10 model against l ∞ attack are shown in Figure 6 . We only consider the certified bounds strictly larger than 0 but smaller than , which are non-trivial bounds not obtained by one-shot Fast-Lin / KW. For the CIFAR10 test set, there are 10% -20% of such points, and their certified bounds are close to being uniformly distributed between 0 and .

We show the histogram of parameter values for CIFAR10 models trained by KW, MMR+at and PER+at. It is clear that the parameter values of KW models are much more concentrated around 0 than those of PER+at models. For both l ∞ and l 2 attacks, the PER+at model has the biggest norms, evidencing that it better uses the model capacity.

As we can see in Equation 6, our proposed hinge-loss based PER is a constant and does not contribute to the parameter update when djic is greater than α, which is usually . It means that when a data point is robust enough against the adversarial attack, PER will not push the decision boundary further away from it. However, KW has a cross-entropy based loss. It will always further push the output logits of the true label bigger and the others smaller. Figure 7 shows the distribution of optimal found by Algorithm 1 for CIFAR10 models against l ∞ and l 2 attacks. Table 1 shows that KW and PER+at have similar certified robust error, which is the area on the right of the vertical red line in Figure 7 . Because of the property of cross-entropy loss, KW pushes too many points far beyond the robustness target we set. This is unnecessary and causes the loss of clean accuracy.

D.2.2 TRAINING BY IBP-INSPIRED MODEL LINEARIZATION:

We use ReLU networks to compare the performance of IBP-inspired model linearization with the ones used in Fast-Lin / CROWN. We observed that the hyper-parameter settings in Table 4 are ill-suited here. Specifically, since the estimation bounds of the output logits is looser, the gradient of the PER term based on IBP-inspired linearization is larger than in the main experiments. As a result, we used a value γ of 3 or 10 times smaller than those in Table 4 . Furthermore, starting with a large might not work, because the bounds will be even looser under a big adversarial budget. So, we adopt a 'warm up' scheme consisting of increasing the value of linearly until it reaches the desired value.

We provide the results in Table 6 below. Note that we still use the tighter linearization method of Fast-Lin / CROWN when we run our certification method (PEC). Despite the looser polyhedral envelope during training, the IBP-inspired model linearization achieves competitive performance with the ones in Fast-Lin / CROWN. In some cases, it has even better performance on the test set. Because of the lower computational complexity and smaller memory consumption, the IBP-inspired method is suitable for machines with limited computational resources.

D.2.3 SEARCHING FOR THE OPTIMAL VALUE OF:

Tables 7 and 8 show the number of bound calculations in the binary search for the optimal in PEC and Fast-Lin / CROWN. In l ∞ cases, the original interval [ , ¯ ] is [0, 0.4] for MNIST and [0, 0.1] for CIFAR10. In l 2 cases, the original interval [ , ¯ ] is [0, 1.2] for MNIST and [0, 0.4] for CIFAR10. The bound of the number calculation does not depend on the model in Fast-Lin / CROWN and is model-dependent in PEC as discussed in Section 4.3. 

:

The value of dic monotonically decreases with the increase of .

Repository: https://github.com/max-andr/provable-robustness-max-linear-regions.

Repository: https://github.com/locuslab/convex adversarial

For certification, there is no need to require an analytical form of the linearization.

The power term q p = 1 p-1 when 1 p + 1 q = 1

Figures and Tables:

linear layer and obtain the lower bound of z

Certified l∞-based bound of a randomly picked input by PEC and KW / Fast-Lin for different values of . The model is the 'FC1' on MNIST trained by 'MMR+at' in Croce et al. (2018) (b) 2D sketch of decision boundary (dark blue), hyperplane defined by (3) (light blue), adversarial budget (red), polyhedral envelope (green) in PEC. The distance between the input data and the hyperplanes is depicted by a yellow circle. The left and right portion correspond to dc bigger and smaller than respectively.

Figure 1: The two phases in PEC algorithm.

Figure 2: CTE and CRE for different values of γ in PER+at. The results of KW, for reference, are the horizontal dashed lines.

Figure 3: The linearization of ReLU function in all scenarios.

Figure 4: The linearization of Sigmoid function in all scenarios.

); Liu et al. (2019), we encourage interested readers to check these works for details. A.3 BOUNDS INSPIRED BY INTERVAL BOUND PROPAGATION Interval Bound Propagation (IBP) introduced in Gowal et al. (

Figure 5: Distributions of certified bounds in (0, ) for CIFAR10 models trained against l∞ attacks. The total numbers of such test points are 1045, 2162, 1396, 1122, 1489 for KW, MMR, MMR+at, PER, PER+at models, respectively.

Figure 7: The distribution of optimal certified bounds of CIFAR10 models trained against l∞ and l2 attacks. The target bounds are marked as a red vertical line. (2/255 for l∞ cases and 0.1 for l2 cases.)

Results

Table content: <table><tr><td/><td>CTE</td><td>PGD</td><td>CRE</td><td>ACB</td><td>ACB</td><td>CTE</td><td>PGD</td><td>CRE</td><td>ACB</td><td>ACB</td></tr><tr><td/><td>(%)</td><td>(%)</td><td>Lin</td><td>KW</td><td>PEC</td><td>(%)</td><td>(%)</td><td>Lin</td><td>KW</td><td>PEC</td></tr><tr><td/><td/><td/><td>(%)</td><td/><td/><td/><td/><td>(%)</td><td/></tr><tr><td/><td colspan="5">MNIST -FC1, ReLU, l∞, = 0.1</td><td colspan="5">MNIST -FC1, ReLU, l2, = 0.3</td></tr><tr><td>plain</td><td>1.99</td><td>98.37</td><td colspan="3">100.00 0.0000 0.0000</td><td>1.99</td><td>9.81</td><td>40.97</td><td colspan="2">0.1771 0.2300</td></tr><tr><td>at</td><td>1.42</td><td>9.00</td><td>97.94</td><td colspan="2">0.0021 0.0099</td><td>1.35</td><td>2.99</td><td>14.85</td><td colspan="2">0.2555 0.2684</td></tr><tr><td>KW</td><td>2.26</td><td>8.59</td><td>12.91</td><td colspan="2">0.0871 0.0928</td><td>1.23</td><td>2.70</td><td>4.91</td><td colspan="2">0.2853 0.2892</td></tr><tr><td>MMR</td><td>2.11</td><td>17.82</td><td>33.75</td><td colspan="2">0.0663 0.0832</td><td>2.40</td><td>5.88</td><td>7.76</td><td colspan="2">0.2767 0.2845</td></tr><tr><td>MMR+at</td><td>2.04</td><td>10.39</td><td>17.64</td><td colspan="2">0.0824 0.0905</td><td>1.77</td><td>3.76</td><td>5.68</td><td colspan="2">0.2830 0.2880</td></tr><tr><td>PER</td><td>1.60</td><td>7.45</td><td>11.71</td><td colspan="2">0.0883 0.0935</td><td>1.26</td><td>2.44</td><td>5.35</td><td colspan="2">0.2840 0.2888</td></tr><tr><td>PER+at</td><td>1.81</td><td>7.73</td><td>12.90</td><td colspan="2">0.0871 0.0925</td><td>0.67</td><td>1.40</td><td>4.84</td><td colspan="2">0.2855 0.2910</td></tr><tr><td/><td colspan="5">MNIST -CNN, ReLU, l∞, = 0.1</td><td colspan="5">MNIST -CNN, ReLU, l2, = 0.3</td></tr><tr><td>plain</td><td>1.28</td><td>85.75</td><td colspan="3">100.00 0.0000 0.0000</td><td>1.28</td><td>4.93</td><td colspan="3">100.00 0.0000 0.0000</td></tr><tr><td>at</td><td>1.02</td><td>4.75</td><td>91.91</td><td colspan="2">0.0081 0.0189</td><td>1.12</td><td>2.50</td><td colspan="3">100.00 0.0000 0.0000</td></tr><tr><td>KW</td><td>1.21</td><td>3.03</td><td>4.44</td><td colspan="2">0.0956 0.0971</td><td>1.11</td><td>2.05</td><td>5.84</td><td colspan="2">0.2825 0.2861</td></tr><tr><td>MMR</td><td>1.65</td><td>6.09</td><td>11.56</td><td colspan="2">0.0884 0.0928</td><td>2.57</td><td>5.49</td><td>10.03</td><td colspan="2">0.2699 0.2788</td></tr><tr><td>MMR+at</td><td>1.19</td><td>3.35</td><td>9.49</td><td colspan="2">0.0905 0.0939</td><td>1.73</td><td>3.22</td><td>9.46</td><td colspan="2">0.2716 0.2780</td></tr><tr><td>PER</td><td>1.44</td><td>3.44</td><td>5.13</td><td colspan="2">0.0949 0.0965</td><td>1.02</td><td>1.87</td><td>5.04</td><td colspan="2">0.2849 0.2882</td></tr><tr><td>PER+at</td><td>0.50</td><td>2.02</td><td>4.85</td><td colspan="2">0.0952 0.0969</td><td>0.43</td><td>0.91</td><td>5.43</td><td colspan="2">0.2837 0.2878</td></tr><tr><td/><td colspan="5">CIFAR10 -CNN, ReLU, l∞, = 2/255</td><td colspan="5">CIFAR10 -CNN, ReLU, l2, = 0.1</td></tr><tr><td>plain</td><td>24.62</td><td>86.29</td><td colspan="3">100.00 0.0000 0.0000</td><td>23.29</td><td>47.39</td><td colspan="3">100.00 0.0000 0.0000</td></tr><tr><td>at</td><td>27.04</td><td>48.53</td><td>85.36</td><td colspan="2">0.0011 0.0015</td><td>25.84</td><td>35.81</td><td>99.96</td><td colspan="2">0.0000 0.0000</td></tr><tr><td>KW</td><td>39.27</td><td>48.16</td><td>53.81</td><td colspan="2">0.0036 0.0040</td><td>40.24</td><td>43.87</td><td>48.98</td><td colspan="2">0.0510 0.0533</td></tr><tr><td>MMR</td><td>34.59</td><td>57.17</td><td>69.28</td><td colspan="2">0.0024 0.0032</td><td>40.93</td><td>50.57</td><td>57.07</td><td colspan="2">0.0429 0.0480</td></tr><tr><td>MMR+at</td><td>35.36</td><td>49.27</td><td>59.91</td><td colspan="2">0.0031 0.0037</td><td>37.78</td><td>43.98</td><td>53.33</td><td colspan="2">0.0467 0.0502</td></tr><tr><td>PER</td><td>39.21</td><td>50.98</td><td>57.45</td><td colspan="2">0.0033 0.0038</td><td>34.10</td><td>52.54</td><td>63.42</td><td colspan="2">0.0369 0.0465</td></tr><tr><td>PER+at</td><td>28.87</td><td>43.55</td><td>56.59</td><td colspan="2">0.0034 0.0040</td><td>25.76</td><td>33.47</td><td>46.74</td><td colspan="2">0.0533 0.0580</td></tr></table>

Table1shows the results with the same adversarial budget used inCroce et al. (2018). Consistently with Section 3.1, our geometry-inspired PEC has better average certified bounds than Fast-Lin / KW given the same adversarial budget. For CIFAR10 model against l ∞ attack, there are 10% -20% test points not certified by Fast-Lin / KW but have non-trivial bounds by PEC. Figure5of Appendix D.2.1 shows the distribution of these certified bounds. Among the training methods, PER / PER+at give better performance in all cases than MMR / MMR+at. When compared with KW, their certified robust error is comparable, but PER+at has better clean test accuracy, particularly on CIFAR10. In fact, PER+at maintains a similar clean test error to adversarial training (at) while achieving competitive certified robust error. In other words, a model trained by PER+at is not as over-regularized as other training methods for provable robustness. Figure6 of

Table content: <table/>

Results of FC1 models with non-ReLU activation functions on MNIST.

Table content: <table><tr><td/><td>CTE</td><td>PGD</td><td>CRE</td><td>ACB</td><td>ACB</td><td>CTE</td><td>PGD</td><td>CRE</td><td>ACB</td><td>ACB</td></tr><tr><td/><td>(%)</td><td>(%)</td><td>Lin</td><td>CRO</td><td>PEC</td><td>(%)</td><td>(%)</td><td>Lin</td><td>CRO</td><td>PEC</td></tr><tr><td/><td/><td/><td>(%)</td><td/><td/><td/><td/><td>(%)</td><td/></tr><tr><td/><td colspan="5">MNIST -FC1, Sigmoid, l∞, = 0.1</td><td colspan="5">MNIST -FC1, Sigmoid, l2, = 0.3</td></tr><tr><td>plain</td><td>2.04</td><td>97.80</td><td colspan="3">100.00 0.0000 0.0000</td><td>2.01</td><td>10.25</td><td>30.78</td><td colspan="2">0.2077 0.2539</td></tr><tr><td>at</td><td>1.78</td><td>10.05</td><td>98.52</td><td colspan="2">0.0015 0.0055</td><td>1.65</td><td>3.48</td><td>7.50</td><td colspan="2">0.2775 0.2839</td></tr><tr><td>PER</td><td>2.29</td><td>8.44</td><td>15.75</td><td colspan="2">0.0843 0.0908</td><td>1.19</td><td>2.36</td><td>7.08</td><td colspan="2">0.2787 0.2849</td></tr><tr><td>PER+at</td><td>2.46</td><td>8.14</td><td>15.00</td><td colspan="2">0.0850 0.0906</td><td>0.67</td><td>1.25</td><td>6.93</td><td colspan="2">0.2792 0.2868</td></tr><tr><td/><td colspan="5">MNIST -FC1, Tanh, l∞, = 0.1</td><td/><td colspan="3">MNIST -FC1, Tanh, l2, = 0.3</td></tr><tr><td>plain</td><td>2.00</td><td>99.57</td><td colspan="3">100.00 0.0000 0.0000</td><td>1.94</td><td>16.46</td><td>61.66</td><td colspan="2">0.1150 0.1789</td></tr><tr><td>at</td><td>1.28</td><td>8.89</td><td>99.98</td><td colspan="2">0.0000 0.0001</td><td>1.36</td><td>3.02</td><td>12.35</td><td colspan="2">0.2630 0.2735</td></tr><tr><td>PER</td><td>2.66</td><td>9.31</td><td>16.02</td><td colspan="2">0.0840 0.0908</td><td>1.39</td><td>2.73</td><td>7.56</td><td colspan="2">0.2773 0.2834</td></tr><tr><td>PER+at</td><td>2.73</td><td>8.45</td><td>14.99</td><td colspan="2">0.0850 0.0907</td><td>0.81</td><td>1.76</td><td>11.80</td><td colspan="2">0.2646 0.2745</td></tr><tr><td/><td colspan="5">MNIST -FC1, ArcTan, l∞, = 0.1</td><td colspan="5">MNIST -FC1, ArcTan, l2, = 0.3</td></tr><tr><td>plain</td><td>1.95</td><td>99.83</td><td colspan="3">100.00 0.0000 0.0000</td><td>2.09</td><td>23.00</td><td>62.82</td><td colspan="2">0.1115 0.1869</td></tr><tr><td>at</td><td>1.33</td><td>8.88</td><td>99.92</td><td colspan="2">0.0001 0.0005</td><td>1.56</td><td>3.04</td><td>10.10</td><td colspan="2">0.2697 0.2784</td></tr><tr><td>PER</td><td>2.78</td><td>9.55</td><td>16.75</td><td colspan="2">0.0833 0.0904</td><td>1.42</td><td>2.66</td><td>7.81</td><td colspan="2">0.2766 0.2828</td></tr><tr><td>PER+at</td><td>2.98</td><td>8.96</td><td>15.64</td><td colspan="2">0.0844 0.0901</td><td>0.83</td><td>1.61</td><td>11.38</td><td colspan="2">0.2659 0.2758</td></tr></table>

, IBP and Fast-Lin are complementary. Our PER and PER+at algorithms still outperform IBP and CROWN-IBP.

Table content: <table><tr><td/><td>α</td><td/><td>γ</td></tr><tr><td>MNIST -FC1, l ∞ MNIST -CNN, l ∞</td><td>constant, 0.15 constant, 0.15</td><td>initial value 0.0064 ×2 every 20 epochs constant, 0.1</td><td>constant, 0.1 constant, 0.3 for PER constant, 0.03 for PER+at</td></tr><tr><td>CIFAR10 -CNN, l ∞ MNIST -FC1, l 2 MNIST -CNN, l 2</td><td>constant, 0.1 constant, 0.45 constant, 0.45</td><td>constant, 0.008 initial value 0.02 ×2 every 20 epochs constant, 0.3</td><td>constant, 3 × 10 -4 for PER constant, 1 × 10 -3 for PER+at constant, 1.0 constant, 1.0</td></tr><tr><td colspan="2">CIFAR10 -CNN, l 2 constant, 0.15</td><td>constant, 0.1</td><td>constant, 0.3 for PER constant, 1.0 for PER+at</td></tr></table>

Values of α, and γ for different experiments.

Table content: <table><tr><td/><td>CTE</td><td>PGD</td><td>CRE</td><td>CRE</td><td>ACB</td><td>ACB</td><td>ACB</td><td>CTE</td><td>PGD</td><td>CRE</td><td>CRE</td><td>ACB</td><td>ACB</td><td>ACB</td></tr><tr><td/><td>(%)</td><td>(%)</td><td>Lin</td><td>IBP</td><td>KW</td><td>IBP</td><td>PEC</td><td>(%)</td><td>(%)</td><td>Lin</td><td>IBP</td><td>KW</td><td>IBP</td><td>PEC</td></tr><tr><td/><td/><td/><td>(%)</td><td>(%)</td><td/><td/><td/><td/><td/><td>(%)</td><td>(%)</td><td/><td/></tr><tr><td/><td/><td colspan="5">MNIST -FC1, ReLU, l∞, = 0.1</td><td/><td/><td colspan="5">MNIST -FC1, ReLU, l2, = 0.3</td></tr><tr><td>plain</td><td>1.99</td><td>98.37</td><td colspan="5">100.00 100.00 0.0000 0.0000 0.0000</td><td>1.99</td><td>9.81</td><td>40.97</td><td>99.30</td><td colspan="3">0.1771 0.0021 0.2300</td></tr><tr><td>at</td><td>1.42</td><td>9.00</td><td>97.94</td><td colspan="4">100.00 0.0021 0.0000 0.0099</td><td>1.35</td><td>2.99</td><td>14.85</td><td>99.23</td><td colspan="3">0.2555 0.0023 0.2684</td></tr><tr><td>KW</td><td>2.26</td><td>8.59</td><td>12.91</td><td>69.20</td><td colspan="3">0.0871 0.0308 0.0928</td><td>1.23</td><td>2.70</td><td>4.91</td><td>41.55</td><td colspan="3">0.2853 0.1754 0.2892</td></tr><tr><td>IBP</td><td>1.65</td><td>9.67</td><td>87.27</td><td>15.20</td><td colspan="3">0.0127 0.0848 0.0705</td><td>1.36</td><td>2.90</td><td>6.87</td><td>9.01</td><td colspan="3">0.2794 0.2730 0.2876</td></tr><tr><td>C-IBP</td><td>1.98</td><td>9.50</td><td>67.39</td><td>14.45</td><td colspan="3">0.0326 0.0855 0.0800</td><td>1.26</td><td>2.80</td><td>6.36</td><td>8.73</td><td colspan="3">0.2809 0.2738 0.2884</td></tr><tr><td>MMR</td><td>2.11</td><td>17.82</td><td>33.75</td><td>99.88</td><td colspan="3">0.0663 0.0001 0.0832</td><td>2.40</td><td>5.88</td><td>7.76</td><td>99.55</td><td colspan="3">0.2767 0.0013 0.2845</td></tr><tr><td>MMR+at</td><td>2.04</td><td>10.39</td><td>17.64</td><td>95.09</td><td colspan="3">0.0824 0.0049 0.0905</td><td>1.77</td><td>3.76</td><td>5.68</td><td>99.86</td><td colspan="3">0.2830 0.0004 0.2880</td></tr><tr><td>PER</td><td>1.60</td><td>7.45</td><td>11.71</td><td>92.89</td><td colspan="3">0.0883 0.0071 0.0935</td><td>1.26</td><td>2.44</td><td>5.35</td><td>59.17</td><td colspan="3">0.2840 0.1225 0.2888</td></tr><tr><td>PER+at</td><td>1.81</td><td>7.73</td><td>12.90</td><td>99.90</td><td colspan="3">0.0871 0.0001 0.0925</td><td>0.67</td><td>1.40</td><td>4.84</td><td>64.79</td><td colspan="3">0.2855 0.1056 0.2910</td></tr><tr><td/><td/><td colspan="5">MNIST -CNN, ReLU, l∞, = 0.1</td><td/><td/><td colspan="5">MNIST -CNN, ReLU, l2, = 0.3</td></tr><tr><td>plain</td><td>1.28</td><td>85.75</td><td colspan="5">100.00 100.00 0.0000 0.0000 0.0000</td><td>1.28</td><td>4.93</td><td colspan="5">100.00 100.00 0.0000 0.0000 0.0000</td></tr><tr><td>at</td><td>1.02</td><td>4.75</td><td>91.91</td><td colspan="4">100.00 0.0081 0.0000 0.0189</td><td>1.12</td><td>2.50</td><td colspan="5">100.00 100.00 0.0000 0.0000 0.0000</td></tr><tr><td>KW</td><td>1.21</td><td>3.03</td><td>4.44</td><td colspan="4">100.00 0.0956 0.0000 0.0971</td><td>1.11</td><td>2.05</td><td>5.84</td><td colspan="4">100.00 0.2825 0.0000 0.2861</td></tr><tr><td>IBP</td><td>1.51</td><td>4.43</td><td>23.89</td><td>8.13</td><td colspan="3">0.0761 0.0919 0.0872</td><td>2.37</td><td>3.85</td><td>51.12</td><td>11.73</td><td colspan="3">0.1534 0.2648 0.1669</td></tr><tr><td>C-IBP</td><td>1.85</td><td>4.28</td><td>10.72</td><td>6.91</td><td colspan="3">0.0893 0.0931 0.0928</td><td>2.89</td><td>4.44</td><td>31.62</td><td>12.29</td><td colspan="3">0.2051 0.2631 0.2178</td></tr><tr><td>MMR</td><td>1.65</td><td>6.09</td><td>11.56</td><td colspan="4">100.00 0.0884 0.0000 0.0928</td><td>2.57</td><td>5.49</td><td>10.03</td><td colspan="4">100.00 0.2699 0.0000 0.2788</td></tr><tr><td>MMR+at</td><td>1.19</td><td>3.35</td><td>9.49</td><td colspan="4">100.00 0.0905 0.0000 0.0939</td><td>1.73</td><td>3.22</td><td>9.46</td><td colspan="4">100.00 0.2716 0.0000 0.2780</td></tr><tr><td>PER</td><td>1.44</td><td>3.44</td><td>5.13</td><td colspan="4">100.00 0.0949 0.0000 0.0965</td><td>1.02</td><td>1.87</td><td>5.04</td><td colspan="4">100.00 0.2849 0.0000 0.2882</td></tr><tr><td>PER+at</td><td>0.50</td><td>2.02</td><td>4.85</td><td colspan="4">100.00 0.0952 0.0000 0.0969</td><td>0.43</td><td>0.91</td><td>5.43</td><td colspan="4">100.00 0.2837 0.0000 0.2878</td></tr><tr><td/><td/><td colspan="5">CIFAR10 -CNN, ReLU, l∞, = 2/255</td><td/><td/><td colspan="5">CIFAR10 -CNN, ReLU, l2, = 0.1</td></tr><tr><td>plain</td><td>24.62</td><td>86.29</td><td colspan="6">100.00 100.00 0.0000 0.0000 0.0000 23.29</td><td>47.39</td><td colspan="5">100.00 100.00 0.0000 0.0000 0.0000</td></tr><tr><td>at</td><td>27.04</td><td>48.53</td><td>85.36</td><td colspan="5">100.00 0.0011 0.0000 0.0015 25.84</td><td>35.81</td><td>99.96</td><td colspan="4">100.00 0.0000 0.0000 0.0000</td></tr><tr><td>KW</td><td>39.27</td><td>48.16</td><td>53.81</td><td>99.98</td><td colspan="4">0.0036 0.0000 0.0040 40.24</td><td>43.87</td><td>48.98</td><td colspan="4">100.00 0.0510 0.0000 0.0533</td></tr><tr><td>IBP</td><td>46.74</td><td>56.38</td><td>61.81</td><td>67.58</td><td colspan="4">0.0030 0.0025 0.0034 57.90</td><td>60.03</td><td>64.78</td><td>78.13</td><td colspan="3">0.0352 0.0219 0.0366</td></tr><tr><td>C-IBP</td><td>58.32</td><td>63.56</td><td>66.28</td><td>69.10</td><td colspan="4">0.0026 0.0024 0.0029 71.21</td><td>72.51</td><td>76.23</td><td>80.97</td><td colspan="3">0.0238 0.0190 0.0256</td></tr><tr><td>MMR</td><td>34.59</td><td>57.17</td><td>69.28</td><td colspan="5">100.00 0.0024 0.0000 0.0032 40.93</td><td>50.57</td><td>57.07</td><td colspan="4">100.00 0.0429 0.0000 0.0480</td></tr><tr><td>MMR+at</td><td>35.36</td><td>49.27</td><td>59.91</td><td colspan="5">100.00 0.0031 0.0000 0.0037 37.78</td><td>43.98</td><td>53.33</td><td colspan="4">100.00 0.0467 0.0000 0.0502</td></tr><tr><td>PER</td><td>39.21</td><td>50.98</td><td>57.45</td><td>99.98</td><td colspan="4">0.0033 0.0000 0.0038 34.10</td><td>52.54</td><td>63.42</td><td colspan="4">100.00 0.0369 0.0000 0.0465</td></tr><tr><td>PER+at</td><td>28.87</td><td>43.55</td><td>56.59</td><td colspan="5">100.00 0.0034 0.0000 0.0040 25.76</td><td>33.47</td><td>46.74</td><td colspan="4">100.00 0.0533 0.0000 0.0580</td></tr></table>

Full results of 9 training schemes and 7 evaluation schemes for ReLU networks.

Table content: <table/>

The Euclidiean norm of parameter for KW, MMR+at, PER+at model against l∞ attack is 18.08, 38.36 and 94.63 respectively. For models against l2 attack, the corresponding Euclidiean norm is 71.34, 62.97 and 141.77 respectively. Optimal Bound Distribution for CIFAR10 Model against l∞ Attack Optimal Bound Distribution for CIFAR10 Model against l2 Attack

Table content: <table><tr><td/><td>2.00</td><td colspan="8">×10 2 KW</td><td/><td>2.00</td><td colspan="7">×10 2 KW</td></tr><tr><td/><td/><td/><td/><td/><td/><td/><td/><td/><td colspan="2">MMR+at</td><td/><td/><td/><td/><td/><td/><td/><td>MMR+at</td></tr><tr><td/><td>1.75</td><td/><td/><td/><td/><td/><td/><td/><td>PER+at</td><td/><td>1.75</td><td/><td/><td/><td/><td/><td/><td>PER+at</td></tr><tr><td/><td>1.50</td><td/><td/><td/><td/><td/><td/><td/><td/><td/><td>1.50</td><td/><td/><td/><td/><td/><td/></tr><tr><td>Number of Test Points</td><td>0.75 1.00 1.25</td><td/><td/><td/><td/><td/><td/><td/><td/><td>Number of Test Points</td><td>0.75 1.00 1.25</td><td/><td/><td/><td/><td/><td/></tr><tr><td/><td>0.50</td><td/><td/><td/><td/><td/><td/><td/><td/><td/><td>0.50</td><td/><td/><td/><td/><td/><td/></tr><tr><td/><td>0.25</td><td/><td/><td/><td/><td/><td/><td/><td/><td/><td>0.25</td><td/><td/><td/><td/><td/><td/></tr><tr><td/><td>0.00</td><td/><td/><td/><td/><td/><td/><td/><td/><td/><td>0.00</td><td/><td/><td/><td/><td/><td/></tr><tr><td/><td colspan="2">0.000</td><td>0.005</td><td>0.010</td><td>0.015</td><td>0.020</td><td>0.025</td><td>0.030</td><td>0.035</td><td>0.040</td><td colspan="2">0.00</td><td>0.05</td><td>0.10</td><td>0.15</td><td>0.20</td><td>0.25</td><td>0.30</td><td>0.35</td><td>0.40</td></tr><tr><td/><td/><td/><td/><td/><td/><td>Values</td><td/><td/><td/><td/><td/><td/><td/><td/><td/><td>Values</td><td/></tr></table>

Results when using IBP-inspired model linearization. The color green, red and gray indicate better, worse and same results compared to those in Table1

Table content: <table><tr><td/><td>CTE</td><td>PGD</td><td>Change</td><td>CRE</td><td>Change</td><td>ACB</td><td colspan="2">Change ACB</td><td colspan="2">Change</td></tr><tr><td/><td>(%)</td><td>(%)</td><td>(%)</td><td>(%)</td><td>(%)</td><td>KW</td><td/><td>PEC</td><td/></tr><tr><td/><td/><td/><td colspan="5">MNIST -FC1, ReLU, l∞. = 0.1</td><td/><td/></tr><tr><td>PER</td><td>1.60</td><td>6.28</td><td>-1.17</td><td>11.96</td><td>+0.25</td><td colspan="5">0.0880 -0.0003 0.0934 -0.0001</td></tr><tr><td>PER+at</td><td>1.54</td><td>7.15</td><td>-0.58</td><td>13.19</td><td>+0.29</td><td colspan="5">0.0868 -0.0003 0.0927 +0.0002</td></tr><tr><td/><td/><td/><td colspan="5">MNIST -CNN, ReLU, l∞. = 0.1</td><td/><td/></tr><tr><td>PER</td><td>1.03</td><td>2.40</td><td>-1.04</td><td>4.64</td><td>-0.49</td><td colspan="5">0.0954 +0.0005 0.0967 +0.0002</td></tr><tr><td>PER+at</td><td>0.48</td><td>1.29</td><td>-0.73</td><td>4.61</td><td>-0.24</td><td colspan="5">0.0954 +0.0002 0.0971 +0.0001</td></tr><tr><td/><td/><td/><td colspan="5">CIFAR10 -CNN, ReLU, l∞. = 2/255</td><td/><td/></tr><tr><td>PER</td><td>29.34</td><td>51.54</td><td>+0.56</td><td>64.34</td><td>+7.11</td><td colspan="5">0.0028 -0.0005 0.0036 -0.0002</td></tr><tr><td>PER+at</td><td>26.66</td><td>43.35</td><td>-0.20</td><td>57.72</td><td>+1.13</td><td colspan="5">0.0033 -0.0001 0.0040 0.0000</td></tr><tr><td/><td/><td/><td colspan="5">MNIST -FC1, ReLU, l2, = 0.3</td><td/><td/></tr><tr><td>PER</td><td>1.21</td><td>2.59</td><td>+0.15</td><td>5.34</td><td>-0.01</td><td colspan="5">0.2840 0.0000 0.2888 0.0000</td></tr><tr><td>PER+at</td><td>0.74</td><td>1.46</td><td>+0.06</td><td>7.81</td><td>+2.97</td><td colspan="5">0.2766 -0.0089 0.2860 -0.0050</td></tr><tr><td/><td/><td/><td colspan="5">MNIST -CNN, ReLU, l2, = 0.3</td><td/><td/></tr><tr><td>PER</td><td>1.11</td><td>2.16</td><td>+0.29</td><td>6.37</td><td>+1.33</td><td colspan="5">0.2809 -0.0040 0.2851 -0.0031</td></tr><tr><td>PER+at</td><td>0.52</td><td>1.12</td><td>+0.21</td><td>7.89</td><td>+2.48</td><td colspan="5">0.2763 -0.0074 0.2812 -0.0066</td></tr><tr><td/><td/><td/><td colspan="5">CIFAR10 -CNN, ReLU, l2, = 0.1</td><td/><td/></tr><tr><td>PER</td><td>33.94</td><td>43.06</td><td>-9.48</td><td>56.80</td><td>-6.62</td><td colspan="5">0.0432 +0.0063 0.0484 +0.0019</td></tr><tr><td>PER+at</td><td>24.85</td><td>31.32</td><td>-2.15</td><td>47.28</td><td>+0.52</td><td colspan="5">0.0528 -0.0005 0.0572 -0.0008</td></tr><tr><td/><td colspan="3">TLin MNIST -FC1, ReLU, l∞ TPEC T PEC T Lin</td><td colspan="3">TLin MNIST -CNN, ReLU, l∞ TPEC T PEC T Lin</td><td colspan="4">TLin CIFAR10 -CNN, ReLU, l∞ T PEC TPEC T Lin</td></tr><tr><td>plain</td><td/><td>9.85</td><td>0.8207</td><td/><td>10.56</td><td>0.8804</td><td/><td>9.33</td><td/><td>0.9331</td></tr><tr><td>at</td><td/><td>10.77</td><td>0.8972</td><td/><td>11.39</td><td>0.9489</td><td/><td>9.12</td><td/><td>0.9128</td></tr><tr><td>KW</td><td/><td>8.48</td><td>0.7066</td><td/><td>11.61</td><td>0.9674</td><td/><td>8.43</td><td/><td>0.8432</td></tr><tr><td>MMR</td><td>12</td><td>8.04</td><td>0.6703</td><td>12</td><td>10.68</td><td>0.8897</td><td>10</td><td>8.05</td><td/><td>0.8053</td></tr><tr><td>MMR+at</td><td/><td>7.68</td><td>0.6402</td><td/><td>11.22</td><td>0.9351</td><td/><td>8.45</td><td/><td>0.8450</td></tr><tr><td>PER</td><td/><td>9.34</td><td>0.7780</td><td/><td>11.17</td><td>0.9305</td><td/><td>8.61</td><td/><td>0.8606</td></tr><tr><td>PER+at</td><td/><td>9.38</td><td>0.7816</td><td/><td>11.74</td><td>0.9784</td><td/><td>8.68</td><td/><td>0.8681</td></tr><tr><td/><td colspan="3">MNIST -FC1, ReLU, l2</td><td colspan="3">MNIST -CNN, ReLU, l2</td><td colspan="4">CIFAR10 -CNN, ReLU, l2</td></tr><tr><td>plain</td><td/><td>9.68</td><td>0.6914</td><td/><td>13.64</td><td>0.9742</td><td/><td colspan="2">11.73</td><td>0.9775</td></tr><tr><td>at</td><td/><td>10.44</td><td>0.7457</td><td/><td>13.76</td><td>0.9829</td><td/><td colspan="2">11.67</td><td>0.9725</td></tr><tr><td>KW</td><td/><td>7.72</td><td>0.5514</td><td/><td>12.63</td><td>0.9021</td><td/><td colspan="2">10.23</td><td>0.8525</td></tr><tr><td>MMR</td><td>14</td><td>5.86</td><td>0.4186</td><td>14</td><td>8.52</td><td>0.6086</td><td>12</td><td>9.05</td><td/><td>0.7542</td></tr><tr><td>MMR+at</td><td/><td>5.91</td><td>0.4221</td><td/><td>12.13</td><td>0.8664</td><td/><td colspan="2">10.33</td><td>0.8608</td></tr><tr><td>PER</td><td/><td>11.47</td><td>0.8194</td><td/><td>13.75</td><td>0.9819</td><td/><td>9.13</td><td/><td>0.7609</td></tr><tr><td>PER+at</td><td/><td>11.34</td><td>0.8100</td><td/><td>13.72</td><td>0.9796</td><td/><td colspan="2">10.71</td><td>0.8926</td></tr></table>

Number of steps of bound calculation for the optimal in Fast-Lin (TLin) and PEC (TPEC) for ReLU networks. Note that TLin is a constant for different models given the original interval [ , ¯ ].

Table content: <table><tr><td/><td>T CRO</td><td>T PEC</td><td>TPEC TCRO</td><td>T CRO</td><td>T PEC</td><td>TPEC TCRO</td><td>T CRO</td><td>T PEC</td><td>TPEC TCRO</td></tr><tr><td/><td colspan="3">MNIST -FC1, Sigmoid, l∞</td><td colspan="3">MNIST -FC1, Tanh, l∞</td><td colspan="3">MNIST -FC1, ArcTan, l∞</td></tr><tr><td>plain</td><td/><td>9.06</td><td>0.7547</td><td/><td>9.69</td><td>0.8078</td><td/><td>8.76</td><td>0.7304</td></tr><tr><td>at PER</td><td>12</td><td colspan="2">10.92 0.9104 8.84 0.7369</td><td>12</td><td colspan="2">11.23 0.9356 9.02 0.7513</td><td>12</td><td colspan="2">11.19 0.9326 8.84 0.7369</td></tr><tr><td>PER+at</td><td/><td>9.67</td><td>0.8060</td><td/><td>9.64</td><td>0.8030</td><td/><td>9.62</td><td>0.8020</td></tr><tr><td/><td colspan="3">MNIST -FC1, Sigmoid, l2</td><td colspan="3">MNIST -FC1, Tanh, l2</td><td colspan="3">MNIST -FC1, ArcTan, l2</td></tr><tr><td>plain</td><td/><td colspan="2">10.55 0.7534</td><td/><td colspan="2">10.96 0.7831</td><td/><td>9.99</td><td>0.7134</td></tr><tr><td>at PER</td><td>14</td><td colspan="2">11.83 0.8447 12.09 0.8633</td><td>14</td><td colspan="2">12.64 0.9032 12.20 0.8717</td><td>14</td><td colspan="2">12.30 0.8783 12.08 0.8626</td></tr><tr><td>PER+at</td><td/><td colspan="2">12.22 0.8728</td><td/><td colspan="2">12.50 0.8928</td><td/><td colspan="2">12.30 0.8786</td></tr></table>

Number of steps of bound calculation for the optimal in CROWN (TCRO) and PEC (TPEC) for non-ReLU networks. Note that TCRO is a constant for different models given the original interval [ , ¯ ].

Table content: <table/>

Peer review (iclr2020):
The paper proposes an approach for computing more refined estimates of robustness in comparison w/ existing linear approximation approaches that only give a yes or no answer with regard to robustness guarantees for a given lp-norm ball with radius epsilon. The nice thing is that as the linear-approximations get better, the contributions in this paper would continue to help. The paper makes two key algorithmic/theoretical contributions: 1. An approach to obtain a better estimate of the radius of the l-p ball where the NN is provably robust. This result is fairly straightforward, and relies on computing the distance of a point to the boundary of adversarial polytope. 2. An approach to exploit the fact that the pixel values are restricted to specific bounds, which might allow us trim away some regions from the l-p norm balls around a given input image w.r.t which we want to be robust, while computing the robustness. This I think is a more interesting contribution. I am leaning towards a reject, however I am open to changing my score. I have several key concerns: 1. Verified Training: Why is there no comparison with IBP and IBP+Crown (Zhang 2019) -- it seems like an appropriate comparison to make. Particularly, when the current paper refers and discusses both of the above works. 2. I am not sure that comparison with CRO entirely suffices in my opinion. Would it be possible to compare with the tighter SDP based approaches (Raghunathan et al., NeurIPS*19 and Dvijotham et al., UAI*19)? Is there a specific reason to not compare (other than that the SDP based approach is not a linear approximation, and probably is much slower)? My main concern here is the utility of pushing boundaries with the linear approximation, while there are potentially tighter relaxations? 3. You claim no overhead compared to CROWN. Don*t the greedy-optimization steps add some overhead, or am I missing something? How expensive are they? (It*s possible I might have missed some discussion in this regard. If so, please point me in the right direction and that should suffice) 4. Can you plot the distributions of the certified epsilon? Are there a few samples for which you can certify a much larger epsilon (than just saying not robust) or are there a lot of samples where you can only show a tiny bit of robustness (compared to CROWN saying not robust)? The gains in the average robustness are somewhat small, and these gains alone are not convincing without being able to see how these gains were obtained. Minor Comment: Missing reference to MixTrain for B* < B helps. Update: Thanks for the detailed response! 1. This makes sense, the first bit seems obvious --> if you don*t train with IBP, you won*t get much out of IBP and this is reasonably well known. Table 5: When trained with IBP and verifying with IBP, it seems to do better or quite comparable to train/verify with PER --- in this sense, the gains seem quite marginal. 2. Since a part of the contribution claimed in this paper is improved robustness guarantees for pre-trained networks, I do feel that comparisons with the UAI*19 paper or the NeurIPS*18 paper would be nice -- however, I do agree that the computational tractability of KW/FastLin/IBP are much more favorable. 3. Thanks -- it is much more clear now. 4. The distributions for MMR/PER seem quite similar and most of the gain seems to come at the lower end (small eps). This still remains my biggest concern -- I was hoping that the distributions would diverge a bit more at larger eps, but this is difficult to confirm with the current set of plots. These plots, as of the current version, are not very useful -- a CDF plot as opposed to a histogram would be much more illustrative in terms of comparing the different approaches. Overlaying them with different opacity might also be useful. I am still leaning towards a weak reject. I am not sure how the scoring system works, the scores are distributed unevenly -- I would judge this a 5 on the 1-10 scale. However, going by the wording, I will stay with a 3.