Expressive Losses for Verified Robustness via Convex Combinations
Authors: Alessandro De Palma
Rudy R Bunel
Krishnamurthy Dj Dvijotham
M. Pawan Kumar
Robert Stanforth
Alessio Lomuscio
Venue: ICLR 2024 poster (2024)
Keywords: Verified Training
Neural Network Verification
Verified Adversarial Robustness
Primary area: societal considerations including fairness, safety, privacy
TL;DR: Expressive losses (ranging from lower to upper bounds to the true robust loss) are all you need to attain state-of-the-art verified robustness.

Abstract: In order to train networks for verified adversarial robustness, it is common to over-approximate the worst-case loss over perturbation regions, resulting in networks that attain verifiability at the expense of standard performance.
As shown in recent work, better trade-offs between accuracy and robustness can be obtained by carefully coupling adversarial training with over-approximations. 
We hypothesize that the expressivity of a loss function, which we formalize as the ability to span a range of trade-offs between lower and upper bounds to the worst-case loss through a single parameter (the over-approximation coefficient), is key to attaining state-of-the-art performance. 
To support our hypothesis, we show that trivial expressive losses, obtained via convex combinations between adversarial attacks and IBP bounds, yield state-of-the-art results across a variety of settings in spite of their conceptual simplicity.
We provide a detailed analysis of the relationship between the over-approximation coefficient and performance profiles across different expressive losses, showing that, while expressivity is essential, better approximations of the worst-case loss are not necessarily linked to superior robustness-accuracy trade-offs.

Published as a conference paper at ICLR 2024
EXPRESSIVE LOSSES FOR VERIFIED ROBUSTNESS VIA CONVEX COMBINATIONS
Alessandro De Palma'a Rudy Bunel? Krishnamurthy (Di) Dvijotham?, M. Pawan Kumar², Robert Stanforth Alessio Lomuscio Inria, École Normale Supérieure, PSL University, CNRS 2 Google DeepMind IImeriall College London alessandzz de-pa de-palma@inria innii..a........... fr.
ABSTRACT
order to train networks for verified adversarial robustness, common to over-approximate the worst-case loss over perturbation regions, resulting in net- works that attain verifiability at the expense standard performance. As shown recent work, better trade-offs between accuracy and robustness can be obtained by carefully coupling adversarial training with over-approximations. We hypothesize that the expressivity of loss function, which formalize the ability span range of trade-offs between lower and upper bounds to the worst-case loss through single parameter (the over-approximation coefficient), is key to attaining state- of-the-art performance. To support our hypothesis, we show that trivial expressive losses, obtained via convex combinations between adversarial attacks and IBP bounds, yield state-of-the-an results across variety of settings in spite of their con- ceptual simplicity. We provide a detailed analysis of the relationship between the over-approximation coefficient and performance profiles across different expressive losses, showing that, while expressivity is essential, better approximations of the worst-case loss are not necessarily linked to superior robustness-accuracy trade-off's
INTRODUCTION
In spite of recent and highly-publicized successes (Jumper et al. 202 Fawzi et al. 2022 serious
concerns over the trustworthiness of deep learning systems remain. In particular, the vulnerability of neural networks adversarial examples (Szegedy et al.) 2014 Goodfellow et al. 2015) questions their applicability to safety-critical domains. As a result, many authors devised techniques to formally prove the adversarial robustness of trained neural networks (Lomuscio & Maganti 2017 Bhlers 2017; Katz er al., (017). These algorithms solve a non-convex optimization problem by coupling network over-upproximaatonn with search techniques (Bunel et al. 2018). While the use of network verifiers was initially limited to models with hundreds of neurons, the scalability of these tools has steadily increased over the recent years (Bunel al.) 2020a Botoeva al. 2020 Henriksen & Lomuscio 2020; Xu et al. 2021 De Palma et al. 202 Wang et al. 2021 Henriksen & Lomuscio 2021 Ferrari et al. 2022). reaching networks of the size of VGG16 (Simonyan & Zisserman [2015] Müller et al.J 2022). Nevertheless, significant gaps between state-of-the-an verified and empirical robustness persist, the latter referring to specific adversarial attacks. For instance, on ImageNet (Deng
et al. 2009), Singh et al. (2023) attain empirical robustness of 57. 777% to foc perturbations of radius c //255, whereas the state-of-the-ar verified robust accuracy (on a downscaled version of
the dataset CChaabazzz al. 2017 9.54% against e 1/255 ZZhng et al. 2022b). In fact, while
empirical robustness can be ac achieved by training the networks against inexpensive attacks (adversarial
training) (Madry et al. 2018: Wong al. 2020 the resulting networks remain hard to verify.
In order to train networks amenable to formal robustness verification (verified training), a number of works (Mirman et al. 2018 Gowal al. 2018 Wong & Kolter 2018 Wong et al. 2018 Zhang et al.)
2020 Xu et al. 2020; Shi et al.) 2021) directly compute the loss over the network over-approximation that are later used for formal verification (verified loss). The employed approximations are typically
Work mostly carried out Imperial College London, and partly the University of Oxford.

---

Published as a conference paper at ICLR 2024
loose, the difficulty of the optimization problem associated with training increases with approx- imation tightness, resulting in losses that are hard to train against (Lee et al., Jovanovic et al.) 2022). As result, while the resulting models are easy to verify, these networks display sub-par standard accuracy. Another line of work enhances adversarial training with verifiabiliy--inducng techniques (Xiao et al.) 20T9: Balluooii & Vechev 2020 [D Palma et al., 2022): by exploiting stronger verifiers, these algorithms yield better results against small perturbations, but under-perform in other settings. More recently, SABR (Müller et al., 2023). combined the advantages of both strategies by computing the loss on ver-aaproximmtions of small "boxes" around adversarial attacks and tuning the size of these boxes on each setting, attaining state-of-the-ar performance. These results were further improved, at the expense of conceptual simplicity and with increased overhead, by carefully coupling IBP or SABR with latent-space adversarial attacks (Mao et al. 2023). While recent work combine attacks with over-aprroximations in different ways, they typically yy seek to accurately represent the exact worst-case loss over perturbation regions (Müller et al. 2023 Mao et al. 2023
Aiming to provide novel understanding of the recent verified training literature, we define class of loss functions, which we call expressive, that range from the adversarial to the verified loss when tuning& parameter E [o, 1]. We hypothesize that this notion of expressivity is crucial to produce state-of-tie ootthe-rrtttttte trade-offs between accuracy and verified robustness, and provide support as follows:
We show that SABR is expressive, and illustrate how other expressive losses can be trivially designed via convex combinations, presenting three examples: (i) CC-IBP, based on combinations between adversarial and over- ver-approximated network outputs within the loss, (ii) MTL-IBP, re- lying on combinations between the adversarial and verified losses, (iii) Exp-IBP, for which the combination is performed between the logarithms of the losses.
We present a comprehensive experimental evaluation of CC-IBP, MTL.-IBP and Exp-IBP on benchmarks from the robust vision literature, demonstrating that the three methods attain state-of-the-ee performance in spite of their conceptual simplicity. We show that a careful tuning of any of the considered expressive losses leads to large improvements, in terms of both standard and verified robust accuracies, upon the best previously-reported results on TinyImageNet and downscaled ImageNet. Our findings point to the importance of expressivity, as opposed to the specific form of the expressive loss function, for verified robustness. Code is available at https://gtt eeriittuur thub. com latpom/aaessaaneeo essandrodepa I ma express vve losses
We analyze the effect of the a parameter on robustness-accuracy trade-offs. Differently from common assumptions in the area, for CC-IBP, MTL-IBP and SABR, better approximations of the worst-case loss do not necessarily correspond to performance improvements.
2 BACKGROUND
We employ the following notation: uppercase letters for matrices (for example, A), boldface letters for vectors (for example, a). [[-] to denote integer ranges, brackets for intervals and vector indices ((a, b) and a(i), respectively). Let f R$ x + Re be a neural network with parameters O E RS and accepting d-dimensional inputs. Given dataset (x,y)
D with points x Rd and labels y E R,, the goal of verified training is to obtain a network that satisfies a given property P IR x R' - {0, 1} on D: yx D = P(f(O, x). y). We will focus on classification problems, with scalar labels E N, and on verifying robustness to adversarial inputs perturbations in C(x, c) == fx' : ||x' x S e):
P(S(0,)) x). v) = [argmmax, f(0, x']] = Vx C(xx))]
(1)
Property PO x) holds when all the points in small neighborhood of x are correctly classified.
2.1 ADVERSARIAL TRAINING
Given a loss function L : X +
R, a network is typically trained by optimizing mine (x)))) (C) x), v)] through variants of Stochastic Gradient Descent (SGD). Hence, training for adversarial robustness requires a surrogate loss adequately representing equation T Bor- rowing from the robust optimization literature, Madry al. (2018) introduce the so-called robust loss:
L (f ().)))))== = max x'E((x..)
((((0))).)))
(2)
2

---

