Probably Approximately Global Robustness Certification
Authors: Peter Blohm
Patrick Indri
Thomas Gärtner
SAGAR MALHOTRA
Venue: ICML 2025 poster (2025)
Keywords: Robustness
Learning Theory
PAC guarantees
Epsilon Nets
Primary area: deep_learning->robustness
TL;DR: A probabilistic global robustness certification methodology based on learning theory.

Abstract: We propose and investigate probabilistic guarantees for the adversarial robustness of classification algorithms.
While traditional formal verification approaches for robustness are intractable and sampling-based approaches do not provide formal guarantees, our approach is able to efficiently certify a probabilistic relaxation of robustness.
The key idea is to sample an $\epsilon$-net and invoke a local robustness oracle on the sample.
Remarkably, the size of the sample needed to achieve probably approximately global robustness guarantees is independent of the input dimensionality, the number of classes, and the learning algorithm itself.
Our approach can, therefore, be applied even to large neural networks that are beyond the scope of traditional formal verification.
Experiments empirically confirm that it characterizes robustness better than
state-of-the-art sampling-based approaches and scales better than formal methods.

Probably Approximately Global Robustness Certification
Peter Blohm Patrick Indri'
Thomas Gärtner'
Sagar Malhotra !
Abstract
checks and, therefore, to the precise notion of robustness investigated. In this paper, we will consider both formal and adversarial methods to check local robustness.
We propose and investigate probabilistic guaran- tees for the adversarial robustness of classifica- tion algorithms. While traditional formal verifica- tion approaches for robustness are intractable and sampling- based approaches do not provide formal guarantees, our approach is able to efficiently cer- tify a probabilistic relaxation of robustness. The key idea is to sample an e-net and invoke a lo- cal robustness oracle on the sample. Remarkably, the size of the sample needed achieve proba- bly approximately global robustness guarantees is independent of the input dimensionality, the num- ber of classes, and the learning algorithm itself. Our approach can, therefore, be applied even to large neural networks that are beyond the scope of traditional formal verification. Experiments empirically confirm that it characterizes robust- ness better than state-of- oftte-of-the-art campling-bused approaches and scales better than formal methods.
Neural Network (NN) robustness is a major desideratum as, for non-robust networks, predictions can be drastically changed with only small perturbations to the input (Szegedy et al., 2014). This behavior can be detrimental in safety- critical applications like autonomous driving (Rao & Frtu- nikj. 2018) or image recognition tasks (Athalye et al., 2018). Hence, methods for evaluating whether NNs are robust to such perturbations are critical to enable their safe and re- liable deployment. Significant research efforts have been invested to assess NN robustness, following two main lines of research:
Formal verification methods have been used to prov- ably certify local robustness of NNs (Katz et al., 2019; Wu et al., 2024; Xu et al., 2021). Recent results have extended these techniques to global robustness certifi- cation (Athavale et al., 2024) albeit only for NNs with up to few hundred parameters.
Adversarial methods rely on local optimization to as- sess whether NNs can withstand adversarial attacks (Goodfellow et al., 2015; Madry et al., 2018; Carlini & Wagner, 2017a). These methods easily scale to large networks, but generally do not provide formal guaran- tees on the global behavior of the network.
1. Introduction
We present a novel sampling-bast based procedure to certify the globul robustness of classifier with high probability. Exist- ing robustness verification methods are decision procedures that provide yes/no answers for a given robustmess criterion, for a specific point in the input space. In general, however, robustness a quantitative property that may depend on additional factors, such as the classifier's confidence in given prediction. As a key contribution, we propose and in- vestigate novel notion of global robustness that quantifies the robustness of any point, given its prediction confidence. Our guarantee is obtained by checking local robustness on a sufficiently large sample of points. The size of the sample quantified using a caaming-theoreti construct, namely e-nets (Haussler& & Welzl, 1986). Our approach is agnos- tic to the specific method used to perform local robustness
Our approach provides a quantitative characterization of robustness for the whole input space parameterized by the prediction confidence of each point. That is, for each point in the input space we are able to give high-probability lower bound for its robustness. This only requires indepen- dently and identically distributed (iid) samples from the data distribution and access to a local robustness oracle. Such an oracle can be efficiently modeled using existing (formal or ad adversarial) methods for assessing local robustness. The sample size required by our approach is independent of the input dimensionality, the number of classes, and the learning al ggorrtthm itself. Our approach can provide distinct robust- ness guarantees for each confidence value after a single sampling procedure. This characterization can be used to in- fer high probbabbbyyl lower bounds on the robustness of new data points, that were not part of the sampling procedure.
'TU Wien, Austria. Correspondence to: Peter Blohm <pe- ter:blohm @ tuwien.ac.at>.
Proceedings of the 42nd International Conference Machine Learning. Vancouver, Canada. PMLR 267, 2025. Copyright 2025 by the author(s).

---

