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))=((dd)
(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() > 0).
Our approach establishes hypothesis test parametrized by a low probability Pe given by the user.
Ho: 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 Jo tme-ldt
log t e -tt
7(m, - N log
Ptn = P(Cert = Falselp < pc)
(6)
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.
Pas(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 a 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 mellmmee1aa... 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/fraaceechh 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. 089481c3 -3 pdf 12F44598d88s711ff3d5777
http:///pooceeeig..../ new. httpppsccccppppr////////li
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 wwweriivv.orggaaa 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.://wgg8.....rm.. 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//////wngggaa..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 wwwfffefffaaaaaa
neurips wttpp/pppp/p./////eeppp /ttp:////5.554444eeeffffffffeee
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://proceeddnn www.igs.neuiiss.. http:/etee..s...epppae////// cc/pppeer/189/ffile/ bccbbeeeebbee
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": "teYjS1ce9BW", "reviewer": "Reviewer_Lats", "summary": "The paper approaches the problem of the robustness assessment of neural networks. To be more precise, it focuses on the corruption robustness, which considers the modification of inputs with random noise instead of adversarial attacks. The main question here is to estimate the probability of the correct classification for the given network and noise model. \n\nThe main development of the paper is the application of the algorithm proposed in (Guyader, 2011) to the robustness estimation. The algorithm iteratively updates a set of particles by simultaneously sampling from the given distribution (noise distribution in this case) and maximizing the target function. For the target function, the authors consider the classification error. Then, using Theorem 1 from (Guyader, 2011) the authors estimate the probability of false classification and certify whether this probability is below the user-specified threshold. \n\n\n(Guyader, 2011) Guyader, Arnaud, Nicolas Hengartner, and Eric Matzner-Løber. \"Simulation and estimation of extreme quantiles and extreme probabilities.\" Applied Mathematics & Optimization 64, no. 2 (2011): 171-196.", "questions": "", "limitations": "", "rating": 7, "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": "Overall the proposed scheme sounds very reasonable and technically developed. To the best of my knowledge, the scheme is novel, although I might be unfamiliar with some of the relevant works. A surprising outcome of the provided analysis is that a lesser number of particles yields a better estimation of the error probability. This can be explained by the growing variance of the target function estimate, which assigns more probability mass to high values. Since we are interested in the quantiles around high values, the high variance is favorable. However, to perform the analysis the authors approximate Gamma distribution with the Gaussian using the central limit theorem. Since the tails analysis is important for this application I would expect a more careful study or some discussion of this phenomenon at least.\n\nUnfortunately, the empirical study is a weak point of this paper. As I understand the target application, the algorithm should be tested for the certification error and for the running time. The authors provide the certification error for the ACAS Xu dataset in Table 2 but do not provide the running times for this dataset. For MNIST, the proposed algorithm runs faster than the competitor, but falsely certifies some networks as robust, hence, making errors. Thus, no clear conclusion can be made in terms of the overall performance (both running time and accuracy). Finally, for ImageNet, the authors do not compare against other algorithms at all. For both ImageNet and MNIST the authors test their algorithm on 5 images. I wonder why such a small number of images has been considered, especially when the algorithm runs quickly even on a laptop (as claimed by the authors).\n\nI think the lack of systematic comparison against other algorithms (from different approaches outlined in the introduction) is a significant flaw of the paper. This comparison has to be done even if it's obvious that the proposed algorithm has better properties. For instance, I can imagine that the considered task is simple enough that an adversarial attack via gradient descent can find a counter-example whenever it is possible. Such a baseline would hint readers what to use and what to try in their concrete example.", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "The authors motivate the proposed algorithm by military applications in the introduction. They also provide the empirical study on the \"Airborne Collision Avoidance System X for unmanned aircrafts\" dataset. I think the Broader Impact section is incomplete without the discussion of these applications.", "review_text": "", "extra_scores": {"needs_ethics_review": "No", "ethics_review_area": "", "time_spent_reviewing": "4"}, "extra_text": {}}, {"review_id": "Z43dFiJ_7oi", "reviewer": "Reviewer_K7DT", "summary": "The paper studies (instance-wise) certification for Deep Neural Networks. Quantitatively, this metric can be defined as an integral, and the common computational approach is using Monte Carlo simulation. \n\nThe authors consider using statistical hypothesis testing as a surrogate of certification, and the key contribution is a more efficient sequential Monte Carlo algorithm. The theoretical guarantees of the proposed algorithm are by bounding the False Positive Rate and False Negative Rate. The theoretical results (Prop 1 to Prop 4) rely on the property of the Last Particle simulation, which is presented in Theorem 1.\n\nThe authors also demonstrate the efficiency and scalability of their algorithm.", "questions": "", "limitations": "", "rating": 5, "confidence": 3, "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": "The workhorse of the paper is a more efficient sequential Monte Carlo algorithm by using the last particle simulation. Both the algorithm and the theoretical analysis strongly rely on previous work. The algorithm improves the crude Monte Carlo simulation by using the Last Particle simulation. In the context of certification, the theoretical results are derived by simply bounding the False Positive Rate and False Negative Rate. It seems that the contribution of this work is incremental compared to previously known results.", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "Yes, the authors mentioned that the Last Particle simulation is sequential, which is not GPU friendly.", "review_text": "", "extra_scores": {"ethical_concerns": "NA", "needs_ethics_review": "No", "ethics_review_area": "", "time_spent_reviewing": "10"}, "extra_text": {}}, {"review_id": "3bH4qKQC8_", "reviewer": "Reviewer_Aovq", "summary": "The authors provide a novel way of accessing neural network robustness. In the classification by [Singh et al., 2018] they provide a method that is complete, but not sound. In other words, their method is guaranteed to certify the model if it satisfies the property, but is capable of producing False Positives - e.g. models that do not satisfy the property can be certified. The derived method is based on statistical hypothesis testing - rather than looking at worst case scenarios, which is done often, they look at the probability of violation of the property over a density of perturbations. The core part of the method is the Last Particle algorithm, invented by [Guyader et al. [2011]], which come with a theorem that states the distribution of its output. This provides the mathematical framework needed to perform a hypothesis testing given a run of the algorithm. The authors demonstrate with several propositions, proved in the Appendices, how the critical probability p_c and the significant level \\alpha affect the power of the test (it basically produces less False Positives as \\alpha and p_c decrease). In addition the authors demonstrate that the proposed method scales logarithmically in the number of calls needed, which is in contrast to other approaches in literature that have linear dependence. Several empirical experiments validate the claims and showcase that indeed the method provides a computationally efficient method, with very good results.", "questions": "", "limitations": "", "rating": 7, "confidence": 3, "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": "The paper is written really good and is easy to follow with clear narrative, proposed method and experimental results. \nUnfortunately, I'm not too familiar with this area of research, hence I can not comment on how well do the authors present or omit any other competitive approaches. \nI think the comparison with ERAN on the simpler problems indeed show very significant promise for this method to be practically applicable. In fact potential combination with the sound solvers, provides both an upper and lower bound on the number of certifications, which can be useful in practice. ", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "As indicated by the authors, the two major limitations are the fact that the method is not parallelizable and does not make any use of model information (in the form of gradients or anything else). I think I would have liked them to provide some more detailed discussion on how this can be extended in the future, or if why there are fundamental blocks to it. For instance one can run multiple chains of the proposed algorithm in parallel, which would provide multiple draws from the same distribution and potentially these could be combined to improve the confidence level bound (though this is speculation, have not actually tried to prove this). In addition, the proposal distributions for resampling the new point seem relatively simple. Since they are looking for a MC that has as invariant distribution \\pi_0, I wonder why they have not even discussed any more sophisticated MCMC methods (or why those would not be applicable to this problem). \n\nFinally, the ImageNet experiments seem a bit small - only 5 test images? Given that this runs on a laptop for 30sec per image, you could have run this over 1500 images per day (and this assuming you only have a single laptop!). I would like to see here a significantly broader evaluation, and with access to even several computers you can probably run this on the whole ImageNet test set. Also there is no comment on running ERAN on that example - how expensive is it or does it always reach infeasible results? From the results on MNIST it seems that it is an order of magnitude slower, but if that implies 30 minutes per image, this is still something that you can definitely run and show us the results. ", "review_text": "", "extra_scores": {"ethical_concerns": "N/A", "needs_ethics_review": "No", "ethics_review_area": "", "time_spent_reviewing": "2"}, "extra_text": {}}]

Author rebuttal:

Meta-review: This paper uses a hypothesis testing based approach to provide a statistical assessment of corruption robustness, with a scalable MC-based computational approach. 

The authors have made an impressive effort to address the concerns of the reviewers. Though not all the concerns are fully addressed, the emerging consensus is that the additional comments, clarifications, and also experiments, have satisfactorily addressed many of the concerns raised. 
Decision: Accept (Poster)