Published as a conference paper at ICLR 2024
However, given the non-convexity of the maximization problem, Madry al. (2018) propose to approximate its computation by a lower bound obtained via an adversarial attack. When C(x, e) is Lo ball, popular attack, PGD, proceeds by taking steps in the direction of the sign of Vx ( x,), y). projecting onto the ball after every iteration. Denoting by Xadv E C(x, e) the point returned by the attack, the adversarial loss is defined follows:
Lav (f(0, = ((a)). S (f((,.x)))))
(3)
Adversarially-trainedd models typically display strong empirical robustness to adversarial attacks and a reduced natural accuracy compared to standard models. However, as shown in the past (Uesato et al. 2018 Athalye et al., 2018), empirical defenses may break under stronger or different attacks (Croce & Hein 2020), calling for formal robustness guarantees holding beyond specific attack scheme. These cannot be obtained in a feasible time on adversarially-tran networks (Xiao et al. 2019). As a result, number of algorithms have been designed to make networks more amenable to formal verification.
2.2
NEURAL NETWORK VERIFICATION
Equation states that a network is provably robust if one can show that all logit differences 2(0 x. y) (f(0,x) [y] f(0, x)) E R", except for the ground truth, are positive V x' E C(x, c).
Hence, formal robustness verification amounts to computing the sign of the following problem:
minx minsy z(0,x' x', [t]
s.t.
x' E C(x,e)
(4)
Problem 4 is known to be NP-hard (Katz et al. 2017): solving it is as hard as exactly computing the robust loss from equation (2) In incomplete verification, the minimization is carried out over a tractable network over-approximattio yielding local lower bounds z(0, x, v) to the logit differences:
z(0, x, v) S minxxe((x.e) z(0,x' y)
ViE [0, [0] 1]]
> O. then the network is proved to be robust. On the other hand, minggy 20,, x. y)] 0, problem 44) is left undecided: the tightness of the bound is hence crucial to maximize the number of verified properties across a dataset (x, y) ~ D. A popular and inexpensive incomplete verifier, Interval Bound Propagation (IBP) (Gowal et al. 2018 Mirman et al. 2018). can be obtained by applying interval arithmetic (Sunaga [958 Hickey et al., 2001 to neural networks (see appendix [A). If an exact solution to (the sign of) problem (4) is required, incomplete verifiers can be plugged in into a branch-and-bound framework (Bunel et al. 2018 20206). These algorithms provide an answer on any given property (complete verification) by recursively splitting the optimization domain (branching), and computing bounds to the solutions of the sub- sub-problems. Lower bounds are obtained via incomplete verifiers, whereas adversarial attacks provide upper bounds. For ReLU activations and high-dimensional inputs, branching is typically performed implicitly by splitting ReLU into its two linear pieces De Palma et al. (2021c); Ferrari et al. (2022).
If min z(0, x, y) [i]
2.3 TRAINING FOR VERIFIED ROBUSTNESS
The verified training literature commonly employs the following assumption (Wong & Kolter 2018):
Assumption 2.1. The loss function L is manslation-invaiiatt C(-z(0, x, y). v) = Furthermore, [(- x, y): y) is monotonic increasing with respect to z x. v) if + y.
v).
Assumption 2.1 holds for popular loss functions such as cross-entropy. In this case, one provide an upper bound to the robust loss L via the so-called verified loss (f x), y). computed on a lower bound to the logit differences z z(,, x. y) obtained from an incomplete verifier Wong & Kolter 2018):
(J x), S (((,,)))) = ((0 x, v).
(5)
number of verified training algorithms rely on a loss of the form Lv (A, x). above, where bounds -2(0,xx x, y) are obtained via IBP (Gowal et al. 2018 Shi et al. 2021). inexpensive linear relaxations [Wong & Kolter 2018), or a mixture of the two Zhang et al. 2020). IBP training has been extensively studied (Wang et al. 2022 Mao et al. 2024). In order to stabilize training, the radius of the perturbation over which the bounds are computed is gradually increased from to the target e value (ramp-up). Earlier approaches (Gowal et al.
2018| Zhang et al. 2020) also transition from the CF (, x). y) + K Ever (f)))), y). with k linearly
natural to the robust loss during ramp-up: (1 K)
increasing from 0 to 0.5 or 1. Zhhan al. (2020) may further transition from lower bounds z z(0, x,
3

---

Published as a conference paper at ICLR 2024
partly obtained via linear relaxations (CROWN-IBPP) to IBP bounds within ( ().0.)),1. y): (1-k) (0))) + + C(- (11-(111))))) 5) ZIBP (, x. y) + ZCROWN-IB ( x. y)) y), with 3 linearly decreased from 1 to 0. Shi et al. (202I) removed both transitions and significantly reduced training times by employing BatchNorm (loffe & Szegedy, 2013) along with specialized initialization and regularization. These algorithms attain strong verified robustness, verifiable via inexpensive incomplete verifiers, while paying a relatively large price in standard accuracy. Another line of research seeks improve standard accuracy by relying on stronger verifiers and coupling adversarial techniques. Examples include maximizing network local linearity (Xiao et al. 2019), performing the attacks in the latent space over network over- approximations (COLT) (Balunovic & Vechev 2020), minimizing the area of over-approximations used verification time while attacking over larger input regions (IBP-R) (De Paima et al. 2022). and optimizing over the sum of the adversarial and IBP losses through specialized optimizer (Fan Li 202T). In most cases & regularization was found to be beneficial. A more recent work, named SABR (Müller et al. 2023), proposes to compute bounds via IBP over parametrized subset of the input domain that includes an adversarial attack. Let us denote by Proj A) the Euclidean projection of set A. Given X3 Proj C(x, Ac)), SABR relies on the following loss:
training 2 with crifiability-inducci
C Z (0, x. y), y), where ZA (0. S 2(0,x', y) Vx C(xx,, Aε) C C(x, c).
(6)
The SABR loss is not necessarily an upper bound for (=(00, x), However, it continuously interpolates between ((f Xadv), y). which it matches when = O, and (f x). y). matched when À 1. By tuning À [0, 1]. SABR attains ofate-oftthe-ee performance under complete veri- fiers (Müller et al. 2023). The recent STAPS (Mao et al. 2023), combines SABR with improvements on COLT, further improving its performance some benchmarks at the cost of added complexity.
Loss EXPRESSIVITY FOR VERIFIED TRAINING
As seen in state-of-the-arr verified training algorithms rely on coupling adversarial attacks with over-approximations, Despite this commonality, there is considerable variety in terms of how these are combined, leading to a proliferation of heuristics. We now outline simple property, which we call expressivity, that we will show to be key to effective verified training schemes:
Definition 3.1. A parametrized family of losses L., (0, x, y) is expressive if:
x. v) S C. (0, x. y) S Ever (f(0, y) A a E [0;
(O, x, v) is continuous and monotonically increasing with respect to [0, 1];
x, (0,((0
(1,0,,,9) Lf
Expressive losses can range between the adversarial loss in equation 3 to the verified loss in equation (5) through the value of a single parameter E [0, 1]. the over-approximation coefficient. As a result, they will be able to span wide range of trade-offs between verified robustness and standard accuracy. Intuitively, if a s 0, then (0, x, y) << (f (()(0x))))) x), resulting in networks hard to verify even with complete verifiers. If a I, then (. x, y) x (f x), y). producing networks with larger verified robustness when using the incomplete verifier employed to compute (6, x. y) but with lower standard accuracy. In general, the most effective a will maximize verifiability via the verifier be employed post-training while preserving as much standard accuracy as possible. The exact value will depend on the efficacy of the verifier and on the difficulty of the verification problem at hand, with larger a values corresponding to less precise verifiers. The loss of SABR from equation (6) satisfies definition 3.1 when setting À = a (see appendix B.44. In order demonstrate the centrality of expressivity, now present three minimalistic instantiations of the definition and later show that they yield state-of-ther thrt results on a variety of benchmarks (16.1)
4 EXPRESSIVITY THROUGH CONVEX COMBINATIONS
We outline three simple ways to obtain expressive losses through convex combinations between adversarial attacks and bounds from incomplete verifiers. Proofs and pseudo-code are provided in appendices B andd respectively.
4

---

Published as a conference paper at ICLR 2024
4.1 CC-IBP
For continuous loss functions like cross-entropy, a family of expressive losses can be easily obtained by taking Convex Combinations (CC) of adversarial and lower bounds to logit differences within L: La, x.)) == f(- [[1 ax) z(0, Xadei v) z x),,),
Proposition 4.1. If C(,,)) is continuous with respect to its first argument, the parametrized loss (a,cc(0, x, is expressive according to definition 3.1
The analytical form of equation (7) when C is the cross-entropy loss, including a comparison to the loss from SABR, presented in appendix [ In order minimize computational costs and to yield favorable optimization problems (Jovanović et al. 2022), we employ IBP to compute z (0, x, y). and refer to the resulting algorithm as CC-IBB. We remark that similar convex combination was employed in the CROWN-IBP (Zhang et al. (020) loss (see {2.3). However, while CROWN-IBP takes a combination between IBP and CROWN-IBP lower bounds to z(0, x, y). we replace the latter by the logit differences associated to an adversarial input Xadv. which is computed via cintoooly-initialzzee FGSM (Wong et al.) 2020) in most of our experiments (see (6] Furthermore, rather than increasing the combination coefficient from 0 to during ramp-up, propose to employ a constant and tunable a throughout training.
4.2 MTL-IBP
Convex combinations can be also performed between loss functions L, resulting in:
La.
(f. (0, x, y) == (1 (f (,,)))))))))))
(f0,
(8)
The above loss lends itself to a Multi-Task Learning (MTL) interpretation (Caruana 1997). with
pirical and verified adversarial robustness as the tasks. Under this view, borrowing terminology from multi-objective optimization, L., (0, x, y) amounts
scalarization of the multi-task problem.
Proposition 4.2. The parametrized loss MT. (0 X. y) is expressive. Furthermore, if Z(- y) is convex with respect to its first argument, (a x. y) S Co,MT x, x, V e [0, 1].
The second part of proposition 4.2 which applies to cross-entropy, shows that
00,x, x, y) can
be seen as an upper bound L. C0,, x for a E [0, Owing to definition 3.1 the bound
will be tight when E {0. 1}. Appendix C shows an analytical form for equation (8) when C is
the cross-entropy loss. As in section 4.1 we use IBP to compute (f x). y): we refer to the resulting algorithm as MTL-IBP. Given its simplicity, ideas related to equation (8) have previously
been adopted in the literature. However, they have never been explored in the context of expressivity and the role of a was never explicitly investigated. Fan & Li (202T) present loss equivalent to equation (). treated as a bascline for the proposed algorithm, but only consider a = 0.5 and use it within costly layer-wise optimization scheme similar to COLT (Balunovic & Vechev) 2020).
While Fan & Li (202T) propose a specialized multi-task optimizer (AdvIBP), we instead opt for scalarizations, which have recently been shown to yield state-of-the-an results multi-task benchmarks when appropriately tuned and regularized (Kurin et al.) [022]] Xin et al. (022). Gowal al. (0018) take convex combination between the natural (rather than adversarial) loss and the IBP loss; however, instead of tuning a constant a, they linearly transition it from 0 to 0.5 during ramp-up (see? 2.3 Mirman et al. (2018) employ C[f(O, x). y) + 0.1 (-softplus(min:z) z(0, x, t)))
4.3
EXP-IBP
For strictly positive loss functions L such as cross-entropy, we can also perform convex combinations between the logarithms of the losses: log Fx.FFx((B (0, x, y) (1 - a) log ((f xndv), y) +
log Lver (J x), v). By exponentiating both sides, we obtain:
Ca Exp (0, x. y) == (( x (1-a) Ler (f(,.)).)))
(9)
which is an expressive loss displaying the over over-approximmtion coefficient in the exponents. Analo- and gously to and (4.2
compute Lver (f, x). y) via IBP, calling the resulting algorithm EXp-IBP. Proposition 4.3. If C R. x N + Ryo, the parametrized loss La ( x, y) is expressive. In addition, L.. Exp (0, x, y) S Mm (f. x, V a E 1).
5

---

Published as a conference paper at ICLR 2024
5 RELATED WORK
As outlined in [2.3 many verified training algorithms work by either directly upper bounding the
robust loss (Gowal et al.
2018
Mirman al. 2018 Wong & Kolter 2018 Zhang et al.) 2020
Xu et al., 2020; Shi et al. ). or by inducing verifiability on top of adversarial training (Xiao
et all] 2019; Balunovic & Vechev 2020 De Palma et al.) 2022 Müller et al. 2023 Mao et al. 2023):
this work falls in the latter category. Algorithms belonging to these classes are typically employed
against Lor perturbations. Other families of methods include Lipschitz-based regularization for
l2 perturbations (Leino et al.) [021; HHuan et al. (021). and architectures that are designed to be
inherently robust for either &2 (Trockman & Kolter 2021; Singla & Feizi [202] [Singla al.. [2022] Singla & Feizi| 2022 Xu et (002)) or Lx (Zhag et al. 202 2022a) perturbations, for which SortNet (Zhang et al. 2022b) is the most recent and effective algorithm. A prominent line of work
has focused on achieving robustness with high probability through randomization (Cohen al.
2019 Salman et al. 2019): : we here focus on deterministic methods.
IBP. presented in 2.2 is arguably the simplest incomplete verifier. A popular class of algorithms replaces the activation by over-approximmtions corresponding to pairs of linear bound, each respectively providing lower or upper bound the activation function (Wong & Kolter 2018
Singh et al. 2018; Zhang et al. 2018)) Singh et al. 2019b). Tighter over-approximmtions can be obtained by representing the convex hull of the activation function (Ehlers 2017 Bunel al. 2020a Xu et al. 2021). the convex hull of the composition of the activation with the preceding linear layer (Anderson et al. 2020; Tjjndraatmadja et al. [2020] De Palma et al.] 2021a b), interactions within the same layer (Singh et al.) 2019at Müller et al.
2022). or by relying on semi-definite
relaxations (Raghunathan et al. 2018 Dathathri et al. [0200] Lan et al. 2022). In general, the tighter
the bounds, the more expensive their computation. As seen in the recent neural network verification competitions (Bak et al.) 2021; Müller et al.) 2022). statc-of-the-ar complete verifiers based on et al.
typically rely on specialized and massively
incomplete verifiers (Wang
2021 Ferrari et al. [022 Zhang et al. 2022c). paired with custom branching heuristics (Bunel
et al. 2020b De Palma al.] 2021c Ferrari al. 2022)
EXPERIMENTAL EVALUATION
We now present experimental results that support the centrality of expressivity, as defined in [ to verified training. In I we compare CC-IBP, MTL-IBP and EXp-IBP with results from the literature, showing that even minimalistic instances of the definition attain state-of-the-art performance on va- riety of benchmarks. In $6.2 and 66.3 we study the effect of the werrapproxiimation coefficient on the performance profiles of expressive losses, highlighting their sensitivity to its value and showing that better approximations of the branch-and-bouut loss do not necessarily results in better performance.
We implemented CC-IBP, MTL-IBP and Exp-IBP in PyTorch (Paszke al. 2019), starting from the training pipeline by Shi et al. 2202T). based on automatic LiRPA (Xu et al. 2020), and exploiting their
specialized initialization and regularization techniques (see appendix F.2). All our experiments use the same 7-layer architecture previous work (Shi et al. 2021 Müller et al. 2023). which employs BatchNorm (Toffe & Szegedy 2015) after every layer. Except on CIFAR-TO with 2/255, for which an 8-step attack is used as previous work (Müller et al., (023). we employ
single-step attacks (Wong et al. 2020) to compute Xady and force the points to be on the perturbation boundary via large step size (see appendices and G.4 ablations the step size and employed adversarial attack, respectively). Unless specified otherwise, the reported verified robust accuracies for our experiments are computed using branch-and-bound, with a setup similar to IBP-R (De Palma eet al. 2022). Specifically, we use the OVAL framework (Bunel et al. 22020b] De Palma et al. c021c). with a variant of the UPB branching strategy (De Palma et al. (2022) and C-3-C N as the bounding algorithm (Wang et al. 2021) (see appendix E). Details pertaining to the employed datasets, hyper-parameters, network architectures, and computational setup are reported in appendix
6.1 COMPARISON WITH LITERATURE RESULTS
Table [ compares the results of CC-IBP, MTL-IBP and Exp-IBP with relevant previous work in terms of standard and verified robust accuracy against Ex norm perturbations. We benchmark on the CIFAR- 10 (Krizhevsky & Hinton 2009). TinylmageNet (Le & Yang. 2015), and downscaled ImageNet
6

---

Published as a conference paper at ICLR 2024
Table 1: Comparison of the expressive losses from 44 with literature results for &so perturbations CIFAR-10, TinyImageNet and downscaled x 64) ImageNet. The entries corresponding the best standard or verified robust accuracy for each perturbation radius are highlighted in bold. For the remaining entries, improvements on the literature performance of the hest-performing Rel.U-based architectures are underlined.
Dataset
Method
Source
Standard acc. [%]
Verified rob. acc. [%
CC-IBP
this work
80.09
63.78
MTL.-IBP
this work
80.11
63.24
EXP-IBP
this work
80.61
61,65
STAPS
Mao al.
2023
79.76
62.98
SABR
al.
79.89
253
SORTNET
hang
67.72
56,94
IBP-R
Mao el al.
80.46
62.03
IBP
Mao el al 2024
68.06
56, 18
ADVIBP
Fan & Li 2021
59.39
48.34
CROWN-IBP
Zhang ot al 2020
71.52
53.97
COLT
Balunovic & Vechev
Z020
78.4
60.5
CIFAR-10
CC-IBP
this work this work
53.71
35.27
MTL-IBP
$3.35
35.44
EXP-1BP
this work
53.97
35.04
STAPS
Mao el al.
2023
52.82
34.65
SABR
Müller ct a
2025
52.38
35.13
SORTNET
Zhang ct al.
20226
54.84
40.39
253
IBP-R
>: Palma et 21 2122
52.74
27.55
IBP
Shi el al.
2021
48.94
34.97
ADVIBP
& 2021
47.14
33.43
CROWN-IBP
Xu et al.
2020
46.29
33.38
COLT
Balunovic Vechev 2020
$1.70
27.50
CC-IBP
this work
38.61
26.39
MTL-IBP
this work
37.56
26.09
EXP-IBP
this work
38.71
TinylmageNet
STAPS
Mao et al.
2023
28.98
22.16
255
SABR
Mao et al
2024
28.97
21,36
SORTNET
hang ct al.
20226
25.69
18.18
IBPt
Mao ct al. 2024
25.40
19.92
CROWN-IBP
Shi ct
2021]
25.62
17.93
CC-IBP
this work
19.62
11.87
MTL.-IBP
this work
20.15
13.13
EXP-IBP
this work
22.73
13.30
ImageNet64
SORTNET
Zhang al. 2022b
14.79
9.54
CROWN-IBP
Xu al.
2020)
16.23
8.73
IBP
Gowal 2018
15.96
6.13
f2x wider network than the architecture used in experiments and larger than those from the relevant works:
202T for IBP, DD Palia al. for IBP-R, Müller al. 2023
SABR.
(64% x 64) (Chrabaszez et al. 2017) datasets. The results from the literature report the best performance attained by each algorithm on any architecture, thus providing a summary of the state-of state-of-the-art. In order to produce fair comparison with literature results, in this section comply with the seemingly standard practice in the area (Gowal et al. 2018 Zhang et al. 2020; Shi et al. [022]] Müller et al.) 2023) and directly tune the evaluation trade-offs, CC-IBP, MTL-IBP and EXp-IBP all attain state-of-the-an
Table I shows that, in terms of robustness-accen accuracc
performance. In particular,
no literature results correspond to better trade-offs in any of the considered benchmarks except for CIFAR-10 with = 8/255, where specialized architectures such as SortNet attain better robustness- accuracy trade-offs. On larger datasets, our Exp-IBP, MTL-IBBP and CC-IBP experiments display significant improvements upon the results from the literature. For TinylmageNet, standard and verified robust accuracies are increased by at least 8.58% and 3.93%. respectively. On downscaled ImageNet, the improvements correspond robust accuracy. In order to further investigate the role of expressivity in these results, we performed TinyImageNet and
least 3.39% for standard accuracy and to at least 2.33% for verified
own tuning of SABR MMäller al. (023), which satisfies definition ImageNet64 and present the relative results in appendix (.6) Table TableW shoows that, when carefully tuned, all the considered expressive losses (CC-IBP, MTL.-IBP, Exp-IBP and SABR) attain relatively similar
7

