Probably Approximately Global Robustness Certification

Thank you very much for your thorough and insightful review. We address your comments in the following.

Dependence on the dataset. We lift local robustness statements about a finite dataset to a (probabilistic) global robustness guarantee over the data distribution, i.e., to a robustness guarantee that generalizes with high probability. Hence, our approach directly addresses the dataset dependence of local robustness methods. For our theoretical statements, we indeed rely on the common assumption that we can get unlabelled iid samples from the data distribution. In our experiments, our sampling procedure may only approximate the data distribution. However, our evaluation shows that this approximation is sufficient to let our guarantee generalize to unseen data. This setup does not undermine our theoretical findings but rather demonstrates that our theory works in practice even in imperfect settings. This is also supported by Theorem 4.6.

Robust accuracy is an empirical measure of model accuracy and local robustness. Given a set of points, robust accuracy quantifies, for these points only, how often a perturbation leads to misclassification. Our method is fundamentally different. Our approach does not aim to measure robustness directly but rather formalizes the conditions for generalization of robustness from a sample to the distribution. For this, we can provide guarantees for any given local robustness oracle, including one based on robust accuracy.

Robustness vs Accuracy. We consider robustness and accuracy to not necessarily be related. This is consistent with the literature on robustness verification (e.g. [a] from gsc4). If ground truth labels are available to the local robustness oracle, then our theory can accommodate a notion of robustness that considers accuracy as well.

Robustness lower-bound (Eq. 30). We use the expression “robustness lower-bound” to refer to the smallest distance to a counter-example reported by a chosen oracle $\mathbf{rob}_f$ on our sample $N$. For each point in the sample, the oracle reports a local robustness radius and in Eq. 30 we take the minimum of these reported values. Our global robustness guarantees are provided with respect to the attack scenario (e.g., a PGD attack) specified by the chosen robustness oracle, and Eq. 30 provides a valid lower-bound for this chosen scenario. While PGD may over-approximate the distance to the class boundary, if a PGD oracle is used then our method provides valid guarantees for adversarial robustness against PGD attacks (Fig. 4). We report lower bounds for both an adversarial and a formal oracle on the same data in Fig. 4 and 5. Compared to PGD, a formal verifier can provide more conservative bounds (Fig. 5).

Adversarial Attacks & Lower bounds (Line 40-43) Our guarantees are provided with respect to a specific oracle and not necessarily with respect to the exact distance to the class boundary. Hence, our results for PGD are high probability robustness lower bounds for the distance required to reach an adversarial example using the PGD attack. We obtain these lower bounds by exact computation of Eq. 30 for our sample $N$ with our chosen robustness oracle.

Experiments. We have performed new experiments with larger architectures, including convBig [2], and with a new robustness oracle using the LiRPA library adopted by the CROWN verifiers. We provide details in the response to reviewer md7J. Both CIFAR and MNIST are commonly used benchmarks in the robustness literature [1, 2]. The additional formal verification benchmarks in Zhou et al. [1] are out of the scope of our work as they do not consider a notion of robustness comparable to ours. In our experiments, we investigate networks of comparable size to [1,2] and often achieve better accuracy.

Other tools. We run more experiments using recent libraries from the $\alpha$-$\beta$ CROWN tool (please see reply to md7J).

Theoretical results. Thank you for the pointers, we will revise the section accordingly to highlight our contributions. Proposition 4.2 does follow from Definition 3.5. Lemma 4.3 is a small technical result stemming from rank statistics which does not directly follow from existing results to the best of our knowledge. However, we will be happy to cite any other relevant literature in your knowledge.

We hope we have addressed your concerns and thank you again for your detailed review. We are very happy to engage in further discussion if you have more questions.

Thank you very much for your review and comments. We address them below.

Size of the certified NNs. Techniques like CROWN and randomized smoothing do indeed scale up to large networks for local robustness certification. However, our work is concerned with using local robustness checks to provide global robustness guarantees. The per-example verification time reported by Wang et al. is large for our application, as meaningful global guarantees require 10K-100K local robustness checks. Approaches that explicitly target global robustness (such as the ones referred to by reviewer gsc4, [a, b, c]) consider significantly smaller networks, with a number of parameters in the order of a few hundreds to a few thousands. Our approach scales significantly better than these approaches.

