Expressive Losses for Verified Robustness via Convex Combinations

We thank the reviewer for their time and feedback. We are glad that the reviewer found the paper to be well written and presented, and idea of expressive losses to be interesting.

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.

We are happy that the reviewer pointed out that convexly combining loss functions is a rather obvious idea that has been around for ages: we absolutely agree! Indeed, one of the main contributions of our work is precisely to show that ideas that are as simple as they are old yield state-of-the-art performance when employed, for the first-time, to meet our novel definition of expressivity (Definition 3.1). We believe that these results provide strong support for the centrality of the notion of expressivity for verified training, the core message of our submission, as well as a novel understanding of the recent literature. In other words, our aim is to show that the performance of recent successes in the literature can be matched by simple techniques, and explained through a very simple definition. We believe this to be at least as valuable for the community as introducing a novel and complex algorithm that outperforms the baselines on selected benchmarks.

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?

We thank the reviewer for the question. As visible in Figures 4a and 4b in appendix F.4, the adversarial and CC/MTL-IBP losses are fairly different even when $\alpha=10^{-3}$. Specifically (we report the raw numbers here for convenience), for the CC-IBP-trained network, $L_{adv}=0.7658$ and $L_{CC-IBP}=1.234$. For the one trained via MTL-IBP: $L_{adv}=0.777$ and $L_{MTL-IBP}=1.192$. This is due to the extremely large values that the IBP loss takes on under these low over-approximation coefficients: $L_{IBP}=272.159$ and $L_{IBP}=65.392$ for the networks trained via CC-IBP and MTL-IBP, respectively. As a result, even when $\alpha = 4 \cdot 10^{-3}$, the MTL-IBP loss still features a significant IBP component.

Why do the optimal alpha's vary so much between the $2/255$ and $8/255$ epsilons for CIFAR-10?

We thank the reviewer for the interesting question. The difference between the type of loss that works the best on smaller perturbations and on larger perturbations on CIFAR-10 is a well-known phenomenon in the literature. Methods that have a strong adversarial training component (IBP-R, COLT) tend to perform particularly well on the $2/255$ setting, and quite poorly when $\epsilon=8/255$, where methods exclusively based on over-approximations typically outperform them (IBP, CROWN-IBP). Intuitively, larger perturbations will yield significantly larger bounds, requiring larger over-approximation coefficients $\alpha$ to effectively regularize them at the cost of a drop in standard accuracy.

We sincerely hope the reviewer can reevaluate our contribution in light of the above responses, and remain available for further discussions and/or clarifications.

Thank you to the authors for their thorough rebuttal. I'm not completely convinced, but I will raise my score to a five for now.

"Nevertheless, we would be happy to test any expressive loss for which the reviewer believes a worse performance should be expected."

If the authors can present an additional, qualitatively distinct example of an expressive loss family which achieves good performance I think that would strengthen the paper considerably and I would find that convincing. I can't immediately think of more ways to interpolate the adversarial and verified loss.

Since the deadline is tomorrow, just testing on one dataset would be acceptable (say, CIFAR10 8/255).

We thank reviewer oQBq for their comprehensive review, summary, and positive evaluation of the contributions we presented. We are particularly happy that the reviewer recognized that our submission "unifies and generalizes" previous work, and that the ideas we present are effective despite being "conceptually simple". We indeed believe these to be amongst the most important contributions in our work.

unclear how stable the results are (for example w.r.t. different seeds) [...] Are the trends consistent w.r.t. the randomness due to different seeds?

We provide an indication of experimental variability in Table 7 in appendix F.5, which reports results under four total runs on CIFAR-10 under perturbations of radius $\epsilon=8/255$. Both MTL-IBP and CC-IBP display relatively small experimental variability in the experiment.

It remains unclear what "tricks" i.e. for regularization and initialization where specifically used. [...] What specialized initialization and regularization techniques where used?

Similarly to relevant previous work (SABR, (S)TAPS), we employ the initialization and regularization techniques introduced by (Shi et al., 2021), in addition to $\ell_1$ regularization. More specifically, (Shi et al. 2021) propose to initialize weights with a low-variance Gaussian distribution to prevent the "explosion" of IBP bounds across layers at initialisation. Furthermore, during the warm-up and ramp-up phases of training (see appendix E.2, "Training Schedule"), (Shi et al. 2021) add two regularization terms to the objective: one that penalizes (similarly to the initialization) bounds explosion at training time, the other that balances the impact of active and inactive ReLU neurons in each layer. We will be happy to include this discussion and further explanations in the next revision of the paper, and thank the reviewer for their question.

We thank reviewer 2HZC for their detailed feedback on the manuscript, which will improve the clarity of the writing. We will make sure that the next revisions will clarify the raised concerns about the presentation, which we address individually below. We are glad that the reviewer found our empirical results to be strong particularly given the simplicity of the losses we employ. Indeed, we believe that our results point to the centrality of expressivity to state-of-the-art training, providing a new understanding of the recent literature.

The mathematical definition of property P in Eq 1 [...]

Equation (1) provides a standard definition of adversarial robustness: no point in a neighborhood of the inputs should be misclassified. This is expressed by saying that all the differences to the ground truth should be positive. The use of argmin instead of min was a typo, and we thank the reviewer for indirectly pointing us to this.

add atleast one example of how $x_{adv}$ could possibly be generated in the background section.

We will provide an example in the appendix in the next revision. As we describe in section 2.1, $x_{adv}$ is obtained by running an adversarial attack, the most common example being PGD by Madry et al. (2018). In short, for $\ell_\infty$ perturbations, PGD proceeds by taking steps in the direction of the sign of the gradient of the network with respect to the input point, clipping to the allowed input perturbation set after every iteration.