---

Published as a conference paper at ICLR 2024
performance profiles and markedly improve upon previously-reported TinyImageNet and ImageNet64 results. Given the costs associated with ImageNet64, we only attempted branch-ame wranch-and-bore and-bound based verification networks with 2 5 10 for all expressive losses, skewing the performance in favor of Exp-IBP owing to its lower loss values (see proposition 4.3 and table 3). We speculate that better trade-offss in this setup may be obtained when employing lower coefficients. In addition, MTL-IBP performs significantly better than the closely-reiated AdvIBP (see
(4.2) on all benchmarks,
confirming the effectiveness of an appropriately tuned scalarization (Xin et al. 2022). Fan & Li (202T) provide results for the use of Lu.s.MII (0, y) within COLT-like stage-wise training procedure, treated as baseline, on CIFAR- 10 with c 8/255, displaying 26. 26.22% IBP verified robust accuracy. These results are markedly worse than those we report for MTL-IBP, which attains 34.61% IBP verified robust accuracy with a = 0.5 table (see appendix F. We believe this discrepancy to be linked to the commonalities with COLT, which under-performs in this setting, and, in line with similar results in the multi-task literature (Kurin et al., 2022), to our use of specialized initialization and regularization from Shi et al. (202T). Additional experimental data is presented in the appendices: appendix G.2 provides an indication of training cost, appendix G.1 presents MNIST results, and appendix G.3 displays verified robust accuracies under less expensive verifiers. Remarkably, on TinylmageNer and downscaled ImageNet, CC-IBP, MTL-IBP and Exp-IBP all attain better verified robust accuracy than literature results even without resorting complete verifiers.
6.2 SENSITIVITY TO OVER ETER-APPROXIMATION COBFFICIENT
Figure I Irpports standard, adversarial, and verified robust accuracies under different verifiers when varying the value of a for CC-IBP, MTL-IBP and Exp-IBP. BaB denotes verified accuracy under the complete verifier from table while CROWN/IBP the one under the best bounds between full backward CROWN and IBP. Adversarial robustness computed against the attacks performed within the employed BaB framework (see appendix F As expected, the standard accuracy steadily decreases with increasing a for both algorithms and, generally speaking (except for MTL-IBP and Exp-IBP when = 8/25s), the IBP verified accuracy will increase with a. As 2023). the behavior of the adversarial and verified robust accuracies under tighter verifiers is less straightforward. In fact, depending on the setting and the algorithm, a given accuracy may first increase and then decrease with a. This sensitivity highlights the need for careful tuning according to the desired robustness-accurge
SABR (Müller et al.
trade-off and verification budget. For instance, figure D suggests that, for e = 8/255, the best trade-offss between BaB verified accuracy and standard accuracy lie around = 0.5 for both CC-IBP, MTL-IBP and Exp-IBP. When e 2/255, this will be around a 10 for CC-IBP, and when a E (10-3, 10 for MTL-IBP, whose natural accuracy decreases more sharply with a (see appendix F. Exp-IBP extremely sensitive between BaB-verified robustness and standard accuracy lying in a small neighborhood of a 10-1 Note that, as expected from proposition 4.3 EXP-IBP requires larger values of a than MTT.--IP in order attain similar performance profiles. Furthermore, larger values appear to be beneficial against larger perturbations, where branch-and-bood is less effective. Appendix G.7 carries out a similar analysis on the loss values associated to the same networks.
on this setup. with the best trade-offs
80
Accuracy [99]
60
60
60
50
50
50
40
40
40
40
40
Sumderd Adreeer
10
10
20-2
200
0
1
100
0.5
1.0
1.0
0.5
1.0
(a) CC-IBP. 2/255.
MTL-IBP.
(c) EXp-IBP.
(d) CC-IBP,
(c) MTL-IBP,
(f) Exp-IBP,
2/268.
2/250.
8/255.
8/205.
8/265.
Figure I: Sensitivity of CC-IBP, MTP and EBP to the convex combination coefficient a. We report standard, adversarial and verified robust accuracies (with different verifiers) under fox perturbations the first 1000 images of the CIFAR- 10 test set. The legend plot [(b] applics to sub- sub-figures.
8

---

Published as a conference paper at ICLR 2024
1.5
1.5
1.5
Validation Loss
1.0
1.0
1.0
1.0
1.0
1.0
0.5
0.5
0.5
0.5
0.5
0.5
0.0
0.0
0.0
0.0
0.0
10
10-2
10-1
10-2
2
(a) CC-IBP, 9/200.
(b) MTL-IBP,
(c) SABR,
(d) CC-IBP.
(c) MTL-IBP,
(1) SABR,
2/255.
c 2/255.
= 8/255.
$/255.
6 $/255.
Figure Relationship between the over-approximation coefficient and the standard loss, the branch-and-boun loss, its approximation error and RMSE (relative to the expressive loss employed during training) on a holdout validation set of CIFAR-10. While the standard loss is computed on the entire validation set, sanch-andd-bunde related statistics are limited to the first 100 images. The dashed vertical line denotes the a value minimizing the sum of the standard and wranch-and-bound losses. The legend in plot 2(b) applies to all sub-figures.
6.3 BRANCH-AND-BOUNNG LOSS AND APPROXIMATIONS
A common assumption in previous work is that better approximations of the worst-case loss from equation 2 will result in better trade-offs between verified robustness and accuracy (Müller et al.
2023 Mao et al., 2023). In order to investigate the link between expressive losses, the worst-case loss, and a principled tuning process, we conduct an in-depth study on a CIFAR-10 validation set for CC-IBP, MTL-IBP and SABR. Specifically, we evaluate on a holdout set taken from the last 20% of the CIFAR- 10 training images, and train the same architecture employed in $6.1 on the remaining 80%, tuning [1 10 3,3 x 10 for c $/255. Given that computing the worst-case loss on networks of practical interest intractable, we replace by CaB (f x,), y), computed by running branch-and. bound (BaB) for 15 seconds on each logit difference, without returning early for verified properties so as to tighten the bound. Figure 2 reports values for the standard loss, the branch-and-han bound loss and two measures for its approximation: the average value of (0. x4, y) Leas (f xx), y)) (BaB Error) and the square root of the average of its square (BaB RMSE). Observe that the best-performing model, here defined as the one with the smallest sum of the standard and BaB losses, does not necessar- ily correspond to the points with the best BaB loss approximation.
10-3 $ 10-2,3 10-2 2] for e 2/235 and
{0.3. 0.4, 0.5. 0.6, 0.7]
(0,,x),
particular, aver-xppros for
(BaB Error 0) display better validation trade-offs for 2/255, and
e 8/255. Given that CRaR (/(00 x), y) 2 (O x), v). the results on e 2/255 demonstrate that accurate worst-case loss approximations do not necessarily correspond to better performance: neither in terms of verified robustness alone, nor in terms of trade-offs with accuracy. As shown in appendix G.5] the selected a values result in similar (state-of-ther the-rrr for ReLU networks) CIFAR- 10 robustness- accuraay trade-offs across the three expressive losses here considered, suggesting the importance of expressivity, rather than of the specific employed heuristic, for verified training.
CONCLUSIONS
We defined a class of parametrized loss functions, which we call expressive, that range from the adversarial loss to the IBP loss by means of single parameter a E j0, 1]. We argued that expressivity key to maximize trade-off' between verified robustness and standard accuracy, and supported this claim by extensive experimental results. In particular, we showed that SABR is expressive, and demonstrated that even three minimalistic instantiations of the definition obtained through convex combinations, CC-IBP, MTL-IBP and Exp-IBP, attain state-of-the-arr results variety of benchmarks. Furthermore, we provided a detailed analysis of the influence of the over-approximation coefficient the properties of networks trained via expressive losses, demonstrating that, differently from what previously conjectured, better approximations of the sanch-and-boune loss do not necessarily result in better performance.

---