Randomized smoothing does not address global robustness but provides certifications for a smoothed version of the original classifier around a given point. For certification, randomized smoothing can only provide local robustness guarantees, whereas we are interested in global robustness guarantees conditioned on the prediction confidence, that provably generalize to unseen data.

Comparison to Webb et al. Our objective is fundamentally different to Webb et al. They provide a statistical estimate for the probability of failure with respect to a given robustness property (as a boolean criterion, see eq. (2) in Webb et al.), with no guarantee on soundness of the estimate. In contrast, we provide a high probability global guarantee on robustness (as a metric) conditioned on the prediction confidence (eq. 24). Furthermore, the sample complexity of our approach does not depend on the dimensionality of the problem, and can be computed a priori (eq. 7). In contrast, Webb et al. provide no formal sample complexity bounds. For any point they consider, they require a number of Metropolis-Hastings transitions that may increase with the dimensionality of the problem. Moreover, Webb et al. rely on a problem-dependent termination condition. We will add this discussion in the related work section.

Number of required samples. The sample size required for our guarantees does not depend on the prediction confidence of the classifier and is instead fully captured by Equation 6 and 7. That is, the sample size depends only on the choice of parameters $\epsilon$ and $\delta$, and scales as $\mathcal O(\frac{1}{\epsilon}(\ln\frac{1}{\epsilon}+\ln\frac{1}{\delta}))$. This is one of the strengths of our approach, as the sample size does not depend on the dimensionality of the problem (see the remarks on the VC dimension below).

VC Dimension. The VC dimension $d$ of the quality space is always equal to 2, for any given neural network, as it only depends on the property (i.e., robustness) we investigate. This is one of the main strengths of our approach, as the VC dimension of our problem does not depend on the choice of the learning algorithm, or on the specifics of the input data. The range space we consider is always constituted by the intersection of two axis-aligned half spaces in the 2-dimensional quality space, that is, it is constituted by the shaded regions in Figure 1.

Unbounded distribution support. Yes, our method does not rely on the assumption that the data distribution is bounded. All our statements are non-parametric in nature. We do not rely on any specific notion of locality in the input space, besides the ones required by the local robustness oracle.

100% vs 99% robustness. If we understand your question correctly, we want to clarify that the method does not depend on the fact that 100% of the observed samples are robust, and the sample complexity is not affected by this (see also above). Our method relies on the fact that if enough points ($\epsilon$-net many) are sampled and the minimum robustness value among them, for a given confidence $\kappa$, is found to be $\rho$, then we can say that with high probability a new point with confidence at least $\kappa$ will be at least $\rho$-robust. Our approach guarantees that such a statement indeed generalizes to test data.

We hope our comments addressed the questions you raised. We are happy to engage in further discussion.

Thank you for your thorough review and for the interesting and relevant references.

Quality of distribution approximation. In the paper, "sufficiently well for our purpose" is intended to reflect that such an approximation is able to provide guarantees that generalize to unseen data. To avoid any misunderstanding, we will further elaborate on this in the paper. Getting enough representative samples from the true data distribution can be challenging in the real-world. However, our experiments demonstrate that the simple sampling procedure we use allows us to obtain global guarantees that consistently generalize to unseen data, despite possible deviations introduced by the sampling procedure itself. The fact that our (Gaussian-noise-based) sampling procedure is sufficient substantiates the practical effectiveness of our approach. We also refer you to our answer to a similar question of reviewer 8m6m.

Impact of sampling on runtime. The influence of the sampling procedure itself on the runtime is negligible compared to the time spent performing the local robustness checks with the oracle. Overall, the runtime of the approach is linear in the sampling complexity in Equation 7 which, in turn, only depends on the chosen parameters $\epsilon$ and $\delta$, and not on the characteristics of the learning algorithm used or on the input dimensionality.

Runtimes in Tables. Thank you for pointing this out, we will make it more explicit in the tables. The runtime reported is the runtime to produce our guarantees from the set of already sampled points, and thus includes evaluating their class, confidence and robustness according to the local robustness oracle. The sampling procedure itself is fast (in total around 10s for the CIFAR10 samples containing ~700k data points), as the vast majority of the runtime is spent in checking robustness. The runtime of this local robustness check heavily depends on the specific oracle chosen. The large runtime in table 3 is determined, for instance, by the large computational requirements of the Marabou verifier. We have performed additional experiments on MNIST using the LiRPA library used by $\alpha$-$\beta$ CROWN as a local robustness oracle, which significantly improves the total runtime (see reply to md7J).