Explicitly 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”

The fact that a network is robust to a specific adversarial attack does not imply that it will be robust to stronger/unseen attacks. Verification methods provide guarantees that no attack will ever succeed and, in the worst-case, incur an exponential runtime (in the number of neurons), which is in practice infeasible for even medium-sized networks. Verified training algorithms allow to verify larger networks in reasonable time, leading to larger verified robust accuracies.

“As seen from Eq 1, network is provably robust if …logit differences … all positive” why and how before even defining what verification is.

The sentence in question does not depend on the notion of formal verification. If one can show that, for $\forall x_0 \in \mathcal{C}(x, \epsilon)$, all logit differences with incorrect classes are positive, then no adversarial example (misclassified point in $\mathcal{C}(x, \epsilon)$) can exist.

“Incomplete verifiers will only prove a subset of the properties” – which properties ? only one is defined.

Each robustness property $P(f(\theta, x), y)$ is a function of the point $x$ and its label $y$. As a result, a given dataset will have as many robustness properties as the number of input/label pairs. We will clarify this in the text in the next revision. Given that, as outlined in section 2.2.1, incomplete verifiers produce lower bounds on (4), a positive bound implies that the solution to (4) is positive too, providing a solution to the verification problem. A negative lower bound, instead, leaves the property at hand undecided.

Can you give an example when o and l are not equal ? [...] Is o the size of the output before softmax evaluation or after?

For multi-class classification, the label is a scalar ($l=1$), as explained before equation (1), and the output dimension of the network ($o$) is equal to the number of classes. As $z$ is the difference between a broadcast scalar (the entry of the network output corresponding to the ground truth) and the vector output of the network, $z$ and $f$ have the same dimensions.

Are the other methods also grid-searched

As common in related work (see for instance SABR, (S)TAPS) the baseline results in Table 1 are taken directly from the literature, and refer to the best results ever reported for any given method in previous work (for instance, across any network architecture). In other words, each baseline was tuned by the authors of the works referenced in the "Source" entry of Table 1.

The runtimes are a bit misleading? Does the runtime also include hyperameter search cost including the cost for best interpolating parameter ?

Runtimes for any algorithm (either ours or a baseline) only refer to a single training run. We would like to point out that the baselines with the best average performance across benchmarks (SABR, (S)TAPS) all feature at least as many hyper-parameters as CC-IBP and MTL-IBP.

We hope to have provided more clarity on the reviewer's concerns, and would be happy to provide further clarifications as needed.

We thank reviewer tVkU for their time, questions and comments. Before addressing them individually, we would like to highlight that, as explained in the general response, the main goal and contribution of our work is the idea that expressivity is all you need for state-of-the-art verified training. We show that extremely simple expressive losses (CC-IBP and MTL-IBP), obtained by casting, for the first time, standard techniques (convex combinations) under the lens of our novel definition, already yield state-of-the-art performance. We are glad that the reviewer found the paper to be well-organized and with a comprehensive evaluation, which we believe should be seen in support of the above point.

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 [...]

As highlighted by reviewer oQBq, our aim is to unify and generalize previous approaches, providing a novel understanding of the state-of-the-art. Therefore, the fact that SABR satisfies our definition of expressivity (as we show in section 3) is intentional, and exactly part of what we aim to show: expressivity is the key to recent advances in the certified training literature.

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.

By "logit differences associated with an adversarial attack", we mean the vector of differences between the ground truth logit ($y$ denotes the ground truth class) and the other logits: $z(\theta, x_{\text{adv}}, y) := f(\theta, x_{\text{adv}})[y] - f(\theta,x_{\text{adv}})$ (see definition in section 2, and the definition of the CC-IBP loss in equation (7)). As described in section 2.1, $x_{\text{adv}}$ is obtained by running an adversarial attack on the network. In our experiments, as described in the second paragraph of section 6, $x_{\text{adv}}$ is output by a single-step attack (random-initialized FGSM) in all settings except for CIFAR-10 when $\epsilon=2/255$. As detailed in section 4.1, also CROWN-IBP carries out convex combinations within the loss, but does so between CROWN-IBP and IBP bounds, and gradually transitions to pure IBP. We refer to section 4.1 for a detailed analysis of the differences between CROWN-IBP and CC-IBP.

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?

As shown in proposition 4.2 and described in the relative section, the CC-IBP loss is a lower bound to the MTL-IBP loss. The two losses trivially coincide for $\alpha=0$ and $\alpha=1$, as they both satisfy definition 3.1. The insight we want to convey by presenting two different losses (and also taking into account the SABR results, see Figure 3 and Table 6), is that expressivity, rather than the specific form of the loss function, leads to state-of-the-art performance.

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.

Note that (S)TAPS, SABR, IBP-R and COLT from Table 1 report results under complete verifiers, and report similar comparisons. Generally speaking, methods trained exclusively using incomplete verifiers (for instance, IBP, CROWN-IBP) display only very minimal improvements in verified accuracy when moving from incomplete verifiers to complete verifiers at evaluation time. Evidence for this can be found in Figure 2, which shows results for IBP training when $\alpha=1$. Importantly, they also produce much lower standard accuracies as shown in Table 1. In addition, Table 4 in appendix F.1 shows the verified accuracies of our models under incomplete verifiers. On larger datasets (TinyImagenet, Imagenet64), both MTL-IBP and CC-IBP already attain significant verified accuracies under CROWN-IBP bounds (hence without resorting to complete verifiers).