Published as a conference paper at ICLR 2024
ETHICS STATEMENT
We do not foresee any immediate negative application of networks that are provably robust to adversarial perturbations. Nevertheless, the development of systems that are more robust may hinder any positive use of adversarial examples (Albert et al. 202T), potentially amplifying the harm caused by unethical machine learning systems. On the other hand, the benefits of provable robustness include defending ethical machine learning systems against unethical attackers. Finally, while we demonstrated state-of-the- oftthe-art performance on suite of commonly-employee vision datasets, this does not guarantee the effectiveness of our methods beyond the tested benchmarks and, in particular, on different data domains.
REPRODUCIBILITY STATEMENT
Code to reproduce our experiments and relevant trained models are available at afftttss///githus Com/ cow/alessandaaaooooooooooooo
lossees Pseudo-code for both losses can be found in appendix [D] Training details, hyper-parameters and computational setups are provided in sections 4 and appendix F Appendix [..8 provides providds an indication of experimental variability for MTL-IBP and CC-IBP by repeating the experiments for a single benchmark a further 3 times.
ACKNOWLEDGMENTS
The authors would like to thank the anonymous reviewers for their constructive feedback, which strengthened the work, and Yuhao Mao, who led us correction of the description of our imple- mentation details in appendix F.2 This research was partly funded by UKRI ("SAIS: Secure AI AssistantS", EP/T026731/1) and Innovate UK (EU Underwrite project "EVENFLOW", 10042508).
The work was further supported by the "SAIF" project, funded by the "France 2030" government investment plan managed by the French National Research Agency, under the reference ANR-23- PEIA-0006. While at the University of Oxford, ADP was supported by the EPSRC Centre for Doctoral Training in Autonomous Intelligent Machines and Systems, grant EP/LO15987// and IBM PhD fel- lowship. AL is supported by a Royal Academy of Engineering Fellowship in Emerging Technologies.
REFERENCES
Kendra Albert, Maggie Delano, Bogdan Kulynych, and Ram Shankar Siva Kumar. Adversarial for good? How the adversarial MI. community's 's values impede socially beneficial uses of attacks. In ICMI. / workshop on A Blessing in Disguise: The Prospects and Perils of Adversarial Machine Learning, 2021.
Ross Anderson, Joey Huchette, Will Ma, Christian Tjandraatmadja, and Juan Pablo Vielma. Strong mixed-integer programming formulations for trained neural networks. Mathematical Programming, 2020.
Anish Athalye, Nicholas Carlini, and David A. Wagner. Obfuscated gradients give false sense of security: circumventing defenses adversarial examples. In International Conference on Machine Learning, 2018.
Stanley Bak, Changliu Liu, and Taylor Johnson. The second international verification of neural net- works competition (VNN-COMP 2021): Summary and results. arXiv preprint arXiv:2109.00498. 2021.
Mislav Balunovic and Martin Vechev. Adversarial training and provable defenses: Bridging the gap. International Conference on Learning Representations, 2020.
E. Botoeva, P. Kouvaros, J. Kronqvist, A. Lomuscio, and R. Misener. Efficient verification of neural networks via dependency analysis. In AAAI Conference on Artificial Intelligence, 2020.
Stephen Boyd and Lieven Vandenberghe. Convex optimization. Cambridge university press, 2004.
Rudy Bunel, Ilker Turkaslan, Philip HS Torr, Pushmeet Kohli, and M Pawan Kumar. A unified view of piecewise linear neural network verification. Neural Information Processing Systems, 2018
10

---

Published as a conference paper at ICLR 2024
Rudy Bunel, Alessandro De Palma, Alban Desmaison, Krishnamurthy Dvijotham, Pushmeet Kohli, Philip HS Torr, and M Pawan Kumar. Lagrangian decomposition for neural network verification. Conference Uncertainty in Artificial Intelligence, 2020a.
Rudy Bunel, Jingyue Lu, Ilker Turkaslan, P Kohli, P Torr, and M Pawan Kumar. Branch and bound for piecewise linear neural network verification. Journal of Machine Learning Research, 2 21(2020), 2020b.
Rich Caruana. Multitask learning. Machine Learning, 28(1):4 1997.
Patryk Chrabaszez, Ilya Loshchilov, and Frank Hutter, downsampled variant of ImageNet as an alternative to the CIFAR datasets. arXiv:1707.08819, 2017.
Jeremy Cohen, Elan Rosenfeld, and Zico Kolter. Certified adversarial robustness via randomized smoothing. In International Conference on Machine Learning. 2019.
Francesco Croce and Matthias Hein. Reliable evaluation of adversarial robustness with an ensemble of diverse parameter- free attacks. In International Conference on Machine Learning, 2020.
Sumanth Dathathri, Krishnamurthy (Dj) Dvijotham, Alex Kurakin, Aditi Raghunathan, Jonathan Uesato, Rudy Bunel, Shreya Shankar, Jacob Steinhardt, Ian Goodfellow, Percy Liang, and Pushmeet Kohli. Enabling certification of verification iagiicattoo-anostiiccc networks via memory-effiiicn semidefinite programming. In Neural Information Processing Systems, 2020.
Alessandro De Palma, Harkirat Singh Behl, Rudy Bunel, Philip H. S. Torr, and M. Pawan Kumar. Scaling the convex barrier with active sets. International Conference on Learning Representations, 2021a.
Alessandro De Palma, Harkirat Singh Behl, Rudy Bunel, Philip H. S. Torr, and M. Pawan Kumar. Scaling the convex barrier with sparse dual algorithms. arXiv preprint arXiv:2101.0588 202
Alessandro De Palma, Rudy Bunel, Alban Desmaison, Krishnamurthy Dvijotham, Pushmeet Kohli, Philip HS Torr, and M Pawan Kumar. Improved branch and bound for neural network verification via Lagrangian decomposition. arXiv preprint arXiv:2 arXiv:2104.067 104.067 18, 2021c
Alessandro De Palma, Rudy Bunel, Krishnamurthy Dvijotham, M. Pawan Kumar, and Robert Stanforth. IBP regularization for verified adversarial robustness via branch-and- bound.. In ICML 2022 Workshop on Formal Verification of Machine Learning, 2022.
Jia Deng, Wei Dong, Richard Socher, Li-Jia Li, Kai Li, and Li Fei-Fei. Imagenet: A large-scale hierarchical image database. In Proceedings of the IEEE conference on computer vision and pattern recognition, 2009.
Yinpeng Dong, Fangzhou Liao, Tianyu Pang, Hang Su, Jun Zhu, Xiaolin Hu, and Jianguo Li. Boosting adversarial attacks with momentum. In Proceedings of the IEEE conference on computer vision and patlern recognition, pp. 9185-9193, 2018.
Ruediger Ehlers. Formal verification of piece-wise linear feed-forward neural networks. Automated Technology for Verification and Analysis, 2017.
Jiameng Fan and Wenchao Li. Adversarial training and provable robustness: A tale of two objectives. In AAAI Conference on Artificial Intelligence, 2021.
Alhussein Fawzi, Matej Balog, Aja Huang, Thomas Hubert, Bernardino Romera-Paredes, Moham- madamin Barekatain, Alexander Novikov, Francisco R Ruiz, Julian Schritwieser,, Grzegorz Swirszez, et al. Discovering faster matrix multiplication algorithms with reinforcement learning. Nature, 2022.
Claudio Ferrari, Mark Niklas Mueller, Nikola Jovanović, and Martin Vechev. Complete verification via multi-neuron relaxation guided and-oh-ddd- International Conference Learning Representations, 2022.
Ian J Goodfellow, Jonathon Shlens, and Christian Szegedy. Explaining and harnessing adversarial examples. International Conference Learning Representations, 2015.

---

Published as a conference paper at ICLR 2024
Sven Gowal, Krishnamurthy Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Uesato, Timothy Mann, and Pushmeet Kohli. On the effectiveness interval bound propagation for training verifiably robust models. Workshop on Security in Machine Learning, NeurlPS, 2018.
P. Henriksen and A. Lomuscio. Efficient neural network verification via adaptive refinement and adversarial search. In European Conference on Artificial Intelligence, 2020.
Henriksen and A. Lomuscio. Deepsplit: An efficient splitting method for neural network verification via indirect effect analysis. In Proceedings of the 30th International Joint Conference Artificial Intelligence (IJCAI21), 2021.
Timothy Hickey, Qun Ju, and Maarten H Van Emden. Interval arithmetic: From principles to implementation. Journal of the ACM (JACM), 2001.
Yujia Huang, Huan Zhang. Yuanyuan Shi, Zico Kolter, and Anima Anandkumar. Training certifiably robust neural networks with efficient local lipschitz bounds. In Neural Information Processing Systems, 2021.
Sergey Ioffe and Christian Szegedy. Batch normalization: Accelerating deep network training by reducing internal covariate shift. In International Conference on Machine Learning, 2015.
Nikola Jovanović, Mislav Balunović, Maximilian Baader, and Martin T. Vechev. On the paradox of certified training. In Transactions on Machine Learning Research, 2022.
John Jumper. Richard Evans, Alexander Pritzel, Tim Green, Michael Figurnow, Olaf Ronneberger,
Kathryn Tunyasuvunakoo, Russ Bates, Augustin Zidek, Anna Potapenko, al. Highly accurate protein structure prediction with alphafold. Nature, 2021.
Guy Katz, Clark Barrett, David Dill, Kyle Julian, and Mykel Kochenderfer. Reluplex: An efficient SMT solver for verifying deep neural networks. Computer Aided Verification, 2017.
A. Krizhevsky and G. Hinton. Learning multiple layers of features from tiny images. Master's 's thesis, Department of Computer Science, University of Toronto, 2009.
Vitaly Kurin, Alessandro De Palma, Ila Kostrikov, Shimon Whiteson, and M. Pawan Kumar. In defense of the unitary scalarization for deep multi-task learning. In Neural Information Processing Systems, 2022.
J. Lan, Y. Zheng, and A. Lomuscio. Tight neural network verification via semidefinite relaxations and linear reformulations. AAAI Conference on Artificial Intelligence, 2022.
Ya and Xuan S. Yang. Tiny imagenet visual recognition challenge. 2015.
Yann LeCun, Corinna Cortes, and CJ Burges. Mnist handwritten digit database. ATT Labs [Online]. Available: http://www.ccu..o/////bb//e
2, 2010.
Sungyoon Lee, Woojin Lee, Jinseong Park, and Jaewook Lee. Towards better understanding of training certifiably robust models against adversarial examples. Neural Information Processing Systems, 2021.
Klas Leino, Zifan Wang, and Matt Fredrikson. Globally-robust neural networks. In International Conference on Machine Learning, 2021.
Alessio Lomuscio and Lalit Maganti. An approach to reachability analysis for feew-forward ReLU neural networks. arXiv:1706.07355. 2017.
Aleksander Madry, Aleksandar Makelov, Ludwig Schmidt, Dimitris Tsipras, and Adrian Vladu. Towards deep learning models resistant to adversarial attacks. International Conference on Learning Representations, 2018.
Yuhao Mao, Mark Niklas Müller, Mare Fischer, and Martin Vechev. TAPS: Connecting certified and adversarial training. Neural Information Processing Systems, 2023.
Yuhao Mao, Mark Niklas Müller, Mare Fischer, and Martin Vechev. Understanding certified training with interval bound propagation. In International Conference Learning Representations, 2024.
12

---

Published as a conference paper at ICLR 2024
Matthew Mirman, Timon Gehr, and Martin Vechev. Differentiable abstract interpretation for provably robust neural networks. International Conference on Machine Learning. 2018.
Mark Niklas Mülerr, Christopher Brix, Stanley Bak, Changliu Liu, and Taylor Johnson. The second international verification of neural networks competition (VNN-COMP 2021): Summary and results. arXiv preprint 2rXiv:2212.1037777 2022.
Mark Niklas Müller, Gleb Makarchuk, Gagandeep Singh, Markus Püschel, and Martin Vechev. PRIMA: General and precise neural network certification via scalable convex hull approximations. Proceedings of the ACM Programming Languages, 2022.
Mark Niklas Müller, Franziska Eckert, Marc Fischer, and Martin Vechev. Certified training: Small boxes are all you need. In International Conference on Learning Representations, 2023.
Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, Alban Desmaison, Andreas Kopf, Edward Yang, Zachary DeVito, Martin Raison, Alykhan Tejani, Sasank Chilamkurthy, Benoit Steiner, Lu Fang, Junjie Bai, and Soumith Chintala. Pytorch: An imperative style, high-perffomance deep learning library. Neural Information Processing Systems, 2019.
Aditi Raghunathan, Jacob Steinhardt, and Percy S Liang. Semidefinite relaxations for certifying robustness to adversarial examples. Neural Information Processing Systems, 2018.
Hadi Salman, Greg Yang. Jerry Li, Pengchuan Zhang, Huan Zhang, Ilya Razenshteyn, and Sébastien Bubeck. Provably robust deep learning via adversarially trained smoothed classifiers. In Neural Information Processing Systems, 2019.
Zhouxing Shi, Yihan Wang, Huan Zhang, Jinfeng Yi, and Cho-Jui Hsieh. Fast certified robust training with short warmup. In Neural Information Processing Systems, 2021.
Karen Simonyan and Andrew Zisserman. Very deep convolutional networks for large-scale image recogmition. International Conference on Learning Representations, 2015.
Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin Vechev. Fast and effective robustness certification. Neural Information Processing Systems, 2018
Gagandeep Singh, Rupanshu Ganvir, Markus Püschel, and Martin Vechev. Beyond the single neuron convex barrier for neural network certification. Neural Information Processing Systems, 2019a.
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. An abstract domain for certifying neural networks. Proceedings of the ACM on Programming Languages, 2019b.
Naman Singh, Francesco Croce, and Matthias Hein. Revisiting adversarial training for ImageNet: Architectures, training and generalization across threat models. arXiv:2303.01870 2023.
Sahil Singla and Soheil Feizi. Skew orthogonal convolutions. In International Conference on Machine Learning, 2021.
Sahil Singla and Soheil Feizi. Improved techniques for deterministic 12 robustness. In Neural Information Processing Systems, 2022.
Sahil Singla, Surbhi Singla, and Soheil Feizi. Improved deterministic 12 robustness on CIFAR-10 and CIFAR-100. In International Conference Learning Representations, 2022.
Teruo Sunaga. Theory of an interval algebra and its application numerical analysis. RAAG Memoirs, 1958.
Christian Szegedy, Wojeiech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian Goodfellow, and Rob Fergus. Intriguing properties of neural networks. International Conference on Learning Representations, 2014.
Christian Tjandraatmadja. Ross Anderson, Joey Huchette, Will Ma, Krunal Patel, and Juan Pablo Vielma. The convex relaxation barrier, revisited: Tightened single-neuron relaxations for neural network verification. Neural Information Processing Systems, 2020.
13

---

Published as a conference paper at ICLR 2024
Asher Trockman and J. Zico Kolter. Orthogonalizing convolutional layers with the cayley transform. In International Conference on Learning Representations, 2021.
Jonathan Uesato, Brendan O' O'Donoghue, Aaron van den Oord, and Pushmeet Kohli. Adversarial risk and the dangers of evaluating against weak attacks. In International Conference on Machine Learning, 2018.
Shiqi Wang, Huan Zhang, Kaidi Xu, Xue Lin, Suman Jana, Cho-Jui Hsieh, and J Zico Kolter. Beta-CROWN: Efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification. Neural Information Processing Systems, 2021.
Yihan Wang, Zhouxing Shi, Quanquan Gu, and Cho-Jui Hsich. On the convergence of certified robust training with interval bound propagation. In International Conference on Learning Representations 2022.
Eric Wong and Zico Kolter. Provable defenses against adversarial examples via the convex outer adversarial polytope. International Conference on Machine Learning, 2018.
Eric Wong, Frank Schmidt, Jan Hendrik Metzen, and J. Zico Kolter. Scaling provable adversarial defenses. Neural Information Processing Systems, 2018.
Eric Wong, Leslie Rice, and Zico Kolter. Fast is better than free: Revisiting adversarial training. In International Conference Learning Representations, 2020.
Kai Xiao, Vincent Tjeng, Nur Muhammad Shafiullah, and Aleksander Madry. Training for faster adversarial robustness verification via inducing relu stability. International Conference on Learning Representations, 2019.
Derrick Xin, Behrooz Ghorbani, Ankush Garg, Orhan Firat, and Justin Gilmer. Do current multi-task optimization methods in deep learning even help? In Neural Information Processing Systems, 2022.
Kaidi Xu, Zhouxing Shi, Huan Zhang, Yihan Wang, Kai- Wei Chang, Minlie Huang, Bhavya Kailkhura, Xue Lin, and Cho-Jui Hsieh. Automatic perturbation analysis for scalable certified robustness and beyond. In Neural Information Processing Systems, 2020.
Kaidi Xu, Huan Zhang. Shiqi Wang, Yihan Wang. Suman Jana, Xue Lin, and Cho-Jui Hsich. Fast and complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. In International Conference on Learning Representations, 2021.
Xiaojun Xu, Linyi Li, and Bo Li. Lot: Layer-wise orthogonal training on improving 12 certified robustness. In Neural Information Processing Systems, 2022.
Bohang Zhang, Tianle Cai, Zhou Lu, Di He, and Liwei Wang. Towards certifying l-infinity robustness using neural networks with l-inf-dist neurons. In International Conference on Machine Learning. 2021.
Bohang Zhang, Du Jiang, Di He, and Liwei Wang. Boosting the certified robustness of I-infinity distance nets. In International Conference Learning Representations, 2022a.
Bohang Zhang, Du Jiang, Di He, and Liwei Wang. Rethinking lipschitz neural networks and certified robustness: A boolean function perspective. In Neural Information Processing Systems, 2022b.
Huan Zhang, Tsui- Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel. Efficient neural network robustness certification with general activation functions. Neural Information Processing Systems, 2018.
Huan Zhang, Hongge Chen, Chaowei Xiao, Sven Gowal, Robert Stanforth, Bo Li, Duane Boning, and Cho-Jui Hsieh. Towards stable and efficient training of verifiably robust neural networks. International Conference Learning Representations, 2020.
Huan Zhang, Shigi Wang, Kaidi Xu, Linyi Li, Bo Li, Suman Jana. Cho-Jui Hsich, and Zico Kolter. General cutting planes for counddpropagationn Information Processing Systems, 2022c.
neural network verification. Neural
14

---

Published as a conference paper at ICLR 2024
A INTERVAL BOUND PROPAGATION
As outlined in 2..2 incomplete verification aims to compute lower bounds z x, y) to the logit differences z(0,x, y) == (f(0,x) x) f(0, x)) of network f(0, x) for the perturbation domain C(x, e). In the following, we will assume that the last layer of [(0, x) and the difference in the definition of 2 y) have been merged into a single linear layer, representing z (, x, y) as an n-layer network. We will henceforth use [a]+ max a, 0) and [a]- == min(a. a, 0). Furthermore, let W; and b2 respectively the weight matrix and the bias of the k-th layer of 200, y)- In the case of monotonically increasing activation functions a, such as ReLU, IBP computes z(0, x. y) as I, from the following iterative procedure:
Figure 3: IBP ReLU over-
approximation. with E [t, ú] for the considered input domain.
i = ec(x)) Wix's + b
in [We] a(i= [Wa)-o + b
k E [2, n]
ú1 maxx) Wix' + b1
4. = [W+]+ ( (ūk-)) + bb
(10)
For 20 perturbations of radius c, C(x, = fx' 1|x x1xx S c}: the linear minimization and maximization oracles evaluate to ú = Wix + [ + b and i Wix [W1 Will + b respectively. IBP corresponds solving an approximation of problem (4) where all the network layers are replaced by their bounding boxes. For instance, given some and á from the above procedure, the ReLUs are replaced by the over-approximation depicted in figure 3 Assuming [W+I+ and [W*]- have been pre-computed for & E [2. n]. the cost of computing z x. y) via IBP roughly corresponds to four network evaluations. This can be further reduced to roughly two network evaluations (pre-compuiing [W& for E [2, n2) by using ú (ix+1e)/2 + (ū,, (i,.11))22 and 1 (i.+i.)/2 (ū.-1) (4/22.
B EXPRESSIVITY PROOFS
We here provide the proofs of the expressivity of CC-IBP (appendix B.I MTL-IBP (appendix B.2 Exp-IBP (appendix BB3), and SABR (appendix B.4).
B.1 CC-IBP
Proposition 4.1. If L(:,)) y) is continuous with respect to its first argument, the parametrized loss (o, x) is expressive according to definition 3.1
Proof. Let us recall that (c, x, = L(- 1-1[(1a))) z(0, Xadv, y) + z(0, x, y)] y). Triv- ially, Co.co x, y) L(f(0, Xadv X,dv), v), and C1,00 x, Lver [fer(f(0, x), v). By definition. z(0, x, y) < z( Xalv: y). as Xadv E C(x,e). Hence,
2 x, y) < (1 - a) 2 X y) + a z x, v) < z(0, x(0,xx Xadv: v) for a e [0.1].
Then, owing to assumption 2.1 and to z0, Xadv, [)l = 20, x, y>[y} = 0, we can apply the loss
function [(-,8) y) while leaving the inequalities unchanged, yielding:
L(f(O, x.d)), 3) (0, v) S Lver Lver (f x).
Finally, if C(-y) is continuous with respect to its first argument, then C(- [[1 a) 2(0, Nadv: y) + z(0,x, x, y)], is continuous with respect to a (composition of continuous functions), which concludes the proof.
B.2 MTL--BP
Proposition 4.2. The parametrized loss L., (0, x, y) is expressive. Furthermore, if C(:y) is convex with respect its first argument, Ca, O y) S (0, x. V [0,
15

---

Published as a conference paper at ICLR 2024
Proof. We start by recalling that La (6. x. y) := = (1-1))aaa (f ((d((()._.d)).....
Xadv).9) y) + ve ((((((()))))) y).
The proof for the first part of the statement closely follows the proof for proposition [.1 while not requiring assumption 2.1 nor continuity of the loss function.
The inequality La,ce A x, u) S L.. x. y) A a E [0. 1] trivially follows from the definition of convex function (Boyd & Vandenberghe 2004 section 3.1.1) and equation (5).
B.3 EXP-IBP
Proposition 4.3. 1f : X + Rya. the parametrized loss La, (0, x. v) is expressive. In addition, Co, Exp (0, x, 1)) S Lo, (0, v) V E [0,
Proof. Recall that Exp (6, x, y) == [(f Xuty), ). [1 Lver (0, y)" It is easy to see that Ex (0, x. y) [(f X 1), and Li (.
Ever f(, f()..)))) v)- As outlined in $4.3) log Exp. x, 1/ = (1 a)) log (0, Xat)); v) + a log Lver ( x), y), which is continuous and
monotonically increasing with respect a, and satisfies the following inequality for a E [0, 1]:
log ((f(() v) < (1 a) log (( Xadv), 3) + log Lver (f0 S log (f v).
By applying the exponential function, which, being monotonically increasing and continuous, pre- serves the monotonicity and continuity of log Fxp 0, x, y). we obtain
(O, Xadv), v) S Exp x, S (f(0, va [0, 1],
proving expressivity. In order to prove that La Exp x. v) I Ca,MIL (0, 0, V E [0, 1]. we start from:
log (1- (1-a) Xmiv) t Lyer (0, x), N
a1 log [( xar)). v) + a log Lver (O,,
which holds for any a E [0, I] owing to the concavity of log. By exponentiating both sides and recalling their definitions, we get (0.8xp(0xx,)) S (0,x,(0,x, V a [0, 1]. conclud- ing the proof.
B.4 SABR
Lemma B.1. For networks with monotonically increasing and continuous activation functionn, if C(x,e) e) := fx': =|Ix' x||30 I <} and when computed via IBP, z 2x x. y) as defined in equation (6)
is continuous with respect to X.
= Proof. For C(x,c) = (x' |x' - -xl1 S c), we can write c( = [x - c,
[lo Un] and C(xx, = (o un.x], with 1o,1 = min (max lo + Xe), ug Aee - de and Uo. = main(maxxxxaa
la + Xe), un Xe) + λe, which are continuous functions of À as max, min, linear combinations and compositions of continuous functions preserve continuity. The SABR bounds (0, x, y) can then be computed as i, from equation (10). using [o,,,, Ho.x] as input domain. In this case, úU = [W+]4 No. + [Wa]- lo.A + by and i = [Wa] lo. + [Wa]- No. -o,A + by- The continuity of (0, y) with respect to À then follows from its computation as the composition and linear combination of continuous functions.
Proposition B.2, If ((:.)) is continuous with respect to first argument and z (0.x, x, y) as defined in equation (6) is continuous with respect to X E 10, 1,, the SABR (Müller et al. (023) loss function L( ZA 0, x, y) y) is expressive according to definition 3.7
Xe) C C(x, e). with Xx = Proj(x aadvv C(x, 6 - Ae)). We can hence define ( X y) = 2x x, y) - z(0 x', S for any x' C(XX, Ae). As C(xy, Aee) C C(XX, Xε) for any X S X, (0, y) will monotonically
Proof. Recalling equation (6). z, (0, x, y) S 2(0,x' y) V x'
decrease with X, and so will (0, x', y). We can hence re-write the SABR loss as:
L( zA (0, x. v). y) = L( (z(e Xadv: 8) + (ZA (0, x, y) - z(0, Xudv: v)) v)
L( [z( 0 X v) + 5x (0. Xulv. v)] v/)
16

---

Published as a conference paper at ICLR 2024
Then, 60 Z1 Z1 x, y) = z(0,x, x. y). proving the last two points of definition 3.1 Continuity follows from
Xadv, y) O, as X Xadv and hence Zo
z(0, Xudv, y). Furthermore,
the fact that compositions of continuous functions (C(..) and Z (,, x.,xy) y)) continuous. The
remaining requirements follow from using assumption 2.1 and the non-positivity and monotonicity of xx (0, X y)-
C Loss DETAILS FOR CROSS-ENTROPY
Assuming the underlying loss function L be cross-entropy,
present analytical form of the expressive losses presented in 44.1 $4.2 and 4.3 along with a comparison with the loss from SABR (Müller al. 2023).
When applied on the logit differences z(0, x. x.y) (see (.3)). the cross-entropy can be written as
2(- x, y). y) = log(1 + Eity e e02((x)))) by exploiting the properties of logarithms and z(0, x. y>lvl = (see 22). In fact:
L(-2 v). v) log
Σ e e-x,xxx x00x,,y)11
log
1
log 1+
Σ it
x00xx,0)1
1+ Eidg e 200,x,0011
C.I CC-IBP
Proposition C.1. When ((-2(0,x, x. v).)))) = log(1 + Eiey (0.x.1))l),,, the loss Ca, v)
from equation 7 takes the following form:
( =(0xxx000)1 (1-a) (-=10xx111)))
L. Co, x, = log
1+
1+
iz
Proof. Using the properties of exponentials:
fo, x, v)
L(- [(1 ax) 2(0, X y) z(0, x)) v)).,) v))
log
1 Σ
(11aa) x(0,,x.. () x(0xx.)]]1]
if
log
1+ Σ
(1-o) (1-a) (0000)0)))xx (=-02(000)11))
it4
c -x,00xxxx.vlll)) (1-a) (-a) (==x(0xxx01)))
log
1+ Σ
izy
C.2 MTL-IBP
Proposition C.2. When ((-z(0,)) x. v).v) log(1 + Eite (00xx.i))) the loss MI, x, v)
from equation takes the following form:
(1-a)
Casm (0, x, = loog
1+
Σ
x Xasi 1//1
1+ Σ
x(0.x.))]3]
if
17