Probably Approximately Global Robustness Certification
This paper is organized as follows. In Section 2. we present the relevant related work. In Section 3, we introduce the preliminaries. Our main contributions are described in Sec- tion 4 and Section 5. We present and discuss our experi- mental evaluation in Section 6. Finally, Section 7 contains concluding remarks.
3. Preliminaries
In this section, we will introduce basic notation and the nec- essary background for our theory. We will further introduce and motivate the notion of a robustness oracle and predic- tion confidence. These abstract concepts will allow results to be easily adapted to different methods of assessing robustness, as shown in our experiments in Section 6.
2. Related Work
After the seminal work by Szegedy et al. (2014) showed that NNs are sensitive to adversarial examples, number of techniques to find such examples were introduced. Many such approaches rely on gradient computation such as the Fast Gradient Signed Method (FGSM, Goodfellow et al., 2015) and an iterative adaptation of it called Projected Gra- dient Descent (PGD, Madry al., 2018). Additionally, the C&W attack (Carlini & Wagner, 2017a) explicitly takes the distance to the original data point into account, to find a particularly close adversarial example. More recently, empirical approaches to assess (Webb et al., 2019; Baluta et al., 2021; Kim et al., 2023) as well as improve (Li et al., 2023; Kim et al., 2023) the robustness of NNs have been introduced, often building from the concept of adversarial training introduced by Goodfellow al. (2015). While these approaches are applicable to large NNs and can be used to empirically assess robustness, they do not provide theoretical robustness guarantees for new points.
3.1. Basic Notation
Consider classification task with n classes on metric imput space X. We define a classifier as f X' + R", where for any instance x E X the classifier returns a vector /(x) E R". In this vector, the i-th component f(x); represents the classifier's output for class i, like the output layer in a NN. We say that the predicted class for x is class(x) arg max4e(1.n) (x); Furthermore, we say conf y (x) E R is the prediction confidence of ʃ for class(x). In the rest of this paper, we will assume that for a class class(x) = c the confidence is given by the softmax function, i.e.,
ex)(f(x)c)
conf, EjEli,) exp(J (x);)
(I)
without restricting the generality of our statements. We assume that the data for the classification task follows a distribution D over X. We write X ~ 'D to indicate that X is a random variable drawn from D, and x ~ D to denote an observed realization of X. If clear from context, proba- bilities Pro that are computed with respect to distribution D will be written as Pr.
In an effort to obtain provable guarantees, a line of research has developed formal methods for the verification of NNs (Katz al., 2019; Chen et al., 2021; Xu et al., 2020). While formally verified NN is provably robust to input pertur- bations (Casadio et al., 2022; Meng et al., 2022), formal verification is limited to small NNs. In fact, it is generally hard to provide guarantees about the behavior of large net- works (Katz et al., 2017) and it is, in particular, hard to detect all adversarial examples (Carlini & Wagner, 2017b). Other approaches have sought to provide approximate (Wu et al., 2020) statistical (Webb et al., 2019; Cohen et al., 2019; Lecuyer et al., 2019) robustness guarantees, as well as to train NNs which are certifiably robust (Li et al., 2023; Sinha et al., 2018; Wang et al., 2018).
3.2. Robustness
We say classifier is robust around a point x, if (xx)) remains constant within some neighborhood N(x) C X' of x. In many applications, N(x) is chosen to be an Log (Goodfellow et al., 2015; Madry et al., 2018) or another norm-bounded ball (Baluta et al., 2021; Carlini & Wagner, 2017a; Leino et al., 2021; Athavale et al., 2024).
How robust f is around is assessed by a robustness or- acle roby(x). The robustness oracle roby(x) returns the distance p to the closest counterexample x' E (x)) s.t. class(f (xx)) * class(f(x)). Examples of robustmess or- acles rob, include verification tools (Katz et al., 2017; Meng et al., 2022; Xu et al., 2021; Athavale et al., 2024), which offer exact results at high computational costs. For such exhaustive search methods, we can state rob, min Ex [||x x'Il class(f(x)) o class(f (f(')) In contrast, heuristic adversarial methods (Goodfellow et al., 2015; Madry et al., 2018: Carlini & Wagner, 2017a) can efficiently find very close points with different class mem- bership, which can be used as an upper bound for p. We will further discuss practically useful robustness oracles based on well-established methods in Section 6.
Recent work has specifically addressed global robustness for NNs. Athavale et al. (2024) and Indri et al. (2024) have recently extended existing formal verification methods to certify global robustness for confident predictions, where confidence is quantified using the softmax function. Sim- ilarly, Kabaha & Cohen (2024) focus on confident predic- tions using a margin-based notion of confidence. However, these methods are limited to NNs with only hundreds of parameters. In this paper, we introduce a probabilistic re- laxation of the notion of global robustness of Athavale al. (2024). We use e-nets (Haussler & Welzl, 1986) to provide high-probability guarantees for this notion of robustness.
2

---

Probably Approximately Global Robustness Certification
The following definition captures this oracle-based notion of robustness around given point.
largest finite set S C y such that for every subset 7 C S. there exists range R E R satisfying R S = T. If no such maximum exists, the VC dimension is infinite.
Definition 3.1 (Local p-robustness). A classifier f : x' + R" is locally p-robust around x according to the robustness oracle roby if
Definition 3.5 (c-net, Haussler & Welzl (1986)). Let ()), R) be a range space and 'D be a probability distribution on V A (finite) set N [ y is an <-net for y with respect to ' if, for every set R E R such that Pr(ft) 2 e, the set R contains at least one point from N, i.e.
rob;(x) 2 p.
(2)
Based on this definition, we need to define a notion of global robustness for a given classifier f. so we can guarantee the classifier will behave robustly regardless of the input. A natural definition of global p-robustness would require local p-robustness for every possible input. However, enforcing this for all inputs in dense spaces like 1 would constrain the classifier to make constant predictions. To address this, a more useful notion of global robustness focuses on spe- cific regions of interest, such as areas where the classifier's 's prediction confidence conf, y (x) is high (Leino al., 2021; Athavale et al., 2024). More confident predictions require larger changes in the output of f to alter the predicted class, so we consequently expect points classified with high confi- dence to be more robust. The following defimition formalizes global robustness, based on a confidence threshold k.
AR E R: Pr(R) 2 - +
(5)
c-nets provide a general notion of coverage. Our approach for certifying PAG-robustness relies on the following theo- rem for constructing e-nets from iid samples.
Theorem 3.6 (e-nets from iid samples (Mitzenmacher & Upfal, 2017)). Let ()), R) be range space with VC dimen- sion d and let Dy be a probability distribution on Y. For any < ô, E S 2. an iid sample from Dy of size s is an c-r y with probability at least 1 if
d d
s s=
- In
In 5
(6)
Definition 3.2 (Global p-n-rooustness). A classifier f X' + RR is globally p-x-robust if it is locally p-robust for all x E X' where the prediction confidence conf (x) is larger than K.
While the big-O notation of this result is convenient for theoretical asymptotic analyses, it neglects constant factors that may be significant in practice. In their proof, how- ever, Mitzenmacher & Upfal (2017) show that Theorem 3.6 always holds if s satisfies the inequality in the following restatement.
Vx E X: conf ((x) 2 K = rxb)(x) 2 p.
(3)
Proposition 3.7 (e-nets from iid samples with constants). Let (V. be range space with VC dimension d and let D be probability distribution over Y. For any 0 < c, 5 < 1 an iid sample from Dy of size is an e-net for y with probability at least 1 5 if
Definition 3.2 is equivalent to the following statement, which states the absence of counterexamples:
1x E X (x))(x)= < A.A conf 2 k.
(4)
Equation (4) highlights that a classifier is certified to be robust if no counterexample exists, that is, if no point with both high confidence and insufficient robustness is found by the oracle. However, certifying robustness in this manner is intractable in general (Katz et al., 2017). In this paper, we focus instead on bounding the probability of encountering counterexamples.
2 In(2)c
(ing
11 5 + dll((s) In (1-e (7)
Proof. See Appendix A.
We refer to the smallest integer s that satisfies the inequality in Proposition 3.7 as s(e, 6, d), and obtain it by computing
3.3. Epsilon Nets
min sEN
2 1 + d(n(2s)) - In (1 c -6///8 (2))
In g
Our robustness guarantees build on concepts from computa- tional geometry and learning theory, and our definitions are based on Mitzenmacher & Upfal (2017).
To obtain sample complexities, we find s(c, 8, d) from Equa- tion (8) using numerical methods.
Definition 3.3 (Range space). Let y be (possibly infinite) set and R. a family of subsets of y called ranges. A range space is a tuple ()7, R).
4. PAG Robustness
Definition 3.4 (VC Dimension, Vapnik & Chervonenkis (2015)). Let (), R) be a range space. The Vapnik- Chervonenkis (VC) dimension of (Y, R) is the size of the
In this section, we present our main theoretical results. We show how to get high high-probability certificates for the follow- ing relaxation of global p-o-robustness (Definition 3.2).
3

---

Probably Approximately Global Robustness Certification
Definition 4.1. Given data-distribution D, classifier
Q Quality space
Robustness
f X' Rd is approximately globally robust according to a robustness oracle roby if, for given confidence K, robustness p. and X ~ D, we have that
(),R)
ilppp R)
Pr (rob,(X) p conf (X) conf,
<.
(p. x)
where 0 < is a chosen parameter.
iR(p, x))
Our relaxation states that all x-confident predictions of ʃ will also be at least p-robust, with high probability. This probabilistic statement is inspired by the work Athavale et al. (2024), where the confidence threshold is introduced as a mechanism for f to abstain from prediction. A key difference to their work is that we are able to decide the probabilistic statement for all values of (p, k) simultane- ously. For this, we devise on sampling- basee methodology using c-nets to obtain the bound in Equation (9).
Confidence
Figure Visualization of the quality space 2 and of the region of counterexamples defined in Equation (12) for two possible pairs of robustness-confidence values (p, r)) and (p, R).
the intersection of two-axis aligned half-spaces in Q, as illustrated in Figure 1.
We rephrase the left-hand side of Equation (9) as
We define the family of these counterexample ranges over possible (p, x) as
Pr (Xoby(X) < p conf, / (X) 2 x) Pr conf (X) 2 k)
(10)
R = {R(p, R): (p,15) E R²).
(13)
Under data distribution D, we have
to then separately provide a lower bound for the numerator (using Proposition 4.2) and an upper bound for the denom- inator (using Lemma 4.3). Both of these bounds can then be realized with the same iid sample. In the rest of this section, we introduce set of novel definitions required for our results and then proceed with the bounds themselves.
Pr(R(p, x:) = Pr (g(X) E ((),
= Pr (rob,(X) < A confy(X) 2 k).
(14)
Given set N S X. we use ((N) to denote the set g(N) {q(x) E Q E N). With these concepts, we can obtain sample complexities independent from the dimensionality of X. We obtain an iid sample N in X, map it to Q, and interpret (NV) as e-net over the range space (2, R). This range space is equivalent to the intersection of two axis- aligned half-spaces in R2, with VC-dimension d 2.
4.1. Quality Space
An important aspect of our method is that our guarantees are independent of the properties of the input space and of the classifier /. This is because our guarantees only consider the two properties of confidence and robustness of given point in the input space. In this section, we formalize this idea. We define a function q that maps a given point X to its robustness-confidern tuple:
4.2. Bounding the Joint Probability
In this section, we define a method that can check under which conditions and for which (p, the inequality
q(x) + (rob, y
(11)
Pr (xob)(X) < p conf , 2 x) < (15)
As ((x) captures precisely the characteristics, or qualities, of each point x that are relevant for our guarantees, it is useful to introduce the concept
holds truc. For our guarantee, we consider an iid sample N from the data distribution D. our iid sample is an c-net, intersects all e-likely ranges. Therefore, if no counterexam- ple to p-os-rbusttness is found in e-net over (2, R), then R(p, x)) is known to be less than e-likely. The following proposition formalizes this idea.
quality space Q. The quality space 2-dimensional real space defined by the outputs of the map q- For given pair (p, k:), we say x is counterexample global p-k-robustness if q(x) E R(p,k), where
Proposition 4.2. Let D be a data distribution and : + RD be a clussifier. Given an e-net q(N) over the range space (Q, R), then for a given confidence n. and robustness radius p. we have that
= ((d)))) & 2n). (12)
The quality space allows us to easily define and detect whether f is robust or not. Each R(p, x) corresponds to
g(N) n R(p, R) = = (R(((())))) <E (16)

---

Probably Approximately Global Robustness Certification
where R(p, x) denotes the set of counterexamples p-K- robustness.
We use Lemma 4.3 with K = conf (X) and p 1 Puii
to obtain & values for which
Proof. As (N) is e-net, it holds that
Pr(conf
(icconf((3) ( > K) 2 Pmin-
(23)
VR E R: Pr(R) 2 (N)R
(17)
As Pr(conf (aannf((()) (X) 2 x) 2 Pr(conf , (X) > k), we arrive
at Equation (19). For compactness, we use
By contraposition, this statement is equivalent to
YR E R: Pr(R) <E = ((V) n R = Then, g(N) n R(p,k) = =0 = Pr(R(p,k)) <
(18)
2sp In )
((s, 6) max KEN
i:i i: sp
(24)
to refer to the largest i which respects the bound in Equa- tion (22). In our sample, we refer the confidence value corresponding to this as 6max- For confidence values K S Kmax, Lemma 4.3 allows to state with high probabil- ity that Pr(conf (X) > K) 2 Pmin- We cannot, however, make a statement about confidence values that were not ob- served frequently enough in the sample, i.e., for k > Rmmax- This upper bound on confidence values being certified is natural, as our statement relies only on the observed sample.
This result allows us to bound the numerator of Equa- tion (9). Note that Proposition 4.2 allows us to give guar- antees on the behavior of f. However, a bound on the joint probability (alone) may lead to vacuous guarantees. In fact, the probability in Equation (15) is trivially zero if consider confidence value k large enough such that Pr(conf , (X)= 2 x) = 0. For this reason, we require addi- tional information about Pr(conf (X) 2 k).
4.3. Bounding the prediction confidence
4.4. PAG Robustness
In this section, we provide a method to lower bound the probability of obtaining given prediction confidence as
We have now introduced all necessary tools and conditions to certify a classifier / to be approximately globally robust. So far, we assumed an e-net in the quality space Q as given. We now discuss how to obtain such an c-net using Theo- rem 3.6 to derive our main contribution: an iid sampling- based procedure that allows us to certify the approximate global robustness of a classifier f with high probability.
Pr(conf ( 2 x) 2 Pmin-
(19)
Equation (19) is implied by the following statement about the cumulative distribution function of confidence:
Pr(conf y (X) < x) Pmin
(20)
Theorem 4.4 (PAG robustness). Let D be a data distri- bution, f X - R" be classifier and roby be a local robustness oracle. With q(x) defined as in Equation (11), with parameters O < c, P.mii 5 < 1
The following auxiliary lemma provides general method to obtain bound for a given quantile of random variable from an iid sample.
2- Consider a sample N D with |N| Z s(c, 2/2,22 2) as per Equation (8) and an integer i([N), Then, with a probability of at least implication holds for all p and for all S Noy:
Lemma 4.3. Let K be real-valued random variable, and N be an iid sample of K with |N| =s. s. Denote with N(a) E
Pmin 8/2) as per Equation (24).
8 the following
R. the ęth -largest element in the sample. Then for parameters
1 > p Z 2 and 0- < 5 < 2.
with probability of at least 5,
we have that
(Q(N) n H(p, ((()))((p))) =0) =
Pr(K S ((6) Sp
(21)
(25)
for any integer i such that
Pr (r(rob((X) < <pl conf , 2 2k) Puuin
< 6
1 r
i << sp
2sp Iu
(22) That is, under the absence of counterexamples in N, the classifier f can be certified to be Probably Approximately Globally (PAG) robust.
Proof sketch. The number of elements in an iid sample that are smaller or equal to the p-quantile Kp of K is a random variable I ~ Binom(s. p). We are interested in finding the largest integer i such that N(a) < Kp holds with probability at least 1 - 8 and, therefore, the largest integer i such that Pr([ 2 i) 2 1 8. We use a Chernoff bound for the deviation of I from its expected value E[1] = sp to obtain an integer that is wwwhhhhghhhhhae probabiltty lower bound for T. LI
We present a proof of Theorem 4.4 that builds on the fol- lowing lemma, which reformulates Proposition 4.2 as con- ditional probability.
Lemma 4.5. Let x 'D be a random data point in X, f ~ X' + R be a classifier, and parameters 0 < e, Pmin S be parameter. Given an e-nel g(N) over the range space
5

---

Probably Approximately Global Robustness Certification
(2,R), for all ps K. such that Pr(conf ( (X) 2 x)
Pmin
Proof sketch. The data processing inequality (Raginsky, 2014) can be used to show (Lemma A.2) that A is an upper bound for the total variation distance of the distribution of instances sampled from D and D' when they are mapped into the quality space Q. The numerator in the right-hand side can be derived by showing (Lemma A.3) that an e-net under DD' an (e + A)-net under D. The denominator can be derived by observing (Proposition A.5) that the quantiles of 'D and 'D' can differ by at most A. The theorem follows (Appendix A) from these results.
it holds that
(c(N) =0)
(26)
Pr (rob,(X) (X) < pll conf (X) 2 k)
Pmin
Proof. Let us define, for brevity, the two random events
E, = (X)b)(X) < p) and E. = (conf 2 s). By
Proposition 4.2 we know
q(N) R(p,k) k) 0 =
<e
(27)
In the following section, we describe how use the theorer- ical results obtained far and practically derive robustness lower-bounds for given classifier.
Furthermore, by the definition of conditional probability
Pr(E, E.) Pr(E, A Ec)
(28)
Pr(Eo)
5. Robustness Lower-Bounde
When Pr(Ee) Pr(conf/ y (X) 2 K) 2 Pmin. it holds that
In the previous section, we described how to provide global robustness guarantees given an iid sample N is found be robust. Specifically, for given choice of parameters and ö, we bound the required size of N. This single sample N can be used to evaluate the robustness with all tuples (p. k). A lower-bound on the robustness of a point x with prediction confidence k = conf, , (x) can be obtained using the small- est observed robustness for a confidence of at least x in the sample N. We define mapping function M (x) + p that maps given confidence lower bound p:
Pr(E, Ee) E Pr(E, A Ec)
E Pmin
(29)
Pmin
which completes the proof.
Proof of Theorem 4.4. We assume that [ 2 s(c, 8/2, 2). Theorem 3.6 then implies that ((N) is an e-net over (2, R) with a probability of at least 1 5/2. We further assert i S.S. <<([NV, 1 pmin: 0/2). Lemma 4.3 then implies that Pr(conf (X) 2 N(a) 2 Puiin with probability of at least - 5/22 as well. We use the union bound to state that both conditions hold true with a probability of at least 1 1- 8. Given that both N(a is a valid quantile bound, ie.. Pr(conf / (X)= 2 NG)) 2 Pmin- and k S N(O). then Pr(conf y (X) 2 K) 2 Puin- The theorem then follows from Lemma 4.5.
corresponding robustness
min rob;(x) XEN
if K S Fimax
M(k)= = s.t.
conf)(x) 2 K
(31)
UNDEFINED
else
Equation (31) assures that no counterexample of p-k- robustness is in N for p = M1s,, and that the returned P satisfies all conditions of Theorem 4.4. The mapping func- tion (k) does not return a robustness lower-bound for confidence values larger than fumax. In this case, for the con- sidered sample size the uncertainty for quantile estimation is too large to guarantee Pr(conf y (X) 2 Kmmx) > 0, as de- scribed in Lemma 4.3, Note that, for > Kmax, we can nev- ertheless guarantee that Pr ( (roby(X) < p conf y (X) 2 k) e. The map M can be constructed from a sample N in [(N log((N])) time, detailed in Algorithm I.
In some settings, it might not be possible directly sample from the data distribution, but rather from distribution D' that is used to approximate the true distribution DD. Even in these settings we can transfer our guarantee, as long as we can quantify the difference between the two distributions.
Theorem 4.6 (PAG under distribution shift). Let D be a data distribution, f X > R.a be classifier and roby be some robustness oracle. Let D be a distribution such that TV D') = A. Consider an tid sample N ~ DD' and parameters 5 and Puin- Consider an that satisfies the conditions in Theorem 4.4 for D'. Then, with probability at least 1 -
For a given mapping M, we now discuss how likely it is that our guarantees hold across all confidence values. This is not directly addressed by our analysis so far and requires to bound
((N))R(p,K)) =0)
Prd (X) < pl conf (X) 2 x)) Pinin
6 A
Pr (xob)(X) < (cooff(()))
(32)
(30)
That is, in the absence of counterexamples f can be certified to be PAG robust with respect to the data distribution D.
We can obtain a bound on this probability as a direct conse- quenee of Proposition 4.2. In this sense, the p- mapping
6

---

Probably Approximately Global Robustness Certification
Quality space Q
How does the runtime of verification proce- dure scale based network size, parameter choices, and oracle?
RQ3:
Robustness
How well can we capture qualitative differences in the behavior of different NNs?
RQ4:
M (m")
(nn)
We answer these questions by applying procedure to the certification of NNs for MNIST (Deng, 2012) and CI- FARIO (Krizhevsky, 2009).
x²1
Fynax
Confidence
Setup We train four different network architectures (Ioffe & Szegedy, 2015; He et al., 2016; Mirman et al.. 2018) on the two classification problems MNIST and CIFAR1O, as illustrated in Table 1. For each architecture, we train, in a cross-validation setup, five instances of the network with standard training and five instances with TRADES (Zhang et al., 2019). We then use the respective validation split of the data to produce our guarantee: we imitate iid samples from the true data distribution by sampling with Gaussian noise from the validation data, As this approximation might not represent the true data distribution perfectly, the theoret- ical strictness of our guarantees might decrease, according to Theorem 4.6. Similar to this, in practical settings, true iid sampling is not always possible, and we investigate whether our guarantees appear to degrade noticeably.
Figure 2. Visualization of the robustness lower-bound map M (x). Each rectangular region under the curve has probability mass smaller than c. The yellow line represents the maximum confidence value above which M (R)) is undefined.
M is not only useful to obtain robustness lower-bounds for individual points, but can furthermore be used to bound the probability that for point x sampled from D, it holds that roby (x) < M (conf (x)).
Proposition 5.1. Consider a classifier f X R" and p-n-mapping M constructed from an c-net (N) as in Equation (31), Let [M] be the size of the codomain of M. Then
Pr (X) < ( < MM...
(33)
Table I. Overview used NN architectures and oracles.
Dataset
Architecture
Params
Oracle
Proof. We use the properties of e-nets together with union bound based on the size of the codomain of the mapping M. As M consists, by construction, of JM discrete steps, | ranges fully cover the area in the quality space below M. In the worst case, we have to assume their probability mass is additive and proceed with a union bound, proving our statement.
FeedForward
39 k
PGD, LiRPA
MNIST
ConvBig
663 k
LiRPA
ResNer20
272 k
PGD
CIFAR10
VGG11 BN
9441 k
PGD
We repeat the randomized verification procedure multiple times for each instance of the NNs with different robustness oracles. A detailed description of the training and verifica- tion procedure provided in Appendix C.
In practical settings, M is typically small; we empirically demonstrate this in Section 6. We illustrate the practical effectiveness of our method in experiments with NNs in the following section.
Robustness Oracles We provide three robustness oracles, and conduct experiments with one based on adversarial techniques and one based on formal methods, as an answer to RQ1. Our adversarial oracle uses PGD (Madry et al., 2018), with a high number of small gradient steps, to report the closest counterexample found. For the experiments with PGD, we set e 10 4, Pmin 0.01, 5 0.01 and thus sample s(c, 5/2, 2) 989534 images. We use PGD to quantify robustness, by performing many small gradient steps from each data point, and we measure the Tox distance to the first adversarial example.
6. Experiments
In this section, we investigate the practical aspects of our the- ory. We aim to show that results translate into practical settings and aim to answer the following research questions:
RQ1: How can different methods for checking local robustness be modeled as oracles?
RQ2: How well do our guarantees hold on unseen data in realistic, imperfect conditions?
The two formal robustness oracles we provide are based on the NN verification tools Marabou (Katz et al., 2019) and
7

---

Probably Approximately Global Robustness Certification
auto_LiRPA' based on LiRPA Xu et al. (2020) respec- tively. We will only conduct multiple experiments using auto.LiRPA, due to the high computational demand of Marabou in our setting. For both of these tools, we certify local robustness in Lae hypercubes of fixed distances, and use binary search to find a lower bound of the radius where the model is robust. our experiments with buttoLiRee we choose E 2.5 10-3, Pmin = 0.05 and 6 = 0.01. We consequently sample s(c, 5/2, 2) = 31635 images.
the 6 runs with violations for the FeedForward network on MNIST originate in one single validation data split, de- tailed in Appendix D. This could be, for instance, due to a distribution shift between this specific validation split under Gaussian noise and the true data distribution. A similar phenomenon can be observed for ResNet20 on CIFARIO.
With these possible explanations in mind, we observe a re- maining total of 5/180 0.028 trials, where our guarantees seem not to generalize the unseen test data expected. This empirical fraction is close to our choice of d = 0.01, and considering our simple approach of estimating the data distribution, our method can be considered relatively re- silient to imperfect sampling settings.
Evaluation After the sampling procedure is completed, we construct the map M as in Equation (31) from the sam- pling split of our data. The map M provides the robustness lower bound obtained with the sampling procedure. We are then interested in empirically checking whether the robust- ness lower bound we obtained holds on the unseen testing split, that is, whether the testing data respects our guarantees. To this end, we define the following estimators. For given confidence value K, we estimate the conditional probability (x(rob((x)) < Mx) | conf (x') 2 K) for x' E Dust. that is, the probability that the testing data does not respect the robustness lower-bound provided by M.
To discuss RQ3, we inspect the runtimes in Table 2. We find that our approach is able to effectively scale large models like the 10 million parameter VGGI1_BA with strict param- eter values for c, 5 and Pmin. that provide strong guarantees. The runtime of our procedure consists mainly of the indi- vidual local robustness checks, so by relaxing c, 5 and pmin the runtime can be casily adjusted to desired durations.
We plot the map M and the testing split of CIFARIO with VGG11 1 BN in Figure 3. To investigate our method on the more challenging examples, we choose to plot the results for one of the 3 experiments for which we observe p.. > 0.01 for some k. Even in this case, the lower bound provided by M generally holds on test data and describes well the specific behavior of the networks, despite very few (7) ex- ceptions. The bounds also allow for a clear differentiation between the formal robustness of adversarially and normally trained networks, observable in Figure 4 in Appendix D too, which answers RQ4 positively.
1xx': (x < M(x) A , 2 k]| [x' conf f 2 x}|
Pe-
(34)
where x' E Dueu- To estimate the worst-case violation of our guarantees, we consider the أ = max Ps and check if 5 S e/Pmin- We furthermore report
ne= = (x' Dres: (xb)(x') < M (conf y (x))). (35)
This helps evaluate Proposition 5.1 empirically. As dis- cussed in Proposition 5.1, [M| denotes the number of steps in M, i.e., the size of its codomain. If Proposition 5.1 holds for our sample, we then expect nhe S |Deea]] | For both MNIST and CIFAR-IO, Dieal= = 10 and thus Deelle = We then expect ne/IM] < for PGD and na/|M| < 10 for LiRP.
7. Conclusion
In this work, we use e-nets to devise a sampling-based ap- proach to provide probabilistic guarantees on the global robustness of a given classifier. Our approach is agnostic to the specific robustness oracle and can thus be adapted to variety of existing approaches. Our guarantees are con- ditioned on the confidence of a prediction to allow for a flexible characterization of robustness. In our experimental evaluation, we used PGD and auto_Li RPA to evaluate local robustness and showed how our method: (i) charac- terizes the behavior of networks trained with both standard and adversarial methods, and (ii) obtains useful global ro- bustness guarantees that transfer effectively to unseen data.
Table 2 reports summary of our experimental evaluation. We perform a total of 230 experiments on 40 NNs, checking our guarantees against the estimators de- scribed above. In the majority of trials (21 1/230) our estima- tors suggest that our guarantees hold across all confidence values. To answer RQ2, we discuss possible explanations for the 19 observed violations, besides the natural variance of our estimators defined in Equations (34) and (35).
Results
In the few cases where our estimators indicate that our guarantees are violated on unseen data, the models under analysis still follow the overall trend described by our guar- antees (see Figure 3), with only slight violations. Consid- ering our results in more detail, we can observe that of
In future work, we will use other informative properties in addition to confidence, such as the predicted class, to further refine our guarantees. Beyond this, more refined robustness oracles and sampling procedures can be used to further improve the scalability and practical resilience of the obtained guarantees. As our approach is agnostic to the
"gigthu.. www.e//oo//eeeeieeeeeeee hnwperffficennntlllgeeeeeaaan LiRPA
8

---

Probably Approximately Global Robustness Certification
CIFAR1 0 v9g11 Lower Bound vs Test Data with Standard Training
CIFAR10 0 vgg11 Lower Bound vs Test Data with TRADES Training
2.2
0.03
2.0
2.2
2,02
c.5
Nax DENOO
Bound
Carfaence
Figure 3. Scatter plot of the CIFAR-10 10 test dataset Diest with Dreal 10000, in the quality space with VGGILBN. The left network is trained with standard methods, the right network is trained robustly with TRADES. The red line depicts the lower bound obtained from validation sample N, with the parameters data points violate the lower bound. Note that, despite this apparent violation, M tightly fits the test data and illustrates the contrasting robustness behaviors of the networks.
10-4, 5 pmin 0.01, with | s(e, 5/2, 2) 989534. On the right-hand side, 5
Table Summary results all experiments. We report worst results aggregated over three to five random seeds over the different data splits used for the TRADES adversarial training. The subscripts indicate standard training (ST) adversarial training (AT) with TRADES, the used oracle is PGD (P) or auto Li RPA (L). For each experiment, we report the values p and ney MM], where bold numbers denote that the estimators consistent with our guarantees for all the S Kmax for all the runs considered. Moreover, we report the number of individual "good runs" are consistent with our guarantees even when considering worst-case ÿ. Finally, report the average runtime per verification run in minutes. More extensive results available in Appendix D.
Experiment
NN
f 103
c/Pmin 103
Tle
M
good runs
runtime
FeedForward
0.00
50.00
0
13
15
25/25
8.3
MNIST
ConvBig
0.00
50.00
0
5-5
15/15
245
FeedForward
1.30
50.00
7
6-9
25/25
8.3
MNIST AT.L
ConvBig
3.39
50.00
44
3-4
13/15
246
MNIST
FeedForward
0.18
10.00
2
38-46
25/25
0.2
MNIST
FeedForward
16.50
10.00
14-22
19/25
0.3
ResNet20
1.35
10.00
3-3
17/25
4.5
CIFARSTP
VGG11_BN
0.00
10.00
0
4-5
25/25
38.8
ResNet20
1.51
10.00
4
24-42
25/25
133.4
CIFARALP
VGGI1_BN
17.00
10.00
9
26-60
22/25
308
properties of the tested object, will investigate other use cases where this approach to probabilistic verification could improve on the state of the art.
der the Slaie-Sktodowssa-Cuurr grant, project Training Al-
liance for Computational systems chemistry (101072930).
Impact Statement
Acknowledgements
This paper presents work whose goal is to advance the field of Machine Learning. There are many potential societal consequences of work, none of which we feel must be specifically highlighted here.
This work was funded in part by the Vienna Science and Technology Fund (WWTF), project StruDI. (ICT22-059); by the Austrian Science Fund (FWF), project NanOX-ML (6728); by the TU Wien DK SecInt and by the European Unions Horizon Europe Doctoral Network programme un-

---

Probably Approximately Global Robustness Certification
References
Haussler, D. and Welzl, E. Epsilon-nets and simplex range queries. In Proceedings of the Second Annual Sympo- sium on Computational Geometry, SCG '86, pp. 61-71, New York, NY, USA, 1986. Association for Computing Machinery. ISBN 0897911944
Athalye, A., Engstrom, L., Ilyas, A., and Kwok, K. Syn- thesizing robust adversarial examples. In International conference on machine learning, pp. 284-293. PMLR, 2018.
He, K., Zhang, X., Ren, S., and Sun, J. Deep residual leamn ing for image recognition. In Proceedings of the IEEE conference on computer vision and pattern recognition, pp. 770-778, 2016.
Athavale, A., Bartocci, E.,, Christakis, M., Maffei, M., Nick- ovic, D., and Weissenbacher, G. Verifying global two- safety properties in neural networks with confidence. In International Conference on Computer Aided Verification, pp. 329-351. Springer, 2024.
2016.
Indri, P., Blohm, P., Athavale, A., Bartocci, E., Weis- senbacher, G., Maffei, M.. Nickovic, D., Gärtner, T., and Malhotra, S. Distillation based robustness verification with pac guarantees. In ICML 2024 Next Generation of Al Safety Workshop, 2024.
Baluta, T., Chua. Z. L., Meel, K. S., and Saxena, P. Scalable quantitative verification for deep neural networks. In 2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE), pp- 312-323, 2021.
Ioffe, S. and Szegedy,
C. Batch normalization: Accelerating deep network training by reducing internal covariate shift. In International conference on machine learning, pp. 448- 456. pmlr, 2015.
Carlini, N. and Wagner, D. Towards evaluating the robust- ness of neural networks. In 2017 IEEE Symposium on Security and Privacy (SP), pp. 39-57, 2017a.
Carlini, N. and Wagner, D. Adversarial examples are not easily detected: Bypassing ten detection methods. In Proceedings of the 10th ACM Workshop on Artificial Intelligence and Security, AlSec 17, pp. 3-14, New York,
Kabaha, A. and Cohen, D. D. Verification of neural net- works' global robustness. Proceedings of the ACM on Pro- gramming Languages, 8(00PSLAI):1010- 1039, 2024.
NY, USA, 2017b. Association for Computing Machinery. ISBN 978440035
Katz, G., Barrett, C., Dill, D. L., Julian, K., and Kochender- fer, M. J. Reluplex: An efficient smt solver for verifying deep neural networks. International Conference on Computer Aided Verification, pp. 97-117. Springer, 2017.
Casadio, M., Komendantskaya, E., Daggitt, M. L.,, Kokke, W., Katz, G., Amir, G., and Refaeli, I. Neural network robustness as a verification property: A principled case study. In Shoham, S. and Vizel, Y. (eds.). Computer Aided Verification, pp. 219-231, Cham, 2022. Springer International Publishing. ISBN 978-3-031-11188-1
Katz, G., Huang, D. A., lbeling, D., Julian, K., Lazarus, C., Lim, R., Shah, P., Thakoor, S., Wu, H., Zeljić, A., Dill, D. L., Kochenderfer, M. J., and Barrett, C. The marabou framework for verification and analysis of deep neural networks. In Dillig, I. and Tasiran, S. (eds.), Computer Aided Verification, pp. 443-452, Cham, 2019. Springer International Publishing. ISBN 978-3-030-25540-4.
Chen, Y.. Wang. S., Qin, Y., Liao, X., Jana, S., and Wag- ner, D. Learning security classifiers with verified global robustness properties. In Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security, CCS '21, pp. 477-494, New York, NY, USA, 2021. Association for Computing Machinery. ISBN 978145005 478144034444
Kim, H., Park, J., Choi, Y., and Lee, J. Fantastic robustness measures: The secrets of robust generalization. In Thirty- seventh Conference on Neural Information Processing Systems, 2023.
Cohen, J., Rosenfeld, E., and Kolter, Z. Certified adversarial robustness via randomized smoothing. In international conference on machine learning, pp. 1310-1320. PMLR, 2019.
Krizhevsky, A. Learning multiple layers of features from tiny images. Technical report, 2009.
Lecuyer, M., Atlidakis, V., Geambasu, R., Hsu, D., and Jana, S. Certified robustness to adversarial examples with differential privacy. In 2019 JEEE Symposium on Security and Privacy (SP), pp. 656-672, 2019
Deng, L. The mnist database of handwritten digit images for machine learning research. IEEE Signal Processing Magazine, 2966):141-14,, 2012.
Leino, K., Wang, Z., and Fredrikson, M. Globally robuss neural networks. In Meila, M. and Zhang, T. (eds.), Pro- ceedings of the 38th International Conference on Ma- chine Learning, volume 139 of Proceedings of Machine Learning Research, pp. 6212 12222 PMLR, 18-24 24 Jul 2021.
Goodfellow, I. J., Shlens, J., and Szegedy, C. Explaining and harnessing adversarial examples. In Bengio, Y. and LeCun, Y. (eds.), 3rd International Conference on Learn- ing Representations, ICLR 2015, San Diego, CA. USA, May 7-9, 2015, Conference Track Proceedings, 2015.
10

---

Probably Approximately Global Robustness Certification
Li, L., Xie, T., and Li, B. SoK: Certified Robustness for Deep Neural Networks. In 2023 IEEE Symposium on Security and Privacy (SP), pp. 1289-1310, 2023.
Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I,, and Fergus, R. Intriguing proper- ties of neural networks. In International Conference on Learning Representations (ICLR), 2014.
Madry, A., Makelov, A., Schmidt, L., Tsipras, D., and Vladu, A. Towards deep learning models resistant to adversarial attacks. In International Conference on Learn- ing Representations, 2018.
Vapnik, V. N. and Chervonenkis, A. Y. On the Uniform Convergence of Relative Frequencies of Events Their Probabilities, pp. 11-30. Springer International Publish- ing. Cham, 2015. ISBN 978-3-319-21852-6
Meng, M. H., Bai, G., Teo, S. G., Hou, Z., Xiao, Y., Lin, Y., and Dong, J. S. Adversarial robustness of deep neural net- works: A survey from a formal verification perspective. IEEE Transactions on Dependable and Secure Comput-
Wang, S., Chen, Y., Abdou, A., and Jana, S. Mixtrain: Scalable training of verifiably robust neural networks. arXiv preprint wrw.v:1811.0062222. 2018.
ing, pp. 2022.
Webb, S., Rainforth, T., Teh, Y. W., and Kumar, M. P. sta- tistical approach assessing neural network robustness. In 7th International Conference on Learning Representa- tions, ICLR 2019, New Orleans. LA, USA, May 6-9, 2019. OpenReview.net, 2019.
Mirman, M., Gehr, T., and Vechev, M. Differentiable ab- stract interpretation for provably robust neural networks. In International Conference Machine Learning, pp. PMLR, 2018.
Wu, H., Isac, O., Zeljić, A., Tagomori. T., Daggitt, M.. Kokke, W., Refacli, I., Amir, G., Julian, K., Bassan, S., et al. Marabou 2.0: versatile formal analyzer of neu- ral networks. In International Conference on Computer Aided Verification, pp. 249-264, Springer, 2024.
Mitzenmacher, M. and Upfal, E. Probability and Com- puting: Randomization and Probabilistic Techniques in Algorithms and Data Analysis. Cambridge University Press, USA, 2nd edition, 2017. ISBN 1107 15418X88X
Raginsky, M. Strong data processing inequalities and & -sobolev inequalities for discrete channels. IEEE Trans- actions on Information Theory, 62:3355-3388 2014.
Wu, M., Wicker, M., Ruan, W. Huang, X., and Kwiatkowska, M. A game- approximate verification of deep neural networks with provable guarantees. The- oretical Computer Science, 807:298-329 2020. ISSN 0304-3975. In memory of Maurice Nivat, a founding father of Theoretical Computer Science Part II.
Rao, Q. and Frtunikj, J. Deep learning for self-driving cars: chances and challenges. In Proceedings of the Ist International Workshop Software Engineering for Al in Autonomous Systems, SEFAIS 18. pp. 35-38, New York, NY, USA, 2018. Association for Computing Machinery. ISBN 978 4503353395.
Xu, K., Shi, Z., Zhang, H., Wang, Y., Chang, K.-W., Huang, M., Kailkhura, B., Lin, X.. and Hsieh, C.-J. Automatic perturbation analysis for scalable certified robustness and beyond. Advances in Neural Information Processing Systems, 33:1 13:1129-1141, 111,, 2020.
Sauer, N. On the density of families of sets. Journal of Combinatorial Theory, Series A, 13(1):145-147, July
1972. ISSN 0097-3165.
Xu, K. Zhang, H., Wang, S., Wang, Y., Jana, S., Lin, X., and Hsieh, C.-J. Fast and Complete: Enabling complete neural network verification with rapid and massively par- allel incomplete verifiers. International Conference on Learning Representations, 2021.
Shelah, S. A combinatorial problem; stability and order for models and theories in infinitary languages. Pacific Jour- nal of Mathematics, (111):247-261, April 1972. ISSN 0030-8730.
Zhang, H., Yu, Y., Jiao, J., Xing, E. P., Ghaoui, L. E., and Jordan, M. I. Theoretically principled trade-off between robustness and accuracy. In Chaudhuri, K. and Salakhutdi- nov, R. (eds.), Proceedings of the 36th International Con- ference on Machine Learning, ICML 2019, volume 97, pp. 7472-7482. PMLR, 2019.
Simonyan, K. and Zisserman, A. Very deep convolutional networks for large-scale image recognition. In Bengio, Y. and LeCun, Y. (eds.), 3rd International Conference Learning Representations, ICLR 2015, San Diego, CA, USA, May 7-9, 2015, Conference Track Proceedings, 2015.
Sinha, A., Namkoong, H., and Duchi, J. Certifiable distribu- tional robustness with principled adversarial training. In International Conference on Learning Representations, 2018

---

Probably Approximately Global Robustness Certification
A. Proofs
Proposition 3.7 (e-nets from iid samples with constants). Let R) be a range space with VC dimension and let 'D a probability distribution over y. For any 0 e, z. an iid sample from Dy of size is an e-netfor y with probability at least 1 8 if
2 1 (n(
+ dll((2)) - In (1--- In 3
Proof. We follow double sampling" argument from Mitzenmacher & Upfal (2017, Theorem 14.8). First, define Fj as the random event that a sample N of size N = 8 is not an e-net:
E = {3R E R:
0))
(36)
We aim show FF(Fa) 6 for large enough Consider then second sample 7 with [T] and define E& the random event that some range R& E R does not intersect N, but has large intersection with T:
E R) ER R ( (RN = (IRNT) 2 68 2 )
F2
(37)
As ({(RNT] = cs, then Pr (I 2 2 should be large. Hence, E1 and E2 should have similar probability in total. Mitzenmacher & Upfal (2017) formalize this intuition with the following expression which considers a fixed range R' such that R' NN = 0 and Pr(X E F²) 2 e. In particular, as Eg c E₁ and consequently Eg = Eg n E1, it follows that
Pr(E2) Pr(E E2) = Pr(E2 E,) 2 Pr [T Pr(Ei)
ES 2
(38)
Pr(E.)
For some fixed range R', the random variable S = RR' n T| follows binomial distribution Bin(s, with expectation B|S] = sp. We can proceed with a Chernoff bound as
Pr PI(II' R AT (B'NTI
2 S Pr (R'TT
sp 2
ss 8
SC
I exp
exp
(39)
where we used the fact that 2 c. While Mitzenmacher & Upfal (2017) relax this expression with exp( -$)) < 2. interest of tighter bounds, we continue instead our derivation without this relaxation. Thus,
1
In the
Pr(E2) Pr(Ez) ED) 2 Pr (T R' Pr(Ei)
ES 2 2
exp
Pr(Ei) S 1 exp
Pr(E2)
(40)
8
Next, we aim to bound the probability of Eg using larger event Elg. Consider again some fixed range R with
ER = ((RON = (RRT) ((RTT) k)}
(41)
with k = es We want to show that Pr(ER) is small. To do so, consider set of 2s elements and assume to partition it randomly into N and T. Fn captures the event that at least elements N U T intersect R but none of these is in N. Of the (2t) possible partitions of N U,, in exactly (2x-²) of them, no element of is in N. Consequently,
2
Pr(ER) < Pr(NOB R = 0 ( (N))N 2 k)
(42)
k
s(s-1) 1) ... (s k ++11 1) (2s)!(s - k)! (2s)(2s - 1) ... (2s - k +
(2s - k))ss
(43)
< 2 2
(44)
The last inequality introduces further albeit small relaxation in the result, as h < s. We then finally consider the event E via the union bound over all the ranges R E R, that is
E = (3R E R (RON = (ROT) 2 $c }}
(45)
2
12

---

Probably Approximately Global Robustness Certification
We then the Sauer-Shelah Lemma (Sauer, 1972; Shelah, 1972) to argue that can consider most (2x)4 ranges when projecting R onto N U.T. By the union bound we then have that Pr( (F2) (2s)d2 sc/2, Finally, arrive at
Pr(F2)
(2x) 225)22-00/2
86/2
Pr(Ei) S
S 6.
(46)
exp
=ac
8
1
exp
-.6
8
We can now simplify the last expression to obtain
(2s) sc/2 < (1 11-exp -exp exp
-F
(47)
-86
-S6
dln(26) +
In) < ln(6) + In
1-exp exp
1
(48)
2
1 (2s) - In (1(1 1- exp
-=8t
2 (n(
In
(49)
8
which concludes the derivation.
Lemma 4.3. Let K be real-valued random variable, and N be an iid sample of K with |N| = s. Denote with N() E R
the 8th -largest element in the sample. Then for parameters 1 > p 2 2 and 0 < 8 < 2. with probability of at least 1 - 6, we have that
Pr(K S (2)) Sp
(21)
for any integer i such that
( 8)
< sp
2sp In
(22)
Proof. Let Kp E be the p-quantile of K, i.e.
Pr(K S Kp) =p
(50)
The number of elements in an iid sample smaller than Kp a binomially distributed random variable ~ Binom(s, p). aim to find an integer that results in high-probabilityy lower bound for that is, we look for the largest such that
Pr Pr(I> 1=116)2116
(51)
or, equivalently,
(r = Σ pd p)
(52)
There no straightforward closed form expression find this integer We proceed using Chernoff bounds for the deviation of / from E[/]= = sp. Recall that Chernoff bounds for some relative deviation [0, 1] is defined as (Mitzenmacher & Upfal, 2017, Chapter 4)
- 2
Pr(T < (1 1)) & exp
(53)
In our discrete setting, the relative deviation 7) of from [ is defined as 17 == sp-i written as
The Chernoff bound can then be
((sp i)2 )
Pr(T < S exp
< 8.
(54)
2sp
13

---

Probably Approximately Global Robustness Certification
We now perform routine calculations to obtain upper bound for i.
(sp i)2
In (6)
(55)
2sp
(sp - 2)2
1
> In
(56)
2sp
sp i #1
2spln In
(57)
8
i < sp
2sp In
(58)
Given Equation (58) holds for a particular i, at least elements in a sample of size are smaller than Kp with probability at least. 1 - 5, i.e. (r(N()) S K,) 2 Finally, the event N(s) S Kp implies Pr(K s N(o)) S p. which then holds true with probability of least 1 well.
Definition A.1 (Total variation distance). Consider two distributions D, D' over X' and let S X be measurable set. The total variation (TV) distance between and DD' defined as
TV(D, D) sup Pr(R) - D' RCX
-P((R).
(59)
Lemma A.2 (Total variation distance in the quality space Q). Consider TV D') their total variation distance. For the function q X + IR? that maps instances into the quality space Q We denote the distribution of the instances after they are mapped onto Q as Dg. D'r It then holds that
distributions 'D and D' over X and denote with
('( S TV(D,D).
(60)
Proof. For case of presentation, we discuss a proof of the statement for more general conditions, which correspond to a version of the data processing inequality (Raginsky, 2014). Let F be a o-algebra on the input space X and consider two probability measures P and Q on F). Let + y measurable map and G be a o-algebra on the space Y With slight abuse of notation we denote with ((P) == P(t (B)), YB E G the pushforward measure induced by (V, We do so analogously for Q too. The total variation distance for probability measures defined as
TV((())((()) supl
sup BE$
P(t (B) Q(-=
(61)
Beg
Note that for every measurable set B E G in the measure space (2,9), the preimage t- t (B) E F is mcasurable set in (X, F). It therefore holds that
sup BEG
< sup P(A) - =
(62)
AEF
from which it follows that
IV((()),t(()) S TV..
(63)
The statement of lemma holds when is the function g that maps to the quality space Q, and y is Q
Lemma A.3. Given two distributions D and 'D' on X such that TV(D, D') s A, if N is e-net for X with respect to D then it is an (c+ AJ-net for X with respect to D.
Proof. Using Definition A.1, TV(D, (() = supaex Pro (R)(R)- - PPr < A. Specifically, Pro (R) 2 c + A implies
that Pro (R) 2 e. As N is an e-net for X' with respect to D', it intersects all R C X such that Pr (Rt) 2 e, and it thus
intersects all R C X' such that (r)(R) 2 e A. Therefore, N is an (e + A)tnet for X' with respect to D.
Lemma A.4. Let K be a random variable sampled from D'. Let D be another distribution such that TV D') < A, and Prp (K S K) & p then we have that
Pro(K $ k) S Sp+A
(64)
14

---

Probably Approximately Global Robustness Certification
Proof. The proof follows from the fact that if TV S A, then probability of event under D and D' can differ by more than A.
Proposition A.5. Consider random variable K ~ D' and let N, NGo p. and 5 be as in the setting for Lemma 4.3 that Pr & N(a) I holds with probability at least 1 5 for any integer such that i < np v 2mp In (1/6). Consider a distribution D such that (D, D') S Then, under the distribution and for the same N, N(g p, and with probability of at least 1-d: ò:
Pro S N()) Sp+A.
(65)
Proof. Using Definition A.I, for any measurable set R S R" it holds that (P)o(R) Prw (R) S A. If we consider the event {K S Noa S IR", with probability of at least 1 8 it holds that:
( Pro(K S (() Pr & N()) + +ASPAA
(66)
where in (+) we used Lemma 4.3.
Theorem 4.6 (PAG under distribution shift). Let D be data distribution, f X R be a classifier and rob, be some robustness oracle. Let D' be distribution such that (D, D') A. Consider itd sample N D's and parameters e, 6 and Pwin- Consider that satisfies the conditions in Theorem 4.4 for D'. Then, with probability at least -
(n(N) n ((N)RR(p,)) =
(30)
Pro (X) < p conf, (X) (X) 2k)
E+
Pmin
That is, in the absence of counterexamples f can be certified to be PAG robust with respect to the data distribution D.
Proof. We show that the two assumptions Theorem 4.4 lead to the statement of the theorem if TV = A.
1. To satisfy assumption 1. in Theorem 4.4, 8 2 (log (4) + d log(2x)). i.e., N is an e-net for X' with respect to D' with probability at least 1 - 5/2. Because of Lemma A.3, N is also an (e + -et for X' with respect to D with probability
at least 1 11-6/- 6/2.
2. To satisfy assumption 2. in Theorem 4.4, < s(1 - Pmin) / 2>(1 Pmin) In (3) for = [(x E N conff(x) < kH). i.e., Pr (conf (X) $ x) < Puin with probability at least 1 - 5/2. Using Proposition A.5 with = Pmins follows that Pro(conf/ (X) S x) S - Pmin + with probability at least - 6/2.
By union bound, the probability that either condition does not hold on a given sample N is at most 5/2 + 5/2 = 5. Thus, with probability of at least 1 6, ,, N will be an (e + A)-net for X' under D and the quantile bound holds under D. The data processing inequality (Raginsky, 2014) can then be used to show (Lemma A.2) that an upper bound for the total variation distance of the distribution instances sampled from D and D' when they are mapped into the quality space Q With this, the theorem follows from the definition of c-nets and Lemma 4.5.
B. Construction of Mapping
In this section, we expand on the definition of the mapping function M in Equation (31). The construction of the map can be performed in single pass over the sorted sample N, and is illustrated in Algorithm 1. This process is O[ NI)), bound by the process of sorting, At inference time, M (k) returns the corresponding to the largest confidence K' S K.
The size of the mapping [M), and the corresponding strictness of Proposition 5.1, can be controlled via quantization. Rounding down robustness radii reduces the size of the codomain of M, keeps the guarantees valid, and reduces the spatial requirements of the mapping.
C. Details on Experimental Setup
In this section, we detail how the experiments were conducted. The full code to train, test and analyze the experiments is available at our repository.
15

---

Probably Approximately Global Robustness Certification
Algorithm 1 Obtain k-p-mapping
Input: e-net N, confidence upper-bound Kmax
Output: K-p-mapping (K)
Let M
Let =
/+ iterate through sample in order of increasing robustness P
for (p, x) E N in lexicographic order do
< k I Emax then
M- M (K 0} // add new step from k to p to the mapping
x²
end
end
return .M
C.1. Software and Hardware Used
We use PyTorch to conduct our experiments and perform training with the MAIR (Kim et al., 2023) library for support of normal and adversarial training. In all instances, for TRADES, we chose the parameter 3 = 6. All the experiments were run on a single desktop machine equipped with an Intel i9-1 1900KF @ 3.50GHz CPU and a NVIDIA GeForce RTX 3080 GPU.
C.2. Robustness Oracles
PGD We adapt the internal PGD function in MAIR to return the distance to adversarial examples. To get fine-grained result, we perform many gradient steps with a small step size. For MNIST, we use a step size of 0.5/256 and up to 200 steps to find an adversarial example. We project our examples to valid pixel values between and 1. For CIFAR-10, we use similar setup with a smaller step size of /256 and up to 500 steps. We constrain adversarial images have L distance of most 0.5 the original data point.
LIRPA (Xu al., 2020) offers a Python interface for NN robustness certification. Similar to Marabou, we perform some MNIST models and use the bound propagation capabilities of LiRPA to obtain bound. The LiRPA library lets us define neighbourhood in X' and gives bounds for the logits of f in this neighbourhood. To check if the class of f stays constant around a given point x, with class(x) = c, we query LiRPA for an upper bound UB(x)
preprocessing
UB(x) = max (f(') - fe(x): ||x - X <).. x'eX
(67)
If this upper bound UB(x) 0, then is robust around x. It is worth noting that the bounds reported by LiRPA are not necessarily tight. This means that LiRPA might underreport robustness radii. Similarly to Marabou, we then use binary search to find the smallest value for p.
Marabou While omitted in the main paper due to the better scalability of auto LiRPA, present Marabou here an additional example for robustness oracle. We use the Python interface of the Marabou 2.0 NN verification tool to verify the following query for our network for given data point x E X' and given robustness radius p:
3x' E X' -|x-xxllll
1oo
class(x) * class(x').
(68)
If the formula is UNSAT, the network is locally p-robust. We perform binary search to get bounded estimate of the local robustness radius, and obtain a lower bound of the Loo local robustness radius with 4 bits of precision, to a value of 0.5. In Figure 6, we choose = 2.5/ In(2) 10-3 and ό = 0.01 and Pmii = 0.05, with a six-step binary search for This results in a sample requirement of s(e, 5/2,2) 2)- = 21294.
C.3. NN Architectures
All network architectures were trained with the MAIR library (Kim et al., 2023), using a normal training procedure or TRADES (Zhang et al., 2019) with a 3 6. We trained instances of each architecture on different splits of the training data. For the respective number of parameters, refer to Table
16

---

Probably Approximately Global Robustness Certification
Feed Forward Network We considered three-layer, fully-connected ReLu networks with (768, 50, 10) neurons, trained on MNIST. Refer to github repository and to Appendix D for the exact (hyper)paramette values.
ResNet20 We downloaded untrained ResNet20 network from this Github repository. Refer Appendix D for the exact hyperparameter values.
ConvBig Similarly to the other architectures, we used an untrained ConvBig architecture (Mirman et al., 2018), but trained our instances independently.
VGG11 This CIFARIO network (Simonyan & Zisserman, 2015; loffe & Szegedy, 2015) is our largest architecture with approximately 10M trainable parameters.
C.4. Datasets and Splits
We use MNIST and CIFARIO for our experiments. We train five instances of each architecture in the manner of 5-fold cross-validation. We then use the respective 20% of the training data to sample data points with Gaussian noise added to the data points. The network does not see the validation split during training, and our guarantees are only obtained from the data in the test split. Finally, the test set, both unknown to the network and our verification procedure, is used to the generalization of our guarantee.
To obtain the sampling datasets, consider the following settings:
For the PGD oracle, we choose the verification parameters e 10-4 and ó = Pmin = 0.01. This results in sample size of s(c, 8/2, 2) = 989534.
For the auto_LiPe RPA oracle, due to the more costly local verification procedure, we relax our parameters to 2.5 10-3 5 0.01 and Pmin 0.05. This results in a sample size of s(c, 8/2, 2) 31635.
For each of our experiments, the sampling dataset is then obtained by uniformly choosing data from the sampling split and adding Gaussian noise with mean of 0 and a standard deviation of 8/256 for both.
D. Additional Results
D.1. Additional Results on MNIST
MNIST feed Lower Bound vs Test Data with Standard Training
MNIST feed Lower Bound vs Test Data with TRADES Training
0.25
0.00
0.20
12-
P40 NO0
0.15
010
130
Gonfdorio
Figure 4. Scatter plot of the MNIST test dataset DES. with D = 10000, in the quality space Q for our feed forward network. The left network is trained with standard methods, the right network is trained robustly with TRADES. Results for parameters 10- = Pain 0.01, with [N] = s(c, 8/2.8/2.) /2.2) 2) = 989534.
17

---

Probably Approximately Global Robustness Certification
MNIST feed Lower Bound Test Data with Standard Training
MNIST feed Lower Bound Test Data with TRADES Training
1894/55667705
LAWN
0.06
0.00
0.00
0.00
0.25
2.2 Contidenc Score
0.55
120 0.0
0.25
0.50
0.75
120
Cormidence Score
Lower Dourd
Tel: Chts
Mee Contideree
Lower Board
Tex: 2h4e
Max Conbterce
Figure 5. Scatter plot of the MNIST test dataset Diss with Diesl 10000, in the quality space Q for our feed forward network. The left network is trained with standard methods, right network trained robustly with TRADES, Results for parameters = 2.5 10-3 8 = Pmin 0.01, with |N| s(c, 6/2, 2) 31635.
MNIST Lower Bound vs Test Data with Standard Training
MNIST Lower Bound vs Test Data with TRADES Training
0.25
0.25-
Formal F Robustness (L Inf distance)
Inf distence)
0.20
0.20
0.15-
0.15-
0.10-
0.05-
Formal
0.05
0.00
0.00-
0.00
0.25
0.50
0.75
1.00
0.b0
0.25
0.50
0.75
1.00
Confidence Score (quantiles)
Confidence Score (quantiles)
Lower Bound
Test Data
Max Confidence
Lower Bound
Test Data
Max Confidence
Figure 6. Scatter plot of the MNIST dataset Drss. with (Desl 10000, in the quality space Q for our feed forward network. The left network is trained with standard methods, the right network is trained robustly with TRADES (5 = 2). Results for parameters e 2.5/ In(2)- 10-3 5 0.01 Pain 0.05, with |N] s(c, 8/2, /2,2) 2) 21892.
18


Reviews:
[{"review_id": "QDNA4mAzVg", "reviewer": "Reviewer_md7J", "summary": "This method tackles the problem of constructing a method for estimating global robustness of a NN (or other function) that has a formal guarantee. The authors take the approach of probabilistically relaxing the definition of robustness and producing a probabilistic certificate of global robustness. The size of the sample required for the certificate is independent of the input dimension, number of classification classes, etc., which is particularly important for scaling to e.g. deep NNs.", "questions": "", "limitations": "", "rating": 4, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for your comments. As you suggested we added additional experiments to demonstrate the potential of our approach. \nIn our reply, we also address the questions about our experimental evaluation from other reviewers. \n\n\n\nWe first point out that\n**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. \n\n\n## New experiments with larger architectures\n\nWe focus on MNIST and CIFAR-10, as these are commonly used in related verification literature (as in [1, 2] referred by `8m6m`).\n \nTo address scaling, we have performed additional preliminary experiments with bigger architectures for adversarial as well as formal verification.\n\nWe run additional experiments with:\n* a VGG network (vgg11_bn [e]), a convolutional architecture with ~10 million parameters, on CIFAR10 with a PGD oracle;\n* ConvBig, a convolutional network used in the references provided by reviewer `8m6m`, on MNIST with a LiRPA (from αβ-CROWN) oracle;\n* the feed forward (FF) network on MNIST (as previously used in the manuscript), with a LiRPA (from αβ-CROWN) oracle.\n\n| Architecture | Training | Oracle | $\\epsilon$ | $p_{\\min}$| $\\delta$ | $\\lvert N\\rvert$ | $\\lvert M\\rvert$ | $\\lvert\\mathbf x_{\\kappa\\leq\\kappa_{\\max}}\\rvert$ | $n_c$ | $\\hat p_\\kappa$ | verification runtime (s) | accuracy |\n|--|--|--|--|--|--|--|--|--|--|--|--|--|\n| vgg11_bn | Standard | PGD | $10^{-4}$ |$0.01$| $0.01$ | $685044$ | 10 | 9559 | 0 | 0 | 731 | 0.9174 |\n| ConvBig | DIFF_AI | LiRPA | $2.5\\cdot 10^{-3}$|$0.05$ | $0.01$ | $21892$ |12 | 9667 | 4 | 0.000309 | 1838 | 0.9320 |\n| MNIST-FF | AT | LiRPA | $2.5\\cdot 10^{-3}$ |$0.05$ |$0.01$ | $21892$  | 7 | 9726 | 1 | 0.000851 | 508 | 0.9328 |\n\nWe 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.\nIn 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$.\nThese results demonstrate that our approach works with a variety of datasets, models, and training procedures.\nWe will include these results in the revised manuscript. \n\n## Scalability\n\nThe scalability of our method is closely tied to the scalability of the chosen local robustness oracle.\nIf 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.\nPGD 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.\nFor 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.\nWith 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.\n\nOur 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).\n\nReferences:\n[e] https://github.com/chenyaofo/pytorch-cifar-models", "claims_and_evidence": "Claims of robustness of certificate are supported by theoretical analysis, see Theorem 4.4 / 4.6.", "methods_and_evaluation_criteria": "Experiments make sense for the problem at hand. There are ablation studies showing a more confident predictions tend to be more robust under the method proposed in the paper, and that there is a strong dependence between prediction confidence and robustness.", "theoretical_claims": "Yes, checked up to Theorem 4.6.", "experimental_designs_or_analyses": "Experiments are sound but could be more impressive and demonstrate scaling, even with a single consumer-grade GPU. MNIST and CIFAR-10 are quite small for 2025 (although no doubt useful for the computationally intensive experiments using formal evaluation).", "relation_to_broader_scientific_literature": "This work is particularly connected to prior work that defines NN robustness as probability, rather than that relating it to formal verification or distance to adversarial examples. Prior work has shown methods that are can estimate probabilistic robustness either at a given point or globally, but have not had a formal guarantee of robustness.", "essential_references_not_discussed": "N/A", "other_strengths_and_weaknesses": "N/A", "other_comments_or_suggestions": "Typo in Line 162 right column: \"For this, we devise on a\" => remove \"on\"", "questions_for_authors": "Could you please provide additional results showing how the method really scales to larget input dimension and model size?", "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": "XWcczj2bFX", "reviewer": "Reviewer_gsc4", "summary": "This paper introduces a novel method for certifying the global robustness of neural networks (NNs). The method employs a sampling procedure to create an $\\epsilon$-net, which is used along with a local robustness verifier to provide probabilistic guarantees on the robustness of the model, depending on its prediction confidence at a given point. Once the sampling procedure is performed, the approach can provide robustness guarantees for every point in the feature space without requiring the sampling procedure to be run again; in this sense, it provides global robustness guarantees. The approach assumes access to the true data distribution of instances in the feature space or a proxy of it (e.g., approximated with Gaussian noise). The experimental evaluation considers a feed-forward NN on MNIST and a ResNet-20 on CIFAR-10, demonstrating that the theoretical guarantees provided by the approach are also confirmed in practice. In particular, the probabilistic robustness guarantees hold with high probability in practice.", "questions": "", "limitations": "", "rating": 4, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you for your thorough review and for the interesting and relevant references. \n\n**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. \nGetting enough representative samples from the true data distribution can be challenging in the real-world. \nHowever, 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. \nThe fact that our (Gaussian-noise-based) sampling procedure is sufficient substantiates the practical effectiveness of our approach. \n We also refer you to our answer to a similar question of reviewer `8m6m`.\n\n**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. \nOverall, 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.\n\n**Runtimes in Tables.** Thank you for pointing this out, we will make it more explicit in the tables.\nThe 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.\nThe 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.\nThe runtime of this local robustness check heavily depends on the specific oracle chosen.\nThe large runtime in table 3 is determined, for instance, by the large computational requirements of the Marabou verifier.\nWe 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`).\n\n**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.\nThe notion discussed by Wang et. al. [c] is a sensitivity-based notion of global robustness. \nTheir definition is not specifically tailored to a classification task, as it does not consider a notion of class explicitly. \nWe 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. \nRather, the notion in Wang et. al. [c] captures a notion of function smoothness over all the input space.\nNot 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.\nWe 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.\nOur 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.\nThis 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.\nWe thank you again for the additional references that we will discuss and compare in more detail in a revised version of the manuscript.\n\nPlease let us know if we can provide any further details.", "claims_and_evidence": "The claims of the paper are sufficiently supported by mathematical proofs and experimental evidence. The experimental evaluation convincingly shows that the theoretical bounds provided by the approach are reflected in practice. However, there are a few small points that the authors should discuss more in depth, in particular the approximation of the data distribution used by their approach and the influence of the sampling procedure on the total runtime of the method.\n\n\n**Update after the authors' response**: the authors have satisfactorily answered to my questions and clarified the minor points.", "methods_and_evaluation_criteria": "The considered models (a feed-forward neural network and ResNet-20) and datasets (MNIST and CIFAR-10) are reasonable and in line or larger than the ones considered in previous related work (like [a]). Moreover, the chosen evaluation criterias are comprehensive to assess that the provided guarantees are satisfied and describe the behavior of the networks well.\n\n[a] Athavale et. al., Verifying global two-safety properties in neural networks with confidence, CAV, 2024.", "theoretical_claims": "I checked the proof of Proposition 4.2, that serves as a building block for bounding the joint probability that the classifier provides a prediction above a certain threshold without being robust on the sample. I also checked the proofs of Lemma 4.3, which establishes a lower bound on the probability of obtaining a given (or bigger) prediction confidence by the classifier, and Lemma 4.5.", "experimental_designs_or_analyses": "The experimental results presented in the paper support the claim regarding the validity of the guarantees on global robustness provided by the proposed approach. Figure 3 shows that the test data closely follows the mapping used by the approach to relate confidence values to lower bounds on robustness. Additionally, Table 1 demonstrates that, in the majority of runs, the global robustness guarantees provided by the approach hold even for unseen test data. However, there are some exceptions where this may not hold, and the authors have detailed the reasons behind these cases.", "relation_to_broader_scientific_literature": "This work is closely related to [a], since both address the global robustness property while considering the confidence of the verified model, i.e., global robustness is verified for inputs where the model exhibits a certain level of confidence in its predictions. While the approach in [a] proposes a method that provides deterministic guarantees on global robustness, the method presented in this paper offers probabilistic guarantees. Although probabilistic guarantees are looser than deterministic ones, this choice enables the proposed method to scale to larger models and leverage standard verifiers for local robustness.\n\nOther definitions of global robustness and verification methods have been proposed in [b], [c], and [d], since there is not a one-size-fits-all definition of global robustness in the literature at the moment. The authors should also discuss these approaches in relation to the ones they consider.\n\n[a] Athavale et. al., Verifying global two-safety properties in neural networks with confidence, CAV, 2024.\n\n[b] Kabaha and Cohen, Verification of Neural Networks’ Global Robustness, Proc. ACM Program. Lang., 2024.\n\n[c] Wang et. al., Efficient Global Robustness Certification of Neural Networks via Interleaving Twin-Network Encoding, IJCAI, 2023.\n\n[d] Calzavara et. al., Beyond Robustness: Resilience Verification of Tree-Based Classifiers, Computers&Security, 2022.\n\n**Update after the authors' response**: the authors have satisfactorily answered to my questions and discussed the suggested references.", "essential_references_not_discussed": "There are no essential references omitted by the authors. However, they could make their discussion of related work more comprehensive by considering additional relevant approaches (see the _Relation To Broader Scientific Literature_ section).\n\n**Update after the authors' response**: the authors have satisfactorily answered to my questions and discussed the suggested references.", "other_strengths_and_weaknesses": "## Strengths\n\n- This is the first approach that provides probabilistic approximate guarantees on the global robustness of neural networks, which can also scale to larger networks than those considered in previous work.\n- The adopted notion of global robustness is intuitive and reasonable.\n- Good theoretical foundation, including proofs of the statements that support the approach.\n- The experimental evaluation is convincing.\n\n## Weaknesses\n\n- The approach works with both the original data distribution of the samples in the feature space and an approximation of it. However, the quality of the approximation used in the experimental evaluation is not clearly discussed.\n- Missing details on how the sampling procedure influences the runtime of the approach.\n- Related work discussion can be improved.\n\n**Update after the authors' response**: the authors have satisfactorily addressed these weaknesses. Thus, I will raise my score.", "other_comments_or_suggestions": "The authors should consider strengthening the discussion of related work by including works [a], [b] and [c] and discussing how the verification approach and/or the global robustness property considered in the current paper differ from those proposed in these three works.\n\n[a] Kabaha and Cohen, Verification of Neural Networks’ Global Robustness, Proc. ACM Program. Lang., 2024.\n\n[b] Wang et. al., Efficient Global Robustness Certification of Neural Networks via Interleaving Twin-Network Encoding, IJCAI, 2023.\n\n[c] Calzavara et. al., Beyond Robustness: Resilience Verification of Tree-Based Classifiers, Computers&Security, 2022.\n\n\n**Update after the authors' response**: the authors have satisfactorily discussed the suggested references.", "questions_for_authors": "- In Section 6 (Experimental evaluation), the authors states that `we discuss how the data distribution $D$ can be approximated sufficiently well for our purposes with Gaussian noise.`. This point is important for the inner workings of the proposed certification approach, but I do not see any comments or results highlighting that the data distribution is well approximated. Could you please provide a comment on this and offer evidence? Have I missed something?\n- The proposed approach requires sampling a large number of instances to obtain global robustness guarantees, e.g., 21,892 instances for the MNIST dataset. How does this step impact the total runtime of your approach? For which specific steps is the runtime reported in Tables 2, 3, and 4 computed?\n\n\n**Update after the authors' response**: the authors have satisfactorily answered to these questions.", "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": "77wuIi3Qwy", "reviewer": "Reviewer_gTTU", "summary": "The authors propose a probabilistic framework to evaluate global robustness in neural networks. Global robustness for a neural network is defined such that a neural network is globally robust if it is robust at all confident predictions. The approach relies on \\epsilon-nets and is evaluated on MNIST and CIFAR-10 datasets.", "questions": "", "limitations": "", "rating": 2, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you very much for your review and comments.  We address them below.\n\n**Size of the certified NNs.** Techniques like CROWN and randomized smoothing do indeed scale up to large networks for *local robustness* certification.\nHowever, our work is concerned with using local robustness checks to provide *global robustness guarantees*.\nThe per-example verification time reported by  Wang et al. is large for our application, as meaningful global guarantees require 10K-100K local robustness checks. \nApproaches 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.\nOur approach scales significantly better than these approaches. \n\n**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.  \n\n**Comparison to Webb et al.** Our objective is fundamentally different to Webb et al.\nThey 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.\nIn 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).\nIn 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.\nMoreover, Webb et al. rely on a problem-dependent termination condition.\nWe will add this discussion in the related work section. \n\n**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.\nThat 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}))$.\nThis 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).\n\n**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.\nThis 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.\nThe 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.\n\n**Unbounded distribution support.** Yes, our method does not rely on the assumption that the data distribution is bounded. \nAll 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. \n\n**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).\nOur 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. \nOur approach guarantees that such a statement indeed generalizes to test data.\n\n\nWe hope our comments addressed the questions you raised. We are happy to engage in further discussion.", "claims_and_evidence": "Some of the claims are not accurate. For instance:\n\n- The authors claim that verification-based techniques for neural networks are limited to networks with small networks, where I guess small networks mean few hundreds of parameters. However, techniques such as CROWN have already scaled to larger networks than those considered in this paper [Wang, Shiqi, et al. \"Beta-crown: Efficient bound propagation with per-neuron split constraints for neural network robustness verification.\" Advances in neural information processing systems 34 (2021): 29909-29921.]. Also, techniques like randomized smoothing [Cohen, Jeremy, Elan Rosenfeld, and Zico Kolter. \"Certified adversarial robustness via randomized smoothing.\" international conference on machine learning. PMLR, 2019.], which could also provide guarantees (even if with some confidence), have already scaled to IMAGENET.", "methods_and_evaluation_criteria": "The evaluation performed by the authors makes sense. However, I miss an empirical comparison, for example, in terms of the number of required samples with comparable methods, such as [Webb, S., et al. \"A statistical approach to assessing neural network robustness.\" Seventh International Conference on Learning Representations (ICLR 2019). International Conferences on Learning Representations, 2019], which seem to be applicable to the same specification.", "theoretical_claims": "Theoretical claims appear correct to me.", "experimental_designs_or_analyses": "While experimental analysis seems sound, as mentioned above, I miss a comparison with comparable samples. Also, it would be important to see how the number of required samples changes with the confidence required.", "relation_to_broader_scientific_literature": "Adversarial verification of neural networks is an important problem, and the probabilistic global notion of robustness considered here is surely important. However, as similar statistical approaches based on samples from the data distribution have already been used for similar problems, it would be important to have at least an empirical comparison with state-of-the-art to be able to judge the importance of the results.", "essential_references_not_discussed": "Most of the key references are mentioned, but, as I mentioned above for the Webb, S., et al. case or the literature in formal verification, some of them are not discussed properly.", "other_strengths_and_weaknesses": "As mentioned above, it is difficult to evaluate the strengths of the paper without a proper comparison with the literature or more extensive experiments to see how the required number of samples changes.", "other_comments_or_suggestions": "N/A", "questions_for_authors": "Apart from the ones mentioned above in terms of comparison with Webb, I have the following ones:\n\n- How do you compute the VC dimension d for your problem with the various neural networks?\n\n- Can your result also be applied if the data distribution support is unbounded?\n\n- As some of your results are based on the fact that all samples are robust, how does your complexity in terms of the number of required samples change if the true robustness probability is not 100%, but say 99%?", "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": "oPna144BkB", "reviewer": "Reviewer_8m6m", "summary": "The authors propose an algorithm that extends local robustness certification techniques to the entire input space with probabilistic guarantees. To achieve this, they introduce a novel approach for quantitatively characterizing a Deep Neural Network's (DNN's) robustness across the input space. Specifically, their method establishes high-probability lower bounds on robustness for each input point using only independent and iid samples and access to a local robustness oracle. The authors leverage existing local robustness testing oracles, such as adversarial attacks like PGD and formal local robustness verifiers, to determine the robust radius around a single sampled data point.\n\n## Update after rebuttal \nI thank the authors for their response. I have decided to maintain my scores and remain on the fence about this manuscript, as I see a mismatch between the theory and the proposed algorithm. The test dataset—or the samples obtained by perturbing it—may not truly represent i.i.d. samples from the global input distribution. Furthermore, relying on the test dataset inherits the same criticism faced by local robustness verification: it does not account for valid inputs (e.g., valid images of an airplane) that differ from those in the test set. Since the test dataset may not be a representative sample of all valid inputs for a given class, global robustness remains an important and unsolved problem.", "questions": "", "limitations": "", "rating": 2, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Thank you very much for your thorough and insightful review.  We address your comments in the following.\n\n**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. \nHence, our approach directly addresses the dataset dependence of local robustness methods.\nFor our theoretical statements, we indeed rely on the common assumption that we can get *unlabelled* iid samples from the data distribution.\nIn our experiments, our sampling procedure may only approximate the data distribution.\nHowever, our evaluation shows that this approximation is sufficient to let our guarantee generalize to unseen data.\nThis setup does not undermine our theoretical findings but rather demonstrates that our theory works in practice even in imperfect settings.\nThis is also supported by Theorem 4.6.\n\n**Robust accuracy** is an empirical measure of model accuracy and local robustness.\nGiven a set of points, robust accuracy quantifies, for these points *only*, how often a perturbation leads to misclassification.\nOur method is fundamentally different.\nOur approach does not aim to measure robustness directly but rather formalizes the conditions for generalization of robustness from a sample to the distribution.\nFor this, we can provide guarantees for *any* given local robustness oracle, including one based on robust accuracy.\n\n**Robustness vs Accuracy.**  We consider robustness and accuracy to not necessarily be related. \nThis is consistent with the literature on robustness verification (e.g. [a] from `gsc4`). \nIf ground truth labels are available to the local robustness oracle, then our theory can accommodate a notion of robustness that considers accuracy as well.\n\n**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$.\nFor each point in the sample, the oracle reports a local robustness radius and in Eq. 30 we take the minimum of these reported values.\nOur 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.\nWhile 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).\nWe report lower bounds for both an adversarial and a formal oracle on the same data in Fig. 4 and 5.\nCompared to PGD, a formal verifier can provide more conservative bounds (Fig. 5).\n\n**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.\nHence, our results for PGD are high probability robustness lower bounds for the distance required to reach an adversarial example using the PGD attack.\nWe obtain these lower bounds by *exact computation of Eq. 30* for our sample $N$ with our chosen robustness oracle.\n\n**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.\nWe provide details in the response to reviewer `md7J`.\nBoth CIFAR and MNIST are commonly used benchmarks in the robustness literature [1, 2].\nThe 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. \nIn our experiments, we investigate networks of comparable size to [1,2] and often achieve better accuracy.\n\n**Other tools.** We run more experiments using recent libraries from the $\\alpha$-$\\beta$ CROWN tool (please see reply to `md7J`).\n\n**Theoretical results**. Thank you for the pointers, we will revise the section accordingly to highlight our contributions. \nProposition 4.2 does follow from Definition 3.5.\nLemma 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.\n\nWe hope we have addressed your concerns and thank you again for your detailed review. \nWe are very happy to engage in further discussion if you have more questions.", "claims_and_evidence": "**Strengths**  \n- The overall approach is mathematically well-motivated, and the use of $\\epsilon$-nets to probabilistically characterize the DNN's robustness across the input space is an interesting theoretical idea.  \n\n**Weaknesses**  \n- The theoretical results and the proposed approach assume access to a sampling technique that can generate iid samples from the data distribution (e.g., MNIST/CIFAR10 images). However, the authors do not clarify how they ensure that their sampling method truly provides iid samples from the entire MNIST or CIFAR10 distribution. Instead, they rely on dataset samples (or dataset samples perturbed with Gaussian noise), meaning the approach inherits the same fundamental limitation as local robustness methods (**dependence on the Dataset**). Consequently, the guarantees remain dataset-dependent, which undermines the paper’s motivation of generalizing robustness guarantees to the entire input distribution.  \n\n- Building on the previous point, the proposed method appears to be a modification of **robust accuracy**, which measures the percentage of $L_{\\infty}$ regions around test data points that are verified as robust in local robustness studies.  \n\n\n- In Section 3.1, the class of the sample $x$ is defined as $\\text{class}(x) = \\arg\\max_{i \\in [1, n]} f(x)_i$. Please correct me if I am wrong, but under this definition, even if the classifier $f$ consistently predicts the wrong class (one that does not match the ground truth) with high confidence, it would still be considered robust. Is this intentional? If so, does this mean that a classifier with very poor accuracy (making incorrect predictions that do not match the ground truth with high confidence) could still achieve a high robustness measure according to the proposed method?", "methods_and_evaluation_criteria": "See the questions from the previous section and additionally:  \n\n- Exactly computing Eq. (30) is an NP-hard problem. Formal verifiers can compute a valid lower bound, while adversarial attacks provide an upper bound. However, both bounds can be imprecise. The authors should report both bounds to present a clearer picture.  \n\n- In lines 40–43, the authors claim: * That is, for each point in the input space we are able to give a high-probability lower bound for its robustness.\"* However, in the CIFAR10 experiments, they use only adversarial attacks, which compute an upper bound for Eq. (30)—a bound that can be significantly far from the optimal. Doesn't this contradict the claim made in lines 40–43? Please let me know if I am misunderstanding something.", "theoretical_claims": "I have not carefully verified the detailed proofs in the Appendix. However, I have reviewed the proofs in the main paper and skimmed through those in the Appendix. They appear to be correct to me.", "experimental_designs_or_analyses": "The experiments are limited to a single standard and adversarially trained MNIST and CIFAR10 network. Additionally, I have some concerns regarding the robustness oracles used—see `Methods and Evaluation Criteria`. Once the authors clarify these doubts, I may have follow-up questions regarding the experimental design and analysis.", "relation_to_broader_scientific_literature": "I believe global robustness is a crucial problem for ensuring the safety of DNNs across the entire input distribution. However, my primary concern is that the guarantees obtained in this work, like those in local robustness studies, are essentially tied to the test dataset.", "essential_references_not_discussed": "I believe the authors have overlooked some of the most recent works on local robustness and local hyper-property verification (I referenced two from NeurIPS 2024 in the previous sections). There is also minimal discussion on GPU-accelerated Branch and Bound (BaB) based complete verifiers. I think the authors should consider using them for the CIFAR10 DNN experiments, which would help them apply formal methods to CIFAR10 networks as well.", "other_strengths_and_weaknesses": "Please refer to the `Claims And Evidence` and `Methods And Evaluation Criteria` section.", "other_comments_or_suggestions": "I would suggest that the authors clarify the theoretical results in Sections 4 and 5, distinguishing between their original contributions and results derived from existing works or modifications of well-known results. This will make the paper much easier to read. For instance, Proposition 4.2 follows directly from Definition 3.5, and (may be wrong but) Lemma 4.3  appears to stem from existing results. Please explicitly mention these sources and highlight any specific extensions or modifications made to the existing results.", "questions_for_authors": "Please refer to the `Claims and Evidence` and `Methods and Evaluation Criteria` sections. I am open to increasing my evaluation if my concerns regarding dataset dependency and the similarity to local robustness are adequately addressed.", "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:

Meta-review: This paper presents a sampling based approach towards certifying global robustness. In particular, the authors attempt to certify the lack of points (or that such regions have low mass) where the model confidence is high but the model prediction is not robust. The authors propose an approach where a certain number of points are sampled and an empirical estimate is constructed. The authors also present an empirical validation of their method when certain popular algorithms such as TRADES are used as robustness oracles for the sample. Overall this is a nice addition to the list of methods on certifying global robustness.
Decision: Accept (poster)