PROVABLY ROBUST CLASSIFICATION OF ADVERSARIAL EXAMPLES WITH DETECTION
Year: 2021

Abstract:
Adversarial attacks against deep networks can be defended against either by building robust classifiers or, by creating classifiers that can detect the presence of adversarial perturbations. Although it may intuitively seem easier to simply detect attacks rather than build a robust classifier, this has not bourne out in practice even empirically, as most detection methods have subsequently been broken by adaptive attacks, thus necessitating verifiable performance for detection mechanisms. In this paper, we propose a new method for jointly training a provably robust classifier and detector. Specifically, we show that by introducing an additional “abstain/detection” into a classifier, we can modify existing certified defense mechanisms to allow the classifier to either robustly classify or detect adversarial attacks. We extend the common interval bound propagation (IBP) method for certified robustness under `∞ perturbations to account for our new robust objective, and show that the method outperforms traditional IBP used in isolation, especially for large perturbation sizes. Specifically, tests on MNIST and CIFAR-10 datasets exhibit promising results, for example with provable robust error less than 63.63% and 67.92%, for 55.6% and 66.37% natural error, for = 8/255 and 16/255 on the CIFAR-10 dataset, respectively.

heading: 1 INTRODUCTION
text: Despite popularity and success of deep neural networks in many applications, their performance declines sharply in adversarial settings. Small adversarial perturbations are shown to greatly deteriorate the performance of neural network classifiers, which creates a growing concern for utilizing them in safety critical application where robust performance is key. In adversarial training, different methods with varying levels of computational complexity aim at robustifying the network by finding such adversarial examples at each training steps and adding them to the training dataset. While such methods exhibit empirical robustness, they lack verifiable guarantees as it is not provable that a more rigorous adversary, e.g., one that does brute-force enumeration to compute adversarial perturbations, will not be able to cause the classifier to misclassify.
It is thus desirable to provably verify the performance of robust classifiers without restricting the adversarial perturbations by inexact solvers, while restraining perturbations to a class of admissible set, e.g., within an `∞ norm-bounded ball. Progress has been made by ‘complete methods’ that use Satisfiability Modulo Theory (SMT) or Mixed-Integer Programming (MIP) to provide exact robustness bounds, however, such approaches are expensive, and difficult to scale to large networks as exhaustive enumeration in the worst case is required (Tjeng et al., 2017; Ehlers, 2017; Xiao et al., 2018).
∗Work was done when the author was an intern at Bosch Center for Artificial Intelligence, Pittsburgh, PA.
‘Incomplete methods’ on the other hand, proceed by computing a differential upper bound on the worst-case adversarial loss, and similarly for the verification violations, with lower computational complexity and improved scalability. Such upper bounds, if easy to compute, can be utilized during the training, and yield provably robust networks with tight bounds. In particular, bound propagation via various methods such as differentiable geometric abstractions (Mirman et al., 2018), convex polytope relaxation (Wong & Kolter, 2018), and more recently in (Salman et al., 2019; Balunovic & Vechev, 2020; Gowal et al., 2018; Zhang et al., 2020), together with other techniques such as semidefinite relaxation, (Fazlyab et al., 2019; Raghunathan et al., 2018), and dual solutions via additional verifier networks (Dvijotham et al., 2018) fall within this category. In particular, recent successful use of Interval Bound Propagation (IBP) as a simple layer-by-layer bound propagation mechanism was shown to be very effective in Gowal et al. (2018), which despite its light computational complexity exhibits SOTA robustness verification. Additionally, combining IBP in a forward bounding pass with linear relaxation based backward bounding pass (CROWN) Zhang et al. (2020) leads to improved robustness, although it can be up to 3-10 times slower.
Alternative to robust classification, detection of adversarial examples can also provide robustness against adversarial attacks, where suspicious inputs will be flagged and the classifier “rejects/abstains” from assigning a label. There has been some work on detection of out-of-distribution examples Bitterwolf et al. (2020), however the situation in the literature on the detection of adversarial examples is quite different from above. Most techniques that attempt to detect adversarial examples, either by training explicit classifiers to do so or by simply formulating “hand-tuned” detectors, still largely look to identify and exploit statistical properties of adversarial examples that appear in practice Smith & Gal (2018); Roth et al. (2019). However, to provide a fair evaluation, a defense must be evaluated under attackers that attempt to fool both the classifier and the detector, while addressing particular characteristics of a given defense, e.g., gradient obfuscation, non-differentability, randomization, and simplifying the attacker’s objective for increased efficiency. A non-exhaustive list of recent detection methods entails randomization and sparsity-based defenses (Xiao et al., 2019; Roth et al., 2019; Pang et al., 2019b), confidence and uncertainty-based detection (Smith & Gal, 2018; Stutz et al., 2020; Sheikholeslami et al., 2020), transformation-based defenses (Bafna et al., 2018; Yang et al., 2019), ensemble methods (Verma & Swami, 2019; Pang et al., 2019a), generative adversarial training Yin et al. (2020), and many more. Unfortunately, existing defenses have largely proven to have poor performance against adaptive attacks (Athalye et al., 2018; Tramer et al., 2020), necessitating provable guarantees on detectors as well. Recently Laidlaw & Feizi (2019) have proposed joint training of classifier and detector, however it also does not provided any provable guarantees.
Our contribution. In this work, we propose a new method for jointly training a provably robust classifier and detector. Specifically, by introducing an additional “abstain/detection” into a classifier, we show that the existing certified defense mechanisms can be modified, and by building on the detection capability of the network, classifier can effectively choose to either robustly classify or detect adversarial attacks. We extend the light-weight Interval Bound Propagation (IBP) method to account for our new robust objective, enabling verification of the network for provable performance guarantees. Our proposed robust training objective is also effectively upper bounded, enabling its incorporation into the training procedure leading to tight provably robust performance. While tightening of the bound propagation may be additionally possible for tighter verification, to the best of our knowledge, our approach is the first method to extend certification techniques by considering detection while providing provable verification. By stabilizing the training, as also used in similar IBP-based methods, experiments on MNIST and CIFAR-10 empirically show that the proposed method can successfully leverage its detection capability, and improves traditional IBP used in isolation, especially for large perturbation sizes.