---

Published as a conference paper at ICLR 2024
Proof. Using the properties of logarithms and exponentials:
Co Lo, y) = (1 - a))(f((, xudv). + Lver (f (f(0,x),))
= (1 - aa log
1+ Σ
2 x00xxx))01
+ aa
1+ Σe
=00xx0))11
izy
i/4
(1-a)
log
1
Σ
e
2 Xat. 2)11
+ log
|+
Σ
2 2(0xx.1116)
i
(1-a)
log
Σ
e
1 Σ
2(0,x.,)]
b
iz
By comparing propositions C.1 and we can see that verifiability tends to play a rel- atively larger role on La,In x. y) if the network displays a large margin of empirical robustness to a given incorrect class (z(0, y]]
particular, given that z(0, Xadv. y) z x, y).
[i] >> O, with + y). the weight of the verifiability of that class on (o,cc(0, x, y) will be greatly reduced. On the other hand, if the network has large margin of empirical ro- bustness to all incorrect classes (z(0, Xadv. y) >> 0), verifiability will still have a relatively large weight on LT. (0,x, y). These observations comply with proposition 4.2 which shows that Ca,ce x, S La,Mn x, y). indicating that La,MI x, y) is generally more skewed towards verifiability.
C.3 EXP-IBP
When L( L(-2(0 2(0, x, y),u) = log(1 + Eieyy ((00xx))) the loss Ex, (0, x, y) from equation takes the following form:
Exp (0, x0,,)) = log(t-a)
Σ
log (1
Σ (=2(000011)))
i
C.4 COMPARISON OF CC-IBP WITH SABR
Proposition C.3. When L(-z(0, 1,0,x,10 k.y)).)
log(1 + E the loss
C(-zx(0, y), v) from equation (6) takes the following form:
[(-zx(0.x,1) 9). v) = log 1+
Σ
iny
where
X 4) (0,
is monotonically decreasing with A.
Proof. We can use 5x x', y) nı (0 x, y) z(0, x', y) < 0, which is monotonically decreasing
with À seen in the proof of proposition B.2 Then, exploiting the properties of the exponential,
can trivially re-write the SABR loss L( - Z (0xx x. y). v) as:
C( ( x. v). L(- [z(0, Xadv, 4) + ( x. v)l
log
+ Σ
(x(0.x...))) +0x
ity
=log
1 Σ
-2 x000xxx.))) (e (c66(0.xx1i))
18

---

Published as a conference paper at ICLR 2024
By comparing propositions C.I and O
that the SABR and CC-IBP losses share similar form, and they both upper-bound the adversarial loss. The main differences are the following: (i) the adversarial term is scaled down in CC-IBP, (ii) CC-IBP computes lower bounds over the entire input region, (iii) the over-approximation term of CC-IBP uses scaled lower bound of the logit differences, rather than its difference with the adversarial z.
D PSEUDO-CODE
Algorithm provides pseudo-code for CC-MTL, MTL-IBP and Exp-IBP.
Algorithm 1 CC/MTL-IBP training loss computation
1: Input: Network f(0,)), input x, label y. perturbation set C(x, c), loss function L,
hyper-parameters o, À
2: Compute Xadv using an attack C(x,e)
3: Compute z0,,x x. y) via IBP on C(x, e) as described in section 2.2.1
4: if CC-IBP then
5: z(0, Xadv, y) + (f(0. X.dv x 1 f(0, x.dx)
6: (0, x, y) L( [(1 ()) z0, Xadv, v) z(0, v))
7: else
8:
(f .x),)/ + ((-22(0, v).
9:
if MTL-IBP then
10:
La (6, x. y) + (1 a) ((f xadv), 3) + a (f v)
11:
else if EEx-IIBP then
12:
C. (0, y) &- L(J x0.x) (1-0)) ()) Lear (1 x)
13:
end if
14:
end if
15: return L. (0, x. y) 1|
E BRANCH-AND-BOUNE FRAMEWORK
We outline the details of the Baach-and-Bourt (BaB) framework employed to verify the networks trained within this work (see 6
Before resorting to more expensive verifiers, rum IBP Gowal et allall22200 2018) and CROWN (Zhang et al. 2018) from the automatic LiRPA library (Xu et al. 2020) as an attempt to quickly verify the property. If the attempt fails, run BaB with timeout of 1800 seconds per data point unless specified otherwise, possibly terminating well before the timeout (except on the MNIST experiments) when the property is deemed likely time out. Similarly a recent verified training work (De Palma et al. 2022), we base our verifier on the publicly available OVAL framework (Bunel et al. 2020a b
De Palma et al. 2021c) from VNN-COMP-2021 (Bak et al. 202T).
Lower bounds to logit differences A crucial component of BaB framework is the strategy employed to compute z(0, x, y). As explained in 22.2 the computation of the bound relies on network over-approximation which will generally depend "intermediate bounds": bounds to intermediate network pre-activations. For ReLU network, the over-approximation quality will depend on the tightness of the bounds for "ambiguous" ReLUs, which cannot be replaced by linear function (0 is contained in their pre-activation bounds). We first use IBP to inexpensively compute intermediate bounds for the whole network. Then, we refine the bounds associated to ambiguous ReLUs by using 5 iterations of o-CROWN (Xu et al., 2021) with step size of decayed by 0.98 at every iteration, without jointly optimizing over them so as to reduce the memory footprint. Intermediate bounds computed only once at the root node, that is, before any branching is performed. If the property not verified at the root, we use 3-CROWN (Wang et al., 2021 as bounding algorithm for the output bounds, with dynamic number of iterations (see (De Palma et al. 2021c section 5.1.2)). and initialized from the parent BaB sub-problem. We employ a step size of 1. decayed by 0.98 at each iteration.
19

---

Published as a conference paper at ICLR 2024
Ad Aversaria attacks Coumter-examples the properties are searched for by evaluating the network on the input points that concretize the lower bound z(0, x, y) according to the employed network vveraaproxximation This is repeated on each BaB sub-problem. and also used to mark sub- aub-problem infeasibility when z z(f,, x, y) overcomes the corresponding input point evaluation. In addition, some of these points are used as initialization (along with random points in the perturbation region) for 500-step MI-FGSM Dong et al. (2018) ad adversarial attack, which is run repeatedly for each property using a variety of randomly sampled hyper-paramettr (step size value and decay, momentum) settings, and early stopped if success is deemed unlikely. In (6.2] we report network to be empirically robust both the above procedure and a 40-step PGD attack (Madry al. (0188) (run before BaB) fail to find an adversarial example.
Branching Branching is performed through activation spitting: we create branch-and and-boudd sub- problems by splitting a ReLU into its two linear functions. other words, given intermediate bounds on pre-activations &3 E [L.. üg] for E [2. - I]I. if the split is performed at the i-th neuron of the k-th layer, la [i] 2 is enforced on a sub-problem, üg [i] < on the other. Let us denote the Hadamard product by @. We employ a slightly modified version of the UPB branching strategy (De Palma et al.) 2022, equation (7)), where the bias of the upper constraint from the Planet relaxation (ReLU convex hull, also known as triangle relaxation).
1 [(0x+, is replaced by the area of the entire relaxation,
[-1+++ @ [+ Intuitively, the area of the ape-appproinatiinn should better represent the weight of an ambiguous neuron the overall neural network relaxation than the distance the upper constraint from the origin. In practice, we found the impact on BaB performance to be negligible. In particular, we tested our variant against the original UPB, leaving the remaining BaB setup unchanged, on the CC-IBP trained network for MNIST with = 0.1 from table I they both resulted in 98.43% verified robust accuracy.
F EXPERIMENTAL DETAILS
We present additional details pertaining the experiments from and appendix G outline dataset and training details, hyper-parameters, computational setup and the employed network architecture.
In particular,
F.1 DATASETS
MNIST (LeCun et al. 2010) is a 10-class (each class being a handwritten digit) classification
dataset consisting of 28 x 28 greyscale images, with 60,000 training and 10,000 test points. CIFAR-
10 (Krizhevsky Hinton 2009) consists of 32 x 32 RGB images 10 different classes (associated to
subjects such airplanes, cars, etc.), with 50,000 training and 10,000 test points. TinylmageNet (Le) YYagg 2013) a miniature version of the ImageNet dataset, restricted to 200 classes of 64 64 RGB images, with 100,000 training and 10,000 validation images. The employed downscaled
ImageNet (Chrabaszez et al. 2017) is 1000-class dataset of 64 x 64 RGB images, with 1,281.167
training and 50,000 validation images. Similarly to previous work (Xu et al. 2020) Shi al. 2021 Müller et al. 2023). we normalize all datasets and use random horizontal flips and random cropping as data augmentation on CIFAR-IO, Tiny ImageNet and downscaled ImageNet. Complying with common experimental practice Gowal et al. (2018); Xu et al. (2020): (Shi et al. (2021): ) Müller et al.
(2023), we train on the entire training sets, and evaluate MNIST and CIFAR- 10 on their test sets, ImageNet and TinylmageNet on their validation sets.
F.2 NETWORK ARCHITECTURE, TRAINING SCHEDULE AND SYPER-PARAMETERS
We outline the practical details of our training procedure.
Network Architecture Independently of the dataset, all our experiments employ 7-layer architec- ture that enjoys widespread usage (with minor modifications) in the verified training literature (Gowal et al. 2018| Zhang et al. 2020 Shi et al. 2021 Müller al. (2023) Mao et al.] 2023). In particular, similarly to recent work (Müller et al.; 2023: Mao et al., 2023). we employ a version modified
by Shii et al. (2021) to BatchNorm (loffe & Szegedy 2015) after every layer. Differently
20

---

Published as a conference paper at ICLR 2024
from Shi et al. (2021): Müller et al. (2023). ) at training time compute IBP bounds to BatchNorm layers using the batch statistics from the perturbed data X,dv These are the same batch statistics employed to compute the training- -ime adversarial logit differences and their associated loss, which are not part of the loss functions used by previous work under the same architecture (Shi et al. 202T] Müller al. 2023). As done by Muäller et al. (2023), the training-time attacks are carried out with the network in evaluation mode. Finally, the statistics used at evaluation time are computed including both the original data and the attacks used during training. The details of the architecture, often named CNN7 in the literature, are presented in table
Train-Time Perturbation Radius
Table 2: Details of the CNN7 architecture.
We train using the target perturbation radius (denoted by as elsewhere in this work) for all benchmarks except on MNIST and CIFAR- 10 when c= 2/255. On MNIST, complying with Shi use Grain 0.2 for = 0.1 and Grain = 0.4 for e = 0.3.
CNN7
Convolutiona: 64 filters of size 3 x 3, stride 1. padding!
BatchNorm layer
RcLU layor
Convelutional layer: 641 filters of size x strie 1. podding 1
et al. (22II).
BatchNorm layer
Rel.U layer
Convolutional layer: 128 filters of size 3 x 3, stride 2, parkting
On CIFAR-10 with c 2/255, in order to improve performance, SABR (Müller)
BatchNorm layer
Rel JU layer
et al. 2023 "shrinks" the magnitude of the computed IBP bounds by multiply-
Convolutional layer: 128 filters of size 3 3. stride 1. paiking
BatchNorm layer
ReLU layer
ing intermediate bounds by a constant
Convolutional layer: 128 fillers of
3, stride or padding
c= 0.8 before each ReLU (for instance,
BatchNorm layer
ReL. layer
following our notation in 2.2 úg-1]+ 1]+
Linear layer: 512 hidden units
would be replaced by 0.8 0.8 - 1) As
BatchNorm layer
a result, the prominence of the attack in the employed loss function is increased. In other to achieve a similar effect, we employ the original perturbation radius to compute the lower bounds z0,, x, y) and use a larger perturbation radius to compute Xadv for our experiments in this setup (see table 3). Specifically,
ReLU layer
Linear layer: us many hidden units as the mumber of classes
"I MNIST CIPAR-IO, 2 Tingeeaaeee ImageNer64.
emain 4.2, the radius employed by IBP-R (De Palma et al., 2022) to perform the attack and to compute the algorithm's 's regularization terms.
Training Schedule, Initialization, Regularization Following Shi et al. (2021), 1, training proceeds as follows: the network is initialized according to the method presented by Shi et al. (202T), which relies on a low-variance Gaussian distribution to prevent the "explosion" of IBP bounds across layers at initialization. Training starts with the standard cross-entropy loss during warm-up. Then, the perturbation radius is gradually increased to the target value érrain (using the same schedule
Table 3: Hyper parametrr configurations for networks trained CC-IBP, MTL-IBP Exp-IBP from tables and
Dassset
Method
4
Autack (steps,
Guas. if of
Total epochs
Warm up Ramp-up
LR decay epochs
0.1
MTL-IBB
CC-IRP
10
10-1
x 10
10
(1. (1.00.e)
(1,10.0)
0.2
0.2
70
70
00-20
0-20
50,60
50,60
MNIST
0.3
MTL.-IBP
CC-IBP
3 10"1
10-
3 10
1 10
(1. (0.00e
(1, 10.0g)
0.4
30
70
0-:20
0-20
50,60
50,60
CC-IBP
1 1
3 10
(8.0.2e)
4/// allack only
160
1-80
120,140
MTL-IBP
103
3
(8,0.25e
4//2ss only
ExP-IBP
0.5 10
10-9
(8.0.25e
4./255 attack only
160
1-90
120,140
CIFAR-10
CC-IBP
10-1
(0.00.))
260
1-80
180,220
MTI.-IBP
6 10
10-
(0.00)))
360
1-80
180,220
EXP-IBP
10
(0.00.
CC-IBP
1x 10
5x 10
(1.10.
160
[+80
140.140
TinylmageNet
MTL.-IBP
(0.00.0
160
120,
EXP-IBP
4 10
10-3
10.0c)
160
1+80
120,140
CC-IBP
5 x 10
10
(1, 10.00.))
80
1+20
60.70
ImageNett4
-TL-IBB
5 10
-x
(1,100e)
30
1-20
60.70
EXP-IBP
10
(1,10.6)
21

---

Published as a conference paper at ICLR 2024
as Shi al. (2021) for fixed number of epochs during the ramp-up phase. During warm- up and ramp-up, the regularization introduced by/Shi et al. (2021) is added to the objective. This is composed of two terms: one that penalizes (similarly to the initialization) bounds explosion at training time, the other that balances the impact of active and inactive ReI.U neurons in each layer. Finally, towards the end of training, and after ramp-up has ended, the learning rate is decayed twice. In line with previous
work (Xiao et al.) 2019, De Palma et al. 2022 Müller et al. 2023: regularization throughout training.
Mao et al. (023)) we employ &
The hyper-paramettr configurations used in table are presented in table The training schedules for MNIST and CIFAR-10 with e 3/255 follow the hyper-parameters from Shi et al.] (202T). Similarly to Müller al. (2023), we increase the number of epochs after ramp-up for CIFAR- 10 with e = $/255: we use 260 epochs in total. On TinyImageNet we employ the same configuration as CIFAR-10 10 with c = 2/255, and ImageNet64 relies on the Tege schedule from Shi et al.] (202T), who did not benchmark on it. Following previous work (Shi et al.) 202I, Müller et al. (023), we use batch size of 256 for MNIST, and of 128 everywhere else. As Shi et al. (2021); p: Müller et al. (2023), we use a learning rate of 5 x 10-5 for all experiments, decayed twice by a factor of 0.2, and use gradient clipping with threshold equal to 10. Coefficients for the regularization introduced by Shi et al. (2021) set to the values suggested in the author's 's official codebase: À = 0.5 on MNIST and CIFAR-IO, 10, À = 0.2 for TinylmageNce On ImageNet64, which not included in their experiments, we
Hlper-paraaeteen
0.2 as for TinylmageNet given the dataset similarities. Single-step attacks were forced to lay on the boundary of the perturbation region (see appendix G.9). while we complied with previous work for the 8-step PGD attack (Balunovic & Vechev 2020 De Palma et al. 2022). As Shi et al. (202I). we clip target epsilon values to the fifth decimal digit. The main object our tuning were the coefficients from the CC-IBP, MTL-IBB and Exp-IBP losses (see (4) and the & regularization coefficient: for both, we first selected an order of magnitude, then the significand via manual search. We found Exp-IBP be significantly more sensitive to the parameter compared to CC-IBP and MTL.-IBP on some of the benchmarks. We do not perform early stopping. Unless otherwise stated, all the ablation studies re-use the hyper- parameter configurations from table In particular, the ablation from 16.2 use the single-step attack for CIFAR- 10 with e = 2/255. Furthermore, the ablation from appendix G.4 uses a x 10 for CC-IBP and a 1 x 10-2 for MTL-IBP in order to ease verification.
F.3 COMPUTATIONAL. SETUP
While each experiment (both for training and post-training verification) was run on a single GPU at time, we used a total of 6 different machines and 12 GPUs. In particular, relied the following CPU models: Intel i7-6850K, 19-7900X CPU, i9-10920s 19- 10940X, AMD 3970X. The employed GPU models for most of the experiments were: Nvidia Titan V, Titan XP, and Titan XP. The experiments of 6.3 and appendix G.S on CIFAR- 10 for 6/255 were run on the following GPU models: RTX 4070 Ti, RTX 2080 Ti, RTX 3090. GPUs of the following models: Nvidia Titan V. Nvidia Titan XP, and Nvidia Titan XP.
F.4 SOFTWARE ACKNOWLEDGMENTI
Our training code is mostly built on the publicly available training pipeline by Shi et al. (02T). which was released under a 3- 3-Clause BSD license. We further rely on the automatic LiRPA library (Xu al., (020)) also released under a 3-Clause BSD license, and on the OVAL complete verification framework (Bunel et al. 2020a De Palma et al. 2021c). released under a MIT license. MNIST and CIFAR- 10 are taken from t torchvisionn
by
dseas (Paszke et al. 2019); we downloaded TinyImageNet from the Stanford CS23 course website Inttp://cs23in stanford. edu/ zip), and downscaled ImageNet from the ImageNet website (https:
7/ 7/www. www.:mmaae-aan net www.:/eennn.ooo///oooo........ wwwpoo/w//wwwaddooooooooooo php).
G ADDITIONAL EXPERIMENTAL RESULTS
We now present experimental results complementing those in 6
22

---

Published as a conference paper at ICLR 2024
Table Comparison of CC-IBP and MTL-IBP with literature results for t. norm perturbations the MNIST dataset. The entries corresponding to best standard verified robust accuracy each perturbation radius are highlighted in bold. For the remaining entries, improvements on the literature performance of the best-performing Rel.U-based architectures are underlined.
Method CC-IBP
Souree
Standard Verified
work
99.30
MTL--APP
this work
99.25
98.38
TAPS
Map al.
2025
99.19
98.39
SABR
Milllr
99.23
98.22
0.1
SORINET
Zhang St al 202220
99.01
98. 14
1BP
ADVIBP
Fam Li
11211
98.97
97.72
CROWN-IBP
Zhang
COLT
Balumoves & Vishee (
99.2
97.1
CC-IBP
this work
98.81
93.58
MTL-IBP
88.80
STAPS
Mao et al.
2023
98.53
93.51
SABR'
Mao al
20241
98.48
93.85
SORTNET
98.46
93.40
IBP
Man et al.
20124
97.66
93.35
ADVTBP
98.42
91.77
CROWN-IBE IBP COLT
hang 21720
98. 18
92.98
Balumovic Vachev
2020)
1x wider network than the architseture employed our experiments.
G.1 COMPARISON WITH LITERATURE RESULTS ON MNIST
We present a comparison of CC-IBP and MTL--IBP with results from the literature on the MNIST (Le Cun et al.) 2010) dataset. Table shows that both methods attain state-of-the-art performance on both perturbation radii, further confirming the results from table I on the centrality of expressivity for verified training. Nevertheless, we point out that, owing to its inherent simplicity, performance differences on MNIST are smaller than those seen on the datasets employed in 6.1
G.2 TRAINING TIMES
Table 5 reports training times for CC-IBP and MTL--BB,, and present comparison with the train- ing times, whenever available in the source publications, associated to the literature results from tables T and Our timings from the table were measured on a Nvidia Titan GPU and using an 20-core Intel 19-7900X CPU. We point out that, literature measurements were carried out different hardware depending on the source, these only provide a rough indication of the overhead associated with each algorithm. Owing the our of single-step attack all benchmarks except one, MTL-IBP and CC-IBP tend to incur less training overhead than other state-of-the-arr approaches, making them more scalable and casier tune. In particular, STAPS displays significantly larger training overhead. As expected, under the same training schedule, the training times of CC-IBP and MTL-IBP are roughly equivalent. While the computational setup of our measurements from table ] was no longer available at the time of the Exp-IBP experiments, the same equivalence applies. For instance, on an Nvidia GeForce RTX 4070 Ti and 24-core Intel 19-10XX0X CPU, training with CC-IBP, MTL-IBP and EXp-IBP TinylmageNet respectively takes 4.60 10 4.57 10*, and 4.59 x 10a seconds.
G.3 ABLATION: POST-TRAINING VERIFICATION
Table reports the verified robust accuracy of the models trained with CC-IBP, MTL-IBP and EXP-IBP from tables] [nddde the verification schemes outlined in 6.. As expected, the verified robust accuracy decreases when using inexpensive incomplete verifiers. The differennce between BaB and CROWN/IBP accuracies varies with the setting, with larger perturbations displaying smaller gaps. Furthermore, CROWN bounds do not improve over those obtained via IBP on larger perturbations, mirroring previous observations note that all three methods already attain larger verified robustness than the literature results from table T under CROWN/IBP bounds TinylmageNet and downscaled ImageNet.
IBP-trained networks (Zhang al. 2020). We
23

---

Published as a conference paper at ICLR 2024
Table 5: Training times of CC-IBP and MTL-IBP compared literature results for Lo perturbations
MNIST, CIFAR-10, TinyImageNet and downscaled (64 x 64) ImageNet datasets.
Dataset
Methed
Source
Training time [s]
CC-IBP
this work this work
2.71 x 10
NTL-IBP
2.69 x 10"
0.1
TAPS
Mao et 2025
4.26 x 10*
SABR
Moller
1.22 x
SORTNET
1.39 10
ADVIBP
Fan &
2121
1.29 10
MNIST
CC-IBP
this work
2.71 10
MTLL-BP
this work
2.72 x 10
0.3
STAPS
Mao et
2025
1.24 x 10
SORTNET
Zann
1.59 x 10*
ADVIBP
Fan &
302T
1,29 10
CROWN-IBP
Zhang
2020
5.58 10
IBP
this work
1.77 x 10
MTL.-IBP IBP
this work
1.76 x 10
STAPS
Muo et
2025
1.41 X 10
250
SORTNET
2022
4.1 10
ADVIBP
Fan &
X22
5.28 10*
CROWN-IBP
Zhang el a
2021
9.13 x 10
COL.T
Balunovic & Vechey 2020
1.39 x 10a
CC-IBP
this work
1.72 x 10*
CIFAR-10
MTL-IBP
this
1,70 10
STAPS
Mao 2023
2.70 10*
SABR
Muller
3025
2.61 X 10*
SORTNET
Zhang al
20226
4.04 x 10*
IBP-R
De Palma
5.89 X 10a
2121
9.51 10
ADVIBP
Fan & Li
2021
5.28 10*
CROWN.IBP
Xu al. 2020
5.23 x 10a
COI.T
Balunovic & Vechey
2020
3.48 x 10
CC-IBP
this work
6.58 x 10*
this
6.56 10
TinyImageNet
STAPS
Mao
2023
3.06 10a
255
SORTNET
hang
20126
1.56 10a
IBP
Sh al
2021
3.53 x 10"
CROWN. IBP
Shi al.
2021
3.67 x 10*
CC-IBP
this
3.26 x 10
ImageNet64
MTL-IBP
this
3.52 10
SORTNET
Zhang al. 20226)
6.58 10
wider network the architecture employed experiments and in the original work (Müller
2023
G.4 ABLATION: ATTACK TYPES
Table the effect of the employed attack type (how to compute X,dv in equations 7 and (8) on the performance of CC-IBP and MTL-IBP, focusing on CIFAR-10. PGD denotes an 8-step PGD (Madry al., 2018) attack with constant step size 7) = 0.25e, FGSM single-step attack with
y 2 2.0e, whereas None indicates that no attack was employed (in other words, X x). While configuration for CC-IBP and MTL-IBP from table I is raised when Xalv = x in order to increase verifiability (see appendix F. As shown in table 7 the use of adversarial attacks, especially for = 2/255, are crucial to attain state-of-the. robust accuracy. Furthermore, the use of inexpensive attacks only adds a minimal overhead (roughly 15% on e = 2/255). an attack indeed employed, neither CC-IBP nor MTL-IBP appear to be particularly sensitive to the strength of the adversary for 8/255, where FGSM slightly outperforms PGD. On the other hand, PGD improves the overall performance on e = 2/255, leading both CC-IBP and MTL-IBP to better robustness acburre trade-offss than those reported by previous work this benchmark. In general, given the overhead and the relatively small performance difference, FGSM appears be preferable PGD most benchmarks.
FGSM and PGD use the same
verified
24

---

Published as a conference paper at ICLR 2024
Table 6: Verified robust accuracy under different post-training verification schemes for networks trained via CC-IBP and MTL-IBP from tables and 4
Verified robust accuracy [%]
Dataset
Method
CROWN/BP
IBP
CC-IBP
98.43
96.37
94.30
MTI.-IBP
98.38
97.17
96.67
MNIST
CC-IBP
93.46
92.22
92.22
0.3
MTI.-IBP
93.62
92.45
92.45
CC.IBP
63.78
52.37
0.00
205
MTI.-IBP
63.24
51.35
0.00
EXP-IBP
61.65
47.87
0.00
CIFAR-10
CC-IBP
35.27
34,02
34.02
MTL-IBP
35.44
34.64
34.64
265
CC-IBP
26.39
23.58
Tiay ImageNet
253
MTL-IBP
26.09
23.65
0.11
EXP-IBP
22.96
CC-IBP
11.87
10.64
0.92
ImageNet654
265
MTI.-IBP
12.13
10.87
1.41
EXP-IBP
13.30
11.42
0.19
G.5 TEST EVALUATION OF MODELS FROM 6..3
Table reports the results obtained by training the values for CC-IBP, MTL-IBP and SABR found in figure on the entirety of the CIFAR- training set, and evaluating on the test set. All the other hyper- parameters comply with those detailed in appendix F In order to reflect the use of Emain 4.2/255 for the attack computation in CC-IBP and MTL-IBP for e = 2/255 (see appendix F). on that setup we compute the SABR loss over the train-time perturbation radius of Guain 3.2/255. Branch-and bound is run with timeout of 600 seconds. These three expressive losses display similar trade-offs between verified robustness and standard accuracy, with CC-IBP slightly outperforming the other algorithms on
2/255 and MTL--BBP on 8/255. Observe that SABR yields a strictly better trade-off than the one reported by the original authors (79.24% and 62.84% standard and verified robust accuracy, respec- tively (Müller et al. 2. highlighting the importance of careful tuning. Given that, for 2/255, the "small box" may be well out the target perturbation set, the result suggest that the performance of SABR itself is linked to definition 3.1] than to the selection of a subset of the target perturba- tion set containing the worst-case input. We remark that this may be in contrast with the explanation from the authors (Mäller et al.) 2023). By comparing with literature results from table T (typically directly tuned on the test set, see appendix (F2). and given the heterogeneity across the three losses con- sidered in this experiment, we can conclude that satisfying expressivity leads to shate-of-the-an results on ReLU networks. Finally, the test results confirm that minimizing the approximation of the branch- and-bound loss does not necessarily correspond to superior robustness accuraac trade-offs (see (6.3)
Table 7: Effect of the type of adversarial attack the performance of CC-IBP and MTL-IBP under txc. perturbations on the CIFAR-I0 test set.
Ascuracy [8]
Method
Attack
Train, time [s]
Std.
Ver, rub.
CC-IBP
FGSM
80.22
62.94
1.08 10
CC-IBP
Nonc
82.12
38.80
9.40 x 1
CC-IBP
PGD
80.09
63.78
1.77 x 10
255
MTL-IBP
FGSM
79.70
62.67
1.08 x 10"
MTL-IBP
Non:
81.22
36.09
9.33 x 10
MTL-IBB
PGD
63.24
1.76 10a
CC.IBP
FGSM
35.27
1.72 10
CC-IBP
None
57.95
33.21
1.48 10
CC-IBP
PGD
53.12
35.17
2.82 10"
MTL-IBP
FGSM
53.35
35.44
1.70 10a
MTL-IBP
None
55.62
33.62
1.44 x 10
MTP-IBP
PGD
53.30
35.19
2.83 x 10"
25

---

Published as a conference paper at ICLR 2024
Table Performance of the CC-IBP, MTL-IBP and SABR models resulting from the validation study presented
figure under & norm perturbations on the CIFAR- 10 test set. The results corresponding the best trade-off
across tuning methods (measured as the sum of standard and verified robust accuracy) is highlighted in bold.
Accuracy [%]
Methed
Tuning criterion
Std.
Ver. rob.
Sid. Ver. rob.
CC-IBP
RaB Loss Std. I Loss
79.95
63,70
143.65
CC-IBP
3 x
BaB Err
81.93
61.12
143.05
MTL-IBP
7 x 10-3
BaB Loss + Std. Loss
79.26
63.33
142.59
MTL-IBP
10-3
79.86
62.43
SABR
x 10
BaB Loss Std. Loss
79.69
63.33
143,02
SABR
3 10
BaB Eer
81.48
60.01
141.49
CC-IBP
10
BaB Loss Std. Loss
53.62
35.11
88.73
CC-IBP
7 x 10
BaB Err
51.45
35.29
86.74
MTL-IBP
3 10
BaB Loss + Std. Loss
57.15
33.84
90.99
MTL-IBP
10
57.15
33.84
90.99
SABR SABR
X 10-1
BaB Loss Std. Loss
57.23
33:47
90.70
x 10
BaB Eir
31.95
35.01
86.96
G.6 TUNING SABR ON TINYIMAGENET AND IMAGENET64
The results of the validation study on CIFAR-10 (table G.5 showed that SABR, which satisfies our definition expressivity from 3 yields similar performance CC-IBP and MTL-IBP when employing the same tuning methodology. Prompted by these results, we carried out our own tuning of SABR on TinylmageNet and downscaled ImageNet, where the gap between our expressive losses (CC-IBP, MTL-IBB and Exp-IBP) and the results from the literature is the largest (see 1 In order reduce overhead and line with the results from table T and previous work (Gowal et al. 2018 Zhang et al. 2020 Shi et al.) 2021 Müller et al., 2023). we directly tuned on the evaluation sets. The resulting SABR hyper-paramette
are identical to those employed for CC-IBP each of the two datasets: table 3 Table 9 shows that SABR displays similar performance profiles to our expressive losses from 4 (except for Exp-IBP on ImageNet64: see the relative remark in 1 confirming the link between satisfying definition 3.1 and attaining state-of-the-ar verified training performance. We ascribe the differences with respect to previously reported SABR results Müller et al.) (2023): Mao et al. (2024) TinylmageNet insufficient tuning and inadequate regularization: for instance, Müller et al. (2033) set a 0.4 and X 10-6 (E1 coefficient); we employ a 10-2 and X 5 10
G.7 Loss SENSITIVITY TO a
Figure 4irreeee the standard, adversarial (under 40-step PGD attack with 1 0.035e) and verified losses (under IBP and CROWN/IBP bounds) of the networks from figure | with the CC-IBP, MTL-
Table Comparison the expressive losses from with our own SABR Muüller et al. 2023 experiments for fxo norm perturbations on TinyImageNe and downscaled (64 641) ImageNet. The entries corresponding to the best standard or verified robust accuracy for each perturbation radius are highlighted in bold.
Dataset
Method
Source
Standard acc. [%]
Verified rob, acc. [%]
CC-IBP
this work
38.61
26.39
MTL-IBP
this work
37.56
26.09
EXP-IBP
this work
38.71
26.18
TinylmageNet
SABR
this work
38.68
25.85
SABR
Müller et al. 2023
28.85
20.46
SABR
Mao et al.
2024
28.97
21.36
CC-IBP
this work
19.62
11.87
MTL-IBP
this work
20.15
12.13
ImageNet64
255
IBP
this work
22.73
13.30
SABR
this work
20.33
12.39
t2x wider network than the architecture used our experiments the original work Müller et
2023
26

---

Published as a conference paper at ICLR 2024
IBP and Exp-IBP losses (see 14 computed with the corresponding training hyper-parameterts In all cases, their behavior closely follows the adversarial loss, which they upper bound. By comparing with figure [] conclude that the losses perform their best in terms of trade-offs between BaB accuracy and standard accuracy when the losses used for training lower bound losses resulting from inexpensive incomplete verifiers. All verified losses converge similar values for increasing coefficients.
G.8 EXPERIMENTAL VARIABILITY
In order provide indication of experimental variability for the results from [ repeat small subset of our CC-IBP and MTL-IBP experiments from table those on CIFAR-IO with 8/255, further three times. Table 10 reports the mean, maximal and minimal values in addition the sample standard deviation for both the standard and verified robust accuracies. In all cases, the experimental variability relatively small.
Table 10: Experimental variability for the performance of CC-IBP and MTL-
IBP for foo norm perturbations of radius #/255 on the CIFAR-I test set.
Standard accuracy [%]
Verified robust accuracy
Method
Mean
Std.
Max
Min
Mean
Std.
Max
Min
CC-IBP
54.04
0.23
54,23
53.71
35.06
0.29
35.34
34.73
MBP
53.77
0.40
54.18
53.35
35.25
0.18
35.44
35.05
G.9 ABLATION: ADVERSARIAL ATTACK STEP SIZE
Table 11: Effect of the attack step size on the performance of CC-IBP and MTL-IBP under &oo norm perturbations on the 1IAAR-10 test set.
Accuracy [%]
Method
Attack
Std.
CC-IBP
e
80.22
62.94
CC-INP
1.25
80.94
62.50
268
MTL-IBP
10.0
79.70
62.67
MTL-IBP
80.43
62.29
CC-IBP CC-IBP
10.0
53.71
35.27
1.25
$4.75
34.77
255
MTL-IBP
1
53.35
35.44
MTL-IBP
54.30
Xadv Section G.4 investiaaess the influence of the type of attack used compute z(0, y) time on the performance of CC-IBP and -TP.-BBP. We now perform complementary ablation by keeping the attack fixed to randomly-initialized FGSM (Goodfellow et al., 2015 Wong al. 2020) and changing the attack step size nj. The results from [6 (except for the PGD entry in table 7 employ a step size 7 = 10.0 (any value larger than 2.0 yields the same effect) in order to force the attack on the boundary of the perturbation region. Specifically, report the performance for 17 1.25 c,
training
Stentrt
10a
10a
CRDWNEEEE
Test Lass
1.0
1.8
1.6
1.6
1.6
1.4
1.4
1.4
1.2
1.2
12-
10'7
1.0
1.0
(a) CC-IBP
MTL-IBP.
(c) EXP-IBP.
CC-IBP,
(e) MTL-IBP.
(0 Exp-IBP,
3/250.
2/235.
c 2/235.
5/200.
c 8/255.
8/250.
Figure 4: Loss values, computed the full CIFAR 10 test set, for the models from Figure 1 The CC-IBP, MTL-IBP and EXp-IBP losses (see (4) are computed using a value employed training, denoted on the axis. legend in (hppppis to all sub-figures.
27

---

Published as a conference paper at ICLR 2024
which shown by Wong et al. 2020) to prevent catastrophic overfitting. Table 11 does not display significant performance differences depending on the step size, highlighting the lack of catastrophic overfitting. We speculate that this is linked to the regularizing effect of the IBP bounds employed within CC-IBP and MTL.-IBP. On considered settings, the use of larger results larger standard accuracy, and decreased verified robust accuracy.
28


Reviews:
[{"review_id": "6W6sBaVb5J", "reviewer": "Reviewer_tVkU", "summary": "This work studies the certified training with over-approximation for robustness certification. Specifically, the authors introduce the idea of expressivity of loss functions and show that it can range from worst-case loss to verified loss, based on which two forms of loss are proposed. The experiments show the performance of the new losses and some findings regarding robustness and accuracy are given.", "questions": "See the Weakness part.", "limitations": "", "rating": 5, "confidence": 2, "soundness": 3, "presentation": 3, "contribution": 2, "strengths": "- The motivation of the paper is sound, and the underlying theory regarding certified training remains unknown and challenging.\n- The paper is generally well-organized and easy to follow.\n- The experiments are comprehensive and different datasets and attack radii are used for the evaluation.", "weaknesses": "- My biggest concern is that the contribution and novelty of the paper are incremental and minor, which is about the expressivity of losses. However, it seems that it somehow borrows the idea of the previous work SABR, which gives an effective loss ranging from adversarial loss and verified loss.  The difference between this work and SABR is not that clear and significant as SABR can induce expressivity by letting $\\lambda=\\alpha$ as shown in Sec. 3.\n- Some key details are not given in the main text. E.g., it is not clear from the main text how the logit differences are associated with an adversarial attack for CC-IBP when it is compared to CROWN-IBP in Sec. 4.1, without which the contribution and novelty are further weakened in terms of the comparison.\n- The insight and intuition of the relationship between CC-IBP and MTL-IBP are not clear. For example, does any case exist where one can be degraded to the other? If so, either theoretical or empirical results are needed to show it.\n- For Table 1, the proposed method is with BaB as a complete method, I wonder if it is fair to compare with some incomplete baselines.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "TF3IVLwKNO", "reviewer": "Reviewer_2HZC", "summary": "The paper proposes \"expressive\" loss functions that interpolate between IBP and adversarial loss in a simple linear combinations and show good empirical performance on a variety of datasets.", "questions": "Please see the weakness section.", "limitations": "", "rating": 6, "confidence": 2, "soundness": 3, "presentation": 1, "contribution": 2, "strengths": "The empirical results seem strong, especially considering the fact that the proposed methods are simple interpolations.", "weaknesses": "The presentation and writing needs a lot of work and it seems the paper is hurriedly written. Specific concerns are below.\n\n\n\tThe mathematical definition of property P in Eq 1 is given in section 2 without any discussion of what it means or entails and why is it interesting/useful. \n\n\tYou could add atleast one example of how x_adv could possibly be generated in the background section.\n\n\tExplicitly write down what “verification” means before using it in section 2.1. I don’t know what the following statement means: “However, formal verification methods fail to formally prove their robustness in a feasible time” \n\n\t “As seen from Eq 1, network is provably robust if …logit differences … all positive” – why and how before even defining what verification is.\n\n\t“Incomplete verifiers will only prove a subset of the properties” – which properties ? only one is defined. \n\n\tThe unlaballed equation with relationship of \\underline{z} and z. I would not write \\underline{z} as an inequation when saying it a lower bound without defining it first say using an example.  \n\n\tCan you give an example when o and l are not equal ? the definition of z requires o to be atleast as big as l, and the definition of z also makes sense only if o and l are equal. Is o the size of the output before softmax evaluation or after? I am having a hard time reconciling dimensions of f( ) and z( ) for translation-invariance.\n\n\tAre the other methods also grid-searched for best hyperparameters  for their respective methods ?\n\n\tThe runtimes are a bit misleading? Does the runtime also include hyperameter search cost including the cost for best interpolating parameter ?", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "ojHbO9Ut6K", "reviewer": "Reviewer_oQBq", "summary": "The authors hypothesize that expressive loss functions yield better training for verified robustness. A family of loss functions $\\mathcal{L}_\\alpha$ is expressive if\n- $\\mathcal{L}(f(\\theta, x_\\text{adv}), y) \\leq \\mathcal{L}_\\alpha(\\theta, x, y) \\leq \\mathcal{L}_v (f(\\theta,x),y)$ for all $\\alpha \\in [0,1]$, where the left/right inequality become an equality if $\\alpha = 0/1$ respectively. \n- $\\mathcal{L}_\\alpha$ is monotonically increasing with $\\alpha$\n\nThey support their hypothesis that expressive loss functions yield better training for verified robustness by showing that trivial expressive losses obtained via convex combinations between adversarial attacks and IBP bounds yield sota results. They further hypothesize that the notion of expressivity is crucial to get sota and argue as follows:\n- They state that sota verified training algorithms rely on coupling adversarial attacks with over-approximations. They show that SABR is expressive - hence the good performance of SABR is inline with their explanation.\n- Other expressive losses can be trivially designed via convex combinations, i.e.\n\t1. CC-IBP: combine adversarial and over-approximated network outputs with in the loss\n\t2. MTL-IBP: combine adversarial and verified losses\n- Experimental evaluation of CC-IBP and MTL-IBP. Both attain sota, particularly on TinyImageNet and downscaled ImageNet. \nFurther, they analyze the parameter $\\alpha$ governing a robustness-accuracy trade-off. Better approximations of the worst case loss do not necessarily correspond to performance improvements. \n\nThe authors experimentally compare CC-IBP and MTL-IBP to prior work and find that the proposed methods match or outperform the literature. They also study the effect of the over-approximation coefficient on the performance profiles of expressive losses. The take away here is that better approximations of the branch-and-bound loss do not necessarily result in better performance. \n\nObserved that standard accuracy decreases with alpha and verified accuracy increases with alpha. The adversarial and verified robust accuracies unter tighter verifiers may first increase and then decrease with $\\alpha$, hence the need for careful tuning according to the desired robustness-accuracy trade-off. \n\nFinally, the assumption that better approximations of the worst-case loss results in better trade-offs between verified robustness and accuracy is investigated. The parameter $\\alpha$ is chosen based on the performance on a hold out set consisting of 20% of the training set. The worst case loss is approximated using a branch-and-bound loss. The authors report that sometimes it is better for the BaB error to be positive and sometimes for the BaB error to be negative.", "questions": "- What are the confidence intervals for the results in the paper with respect to different seeds? Are the trends consistent w.r.t. the randomness due to different seeds? \n- What specialized initialization and regularization techniques where used?", "limitations": "", "rating": 8, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "- The presentation is mostly good.\n- Training certifiable networks is a relevant research problem. \n- The ideas are conceptually simple yet seem to be effective. \n- The work unifies and generalizes successfull approaches. \n- The authors provided code.", "weaknesses": "- It remains unclear how stable the results are (for example w.r.t. different seeds). \n- Writing could be improved in some parts of the paper, i.e. Section 6.3. \n- It remains unclear what \"tricks\" i.e. for regularization and initialization where specifically used.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "jaAguLQsSL", "reviewer": "Reviewer_eo5p", "summary": "This paper proposes a scheme for convexly combining verified and adversarial loss functions to train verifiably robust models.", "questions": "1. In table 3, the alpha parameter for the MTL-IBP method can get very low (e.g., $4 \\cdot 10^{-3}$ for CIFAR-10 $2/255$). Does this not mean that the loss essentially just reduces to the adversarial loss?\n\n2. Why do the optimal $alpha$'s vary so much between the $2/255$ and $8/255$ epsilons for CIFAR-10? As in Q1, the MTL-IBP loss boils down to just the adversarial loss for $2/255$, and changes to a $50/50$ split for $8/255$.", "limitations": "", "rating": 8, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 1, "strengths": "1. The paper is generally well written and presented.\n\n2. The contribution is generally clear.\n\n3. The idea of expressive loss functions as interpolating between verified and adversarial losses is interesting.", "weaknesses": "1. My main concern is that the paper is not sufficiently novel to merit publication. Convexly combining loss functions is a rather obvious idea; indeed (8) is just a linear combination of two loss functions, something which has been around for ages.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (poster)