Different definitions of robustness. The definition in Kabaha and Cohen [b] essentially corresponds to the definition we use, as global robustness is defined as robustness for those points which are classified with large enough (margin-based) confidence. The notion discussed by Wang et. al. [c] is a sensitivity-based notion of global robustness. Their definition is not specifically tailored to a classification task, as it does not consider a notion of class explicitly. We think our notion is more convenient for a classification task, as our method allows us to provide statements about the robustness conditioned on a specific confidence value. Rather, the notion in Wang et. al. [c] captures a notion of function smoothness over all the input space. Not too dissimilarly, the definition in Calzavara et. al. [d] considers global robustness as stability in the output on a subset of the input features, together with a label-based notion of robustness. We think these definitions are equally viable for their respective tasks, with our specific choice simply being a natural definition for the (classification) problem at hand. Our definition only imposes constraints over the behavior of the model for changes that affect the output class, and it is thus a more interesting notion, compared to function smoothness, for classification tasks. This class-based setting also gives us access to prediction confidence as a natural indicator of robustness, as both softmax and margin-based confidence are proportional to the required changes in the output-space to change the class. We thank you again for the additional references that we will discuss and compare in more detail in a revised version of the manuscript.

Please let us know if we can provide any further details.

Thank you for your comments. As you suggested we added additional experiments to demonstrate the potential of our approach. In our reply, we also address the questions about our experimental evaluation from other reviewers.

We first point out that the goal of our experiments is to show that our robustness guarantees indeed generalize to unseen data. Our approach’s complexity scales linearly with the complexity of local robustness checks. We investigated the additional oracles and models proposed by the reviewers.

New experiments with larger architectures

We focus on MNIST and CIFAR-10, as these are commonly used in related verification literature (as in [1, 2] referred by 8m6m).

To address scaling, we have performed additional preliminary experiments with bigger architectures for adversarial as well as formal verification.

We run additional experiments with:

• a VGG network (vgg11_bn [e]), a convolutional architecture with ~10 million parameters, on CIFAR10 with a PGD oracle;
• ConvBig, a convolutional network used in the references provided by reviewer 8m6m, on MNIST with a LiRPA (from αβ-CROWN) oracle;
• the feed forward (FF) network on MNIST (as previously used in the manuscript), with a LiRPA (from αβ-CROWN) oracle.

We report architecture, training procedure, the robustness oracle, the size of the mapping $\lvert M \rvert$, the number of predictions for which $\kappa$ is smaller equal than $\kappa_{\max}$ denoted by $\lvert\mathbf x_{\kappa\leq\kappa_{\max}}\rvert$, the estimators $n_c$ and $\hat p_\kappa$ from Sec 6, the runtime of the verification, and the accuracy of the classifier. In all our additional experiments, our approach obtains global robustness guarantees that generalize to unseen data, as in all cases $\hat p_{\kappa}<\epsilon/p_{\min}$ and $n_c \leq \lvert D_{\text{test}}\rvert\lvert M\rvert \epsilon$. These results demonstrate that our approach works with a variety of datasets, models, and training procedures. We will include these results in the revised manuscript.

Scalability

The scalability of our method is closely tied to the scalability of the chosen local robustness oracle. If results for a single local robustness check can be computed in a time $t$, then we can expect a total runtime of $t\cdot s$, with $s$ the sample complexity obtained from Equation 7. PGD scales well in practice: the verification runtime for VGG (~12mins) does not significantly increase in comparison to our results on the different Resnet20 networks (5-20mins, depending on the average robustness of the specific network), even though vgg11_bn has about 40 times as many parameters. For some of our experiments with the bigger models, we cannot yet provide results for formal verification with LiRPA, as the GPU hardware requirements of the tool surpass the capabilities of our consumer GPU. With reference to the discussion with reviewer gttu, we also want to point out that while CROWN verifiers can verify properties on larger networks, the per-sample verification time as reported, for instance, in Wang et al., is still prohibitive to provide global robustness guarantees.

Our experiments show that we obtain good global guarantees that generalize to unseen data for relatively smaller models and input dimensions (28x28x1 grayscale images for MNIST on a smaller network) as well as for larger models and input dimensions (32x32x3 color images on a larger Resnet or VGG network).

References: [e] https://github.com/chenyaofo/pytorch-cifar-models