heading: 2 BACKGROUND AND RELATED WORK
text: Let us consider an L-layer feed-forward neural network, trained for a K-class classification task. Given input x, it will pass through a sequential model, with hl denoting the mapping at layer l, recursively parameterized by
zl = hl(zl−1) = σl(W > l zl−1 + bl), l = 1, · · · , L Wl ∈ Rnl−1×nl , bl ∈ Rnl (1)
where σl(.) is a monotonic activation function, z0 denotes the input, and zL ∈ RK is the preactivation unnormalized K-dimensional output vector (nL = K and σL(.) as identity operator),
referred to as the logits. Robust classifiers can be obtained by minimizing the worst-case (adversarial) classification loss, formally trained by the following min-max optimization Madry et al. (2017)
minimize θ E (x,y)∼D [ max δ∈∆ `(fθ(x + δ), y) ] . (2)
where θ denotes network parameters, vector fθ(x) = zL is the logit output for input x, `(.) is the misclassfication loss, e.g., `xent(.) defined as the cross-entropy loss, and ∆ denotes the set of permissible perturbations, e.g., for `∞-norm ball of radius giving ∆ := {δ | ‖δ‖∞ ≤ }. Although augmenting the training set with adversarial inputs, obtained by approximately solving the inner maximization in Eq. 2, empirically leads to improved adversarial robustness Madry et al. (2017); Shafahi et al. (2019); Wong et al. (2019); Zhang et al. (2019), inexact solution of the inner maximization prevents such methods from providing provable guarantees. In critical applications however, provable verification of classification accuracy against a given threat model is crucial.

heading: 2.1 PERFORMANCE VERIFICATION AND NETWORK RELAXATION
text: Given input (x, y), a classification network is considered verifiably robust if all of its perturbed variations, that is x + δ for ∀δ ∈ ∆ , are correctly classified as class y. Such verification can be effectively obtained by
p∗i = min zL∈ZL c>y,izL where , ZL := {zL|zl = hl(zl−1), l = 1, ..., L, z0 = x + δ, ∀δ ∈ ∆ }
where cy,i = ey − ei for i = 1, 2, ..,K, i 6= y, and ei is the standard ith canonical basis vector. If p∗i > 0 ∀i 6= y, then the classifier is verifiably robust at point (x, y) as this guarantees that zi ≤ zy ∀i 6= y for all admissible perturbations δ ∈ ∆ . The feasible set ZL is generally nonconvex, rendering obtaining p∗i intractable. Any convex relaxation ofZL however, will provide a lower bound on p∗i , and can be alternatively used for verification. As outlined in Section 1, various relaxation techniques have been proposed in the literature. Specifically, IBP in (Mirman et al., 2018; Gowal et al., 2018) proceeds by bounding the activation zl of each layer by propagating an element-wise bounding box using interval arithmetic for networks with monotonic activation functions. Despite its simplicity and relatively small computational complexity (computational requirements for bound propagation for a given input using IBP is equal to two forward passes of the input), it can provide tight bounds once the network is trained accordingly.
Specifically, starting from the input layer z0, it can be bounded for the perturbation class δ ∈ ∆ as z0 = x− 1 and z0 = x + 1, and zl for the following layers can be bounded as
zl = σl(W > l zl−1 + zl−1 2 − |W>l | zl−1 − zl−1 2 ), zl = σl(W > l zl−1 + zl−1 2 + |W>l | zl−1 − zl−1 2 ),
(3)
where | · | is the element-wise absolute-value operator. The verification problem over the relaxed feasible set ẐL := {zL | zL,i ≤ zL,i ≤ z̄L,i}, where ZL ⊆ ẐL is then easily solved as
p∗i = min zL∈ZL c>y,izL ≥ min zL∈ẐL c>y,izL = zL,y − z̄L,i. (4)

heading: 2.2 ROBUST TRAINING OF VERIFIABLE NETWORKS
text: It has been shown that convex relaxation ofZL can also provide a tractable upper bound on the inner maximization in Eq. 2. While this holds for various relaxation techniques, focusing on the IBP let us define
JIBP ,θ (x, y) := [J IBP 1 , J IBP 2 , ..., J IBP K ] where J IBP i := min zL∈ẐL c>y,izL (5)
with (θ, ) implicitly influencing ẐL (dropped for brevity), and upperbound the inner-max in Eq. 2
max δ∈∆
`xent(fθ(x + δ), y) ≤ `xent(−JIBP ,θ (x, y), y), `xent(z, c) := − log ( exp(zc)∑
i exp(zi)
) (6)
By using this tractable upper bound of the robust optimization, network can now be trained by
minimize θ ∑ (x,y)∈D (1− κ)`xent(−JIBP ,θ (x, y), y) + κγ`xent(fθ(x), y), (7)
where γ trades natural versus robust accuracy, and κ is scheduled through a ramp-down process to stabilize the training and tightening of IBP Gowal et al. (2018) (where γ = 1 is selected therein).

heading: 3 VERIFIABLE CLASSIFICATION WITH DETECTION
text: In this paper, we propose a new method for jointly training a provably robust classifier and detector. Specifically, let us augment the classifier by introducing an additional “abstain/detection”. This can be readily done by extending the K-class classification task to a (K + 1)-class classification, with the (K + 1)-th class dedicated to the detection task, and the maximum weighted class is finally chosen as the classification output. The classifier is then trained such that adversarial examples, or ideally any other example that the network would misclassify, are classified in this abstain class, denoted by a, thus preventing incorrect classification.
Formally, the classifier can be denoted as in Eq. 1, with the only difference that the final output is K + 1 dimensional, i.e., zL ∈ RK+1; simply by substituting the last fully-connected weight matrix WL of dimension nL ×K with that of dimension nL × (K + 1), and similarly for bL.

heading: 3.1 VERIFICATION PROBLEM FOR CLASSIFICATION WITH ABSTAIN/DETECTION
text: It is desirable to provably verify performance of the joint classification/detection. In contrast to existing robust classifiers, however, on a perturbed image x + δ, the classification/detection task is considered successful if the input is classified either as the correct class y, or as the abstain class a; as both cases prevent misclassification of the adversarially perturbed input as a wrong class. On clean natural images however, classification/detection is considered successful only if it is classified as the correct class y, and abstaining is considered misclassification.
In order to certify performance in adversarial settings, it is now sufficient to verify that the network satisfies the following for a given input pair (x, y) and δ ∈ ∆ and i = 1, ..,K, i 6= y: max{c>y,iz, c>a,iz} ≥ 0 ∀z ∈ ZL := {zL|zl = hl(zl−1) l = 1, ..., L, z0 = x + δ, ∀δ ∈ ∆ } (8) where cy := ey−ei and ca := ea−ei, a denotes the “abstain” class, and the dependence of ZL on (x, y, , θ) is omitted for brevity. Verification can be done effectively by seeking a counterexample
π∗i := min z∈ZL max{c>y,iz, c>a,iz}. (9)
If π∗i ≥ 0 ∀i 6= y , the specification is then satisfied and the performance is verified. Similar to previous verification methods, to overcome the non-convexity of the optimization in Eq. 9, one can lower bound the problem by expanding the feasible set ZL ⊆ ẐL , where ẐL is convex, as stated in Theorem 1, and proved in Appendix A.1.
Theorem 1: For any convex ẐL s.t. ZL ⊆ ẐL, Eq. 9 can be bounded by the convex relaxation
max 0≤η≤1 min z∈ẐL
( η ca,i + (1− η) cy,i )> z ≤ min
z∈ZL max{c>y,iz, c>a,iz}. (10)
Although Theorem 1 holds for any convex relaxation of ZL, for IBP relaxation in Gowal et al. (2018) it can be further simplified by substituting z = W>LzL−1 + bL, thus not propagating the intervals through the last layer for tighter bounding, and solved analytically as follows.
Theorem 2: The optimization in Eq. 9 can be lower-bounded by the convex optimization Ji(x, y) = max
0≤η≤1 min zL−1∈ẐL−1 (ω1 +η ω2) >zL−1 +η ω3 +ω4 ≤ min z∈ZL max{c>y,iz, c>a,iz} (11)
in which ω1 := W>Lcy,i, ω2 := W > L (ca,i−cy,i), ω3 := b>L (ca,i−cy,i), ω4 := b>Lcy,i and convex set ẐL−1 is a convex relaxation of ZL−1 on the hidden values at L− 1. Furthermore, Ji(x, y) can be analytically obtained as outlined in Alg. 1
Note that since η is the dual variable, any selection within the feasible set serves as a (looser but valid) lower bound, while the maximization makes the bound tight; see Appendix A.2 and A.3 for proof and a step-by-step algorithm description. Similar to other convex relaxation-based verification methods, in order for a networks to provide verifiable performance, one needs to incorporate bound propagation in training.
Algorithm 1 Solution for Ji(x, y) in Theorem 2 1: Input. Bounds on layer L− 1 : zL−1, z̄L−1, and weight matrix WL 2: ω1 = WLcy,i and ω2 = WL(ca,i − cy,i), ω3 := b>L (ca,i − cy,i), and ω4 := b>Lcy,i 3: ζ = [ζ1, ..., ζnL ] := −ω1/ω2 and vector of indices s that sorts ζ , i.e., ζs1 ≤ · · · ≤ ζsnL−1 4: u1 = Πs(ω1 ◦ zL−1) , ū1 = Πs(ω1 ◦ z̄L−1), u2 := Πs(ω2 ◦ zL−1) , ū2 := Πs(ω2 ◦ z̄L−1)
where operators ◦ and Πs(.) denote element-wise multiplication, and permutation according to indices s, respectively.
5: m = minζsj≥0 j and M = maxζsj≤1 j for j = 1, ..., nL−1 6: for η = 0, ζsm , ζsm+1 , · · · , ζsM−1 , ζsM , 1 do 7: Compute
g(η) = nL−1∑ j=1 ( 1{ω1,j+ηω2,j≤0} (ū1,j + ηū2,j) + 1{ω1,j+ηω2,j≥0} ( u1,j + ηu2,j ) ) + η ω3 + ω4
8: return max g(η) over the computed values.

heading: 4 TRAINING A VERIFIABLE ROBUST CLASSIFICATION WITH DETECTION
text: In order to train a robust classifier with detection, let us start by formalizing the objective of an adversarial attacker. Naturally, an adaptive attacker’s objective is to craft perturbation δ such that it simultaneously evades detection and causes misclassification. Formally, this can be tackled by seeking δ such that loss corresponding to the winner of the two classes y and a (higher logit leading to smaller cross-entropy loss) is maximized, i.e.,
max δ∈∆
min { `xent(fθ(x + δ), y), `xent(fθ(x + δ), a) } (12)
where `xent(z, c) denotes the cross-entropy loss for class c = y and c = a, and I = {1, 2, ...,K, a} denotes the class index set with K + 1 elements.
Let us now define
Labstainrobust (x, y; θ) := max δ∈∆
min { `xent\a(fθ(x + δ), y), `xent\y(fθ(x + δ), a) } (13)
in which the inner maximization is closely related to that of the adversarial objective in Eq. 12 with a small difference: loss terms `xent\a and `xent\y are defined as
`xent\a(z, y) := − log ( exp(zy)∑ i∈I\{a} exp(zi) ) , and `xent\y(x, a) := − log ( exp(za)∑ i∈I\{y} exp(zi) ) .
This small alteration to the cost, while not changing the minimization “winner” between the true class y and rejection class a in Eq. 12 and 13, i.e.,{ za ≤ zy ⇒ `xent(fθ(x+ δ), y) ≤ `xent(fθ(x+ δ), a) and `xent\a(fθ(x+ δ), y) ≤ `xent\y(fθ(x+ δ), a) zy ≤ za ⇒ `xent(fθ(x+ δ), a) ≤ `xent(fθ(x+ δ), y) and `xent\y(fθ(x+ δ), a) ≤ `xent\a(fθ(x+ δ), y)
favorably influences the training process. That is so since, for δ such that, for instance za < zy , minimizing Labstainrobust (x, y; θ) during training reduces to minimizing `xent(fθ(x + δ), y) which in turn leads to further increasing zy while decreasing the logit value za; and similarly, increasing zy while decreasing zy if zy < za. Intuitively however, the true objective of the classifier augmented with detection on adversarial examples is to increase both zy and za while reducing zj , ∀j 6= a, y; thus preventing any gap in between the boundary of the classes a and y, which can potentially lead to successful adaptive attacks. Hence, minimizing Eq. 12 would be in contrast with the true underlying objective, and Eq. 13 simply prevents the raised issue.
Upon defining Lnatural(x, y; θ) := `xent(fθ(x), y) and Lrobust(x, y; θ) := maxδ∈∆ `xent(fθ(x+δ), y), we then define the overall training loss as
L = Lrobust(x, y; θ) + λ1L abstain robust (x, y; θ) + λ2Lnatural(x, y; θ), (14)
where Lnatural(x, y; θ) captures the misclassification loss of the natural (clean) examples, and Lrobust(x, y; θ) denotes that of adversarial examples without considering the rejection class, i.e., similar to that of Gowal et al. (2018), and parameters (λ1, λ2) trade-off clean and adversarial accuracy. To train a robust classifier, we proceed by minimizing the overall loss Eq. 14, by first upperbounding Lrobust(x, y; θ) and Labstainrobust (x, y; θ).

heading: 4.1 UPPERBOUNDING THE TRAINING LOSS
text: Using Theorem 2, and restricting 0 < η ≤ η ≤ η̄ < 1, let us now define Jη,η̄i (x, y), where trivially
J η,η̄
i (x, y) := max 0≤η≤η≤η̄≤1
(ω1 + ηω2) >ẑL−1 + η ω3 + ω4 ≤ Ji(x, y) (15)
and can also be solved analytically similar to Theorem 2. By generalizing the findings in Wong & Kolter (2018); Mirman et al. (2018), we can upper bound the robust optimization problem using our dual problem in Eq. 15, according to the following Theorem, which we prove in Appendix A.4.
Theorem 3: For any data point (x, y), and > 0, and for any 0 ≤ η ≤ η̄ ≤ 1, the adversarial loss Labstainrobust (x, y; θ) in Eq. 13 can be upper bounded by
Labstainrobust (x, y; θ) ≤ L̄abstainrobust (x, y; θ) := `xent\a(−J ,θ(x, y), y) = `xent\y(−J ,θ(x, y), a) (16)
where J ,θ(x, y) is a (K + 1)-dimensional vector, valued at index i as [J ,θ(x, y)]i = J η,η̄ i (x, y).
Note that maximization over η for obtaining J η,η̄
i (x, y) can be done either by bisection (concave maximization) or by following Alg. 1 and substitutingm = minζsν≥η ν , and M = maxζsν≤η̄ ν Remark 1. Setting η = η̄ = 0 forces η = 0 which reduces J η,η̄
i (x, y) in Eq. 15 to that in Eq. 5, .i.e,
J IBPi (x, y) = J η,η̄ i (x, y)|η=η̄=0, also bounding loss term Lnatural(x, y; θ) as
Lrobust(x, y; θ) ≤ L̄robust(x, y; θ) := `xent(−JIBP ,θ (x, y), y). (17)
Remark 2. While setting η = 0 and η̄ = 1 gives tighter bounds, (and is thus used for the verification counterpart in Theorem 2), strictly setting 0 < η ≤ η̄ < 1 empirically yields better generalization of the network. This can be intuitively understood by rewriting ω1 + ηω2 = W>L (ηca,i + (1− η)cy,i) which is a convex combination of the verification constraints for the correct and the abstain class. Thus η 6= 0 6= 1 will lead to minimizing a combination of both terms, preventing gaps in between the two classes. Also, higher values of η increase the influence of the term corresponding to the abstain case, and vice versa, whose tuning can promote abstaining by considering how desirable such outcome is (or is not).
Utilizing upperbounds in Eq. 16 and Eq. 17, we can proceed to training the network by minimizing the tractable upperbound on the overall loss
min θ L ≤ min θ `xent(−JIBP ,θ (x, y), y) + λ1`xent\y(−J ,θ(x, y), a) + λ2`natural(fθ(x), y) (18)
Note that setting λ1 = 0 and γ = λ2 - and incorporation of a ramp-down process by parameter κ as detailed in Section 5 - reduces the training in Eq. 18 to that of Gowal et al. (2018) without detection.
Complexity. Since given IBP bounds on zL−1, the solution to Eq. 16 is analytically available (that is after sorting whose complexity is negligible in comparison with forward pass), computing Eq. 18 imposes the same computational complexity as in IBP, which is twice the normal training procedure, as it requires propagating the upper and lower bounds via forward pass.

heading: 5 EXPERIMENTS
text: Empirical performance of the proposed robust classification with detection on MNIST-10 and CIFAR-10 datasets is reported in this section, and is compared with the state-of-the-art alternatives. The training procedure is stabilized as detailed next 1.
1Code is available at https://github.com/boschresearch/robust_classification_ with_detection

heading: 5.1 STABILIZING THE TRAINING PROCEDURE
text: We incorporate the following mechanisms to stabilize the training procedure in our tests, where the first two have been previously used in (Gowal et al., 2018) and (Zhang et al., 2020) as well.
Ramp down of κ: To stabilize the trade-off between nominal and verified accuracy, let us introduce parameter κ in the overall loss by trading the natural and robust loss as
L = (1− κ) ( L̄robust(x, y; θ) + λ1L̄
abstain robust (x, y; θ)︸ ︷︷ ︸
Robust loss
) + κ λ2Lnatural(x, y; θ)︸ ︷︷ ︸
Natural loss
(19)
Setting κ = 0.5 renders the optimization identical to that in Eq. 18. During the training however, we incorporate a ramp down procedure where κ starts at value κstart = 1, thus training the model to fit the natural data, and slowly decreasing it to value κend = 0.5, similar to that in Gowal et al. (2018).
Ramp up of : It is very important during the training process to start at = 0 and gradually increase it to train, while also setting train larger than test can improve generalization.
Ramp down of η and η̄: Setting 0 < η and η̄ < 1 helps with better generalization. Furthermore, setting large η and η̄ promotes the abstain class in loss term L̄abstainrobust by increasing the weight of ω2 in Eq. 15. Thus, we can further stabilize the training process through a ramp down procedure where these parameters start at η = η
start and η̄ = η̄start, and are gradually reduced to η = ηend and η̄ = η̄end,
with η end < η start and η̄end < η̄start.
Furthermore, although the term L̄robust(x, y; θ) could in theory be excluded from the training process, as the term Lnatural(x, y; θ) prevents the degenerate solution of always classifying all images in the abstain class, it’s inclusion empirically helps the stability of the training process.

heading: 5.2 EMPIRICAL RESULTS ON MNIST AND CIFAR10
text: The classification networks are identical to the large network in Gowal et al. (2018), also detailed in Table 2, trained by minimizing the loss in Eq. 18 with the above stabilizing schemes. Selection of parameters for each datasets is detailed in Appendix B. Since most recent detector networks have shown very low performance against adaptive attacks, and lack provable performance Tramer et al. (2020), we only compare the performance with other provable robust classification methods, while focusing on the different decomposition in the reported natural and robust accuracy among these two. As numbers in Table 1 suggest, the proposed detection/classification network shows improved robustness against other methods, including IBP in isolation (without the detection capability), specially against larger perturbations in the CIFAR-10 dataset, which intuitively is pleasing: as larger perturbations are naturally more distinguishable, the detection capability of the network is successfully leveraged for improving the adversarial robustness. Let us now take a closer look at the performance by focusing on the detection capability.
Effectiveness of the detection class. By nature, the proposed classification “adaptively chooses” between (robust) correct classification and detection of adversarial or difficult inputs during the training. This gives rise to two phenomena:
(1) In verifiably robust methods, natural image accuracy declines as robustness improves. In the proposed approach however, a considerable number of misclassified natural inputs are in fact abstained on, which in certain applications is more favorable than assigning them to a wrong class, as classifiers without detection capability would: compare 30.5% abstain and 25.6% ‘wrong-class misclassification’ (other than abstain and the correct class) in IBP-with-detection, with that of 53.7% ‘wrongclass’ misclassification in IBP on natural CIFAR-10 images in networks trained for = 8/255.
(2) Regardless of the training procedure, the proposed classifier with detection can still be verified using verification in Eq. 4 to obtain its guaranteed robustness with only considering the correct class. Thus, comparing this verification percentage with that of Eq. 11 highlights the effectiveness of the abstain class in detecting perturbed images and increasing robustness: for instance, using our method 76.07% maximum robust error successfully decreases to 63.63% by considering the detection capability, on CIFAR-10 trained for = 8/255, compared to 69.92% in IBP without detection.
+ As reported in Zhang et al. (2020), achieving the 68.44% IBP verified error requires extra PGD adversarial training loss, without which the verified error is 72.91% (LP/MIP verified) or 73.52% (IBP verified), thus our result should be compared to 73.52%. * Best reported numbers for IBP are computed using mixed integer programming (MIP), which are strictly smaller than IBP veified error rates, see table 3 and 4 in Gowal et al. (2018). For fair comparison, we report IBP verified error rates from table 3 therein. ** Best reported results from the literature may use different network architectures, and empirical PGD error rate may have been computed under different settings, e.g., number of steps and restarts. *** Number in the IBP rows in this table are the best between (Zhang et al., 2020) and our experiments, while results from (Gowal et al., 2018) are reported under best literature record for IBP. † It is important to note that unlike robust classification, the proposed joint classification/detection does successfully leverage the detection capability to decrease the verified error rate by rejecting some adversarial examples, which makes direct comparison of these values difficult. However since there exists no other verifiable detection scheme, such comparison is made here to show the effect of successful detection; see Figure 1 for a detailed discussion on this.
See Fig. 1 for decomposition of the performance metrics of the proposed network over CIFAR-10 dataset, demonstrating the effectiveness of the abstain class in detecting “difficult” natural images while also increasing the robustness certificate over adversarial inputs.

heading: 5.3 NATURAL VERSUS ADVERSARIAL ERROR TRADEOFF
text: Reporting a single set point in the Pareto Frontier as reported in Table 1 gives limited understanding on how different methods trade off natural versus robust error. To address this, a more detailed study on this trade-off in IBP-based robust classification with and without detection is discissed here.
In order to get the best performance for IBP-based robust training without detection (that is λ1 = 0), and since it is not known whether varying κend or λ2 will lead to a better performance, we have
trained the classification networks in two ways: (1) setting κend = 0.5 and varying λ2 ∈ [0, 3], and (2) setting λ2 = 1 and varying κend ∈ [0, 0.5], to get multiple set points along the Pareto Frontier. Similarly, for IBP-with-detection-based classification, we have set κend = 0.5 , λ1 = 0.6, 0.8, 1.0 for MNIST and λ1 = 1.0 for CIFAR-10, and varied λ2 ∈ [1 4] to get various points along the frontier. The network is trained for various values, with other training parameters as stated in Appendix B.
Results are plotted in Fig. 2 and 3 (presented in the Appendix due to space limitation). As shown, the classifier enhanced with detection capability is better able to trade natural and robust accuracy, thus attaining higher robustness by trading small decrease in natural accuracy. This together with the fact that the natural accuracy decrease is also partly handled by abstaining of such natural images that would have been misclassified (as one of the original K classes) otherwise, demonstrates the effective utilization of the detection capability in the proposed method. It is important to note that IBP w/detection allows us to obtain additional regions on this Pareto frontier that traditionalrobust-classifiers without detection cannot obtain, and could potentially provide additional gain to what is achievable by other various improvement techniques such as tighter relaxation and bound propagation methods.

heading: 6 CONCLUSION
text: We proposed a new method for jointly training a provably robust classifier and detector. By introducing an additional “abstain/detection” into a classifier, we have proposed a verification scheme for classifiers with detection under adversarial settings, and shown that such networks can be efficiently trained be extending the common IBP relaxation techniques. The effectiveness of the proposed detection scheme with provable guarantees versus SOTA robust verifiable classification methods is corroborated by empirical tests on MNIST and CIFAR-10, specially against large perturbations.

heading: A APPENDIX
text: A.1 PROOF OF THEOREM 1
Since ZL ∈ ẐL it trivially holds that
min z∈ẐL max{c>y,iz, c>a,iz} ≤ min z∈ZL max{c>y,iz, c>a,iz} (20)
The lower bound is now a convex minimization, which can be rewritten as
min z∈ẐL max{c>y,iz, c>a,iz} = min τ,z∈ẐL τ s. t. c>y,iz ≤ τ , c>a,iz ≤ τ.
Defining the slack variables ηa ≥ 0 and ηy ≥ 0 for the inequality constraints, the Lagrangian can be written as L(τ, z, ηa, ηy) = τ + ηa(c>a,iz− τ) + ηy(c>y,iz− τ) and minimizing L(τ, z, ηa, ηy) with respect to the primal variable τ , yields ηa + ηy = 1. Defining η := ηa = 1− ηy , and using the fact that the dual maximization always serves as a lower bound on the primal we get
max 0≤η≤1 min z∈ẐL
( η ca,i + (1− η) cy,i )> z ≤ min
z∈ZL max{c>y,iz, c>a,iz}.
A.2 PROOF OF THEOREM 2
Following on the statement of Theorem 1 and by substituting z = W>LzL−1 + bL, we get
max 0≤η≤1 min zL−1∈ẐL−1
( η ca,i+(1−η) cy,i )>( W>LzL−1+bL ) ≤ min
z∈ẐL max{c>y,iz, c>a,iz} (21)
which can be reordered as
max 0≤η≤1 min zL−1≤zL−1≤z̄L−1
(ω1 + ηω2) >zL−1 + η ω3 + ω4 (22)
where ω1 := WLcy,i, ω2 := WL(ca,i − cy,i), ω3 := b>L (ca,i − cy,i), and ω4 := b>Lcy,i, which then equals
max 0≤η≤1
(ω1 + ηω2) >ẑL−1 + η ω3 + ω4 (23)
where minimization w.r.t. zL−1 is solved by the (this is under the setting for most networks with positive activations, and thus lower bound zl is always non-negative)
[ẑL−1]j = { [z̄L−1]j if [ω1 + ηω2]j ≤ 0 [zL−1]j if [ω1 + ηω2]j ≥ 0
(24)
and can be rewritten as
max 0≤η≤1 nL−1∑ j=1 [ ω1+ηω2 ] j ( 1{ω1,j+ηω2,j≤0}[z̄L−1]j+1{ω1,j+ηω2,j≥0}[zL−1]j ) +η ω3+ω4 (25)
and can be rewritten as
max 0≤η≤1 nL−1∑ j=1 ( 1{ω1,j+ηω2,j≤0}[ω1 ◦ z̄L−1 + ηω2 ◦ z̄L−1]j + 1{ω1,j+ηω2,j≥0}[ω1 ◦ zL−1 + ω2 ◦ zL−1]j ) + η ω3 + ω4 (26)
where “◦” denotes the elementwise multiplication. Thus, due to the concavity of the dual, optimal η can be found by evaluationg the objective in between the break points which are given by ζ := [ζ1, ..., ζnL−1 ] with its j-th element defined as ζj := −ω1,j/ω2,j .
To do this, let us use s to denote the nL-ary tuple of indices that sorts ζ. That is
ζ̃ = [ζ̃1, ..., ζ̃nL−1 ] := Πs(ζ) := [ζs1 , ..., ζsnL−1 ] s.t. ζs1 ≤ ... ≤ ζsnL−1
with operator Πs(.) denoting the permutation of its arguments according to s, such that ζ̃i = ζsi∀i, and ζ̃ is sorted in the increasing order .
We can also rewrite the problem by summing over the indices in the sorting set s instead, as
max 0≤η≤1 nL−1∑ j=1 ( 1{ω1,j+ηω2,j≤0}[ω1 ◦ z̄L−1 + ηω2 ◦ z̄L−1]sj + 1{ω1,j+ηω2,j≥0}[ω1 ◦ zL−1 + ω2 ◦ zL−1]sj ) + η ω3 + ω4. (27)
Now let us define u1 := Πs(ω1 ◦ zL−1) , ū1 := Πs(ω1 ◦ z̄L−1), u2 := Πs(ω2 ◦ zL−1) , ū2 := Πs(ω2 ◦ z̄L−1), we get
max 0≤η≤1 nL−1∑ j=1 ( 1{ {η≤ζ̃j and ω2,sj>0} or {η≥ζ̃j and ω2,sj<0}
} (ū1,j + ηū2,j) + 1{
{η≥ζ̃j and ω2,sj>0} or {η≤ζ̃j and ω2,sj<0} } (u1,j + ηu2,j) ) + η ω3 + ω4. (28)
In order to break the objective of maximization into piece-wise linear programming subproblems, let us first identify the (indices of) ζsi values that fall in the feasible set 0 ≤ η ≤ 1 by
m = min ζsν≥0 ν and M = max ζsν≤1 ν
The overall maximization can now be reduced to piece-wise subproblems over sets ζ̃ν ≤ η ≤ ζ̃ν+1 for m− 1 ≤ ν ≤M as
max max{0,ζ̃ν}≤η≤min{1,ζ̃ν+1} nL−1∑ j=1 ( 1{ {η≤ζ̃j and ω2,sj>0} or {η≥ζ̃j and ω2,sj<0}
} (ū1,j + ηū2,j) + 1{
{η≥ζ̃j and ω2,sj>0} or {η≤ζ̃j and ω2,sj<0} } (u1,j + ηu2,j) ) + η ω3 + ω4. (29)
Since each of these subproblems are maximized at the boundaries of the feasible sets, the overall maximization essentially reduces to evaluation of the following objective function at (M −m+ 3) points η = 0, ζ̃m, ζ̃m+1, · · · , ζ̃M−1, ζ̃M , 1
g(η) = nL−1∑ j=1 ( 1{ω1,j+ηω2,j≤0} (ū1,j + ηū2,j) + 1{ω1,j+ηω2,j≥0} ( u1,j + ηu2,j )) + η ω3 + ω4
Values of g(η) can be efficiently computed by a forward cumulative sum and forward-backward cumulative sum of u1 and u2, ū1 and ū2, thus imposing the overall complexity which is dominated by the sorting at O(nL−1 log(nL−1)) in an efficient implementation. .
A.3 DESCRIPTION OF ALGORITHM 1
Here is a step-by-step walk-through for Algorithm 1, with insight on how these steps are performed.
1. Form vectors ω1 and ω2, which are the last layer values as ω1 = WLcy,i, ω2 = WL(ca,i − cy,i) , ω3 := b>L (ca,i − cy,i), and ω4 := b>Lcy,i.
2. Define ζ = [ζ1, ..., ζnL ] := −ω1/ω2 and get the vector of indices s that sorts it, i.e., ζs1 ≤ · · · ≤ ζsnL−1
3. Form the element-wise product of (ω1, ω2) with (zL−1, z̄L−1)), and sort them according to the index set s. u1 = Πs(ω1 ◦zL−1) , ū1 = Πs(ω1 ◦ z̄L−1), u2 := Πs(ω2 ◦zL−1) , ū2 := Πs(ω2 ◦ z̄L−1).
4. Get the lowest and highest indexes (m,M) such that the sorted ζ vector value at those indices are in the feasible set, between 0 and 1.
5. Iterate over the feasible values of η = 0, ζsm , ζsm+1 , · · · , ζsM−1 , ζsM , 1 and compute the corresponding objective values
g(η) = nL−1∑ j=1 ( 1{ω1,j+ηω2,j≤0} (ū1,j + ηū2,j) + 1{ω1,j+ηω2,j≥0} ( u1,j + ηu2,j ) ) + η ω3 + ω4
6. Return the maximum value of g(η) over the evaluated points.
A.4 PROOF OF THEOREM 3
Let us start by splitting the feasible set into disjoint sets of
ẐaL−1 := {zL−1 | zL−1,a ≥ zL−1,y}, and Ẑ y L−1 := {zL−1 | zL−1,a < zL−1,y}
where ẐL−1 = ẐyL−1 ∪ Ẑ a L−1, and Ẑ y L−1 ∩ Ẑ a L−1 = ∅.
Proof is carried out by considering z ∈ ẐyL−1 and z ∈ ẐaL−1, separately.
Restricting z ∈ ẐyL−1 we have `xent\a(fθ(x + δ), y) ≤ `xent\y(fθ(x + δ), a) which leads to
Labstainrobust (x, y; θ) = max δ∈∆
min { `xent\a(fθ(x + δ), y), `xent\y(fθ(x + δ), a) } (30)
≤ max zL−1∈ẐyL−1 `xent\a(zL, y) s.t. zL = W>LzL−1 + bL (31)
Loss function `xent\a is the cross entropy loss defined on the K-dimensional vector [zL,1, · · · , zL,K ] and class y, and thus following Wong & Kolter (2018) given its transnational invariance equals
max zL−1∈ẐyL−1 `xent\a(zL, y) = max zL−1∈ẐyL−1
`xent\a(zL − zL,y1, y) s.t. zL = W>LzL−1 + bL (32)
with 1 denoting the (K + 1)-dimensional vector of all ones. Given the invariance of `xent\a with respect to zL,a, it can finally be upperbounded by taking the upperbound for all i indices where i = 1, ...,K, i 6= a, y and lowerbound at index i = y. Note that for i = y, value [zL − zL,y1]i = 0, and a lower bound on other entries i = 1, ...,K, i 6= a, y can be obtained by
zL,i − zL,y =−max{zL,y − zL,i, zL,a − zL,i} = −max{c>y,iz, c>a,iz} (33)
≤ − min zL∈ZL
max{c>y,iz, c>a,iz} ≤ −Ji(x, y) ≤ −J η,η̄ i (x, y) (34)
where the first equality holds since ẐyL−1 := {zL−1 | zL−1,a < zL−1,y} for z ∈ Ẑ y L−1, second inequality is due to Theorem 2, and third inequality is given by Eq. 15.
Thus, for z ∈ ẐyL−1 the loss term is now upperbounded by
Labstainrobust (x, y; θ) ≤ `xent\a(−J ,θ(x, y), y)
where
[J ,θ(x, y)]i = { 0 if i = a, y J η,η̄ i (x, y) otherwise. (35)
Similarly, it can be shown that for Thus, for z ∈ ẐaL−1 the loss term is now upperbounded by
Labstainrobust (x, y; θ) ≤ `xent\y(−J ,θ(x, y), a).
The equality of `xent\y(−J ,θ(x, y), a) = `xent\a(−J ,θ(x, y), y) trivially follows from the fact that [J ,θ(x, y)]i = 0 for i = a, y.
Thus, since ẐL−1 = ẐyL−1 ∪ ẐaL−1, the proof is complete. .

heading: B APPENDIX: EXPERIMENT SET UP
text: Training parameters and schedules are similar to (Gowal et al., 2018) and (Zhang et al., 2020), and outlined in detail here. For training the classifier network with architecture given in Table 2, for both datasets, Adam optimizer with learning rate of 5 × 10−4 is used. Unless stated differently, κ is scheduled by a linear ramp-down process, starting at 1, which after a warm-up perio,d is ramped down to value κend = 0.5. Value of during the training is also simultaneously scheduled by a linear ramp-up, starting at 0, and ramped up to the final value of train, reported in Tabel 1, and networks are trained with a single NVIDIA Tesla V100S GPU.
• For MNIST, the network is trained in 100 epochs with batchsize of 100 (total of 60K steps). A warm up period of 3 epochs (2K steps) is used (normal classification training with no robust loss), followed up by a ramp-up duration of 18 epochs (10K steps), and the learning rate is decayed ×10 at epochs 25 and 42. No data augmentation is used. Furthermore, fixed selection of η̄ = 0.9 and η = 0.1 during training is used for this dataset with no ramp-down. Reported numbers in Table 1 corresponds to λ1 = 1 and λ2 = 2 for = 0.3, and λ1 = 0.6 and λ2 = 1 for = 0.4 respectively.
• For CIFAR10, the network is trained in 3200 epochs with batchsize of 1600 (total of 100K steps). A warm up period of 320 epochs (10K steps) is used (normal classification training with no robust loss), followed up by a ramp-up duration of 1600 epochs (50K steps), and the learning rate is decayed ×10 at epochs 2600 and 3040 (60k and 90K steps). Random translations and flips, and normalization of each image channel (using the channel statistics from the train set) is used during training. Furthermore, during training for all values we have selected η̄start = 1.0 and η̄end = 0.9. Additionally, ηend = 0.1 is used during training, with η
start = 0.1 for = 2/255 (no ramp down), η start = 0.3 for = 8/255, η start = 0.4
for = 12/255, and η start = 0.5 for = 16/255. The intuition behind these parameters selection lies in Remark 2, as large η values promote the abstain option more, so for large , we start with larger η
start as well. Reported numbers in Tabel 1 correspond to λ1 = 1
for all values, and λ2 = 3.0 for = 2/255, λ2 = 2.9 for = 8/255, and λ2 = 3.1 for = 16/255 to insure similar natural accuracy for fair comparison against other methods.
B.1 PARETO FRONTIER FOR MNIST DATASET
B.2 EMPIRICAL ATTACK SUCCESS RATE USING PGD ATTACKS
In order to obtain empirical attack success on the trained networks, adversarial perturbations are sought by solving
max δ∈∆ ( max i 6=a,y zL,i −max{zL,y, zL,a} )
(36)
This attack is indeed an adaptive attack as it aims at circumventing the detection while trying to cause misclassification (Tramer et al., 2020). Perturbations are sought by maximizing this objective using PGD with 200-steps for mnist and 500-steps for CIFAR-10 Madry et al. (2017), with 10 random restarts. It is interesting to note that the achieved attack success rate in Table 1 is well below the verified robust error, further implying the effectiveness of incorporation of the detection mechanism as the true robustness of the system against practical adaptive PGD attacks are considerably stronger in comparison to robust classification without detection.

Review summaries:
This paper aims to train networks that can map a possibly $\ell_\infty$-perturbed input to its class provably or map this input to the “abstain class” provably. This is achieved by training on the IBP output boxes together with a new loss function. The method diverts from the classical setting in which the classifier needs to be robust, by allowing the classifier to abstain. While this is an interesting idea, the paper seems to be rushed and not carefully written. The notation could be improved and presentation could be simplified. It seems as if the results from related work (Balunovic et. al. [3] and Mirman et. al. [4]) are missing in Table 1 and thus are not compared against. Further, some questions remain open after reading the paper:

This paper deals with the problem of bounding the amount of errors that a model can make when attacked by an adversary limited to small perturbation of an input image. Similarly to previous paper, it proposes to extend the classifier with a detector to identify adversarial examples. As opposed to previous papers, the authors suggest to perform formal verification to prove that the samples are either robustly classified or abstained on (as opposed to testing the classifier + detector adversarially which would have left open the question of whether or not the attack against the pair was done in an adequate way). The method used for this is based on the simple IBP algorithm but the authors propose a proper encoding of the max(abstain_logit, gt_logit). They also follow the IBP strategy of using the bound resulting from verification as part of the training objective in order to encourage the network to behave properly.

In this paper, the authors propose an additional "abstain/detection" loss term into training, so that the classifier can either robustly classify or detect an adversarial attack. They extend the interval bound propagation method for certified robustness under L_infity perturbations (a simple bounding in changes of the weight after each NN layer application, using a box constraint). Hyperparameters in the objective trade-off between clean and adversarial accuracy.