Efficient Statistical Assessment of Neural Network Corruption Robustness
Authors: Karim TIT
Teddy Furon
Mathias ROUSSET
Venue: NeurIPS 2021 Poster (2021)
Keywords: deep learning
robustess
reliability
Monte Carlo

Abstract: We quantify the robustness of a trained network to input uncertainties with a stochastic simulation inspired by the field of Statistical Reliability Engineering. The robustness assessment is cast as a statistical hypothesis test: the network is deemed as locally robust if the estimated probability of failure is lower than a critical level.
The procedure is based on an Importance Splitting simulation generating samples of rare events. We derive theoretical guarantees that are non-asymptotic w.r.t. sample size. Experiments tackling large scale networks outline the efficiency of our method making a low number of calls to the network function. 

Efficient Statistical Assessment of Neural Network Corruption Robustness
Karim Tit
Teddy Furon
Thales Land and Air Systems, BU IAS Rennes, France Univ. Rennes, Inria, CNRS, IRISA Rennes, France karim. Barim.tit@ine tit@inria.ffr
Univ. Rennes, Inria, CNRS, IRISA Rennes, France
feddy.fuuroninniis fr
Mathias Rousset
Univ. Rennes, Inria, CNRS, IRMAR Rennes, France
mathias roo.lstirruuss.iiiiia....
Abstract
We quantify the robustness of trained network to input uncertainties with a stochastic simulation inspired by the field of Statistical Reliability Engineering. The robustness assessment is cast as a statistical hypothesis test: the network is deemed as locally robust if the estimated probability of failure is lower than critical level. The procedure is based on an Importance Splitting simulation generating samples of rare events. We derive theoretical guarantees that are non- asymptotic w.r.t sample size. Experiments tackling large scale networks outline the efficiency of our method making low number of calls to the network function.
Introduction
Despite state-of-the-art performances on many Computer Vision and NLP tasks, Deep Neural Net- works (DNNs) have been shown be sensitive to both adversarial and random perturbations (Gilmer et al. 2019 Franceschi et al. 2018). Concerns about their safety and reliability have come forth as their applications move critical fields, such as the defense sector self-driving vehieles.
Certification A posteriori certification aims at verifying the correct behavior of a trained network : _". This expected property is usually defined locally (a.k.a. instance-wise property): the network performs correctly in the neighborhood Vxx.) C IR" of particular input E IR". Let us denote ((-1x.) R {0. 1} the function indicating violation of the expected property. The network is locally correct if xx = O for any x E V(x.).
In classification, the property takes the name of robustness and reads the output of the network remains unchanged over the neighborhood (xx.). It certifies that the network robust against inputs corrupted by uncertainties of limited support adversarial perturbations of constrained distortion.
The certification mechanism has two desired features as defined
Singh et al. 2018):
Soundness: does not certify the network when the property does not hold.
Completeness: it does certify the network whenever the property holds.
35th Conference on Neural Information Processing Systems (NcurIPS 2021).

---

Corruption robustness assessment Adversarial robustness corresponds to worst-case analysis whereas corruption robustness considers random perturbations of the inputs. The key ingredient is the introduction of a statistical model To of epistemic uncertainties occurring along the acquisition chain of the input. For instance, |ranceschi et al. 2018 take Gaussian and uniform distributions over the 1p ball (x,) of radius centered on X
This recent trend goes with a quantitative assessment gauging to what extent given property holds or does not hold. For instance, Webb et al. 2019] estimate the probability that a property is violated under a given statistical model of the inputs. This approach makes no assumption about the network under scrutiny as it is used as a black box. This grants the scalability to tackle deep networks. The main difficulty lies in the efficiency, i.e. the computational power needed estimate weak probabilities. Their lack of soundness stems from the inability to determine if the probability of violation is exactly zero or too small to be estimated.
Section 2 presents a brief overview of robustness assessment procedures outlining the assumptions made about the network and their limitations.
This work presents a scalable and efficient procedure assessing corruption robustness under a large panel of statistical models. It provides completeness and theoretical guarantees the lack of soundness.
2 Related work
This section reviews the ofate-of-the-arr in certification and corruption robustness assessment.
Assessment by example Distortion constrained adversarial attacks, like PGD, look for property violations, a.k.a. adversarial examples, inside the ball Bx.c(x)) In the context of robustness, they take advantage of the fast computation of the gradient of the network function thanks to propppropaattion.. They are fast, complete but unsound priori. The network is not certified if the attack succeeds, but failure says nothing about the property: attacks are empirical processes without guarantees.
Formal certification Using SMT solver, Katz et al. 2017 provide sound and complete certification method, called ReI.Uplex, designed for Neural Networks with ReL.U activation functions. However the same paper shows that the problem of sound and complete certification of neural networks (even restricted ReLU activations) is NP-complete. Scaling to large modern networks seems difficult. In addition, although these formal methods are complete in theory, in practice the procedure might give up, terminating undecided with a 'timeout' if the underlying solver is too slow.
Incomplete certification To gain scalability. researchers have proposed sound but by-design in- complete verification methods resorting to abstract domains which are usually convex approximations of the input domain. [Singh et al. (2019) obtain significant speeding up compared to ReI.Uplex and other complete certifiers. They introduce a verification benchmark called ERAN (see Sect. (5) Weng et al. [2018) design another incomplete certification based on lower and upper linear functional bounds of Multi-Layer Perceptrons (MLPs) with ReLU activation.
generalized to MLPs with general activation functions in [Zhang et al.) 2018 and to Convolutions Neural Networks (CNNs) in [Boopathy et al. 2019 Weng et al. 2019]. All these certifications methods rely on lower bounds of the minimum distance of adversarial examples. They thus pessimistic in the sense that they can reject many valid propertics because the lower bound is not always tight enough. In order to be 'more complete', [Salman et al. [019)] solve the optimal convex relaxation (only for specific problems on MNIST and CIFARTO datasets) with extensive computational resources. They conclude that the tightness of the lower bounds cannot be improved, suggesting that this approach has found its limit.
Statistical assessment Corruption robustness assumes a statistical model mo of noisy inputs like Gaussian or uniform distributions over the 4p ball Bp.c (x,). Franceschi al. (2018) study the robustness of both linear and deep neural networks. They obtain precise bounds for linear classifiers
which they extend to non-linear classifiers with 'locally approximately flat decision boundaries'. Webb et al. 2019 introduce a robustness metric (the lower, the more robust) is defined by:
== <x(((X(x)) = 1) = [ (xx(x))=((de)
(1)
2

---

The quantitative assessment is in stark contrast with the adversarial robustness literature taking worst-case analysis. A connection is established when To is the uniform distribution over the ball (x.( the volume of the set of adversarial examples equals vol (x.)). Baluta et al. [021] name probability p the adversarial density.
The main difficulty lies in the estimation of this integral, in particular when the event {x x 1 rare under distribution To. Baluta al. [2021] use a crude Monte Carlo simulation, Webb et al. [2019) use Importance Splitting (a.k.a. multi-level splitting) with a rejuvenative mechanism based on the Metropolis-Hasting
algorithm. These two last works make no assumption about the network as their procedure uses it as a black box. This grants scalability (in the sense that it tackles deep networks). The efficiency of the statistical test/estimation procedure is measured by the runtime or the number of calls to the black-box model.
The quantitative assessment falls back to certification by taking final decision: the network is deemed reliable the probability of violation smaller than Pe > 0, a critical probability set by the user. strikes the trade-off between the lack of soundness and the efficiency: a low Pe increases the soundness but requires estimating probabilities as low as which is computationally demanding.
3 Our approach to corruption robustness assessment
Our approach uses statistical hypothesis testing as certification surrogate. As in BBaluta al. 2021 the user sets a low critical probability Pr: and the test assesses whether is lower or larger. However, rather than a testing approach powered by crude Monte Carlo simulations, our workhorse more efficient Sequential Monte Carlo algorithm [Naesseth et al., 2019]. This so-called 'Last Particle'
simulation was invented by Guyader al.
[011] and variant of the Adapative Multi-Level We show that, with carefully chosen termination condition, it is advantageous both in terms of computational efficiency and theoretical guarantees.
Sampling employed by Webb et al. [2019]
Sect. 3.J presents the 'Last particle' simulation that Sect. [322 applics to statistical hypothesis testing in the framework of robustness assessment. Alg. gives the pseudo-code of our procedure.
3.1 The Last Particle simulation
The goal of the Last Particle simulation is efficiently generate samples drawn according a reference probability distribution To but in a region R : (y h(y) > 0} C R" where h R - R, the so-called the score function. Efficiency is the ability to perform this task using few calls the score function, even when probability (R)) is small.
The simulation manages set of N particles (i.e. samples) which are initially i.i.d. with respect to mo- The name 'Last Particle' comes from the fact that the simulation 'kills' the sample with the lowest score each step. The score of this last particle becomes the intermediate level La iteration (Alg. M line 6). Then, that particle is refreshed by sampling according to mu but conditioned on the
event (x(X) L& }. This sampling procedure is performed by Gen (L, 1) line 11 and detailed in Sect. Gen( N) then simply means sampling N random vectors according to To (line 3
The algorithm stops when the number of iterations reaches integer
any iteration if the intermediate threshold La is positive which means the simulation has generated samples as required.
Consider the function A IR + R4 defined as
A(f) log no (h(X) > e)-
This function unknown in practice, but one can easily see that is non decreasing.
During one run of Alg. the intermediate levels are random variables following an increasing order by construction: L1 < L2 < < Lg. We here copy the main result of the Last Particle simulation:
Theorem ([Guyader et al. 2011)). ). The variables A ([I),A(L2)) ... are distributed as the succes-
sive arrival times of a Poisson process with rate N: A(Lx) 1/N E where E(1).
As the sum of i.i.d. exponential random variables is distributed as a Gamma random variable, this theorem states that A(La) ~ I'kk N) (i.e. scale & and rate N).
Herr and after, denotes distributional equality between random variables.
3

---

Algorithm Robustness assessment with Last Particle simulation
Require: Number of particles N, critical probability level Pe, confidence interval level o
Ensure: Cert
1: Initialize: + I/N,
+ 1, Cert + False, Stop +- Fulse
2: m -Comp_m(pp:00 a,
> See Sect. 3,3
3: {x t No
D> See Sect.
4: while k S & Stop False do
5:
i" + arg WW h(x;)
6:
L c h(x;-)
7:
if L& > 0 then
8:
Stop True
9:
Past t pk-1
end
11: X.. + Gen 1)
See Sect.
12:
k+
13:
end while
14: if Stop = False then
15: Cert < True
16: Pest + Pe
17: end if
18: return Cert, Post
3.2 Corruption robustness assessment as a statistical test
In the framework of robustness assessment of classifiers, the score function is related to the usual loss in the adversarial example literature:
fx(x) (x)) h(x): := kxf((x.)
where f(x) represents the predicted probabilities (or logits) vector and c(x) == arg max; f' (x) is
the predicted class for input x. Note that h(x,) < O and that the violation indicator function of Sect. simply (x(xx,) 1 (h(x) > 0). The input Wo models the corruption distribution around x,- The
probability of robustness violation defined is writes as (x())X > 0).
Our approach establishes hypothesis test parametrized by a low probability Pe given by the user.
No: The probability of robustness violation > Pe- The network should not certified.
:1: The probability of robustness violation p < Pe. The network can certified.
For given true probability of violation p, establish the following properties.
Proposition 1. The probability false positive Pip(p) equals:
(p) P(Cert Truelp > pc) Jo log pm dt
7(m, - llggp)
(4)
tt
I(m)
Proof. Certification means that, according the Alg. I even after m loops, the intermediate threshold Lm is still lower than 0. This happens with probability:
7m,, -N logp)
Pip(p) P(Lm <0) = PP((LMm) < <(O))
(5)
[(m)
since A(Lm) ~ I(m, N) and A(0) = log p: (8) being the lower incomplete gamma function.
Proposition 2. The probability of false negative Ptn (p) equals:
f I log e 'tt
7(m, - N log
Ptn = P(Cert = Falselp < pc)
(6)
Jo tme-ldt
I(m)

---

Proof. The certification failed because L > 0 for some K I m. or equivalently A(Lx) A(O). Note that this was not true iteration K' (otherwise the while loop would have be broken earlier).
In other words, K - 1 = supfi Σj=1 E, < -N -Nlogp E)~E(1)), so that K - 1 follows the Poisson distribution P log p). The probability of false negative is the c.d.f. of K at 1:
Pin (p) = P( & m) = P(K - 1 m m 7(m. - log
(7)
r(m)
where 7(s, x) is the upper incomplete gamma function.
This shows that (p) is an increasing function and the worst case happens when converges to Pei
Vp Pey Pp)(p) S (pn(p))
(ip(pe)
(8)
Remark that the trade-off between false positive and false negative probabilities is hard at p = Pe- Yet, Eq. (7 tells that Ptn is quickly vanishing as p 0, especially when N is large.
3.3 Corruption robustness assessment as a certification problem
In the context of certification, we show that that our procedure is complete but not sound, ii) false positive probability drives the lack of soundness.
false negative is not bad event since it avoids to certify when the probability of violation
is not zero. At the same time, our procedure always certifies whenever the property holds since Pt (0) 0. On the contrary, false positive remains an error since we certify when p > Pe 0. Let us quantify the lack of soundness by
1 - (1-Pr((p) if <p
Sound (p) = (ps(p) == PPNod
(pp(pp) otherwise
Let us recall that in our case it holds simply - (p) Pip(p).
Proposition A suitable choice of the maximum number of iterations m in Alg. Acan control the lack of soundness by the critical probability Pe. and required significance level a E (0, 1) s.t.
Pos(p) S a, vp 2 Pc.
(10)
Proof. This amounts to enforce that Pip(p) S a, Vp > Pe. Since - log is decreasing function,
the worst case occurs in (5) when p + Pe- It is thus safe to ensure (Pe) a. This is done by carefully selecting s.t. the a-qquantle of the r.v. I(m, N) equals log Pe- The routine Comp_m in Alg. solves this numerically with a line search (see Appendix for some approximations). O
If assume Bayesian approach where the p.d.f. of p is denoted by fr :0,0 - R,, then the probability of not being sound is given by
Pc f (1 Pta(p))fr(()pp L [ (
Sound) Sound)
(11)
pe Jm fr(p)dp + S = a++
<
pc).
(12)
The lack of soundness decreases if both a and Pe are small. This makes the point with the state-of- the-art. [Baluta et al.] [202T) are unable set Pa low value because their simulation is based on crude Monte Carlo, whereas Webb et al. [2019] do not give any guarantee similar to our level a.
Efficiency Appendix A proposes approximated closed forms outlningg that m scales as log l/Pc. This is also visible in the typical values given in Table A lower significance level moderately increases the number iterations. Dection[dettall how to sample a new particle at each iteration as needed in line I1 Alg. [ This method consumes a fixed number of calls to the network. In total, the maximum number of calls scales as O(log 1/p.). This in stark contrast with [Baluta al. 2021] where the number of calls is proportional to 1/p.- Note that this is a maximum: our procedure makes an early stop whenever Tak > 0 (line Alg. and outputs Cert. False as well as failure
probability estimate Pest-
5

---

Table 1: Maximum number of iterations m and its approximation mn (see App. A
N
Pe
Ot
0.1
Ct = 0.01
= 0.001
m72
m
m1
m
20
10
489
489
512
514
529
532
20
10 30
1430
1431
1470
1471
1499
1502
10
10-10
251
251
267
269
280
283
10
10 30
726
726
754
755
774
777
10
56
56
64
65
69
73
2 10
154
155
167
169
177
180
4
Sampling procedures
This section details the crucial ingredient of our procedure: sampling a new input whose score h(X) above given level L. This random generator called Gen(L, , 1) in line Alg. | considers a case where the statistical model To and the network are so simple that this sampling is easy. This section details more general scenarios making no assumption about the score function. Our sampling is rejection procedure relying on reversible proposals and transformations.
Appendix B
4.1 Reversible proposals
We call a (parametric) proposal any random function K proposal generate a Markov chain which said to be reversible (detailed balance) with respect to the distribution if the following assertion holds:
X R. R". Iterations of i.i.d.
Vs > 0, X ~
(X))( ~ (K(X, X).
(13)
simple example for To = NO,,, o II,) is given in |uuyader et al. 2011
K K(X, X+ sN with
(14)
VI+
The rejection method described in Alg. 2 takes as input set X' of particles whose score is larger than L. It ramdomly picks one particle in X' and applies t times a fresh proposal, followed by rejection based on the score. the selected sample larger than L. then one application of the proposal keeps invariant while the rejection ensures that the score remains above By induction, iterating maintains these two properties, and in fact leaves invariant the conditional distribution thanks reversibility (see [Guyader et al., 2011 and App. E).
realization of the distribution To conditioned by score
Alg. | Juses the procedure of Alg. 2 as follows. At iteration k. is indeed La. i.e. the score of the "last' particle x,,, and X = {x, hight which contains (N - 1) particles whose score is larger than L. The output is 'fresh' particle and the number of particles equals N from one iteration another.
The parameter s plays the role of strength: s = implies that the proposal just copies the input, while s - +000 means that K (x, s) does not depend on The proposal strength is thus important. With a small value, the proposal makes small moves. A large value explores faster but leads to higher rejection rate. Appendix [D] presents a strategy to automatically control its value depending on the past behavior of the algorithm in order to maintain a given rejection rate.
Theoretically, under some irreducibility assumption, infinity of iterations in Alg. provides fresh particle statistically independent of the particles in as needed in Alg.
Proposition 4. Assume that, the proposal K(x, 8) has a density bounded from from below uniformly in x and Z 8q- Then the distribution of A (T.m) converges towards the Gamma distribution (NN, exponentially fast with the number of proposal applications.
Proof and Remarks. The proof is given in Appendix and uses a classical probabilistic coupling argument. It requires the lower bound assumption which is form of strong irreducibility of the proposal. This is compliant with the proposals used in this work. particular all the formulas given in Prop. and after hold true asymptotically for large t.

---

Algorithm 2 Sampling one particle Gen(L,1) 1)
Require: threshold L, finite set X of particles whose score is larger than L Ensure: new particle X
1: X < (())
Draw uniformly particle in X'
2: for == 11:dd
3:
Z ((X,s)
mo reversible proposal.
See Sect. 4.1 > Reeeection
4:
if hZ)) > then
5:
X - z
6:
end if
7:
end for
8: return X
In practice, we choose the number of iterations approximately proportional to the inverse of rejection rate, maintained approximately constant by tuning the proposal strength (see App. DD.
Refreshing a particle consumes calls to the score function. This is done once per iteration of Alg. Therefore, our method globally consumes Ol log 1/P.) calls. This means that the figures in Table are to be multiplied by 4. [eebb et al. [2199] also manage sample of size N, but all the particles are separately refreshed at each iteration by applying Metropolis-Hastin
transitions. Their number of calls per iteration is N times larger than our. Moreover, their typical setup is N s 1000 and t 1000, while ours is N x 2 and 50. Our complexity is thus smaller by 4 orders of magnitude.
4.2 Isoprobabilistic transformation
The proposal (14) is simple but reversible only w.r.t. the normal distribution. The transformation method is well known in the field of Statistical Reliability Engineering [Melchers and Beck 2018). It amounts to work with a latent random vector G ~ (O,: La) and to apply the transformation X TGG, x.) mapping the normal distribution to the reference model To. Some well known examples are:
Nxxo: II)::: d = n and T(G, x,) = xx + oG
X ~ U (B+oo,c (xo)): d and 7(G, X.)
((20-1(()) 1) (component-wise)
X Lx(, (x.)): d + 2 and TG, = =x, eG (((1:)).)) G
More complex examples are inverse Rosenblatt or Nataf transformations Melchers and Beck 2018
This transformation is composed with h to redefine the score function hG = h T that applies on latent vector G, i.e. random vectors suitable for the proposal (14). This amounts to use Alg. [ directly on the latent variable with score function hg and in conjunction with Alg. 2 and proposal
[4]
5 Experimental evaluation
This section presents experimental results on ACAS Xu, MNIST, and ImageNet datasets with some trained classifications networks listed in App. F3 were run on a laptop PC (CPU=Intel(R) CTr)(TM) 17-9750H, GPU=GeForce RTX 2070) except for experiences on ImageNet which were run Nvidia V100 GPU.
together with implementation details. Experiences
5.1 Idealized case
This section considers a setup where To -N(x;; o2I,) and score function is linear. This setup is ideal because sampling fresh particle is straightforward (i.e. without Alg. 2) shown in App.
Fig. shows the impact of N. In terms of hypothesis testing (see Sect. 3.2 a larger N yields steeper functions: (p) (resp. Pmn (p)) quickly vanishes to zero as gets larger (resp. smaller) than Pe- In terms of certification (see Sect. 3.3). ) a small is not a bad choice: the probability (ns(p) of not being sound takes lower values in the range p Pe. For Pe, (ns(p) is lower than (as stated by Prop- 3 but converges to more slowly. Last but not least, the procedure makes only 167 calls the
score function for N 2, instead of 1470 for N 20.

---

Table 2: ACAS Xu Confusion matrix comparing ERAN [DeepPoly+MiLL]] and Last Particle [N = Pr. = 10 t 40]
ERAN
Certified
Uncertified
Infeasible
TimeOut
Certified
107
9
Last Particle
Uncertified
103
0
5.2 ACAS Xu
We evaluate our method on the ACAS Xu (Airborne Collision Avoidance System X for unmanned aircrafts) case study [Owen al. 2019]. consists in 45 neural networks used approximately compress a large lookup table (2GB) containing discrete decisions ('Clearof-coonlicts, 'weak right', 'strong right', week left', 'strong left') as well input/output properties. This makes 45 225 cases. We compare our method with the complete certification based on DeepPoly (Singh et al. 2019] and Mixed-Integer Programming from the ERAN benchmark.
Table 2 contains the confusion matrix taking into account the cases for which the ERAN complete certification fails because the Gurobi optimizer either outputs 'infeasible' status reaches timeout (set to 600 seconds). Unsurprisingly, our method is complete in the sense that it certifies all cases certified by ERAN. It is not sound as it admits 9 false positives. This is due the critical probability Pe which is not low enough (the decisions were exactly the same over 10 runs). Yet, our method takes decision on the unsolved cases by ERAN. In addition our method faster for all ACAS Xu properties except for the property 4, confer figure
5.3 MNIST
We compare our procedure with with the DeepPoly incomplete certification on MNIST [LeCun et al., 1990] with 4 neural networks from the ERAN benchmark (see App. F3). We focus on Lx uniform robustness since the implementation provided for DeepPoly cannot deal with L-2 norms. We run our algorithm with N = 2. Pc 10- and 40. As in ACAS Xu experiment, our method runs faster than the ERAN method as shown table Interestingly, the average runtime of our method decreases with larger since the probability p of violation is bigger, whereas DeepPoly computation time increases with the size of the input space tested. On the one hand DeepPoly provides an efficient lower bound to both corruption and adversarial robustness, on the other hand our method provides simulations (runs) on the same image always give the same
fast upper bound. 10 independent output and the standard deviation is thus empirically negligible in our setting.
N
N 20
Estimated probabilities in log
-2
Prn(p) Pip(P)
-2
(n)(p)
-3
36
34
32
30
-36
-34
32
-30
log.v(p)
log10 (p)
Figure 1: Estimated probabilities false positive, false negative, and not sound certification, vs. true 0.01. Estimation over 1000 runs.
violation probability in the ideal setup where P. 10 30

---

Table 3: MNIST Comparison ERAN [DeepPoly] and Last Particle [N P. - 10 10-35, - 40)
35,1
ERAN
Last Particle
Certified (%)
runtime (sec.)
Certified (%)
runtime (sec.)
0.015
82
5.69
99
1.04 = 0.005
0.03
62
5.92
97
1.03 + 0.01
0.06
28
8.13
93
1.00 + 0.01
0.1
22
8.84
85
0.96 + 0.02
Table 4: ImageNet- Last Particle [N
2,P: = 10-15 = 20]
Network
Avg. runtime (in sec. =std)
Avg. number of calls
Certified (%)
0.02
20.78 = 0.74
1388
71
MobileNet
0.03
18.74 = 0.18
1274
64
0.06
14.5 + 0.11
1037
50
0.02
33.86 = 1.14
1537
81
ResNet50
0.03
31.38 = 0.48
1434
71
0.06
25.51 + 0.67
1160
59
ImageNet
For the last experiment, our method analyses 2 neural networks (ResNet50 et MobileNet) with 100 test images from ImageNet dataset (Deng et al. 2009) correctly classified by each network. These experiments were run on Nvida V100 GPU. The average number of calls reported is rounded up and the average runtime is for pass over one image. The robustness is again defined against noise uniformly distributed over Toxe radius e. As one can notice, the compute time increases reasonably the input space dimension and network size.
Conclusion
The paper proposes statistical simulation to make assessment corruption robustness. It looks this problem from a hypothesis testing (false positive/ false negative) and from a certification (completeness/ / soundness) points of view. The procedure is scalable, efficient, complete and comes with guarantees on the lack of soundness. There are two limitations: 1) The Last Particle simulation is sequential, which is not GPU friendly. Yet, we provide code processing several inputs x. in parallel. 2) Our procedure is general as uses the network as a black-box classifier. But, it does not exploit its gradient easily computed thanks to backpropagation. More sophisticated mixing kernels using gradients information (e.g. Langevin Monte Carlo, Hamiltonian MC) can accelerate convergence.
Average runtime
Last Particle ERAN
20
10
0
3
5
All
ACAS Xu property id
Figure ACAS Xu runtimes in sec. of ERAN (Deep Zonotope) and Last Particle algorithm [N = 2,p. = 10-50 - 40]

---

Acknowledgement and Disclosure of Funding We thank Arnaud Guyader for fruitful discussions. This work funded by ANR/AID Chaire SAIDA. KT gratefully acknowledges PhD funding via grant from the AID (Agence pour I'Innovation de Défense). In addition we thank the reviewers for their detailed and relevant comments.
Broader Impact
As deep learning applications move to the physical world it is crucial to understand to what extent and in which situations their predictions can be trusted. Both adversarial and corruption robustness assessment methods are key step towards building trustworthy deep-learning based cyber-physke systems. At the same time limits such methods should always be clearly established and their dependence on data explicit.
References
Justin Gilmer, Nicolas Ford, Nicholas Carlini, and Ekin Cubuk. Adversarial examples natural consequence of test error in noise. In Kamalika Chaudhuri and Ruslan Salakhutdinov, editors, Proceedings of the 36th International Conference Machine Learning, volume 97 of Proceedings of Machine Learning Research, pages 2280 2289.. PMLR, 09-15 Jun 2019. URL http://
proceedings mlr wwwpppssssseeppp mealmmee1aa... html
Oves Franceschi, Alhussein Fawzi, and Omar Fawzi. Robustness of classifiers uniform Ep and gaussian noise. In Amos Storkey and Fernando Perez-Cruz, editors, Proceedings of the Twenty-First International Conference on Artificial Intelligence and Statistics, volume 84 of Proceedings of Machine Learning Research, pages 1280 1280-1288. PMLR, 09-11 Apr 2018. URL httt://prroceedings mlr. wwwpppresssvee v vrress//84/fraacecchh franceschi 18a. html
Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin Vechev. Fast and effective robustness certification. In S. Bengio, H. Wallach, H. Larochelle, K. Grauman, N. Cesa- Bianchi, and R. Garnett, editors, Advances in Neural Information Processing Systems, volume 31. Curran Associates, Inc., 2018. URLhtttps: http:///pooceeeig..../ new. httpppscceeppppr////////li 12F44598d88s711ff3d5777 089481c3 -3 pdf
Stefan Webb, Tom Rainforth, Yee Whye Teh, and M Pawan Kumar. A statistical approach to assessing neural network robustness. In International Conference Learning Representations, 2019.
Guy Katz, Clark Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. Reluplex: An efficient SMT solver for verifying deep neural networks. In Rupak Majumdar and Viktor Kunčak, editors, Computer Aided Verification, pages 97-117, Cham, 2017. Springer International Publishing. ISBN 978-3-319-63387-- URL httttttss///iiiiii www.riivv.orggaaao abs/ 1////331..66
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. An abstract domain for certifying neural networks. Proc. ACM Program. Lang., 3(PPL)), January 2019. doi: 10.1145/ 3290354. URL https:://oi..rg 10.
Lily Weng, Huan Zhang, Hongge Chen, Zhao Song. Cho-Jui Hsich, Luca Daniel, Duane Boning, and Inderjit Dhillon. Towards fast computation certified robustness for ReLU networks. In Jennifer Dy and Andreas Krause, editors, Proceedings of the 35th International Conference Machine Learning, volume 80 of Proceedings of Machine Learning Research, pages 5276-5285. PMLR, 10-15 Jul 2018. htt:
mlr www.pprssssseee /weess//vO//e htt.://wgg1.....rc.. html
Huan Zhang, Tsui- Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel. Efficient neural network robustness certification with general activation functions. In Advances in Neural Information Processing Systems (NuerIPS), dec 2018.
Akhilan Boopathy, Tsui-Wei Weng. Pin- Eu Chen, Sijia Liu, and Luca Daniel. CNN-Cert: An efficient framework for certifying robustness of convolutional neural networks. In AAAI, Jan 2019.
Lily Weng, Pin-Ya Yu Chen, Lam Nguyen, Mark Squillante, Akhilan Boopathy, Ivan Oseledets, and Luca Daniel. PROVEN: Verifying robustness of neural networks with a probabilistic approach. In Proceedings of the 36th International Conference Machine Learning, volume 97 of Proceedings
10

---

of Machine Learning Research, pages 6737-6736. PMLR, 09-15 Jun 2019. URL http:// proceedings mlr. wwm.m.rrppee.. wwt.s..ress/v9///// https//////wngg1aa..b html
Hadi Salman, Greg Yang, Huan Zhang, Cho-Jui Hsieh, and Pengchuan Zhang. A convex relax- ation barrier to tight robustness verification of neural networks. In H. Wallach, H. Larochelle, A. Beygelzimer, Alché-Buc, Fox, and R. Gamett, editors, Advances in Neural Information Processing Systems, volume 32. Curran Associates, Inc., 2019. URL wwwfffeffffaaaaa
neurips wttpp/pppp/p.//////epp /ttp:////55554444eeeffffffffee
Paper. pdf
Teodora Baluta, Zheng Leong Chua, Kuldeep S. Meel, and Prateek Saxena. Scalable quantitative verification for deep neural networks. In Proc. Int. Conf. on Software Engineering, 2021.
Christian Naesseth, Fredrik Lindsten, and Thomas B. Schön. Elements of sequential monte carlo. Foundations and Trends in Machine Learning. 12(3):307-3922 2019. ISSN 1935-8237. doi: 10.1561/22000000074, http: doi org. 156122000000744
Arnaud Guyader, Nicolas Hengartner, and E. Matzner-Lpher. Simulation and estimation of extreme quantiles and extreme probabilities. Applied Mathematics & Optimization, 64:171-196, 10 2011. doi: 10.10077:000245-01-91333
Robert E Melchers and André T Beck. Structural reliability analysis and prediction. John wiley & sons, 2018.
Michael Owen, Adam Panken, Robert Moss, Luis Alvarez, and Charles Leeper. ACAS Xu: Integrated collision avoidance and detect and avoid capability for UAS. In 2019 IEEF/AIAA 38th Digital Avionics Systems Conference (DASC), pages 1-10, 2019. doi: 10.1099DASCC4569.00 2019. 9081758.
Yann LeCun, Bernhard Boser, John Denker, Donnie Henderson, R. Howard, Wayne Hub- bard, and Lawrence Jackel. Handwritten digit recognition with a back-propagation net- work. In D. Touretzky, editor, Advances in Neural Information Processing Systems, volume 2. Morgan- Kaufmann, 1990. URL lattps://procedddnn www.igs.neuiiss.. http:/eeee..s.c.epppae////// cc/pppee//189/ffile/ bccbbe6eebbee
pdf
J. Deng, K. Li, M. Do, H. Su, and L. Fei-Fei. Construction and Analysis of a Large Scale Image Ontology. Vision Sciences Society, 2009.
Martin Hairer and Jonathan C Mattingly. Yet another look at harris' ergodic theorem for markov chains. In Seminar Stochastic Analysis, Random Fields and Applications VI, pages 109-117. Springer, 2011.


Reviews:
[{"review_id": "xM1xLcOlFEH", "reviewer": "Reviewer_AB2m", "summary": "This paper provides a method to assess the robustness of a given neural network by checking the stability of the performance of the network around the neighborhood of a given input. Broadly speaking, if a given network is robust, then it is expected to be invariant under certain perturbations of every input.\nSpecifically, the authors assume that the input satisfies a specific probability distribution beforehand, and then they apply the so called ”last particle” algorithm to compute probability that whether the network at a given input is certified to violate the robustness assumption or not through the hypothesis testing.\nFinally, they do experiments on three public datasets: ACAS Xu, MNIST, and ImageNet. By comparing the results with DeepPoly [Singh et al.,2019] and Mixed- Integer Programming from the ERAN benchmark, the authors show that their method can be more efficient and have lower false positive rates.", "questions": "", "limitations": "", "rating": 5, "confidence": 4, "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": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "Features:\nThis paper provides an approach using statistical hypothesis testing as a surrogate of certification process, which is not an new idea. Basically, it can be seen as combining the works from [Baluta et al.,2021], [Webb et al.,2019], [Singh et al.,2019], [Weng et al.,2018], [Zhang et al., 2018], and so forth. Specifically, [Baluta et al.,2021] and [Webb et al.,2019] study the robustness of a network by Statistical assessments and [Singh et al.,2019], [Weng et al.,2018], and [Zhang et al., 2018] verify the robustness of the network by some incomplete certification processes. That means, their methods does not certify the network to be non-robust whenever it violates the robustness assumption.\n\nIn this paper, the authors improve the efficiency of the statistical assessments of neural networks by replacing the crude Monte Carlo and adaptive multi-level sampling in [Baluta et al.,2021] and [Webb et al.,2019], respectively by the ‘Last Particle’ simulation invented by [Guyader et al.,2011]. Moreover, they reduce the incompleteness of the certification processes of the works from [Singh et al.,2019], [Weng et al.,2018], [Zhang et al., 2018], and so forth in Proposition 3 by controlling the significance level and the critical probability for the hypothesis testing to be small.\n\nIn overall, I feel that this paper is well written and clearly pointing out the gaps between previous works from other researchers and states their improvements combined with theoretical guarantees.  From a theoretical perspective, the paper is promising.\n\nLimitation: The method is not practical.\n1. The method seems extremely time consuming (the empirical evaluation is for TWO datapoints!!).\n2. The method seems to be even more consuming beyond Gaussian input; in any case, there are no simulations provided for that case.\n3. The input distribution needs to be known beforehand.\n4. t and pc are changed from one application to another, meaning that they are tuning parameters. But there is no insight into how these parameters should be chosen in practice (other than making the results look as good as possible...).\nAnd it seems that the method is not directly related to any practical method either.\n\nHence, while the theory is potentially interesting, it is not clear why we should be interested in that theory in the first place. ", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "Yes.", "review_text": "", "extra_scores": {"ethical_concerns": "No.", "needs_ethics_review": "No", "ethics_review_area": "", "time_spent_reviewing": "4"}, "extra_text": {}}, {"review_id": "kpvw-DE_Ej", "reviewer": "Reviewer_kvKQ", "summary": "Summary: In this work, the authors propose a “sound” method for checking local, distributional robustness properties of neural networks. The authors carefully construct a hypothesis testing framework and do a good job at providing clear exposition of their framework. The authors also provide this method with clearly stated sampling procedure/last particle simulation. The authors validate their framework by providing statistical verification of Acas Xu, MNIST, and ImageNet. Though they only consider 5 test images from ImageNet and fail to realize their “soundness” on Acas Xu. ", "questions": "", "limitations": "", "rating": 5, "confidence": 4, "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": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "Summary Pros:\n\nThe writing of the paper is very clear and the authors are studying the important problem of robustness, albeit not “adversarial” robustness necessarily. \n\nThe exposition of soundness and completeness is correct and clear, despite the fact that I disagree with deeming this method “sound” \n\nThe authors have an experimental section which is a promising start to validation of their methodology.  \n\nSummary Cons:\n\nOne of my major criticism is that, ultimately, this paper proposes to use a hypothesis testing (or statistical model checking depending on what community you’re from) approach for “certifying” distributional robustness. Unfortunately, claiming soundness is a bit of an over-claim considering this is a machine learning community. The authors establish a statistical guarantee on par with works such as smoothing; however, those who work in smoothing never claim soundness as having confidence intervals is fundamentally different to the kind of guarantee given by methods such as bound propagation. Further on this point, this kind of soundness is controllable by other approaches, specifically [1], by simply considering a standard concentration inequality or even a sequential bound such as established in [2], so while it is a technical improvement as the authors of [1] do not explore the confidence intervals of their method, it feels like a relatively minor one unless the authors can perform more experiments and compare the convergence of $\\alpha$ under their assumptions to concentration bounds (which they will best handily) and sequential bounds without the need for such complicated sampling procedures (which it is less clear they will best).\n\nI think the paper needs strengthening both in terms of its motivation and empirical validation. One of the appeals of SMT and Abstract Interpretation frameworks is their ability to be sound (and practically complete in the case of SMT), but of course these methods do not scale. The appeal of statistical guarantees on robustness is that they scale to the likes of ImageNet despite not generally being sound against adversarial examples ([3,4] do have such guarantees). This method, on the other hand, does not have the same soundness or completeness as SMT or bound propagation techniques and is therefore poorly positioned for safety verification and does not have (or at least is not empirically demonstrated to have) the scalability of statistical methods. \n\n\n[1] - https://arxiv.org/pdf/1811.07209.pdf\n[2] - https://dl.acm.org/doi/fullHtml/10.1145/3310226\n[3] - https://arxiv.org/abs/1902.02918\n[4] - https://arxiv.org/pdf/1903.01980.pdf", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "Yes, the authors have adequately addressed this.", "review_text": "", "extra_scores": {"ethical_concerns": "I have no ethical concerns about this paper.", "needs_ethics_review": "No", "ethics_review_area": "", "time_spent_reviewing": "2-3 hours"}, "extra_text": {}}, {"review_id": "75mwLa-RHrq", "reviewer": "Reviewer_YGbw", "summary": "This paper considers the computation of probabilistic, or corruption robustness of a neural network. This is achieved through an adaptation of a rare-event sampling scheme previously proposed for computing corruption robustness. The main contribution is the derivation of finite-sample theoretical guarantees on the probability of violation, in particular, whether it is equal to or greater than zero. ", "questions": "", "limitations": "", "rating": 3, "confidence": 4, "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": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "One of my major concerns with the paper is that the property to be certified is not formally stated, nor clearly motivated. As a result, it is difficult to assess the contribution. \n\nMy understanding is that it concerns “whether the probability $p$ of violation is zero, or greater than zero”. This is distinct from the usual definition in adversarial robustness (“whether there exists a violation in the region”), as it is in theory possible that there are violations but they have probability zero, yet the paper seems to conflate these notions throughout. Notions like “soundness” and “completeness” are not formally defined either. It would greatly benefit the paper if the authors precisely state what the property is in the Introduction (which currently almost exclusively focuses on related/previous work, instead of the novel contributions and approach of the paper), and at the beginning of Section 3.\n\nIt is also not clear to me, from the paper, what the motivation of certifying whether $p > 0$ is. Previous works such as (Baluta et al. 2021) and (Webb et al. 2019) motivate corruption robustness as a means of quantitatively assessing how robust a DNN is, and ensuring this is sufficiently small. On the other hand, the paper appears to primarily compare to formal adversarial certification methods (e.g. DeepPoly), on the grounds that such methods are sound but not complete, while the paper’s method is complete but not sound. Aside from the issues with the property definition (see above), in this case why do the authors not compare to empirical attacks like PGD, for instance in the experiments in Section 5.2/5.3? In Line 47 the authors suggest that PGD is not complete or sound, but this is not true. PGD is complete, since it will not find an adversarial example (i.e. it will output Cert=True) if one does not exist (i.e. property holds). **AR**: Unfortunately I am still not convinced, in light of the authors' response, that there is a strong case for certifying whether p > 0 using statistical methods. Without soundness, it is doubtful to what extent this can be considered a \"certification\" method, as empirical PGD attacks perform much the same function, and though they do not come with guarantees on false positives, they would likely be more effective in finding adversarial examples when they do exist since they make use of gradients (e.g. consider Table 2 w/ PGD). That said, I agree with the need to provide guarantees (such as those established in Prop 1 and 2) for statistical robustness assessment, and applaud the authors' promising work towards this goal.\n\nThe paper adapts the splitting-based estimation methodology introduced by (Webb et al. 2019) for corruption robustness, in order to improve efficiency and to be able to compute guarantees. To achieve this, they use the “Last Particle” variant introduced by (Guyader et al. 2011), which resamples just a single particle at each level rather than a proportion of them. \n\nThe main novelty appears to be the derivation of guarantees for the hypothesis test (Proposition 1 and 2), which enables guarantees on the soundness. This is very nice and backed-up in the idealized case by Section 5.1. However, in practice, Algorithm 2 is used, which does not guarantee independence of samples given finite iterations (as acknowledged in Section 4). This compromises the non-asymptotic guarantees claimed by the paper. It would be useful to examine with an experiment how much of a problem this is in practice.  At the very least, it should be clearly stated at the beginning of the paper that the guarantees only hold in the idealized case.\n\nRegarding the efficiency of the procedure, it is good to see that it can scale to ImageNet. Given the similarity to the AMLS used by (Webb et al. 2019), it would be good to see an experimental comparison of the efficiency of the schemes in practice for DNNs. It is argued in lines 208-211 that the paper’s method is 4 orders of magnitude faster, but I think this is overstated because AMLS sets the new level $L_k$ at each iteration $k$ using the score of the particle at the cut-off quantile, meaning that the level increases more quickly per iteration. **AR**: I appreciate the authors' argument that their method (with the specific choice of hyperparameters K = 1, N = 2, M = 100) is orders of magnitude faster than Webb et al. However, as the authors note, these choices are inherently linked to the quality of the approximation to the idealized algorithm. By choosing to only maintain 2 particles, though computational speed is gained, the approximation becomes coarser. Careful theoretical or empirical analysis/comparison of the tradeoffs for neural network robustness would be an very interesting contribution, however as-is I do not believe the paper's justification is sufficient.\n\nIn summary, the paper makes some nice contributions to extending corruption robustness methodology, albeit not particularly novel. However, I have serious concerns over the motivation of the certification problem, the clarity of the paper, and the lack of important experimental evaluations to justify the approach. **AR**: In light of the author response, I will keep my score. The paper identifies and attempts to tackle the important problem of how to compute statistical robustness efficiently for neural networks, with guarantees. However, given the prior work of Webb et al., there is insufficient theoretical and/or empirical justification for the paper's approach, in particular, the quality of the approximation, and its impact on the claimed guarantees. \n", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "I would suggest that the authors make it clearer that the guarantees for their method only hold in the idealized case, and not with e.g. Algorithm 2. ", "review_text": "", "extra_scores": {"needs_ethics_review": "No", "ethics_review_area": "", "time_spent_reviewing": "12"}, "extra_text": {}}]

Author rebuttal:

Meta-review: This paper covers the interesting topic of how to efficiently estimate statistical robustness in deep neural networks with accompanying theoretical results about performance.  

However, the reviewers have highlighted a number of shortfalls in the work, such as not making a sufficiently strong case for itself in its underlying motivations; issues with the experimental evaluations and, in particular, the comparisons made to previous approaches; the practicality of the approach; and the general level of advancement compared to previous work (particularly that of Webb et al 2019 and Baluta et al 2021).  In light of these, all the reviewers and I agree that the paper is not currently ready for publication in its current form.

On a separate point of note that did not affect the decision-making process for the paper but might be of interest to the authors: there is actually a recently published follow-up work to Webb et al 2019 that I don't think was mentioned by the reviewers and is not cited in the submission, but seems to be quite relevant:

Statistically Robust Neural Network Classification. Wang et al. UAI 2021.
Decision: Accept (Poster)