Fast Geometric Projections for Local Robustness Certification
Authors: Aymeric Fromherz
Klas Leino
Matt Fredrikson
Bryan Parno
Corina Pasareanu
Venue: ICLR 2021 Spotlight (2021)
Keywords: verification
robustness
safety

Abstract: Local robustness ensures that a model classifies all inputs within an $\ell_p$-ball consistently, which precludes various forms of adversarial inputs.
In this paper, we present a fast procedure for checking local robustness in feed-forward neural networks with piecewise-linear activation functions.
Such networks partition the input space into a set of convex polyhedral regions in which the network’s behavior is linear; 
hence, a systematic search for decision boundaries within the regions around a given input is sufficient for assessing robustness.
Crucially, we show how the regions around a point can be analyzed using simple geometric projections, thus admitting an efficient, highly-parallel GPU implementation that excels particularly for the $\ell_2$ norm, where previous work has been less effective.
Empirically we find this approach to be far more precise than many approximate verification approaches, while at the same time performing multiple orders of magnitude faster than complete verifiers, and scaling to much deeper networks.

Published as a conference paper at ICLR 2021
FAST GEOMETRIC PROJECTIONS FOR LOCAL ROBUSTNESS CERTIFICATION
Aymeric Fromherz'
Klas Leino*
Carnegie Mellon University Pittsburgh, PA, USA fromherz cmu. edu
Carnegie Mellon University Pittsburgh, PA, USA kleinoêcs cmu edu
Matt Fredrikson
Bryan Parno
Corina Pasăreanu Carnegie Mellon University and NASA Ames Moffett Field, CA, USA pcori na cmm edu
Carnegie Mellon University Pittsburgh, PA, USA mf ofredri k cmu. edu
Carnegie Mellon University Pittsburgh, PA, USA pa narno@con cmm.. edu
ABSTRACT
Local robustness ensures that model classifies all inputs within by-ball con- sistently, which precludes various forms of adversarial inputs. In this paper, we present fast procedure for checking local robustness in feed-forward neural net- works with piecewise-linear activation functions. Such networks partition the input space into set of convex polyhedral regions in which the network's behavior is linear; hence, a systematic search for decision boundaries within the regions around given input is sufficient for assessing robustness. Crucially, show how the regions around point can be analyzed using simple geometric projections, thus admitting an efficient, highly-paralle ularly for the &2 norm, where previous work has been less effective. Empirically we find this approach to be far more precise than many approximate verification approaches, while at the same time performing multiple orders of magnitude faster than complete verifiers, and scaling to much deeper networks. An implementation of our proposed algorithm is available GitHub
GPU implementation that excels partie-
INTRODUCTION
We consider the problem of verifying the local robustness of piecewise-linear neural networks for given &p bound. Precisely, given a point, x, network. F, and norm bound, c, this entails determining whether Equation [
Vz' Vz 2'11 S
F( F(x')
(I)
This problem carries practical significance, as such networks have been extensively shown to be vulnerable adversarial examples (Papernot et al., 2016 [Szegeyy et al. 2014), wherein small- norm perturbations are chosen to cause arbitrary misclassifications. Numerous solutions have been proposed to address variants of this problem. These can be roughly categorized into three groups: learning rules that aim for robustness on known training data (Croce al. 2019: Madry et al. 2018
Wong & Kolter 2018 Zhang et al. 2019 Xiao et al. 2019), post-processing methods that provide time (Cohen al. 2019 Lecuyer et al. 2018). and network
stochastic guarantees at inference
verification (Balunovic et al. 2019 Cheng et al.
2017 Dutta et al. 2018 Ehlers 2017 Fischetti
Jo 2018 Gowal et 2018 Jordan et al. 2019 Katz et
2017 2019 Singh et al. 2019b] Tjeng &
Tedrake 2017 Wang et al. 2018: Weng et al. 2018).
We focus the problem of network verification-for given model and input, determining if Equation I [holss-pariicuarryy for the l norm. Historically, the literature has primarily concentrated
First two authors have equal contributions
Code available

---

Published as a conference paper at ICLR 2021
on the loo norm, with relatively little work the & norm; indeed, many of the best-scaling verification tools do not even support verification with respect to the & norm. Nonetheless, the &2 norm remains important to consider for "imperceptible" adversarial examples (Rony al. 2019). Furthermore, compared to the &o norm, efficient verification for the &a norm presents a particular challenge, constraint-solvingg (commonly used in verification tools) in Euclidean space requires non-linear objective function, and cannot make as effective use of interval-boume propagation.
Existing work on verifying local robustness for the l norm falls into two primary categories: (1) expensive, but exact decision procedures, e.g., GeoCert (Jordan et al. 2019) and MIP (Tieng & Tedrake, 2017), or (2) fast, but approximate techniques. e.g., FastLin/CROOn
(Weng al., 2018))
Zhang et al. 2018). While upproximate verification methods have shown promise in scaling to larger networks, they may introduce an additional penalty to robust accuracy by flagging non-adversarial points, thus limiting their application in practice. Exact methods impose no such penalty, but as they rely on expensive constraint-solvigg techniques, they often do not scale well to even networks with a few hundred neurons.
In this paper, we focus on bridging the gap between these two approaches. In particular, we present a verification technique for Equation that neither relies on expensive constraint solving nor conservative aperxopproiittiinn of the decision boundaries.
Our algorithm (Section 2) leverages simple projections, rather than constraint solving, to exhaustively search the model's decision boundaries around a point. The performance benefits of this approach are substantial, especially in the case of lz robustness, where constraint solving is particularly expensive while Euclidean projections can be efficiently computed using the dot product and accelerated on GPU hardware. However, our approach also applicable other norms, including foo (Section (33) Our algorithm is embarassingly parallel, and straightforward to implement with facilities for batching that are available in many popular ML libraries. Additionally, we show how the algorithm can be easily modified to find certified lower bounds for rather than verifying a given fixed value (Section 2.3
Because our algorithm relies exclusively on projections, it may encounter scenarios in which there is evidence to suggest non-robust behavior, but the network's exact boundaries cannot be conclusively determined without accounting for global constraints (Section 2 Figure [b). In such cases, the algorithm will return unknown (though it would be possible to fall back on constraint solving). However, we prove that if the algorithm terminates with a robust decision, then the model satisfies Equation [ and likewise if it returns not_ robuut, then an adversarial example exists (Theorem [ Note that unlike prior work approximate verification, our approach cases from unknown, providing a concrete adversarial example in the former. In this sense, the algorithm be characterized as sound but incomplete, though experiments show that in practice the algorithm typically comes to a decision.
often separate not robust
2019 Tjeng We show that implementation outperforms existing exact techniques (Jordan et al.
& Tedrake 2017) by multiple orders of magnitude (Section 3.1 Table [a] and Section 3.3 while rarely being inconclusive on instances for which other techniques do not time out. Moreover, find our approach enables scaling to far deeper models than prior work - a key step towards verification of networks that are used in practice. Additionally, on models that have been regularized for efficient verification (Croce et al., 2019, Xiao et al. 2019), our technique performs even faster, and scales to much larger models including convolutional networks than could be verified using similar techniques (Section 3. Table 2ap. Finally, we compare our work to approximate verification methods (Section 3.2). We find that while our implementation is not as fast as previous work on efficient lower-bound computation for large models (Weng et al., 2018). our certified lower bounds are consistently tighter, and in some cases minimal (Section 3.2 Table 2b}.
ALGORITHM
In this section we give a high-level overview of our proposed algorithm, and present some implemen- tation heuristics that improve its performance (Section 2.2). We also propose variant (Section 2.3 to compute certified lower bounds of the robustness radius. Correctness proofs for all of the algorithms discussed in this section provided in Appendix Al Because our algorithm applies arbitrary bp
2

---

Published as a conference paper at ICLR 2021
Cp
Cp
C
Cp
A
Ag
AD
z
A
(a)
(b)
Figure 1: a Illustaaioon of the FGP algorithm. We begin in Ao (left). We see that activation constraints, C1 and C2 are in the e-ball, thus we enqueue A and A2 (center). When searching A1. we see that a decision boundary, CB, is within the c-ball. The projection p onto CB is an adversarial example; we return not robust (right). (b) Illustration of the cases requiring FGP to return unknown when analyzing boundary constraint, Cp. found within the e-ball about The true boundary is shown in solid blue; the infinite prolongation of the boundary we are projecting against is shown in dotted blue. In each case the projection, p. lies outside of A, and is in fact not adversarial example. In the case on the left, an adversarial example, a, exists in A. while on the right local robustness is satisfied in A. However, cannot distinguish between these cases as p $ A in both; in both cases we must return unknown.
norms, the un-subscripted notation section.
to refer to a general Ep norm for the remainder of this
2.1 THE BASIC FAST GEOMETRIC PROJECTIONS ALGORITIM
We propose the Fast Geometric Projections (FGP) algorithm, which takes a model, F, an input, and a bound, e, and either proves that Equation is satisfied (i.e., e-local robustness), finds an adversarial input at distance less than e from æ. or returns unknown. Our algorithm assumes F(x) (f where RT + R" is the function computed by neural network composed linear transformations with ReLU activations (i.e., f is a ferd-forwrrd ReLU network).
The algorithm relies analysis of all possible activation regions around x. An activation region a maximal set of inputs having the same activation pattern of ReLU nonlinearities.
Formally, let fu (x) denote the pre-activation value of neuron in network F when evaluating x. We say that neuron u is activated (x) 2 O. An activation pattern, A, is a Boolean function over neurons that characterizes whether each neuron is activated. Then the activation region, A, associated
with pattern A is the set of inputs that realize A: A == xx Vu.(fu()) 2 0) + A(u)).
Because we assume that F is piecewise-linet linear composition of linear transformations and ReLU activations, we can associate the activation status A(u) of any neuron with a closed half-space of RT (Jordan et al. 2019). The activation constraint, C.. for neuron u and pattern A is the linear inequality i x + by < O, where Wy and by satisfy Vz E RT .... + b < 0 < A(u). The coefficients, We are equal to the gradient of fu with respect to its imputs, evaluated a point A. Crucially, because the gradient is the same at every point in A, the constraints can be computed from the activation pattern alone via backpropagation. More details on this computation are given in Appendix B
The intersection of these constraints yields the activation region A, and the facets of À correspond to the non-redundant constraints. The convexity of activation regions follows from this observation, as does the fact that the decision boundaries are also linear constraints of the form f(x), 2 f()), for classes i and j.
The FGP algorithm performs a search of all activation regions that might be at distance less than e from We begin by analyzing the region, Ag, associated with the activation pattern of the input, æ, as follows.
First, we check see if As contains decision boundary, C. that is at distance less than from æ; so, we take the projection, p. from x onto C. Intuitively, the projection is an input satisfying C = j pll S || x'I]- Similarly we define the
that is at minimal distance from æ, i.e. Yx "C'')((")
3

---

Published as a conference paper at ICLR 2021
distance, d, from to constraint decision boundary, C, as d(xz, C) mina"s((aa) || -0--21p z'11 ie.. is the distance from r to its projection onto C. If p does not have the same class as x according to F (or lies directly on the decision boundary between classes), then p is adversarial example. If p has the same class as z, it means that the projection to the decision boundary is outside of the activation region are currently analyzing: however, this is not sufficient to conclude that point on the decision boundary is inside both the current activation region and the e-ball (see Figure lb). Therefore, we return unknown.
Otherwise, we collect all activation constraints in Ao: there is one such activation constraint per neuron u in the network; thus each constraint corresponds to the neighboring region, AA, which has the same activation pattern as Ag. except with neuron u flipped, i.e., Ao(u') * AA (u') < u = a'. For each constraint Cu, we check whether it might be at distance less than e from x using geometric projection. A Although C. is only valid in the polytope corresponding to the activation region Åo, we compute the distance to the hyperplane corresponding to the infinite prolongation of C.. As such, we only obtain a lower bound the distance from to C.. If the computed distance is smaller than e, we enqueue the corresponding activation region it has not been searched yet. Thus the queue contains unexplored regions that might be distance less than c from æ. The algorithm continues to analyze each enqueued region in the same way, each explored region enqueuing neighbouring regions that might be at distance less than from æ, until the queue is empty. Exhausting the queue means that we did not find any adversarial examples in any activation region that might intersect with the e-ball centered at z. We therefore conclude that x is locally e-robust. An illustration of simple execution of this algorithm is shown in Figure la
Conditions on Adversarial Examples. It is common in practice include domain-specific condi- tions specifying which inputs are considered valid adversarial examples. For example, in the image domain, adversarial examples are typically subject to box constraints requiring each pixel be in the range [0, 1]. These constraints can easily be incorporated into the FGP algorithm by checking them when we check if F(z) * F(p). when a decision boundary is found. If p not valid adversarial example, the algorithm would return unknown.
Correctness. We show that when the FGP algorithm returns not robust, there exists an adversarial example, and when it returns robust, the model is locally robust at z, with radius c. However, the algorithm may also return unknown, in which case we do not claim anything about the robustness of the model. A complete proof of Theorem i provided in Appendix A.
Theorem 1. (1) When the FGP algorithm returns nob_ro, there exists an adversarial example, p. such that x - pll I and F(x) + F()). (2) When it returns robust, Equation 7 holds.
2.2 HEURISTICS FOR FGP
To improve the performance and precision of our algorithm, we use several additional heuristics.
Batching, The gradient backpropagations for computing constraints and the dot product projections for calculating distances lend themselves well to batching on the GPU. In our implementation we dequeue multiple elements from the queue at once and calculate the constraints and constraint distances for the corresponding regions in parallel, leading to a speedup of up to 2x on large examples for well-chosen batch size (~010-000
Caching Intermediate Computations. We observe that activation constraints for the first layer are invariant across all regions, as there is no earlier neuron to depend on. Thus, we can precompute all such constraints once for all inputs to be analyzed.
Exploring the Full Queue. If the analysis of a decision boundary is inconclusive, the FGP algorithm, as presented, stops and returns unknown. We also implement a variant where we instead record the presence of an ambiguous decision boundary but continue exploring other regions in the queue. If we empty the queue after unsuccessfully analyzing decision boundary, we nevertheless return unknown. However, oftentimes true adversarial example is found during the continued search, allowing to return not_robuss conclusively.
Table I displays the results of experiments evaluating the impact of exploring the entire search queue instead of stopping at the first decision boundary (as described in Section The experimental results show that this heuristic decreases the number of unknown results by approximately 50% while
4

---

Published as a conference paper at ICLR 2021
Vanilla
Full Queue
Model
Time (s)
U
Time (s)
mnist20x3
0.012
7
0.012
mnist20x6
0.177
8
0.174
mnist20x9
4.897
16
7.389
mnist40x3
5,417
9
6.712
Table Comparison of FGP and its variant with full exploration of the queue
only having a minor impact on the speed of the execution. Moreover, we reduce the number of unknown results to the extent that we recover the results obtained by GeoCent in every instance for which GeoCert terminates, except non-robust points on mnist40x3, while nevertheless performing our analysis two three orders of magnitude more quickly.
2.3 CERTIFIED LOWER BOUNDS
We now consider the related problem of finding lower bound the local robustness of the network. A variant of the FGP algorithm can provide certified lower bounds by using priority queue; constraints are enqueued with priority corresponding their distance from x, such that the closest constraint is always at the front of the queue. We keep track of the current certified lower bound in variable, B. At each iteration, we set the maximum of the old B3 and the distance from x to the constraint at the front of the queue.
The algorithm terminates either when all constraints at distance less than the initially specified e were handled, or when decision boundary for which the initial algorithm returns unknown or not_rop not_robust found. In the first case, we return e; in the second, we return the value stored in 3 at this iteration.
The proof of this variant is similar to the proof of the FGP algorithm. It relies on the following loop invariant, which we prove in Appendix A.2
Loop Invariant 1. (1) All activation regions at distance less than 3 from x were previously visited, (2) 3 is always smaller than e, and (3) there is no adversarial point at distance less than B.
EVALUATION
In this section, we evaluate the performance of our implementation of the FGP algorithm and its variant for computing lower bounds. Section 3.J discusses the performance of FGP compared to existing tools that perform exact & robustmess verification. Section 3.2 compares the lower bounds certified by our FGP variant from Section 2.3 to those of other approximate certification methods. In short, we find that our approach outperforms existing exact verification tools by several orders of magnitude (2-4), and produces more precise lower bounds (3-25 times larger) than the relevant work on approximate certification.
Additionally, in Section 3.1 we explore the scalability of our algorithm. We find that when the networks are strongly regularized for verifiability, our approach even scales to CNNs. Finally, we remark the flexibility of FGP with respect the norm in Section 3.3 and observe that our approach is also faster than existing complete verification tools when performing Lo robustness verification.
We performed experiments on three standard datasets: MNIST. Fashion-MNIST. and CIFAR10. We evaluated both on models trained for robustness using ad adversarial training (Madry et al. 2018). and on models trained for verifiability and robustness using maximum margin regularization (MMR) (Croce et al. 2019) or ReLU Stability (RS) (Xiao et al. 2019). We refer to each model by the dataset it was trained on, followed by the architecture of the hidden layers. For example, "mnist20x3" refers to a model trained on MNIST with 3 hidden layers of 20 neurons each. The "cnn" architecture refers to common CNN architecture used to benchmark CNN verification in the literature; details are given in Appendix C Models marked with "** were trained with MMR; models marked with "4" were trained with RS; all other models were trained using PGD adversarial training (Madry et al. 2018). The hyperparameters used for training given in Appendix C
5

---

Published as a conference paper at ICLR 2021
FGP
GeoCert
MIP
Model
Time (s)
R
NR
U
TO
VRA
Time (s)
R
NR
TO
VRA
Time (s)
R
NR
TO
VRA
VRAm
mmist20xc3
0.012
87
0.82
10.99
33
0.84
m0is
0.174
79
9
0.74
78.93
9
42
0.44
>120
100
0.00
0.85
mmist20x9
7,389
44
16
0.42
>120
10
10
80
0.10
>120
100
0.00
0.82
mnist4lxx3
6.712
>120
100es
14
0.73
54.85
41
>120
100
0.76
fmmist200xx*
0.087
66
12
19
0.60
>120
28
67
0.26
>120
100
0.00
0.75
100
0.057
86
7
0.61
>120
50
0.57
>100
100
0.00
0.66
cifar-cnn'
0.088
86
14
0.27
not supported
>120
100
0.00
0.27
(a)
FGPLB Mean Bound
Fastl Meon Bound
Model
Median Ratio
fmmist500x4
0.124
0.078
0.329
fimnss550xx5
0.134
0,092
0.693
000xx
0.083
0.021
0.035
(b)
Table 2: (a) Comparison of lz local robustness certification (FGP vs. GeoCert vs. MIP) on 100 arbitrary test instances, including the median runtime, the certification result either robust (R), not_robust (NR), unknown (U), or a timeout (TO) - and the corresponding Verified robust accuracy (VRA). The upper bound the VRA (VRAuB) is also given. Each instance is given time budget of 120 seconds. Results are for 0.25, except on CIFARIO I0, where we use e = 0.1, as was used
by (Croce et al. 2019). (b) Comparison of the lower bound obtained by FGP (Section 2.3 to that obtained by FastLin.
In each experiment, measurements are obtained by evaluating on 100 arbitrary instances from the test set. All experiments were run on a 4.2GHz Intel Core i7-7700K with 32 GB of RAM, and a Tesla K80 GPU with 12 GB of RAM.
3.1 LOCAL ROBUSTNESS CERTIFICATION
We first compare the efficiency of our implementation to that of other tools certifying local robustness. GeoCert (Jordan al. 2019) and MIP (Tjeng & Tedrake 2017) the tools most comparable to ours as they are able to exactly check for robustness with respect to the l2 norm. We used commit hash 8730aba for GeoCert, and v0.2.1 for MIP. Specifically, we compare the median run time over the analyses of each of the selected 100 instances, the number of examples on which each tool terminates, the result of the analyses that terminate, and the corresponding verified robust accuracy (VRA). i.c.. the fraction of point' that were both correctly classified by the model and verified as robust. In addition, we report an upper bound on the VRA for each model, obtained by running PGD attacks (hyperparameters included in Appendix [ on the correctly-classifie points on which every method either timed out or reported unknown. Results are given for an l2 norm bound of e = 0.25, with a computation budget of two minutes per instance. The results for these experiments are presented in Table 2a
We observe that FGP always outperforms GeoCert by two to three orders of magnitude, without sacrificing precision; i..., we rarely return unknown when GeoCert terminates. MIP frequently times with time budget of 120 seconds, indicating that we are faster by at least four orders of magnitude. This is consistent with the 100 to 1000 seconds per solve on a MNIST model with three hidden layers of 20 neurons each reported by Tieng & Tedrake (2017); their technique performs best on the E or loo norms. In addition, we find that FGP consistently verifies the highest fraction of points, and yields the best VRA. Moreover, on mnist20x3, FGP comes within 2 percentage points of the VRA upper bound. This suggests that FGP comes close to verifying every robust instance on this model.
Models Trained for Verifiability. Adversarial training (Madry et al.) 2018), used to train the models in Sections [.2) attempts to ensure that points on the data manifold will be far from the model's 's decision boundary. Even if it achieves this objective, it may nonetheless be difficult to verify because the performance of FGP depends not only on the decision boundaries, but also on the internal activation constraints. Thus, we expect certification will be efficient only when the points to be certified are also far from internal boundaries, leading to fewer regions to explore. Recent work has sought to develop training procedures that not only encourage robustness, but that also optimize

---

Published as a conference paper at ICLR 2021
Wong & Kolter 2018 Xiao et al. 2019). Maximum margin regularization (MMR) (Croce et al. 2019) and ReLU stability (RS) (Xiao et al. 2019) are
for efficient verification (Croce al., 2019
particularly suited to our work, they follow from the same intuition highlighted above.
Using MMR, FGP is able to scale to much larger models with hundreds or thousands of neurons, and tens of layers, as shown in the bottom half of Table Zal Here again, we that FGP outperforms the other approaches in terms of both time and successfully-verfiee points. By comparison, while GeoCert also experienced improved performance on the MMR-trained models, our method remains over three orders of magnitude faster. MIP continued to time out in nearly every case.
We found that we were able provide even stronger regularization with RS, allowing CNNs (Table 2a). which have far more internal neurons than even large dense networks, We found that these highly regularized CNNs verified more quickly than some of the less-regularized dense networks, though, as with other methods that produce verifiable CNNs, this came at the cost of penalty on the model's accuracy.
scale to
3.2 CERTIFIED LOWER BOUNDS
We now evaluate the variant of our algorithm computing certified lower bounds on the robustness radius (Section 2.3). To this end, we compare the performance our approach to FastLin (Weng et al.) 2018), which is designed to provide quick, but potentially loose lower bounds on the local robustness of large ReLU networks. We compare the certified lower bound reported by our implementation of FGP after 60 seconds of computation (on models large enough such that FGP rarely terminates in 60 seconds) to the lower bound reported by FastLing Fastl .in always reported results in less than two seconds the models analyzed. The results are presented in Table 26 The mean lower bound is reported for both methods, and we observe that on the models tested, FGP is able to find a better lower bound on average, though requires considerably more computation time.
Because the optimal bound may vary between instances, we also report the median ratio of the lower bounds obtained by the two methods on each individual instance. Here we see that FastLin may indeed be quite loose, as on a typical instance it achieves as low as 4% and only as high as 69% of the bound obtained by FGP. Finally, we note that when FGP terminates by finding a decision boundary, if the projection onto that boundary is true adversarial example, then the lower bound is tight. In our experiments, there were few such examples - three on fmnist500x4 and one on fmnist1000x3 however, in these cases, the lower bound obtained by FastLin was very loose, achieving 4-15% of the optimal bound on fmmist500x4, and only 0.8% of the optimal bound on fmnist1000x3, This suggests that while FastLin has been demonstrated scale to large networks, one must be careful with its application, as there may be cases in which the bound it provides is too conservative.
3.3 GENERALIZATION TO OTHER NORMS
The only aspect of FGP that depends on the is the projection and the projected distance computation, making our approach highly modular with respect to the norm. As such, we added support for loo robustness certification by providing a projection and a projected distance computation in FGP.
In this section, we compare the efficiency of this implementation to GeoCert (Jordan et al. 2019) and ERAN (Singh et al. 2019a). ERAN uses abstract interpretation to analyze networks using conservative verraaproxximtioon
As such, the analysis can certify that an input robust, but can yield false positives when flagging an input not robust. In this evaluation, we use the DeepPoly abstract domain, and the complete mode of ERAN which falls back on constraint solving when an input is classified as not robust.
Our experimental setup is similar to the one presented in Section 3.1
For each network, we arbitrarily pick 100 inputs from the test set and report the median analysis time of each tool. We give each tool a time budget of 120 seconds per input. We report the number of instances on which each tool terminates within this time frame, as well as the results of the analyses that terminate. Results are given in Table 3 for an foc norm bound of = 0.01, which contains roughly the same volume as the l2 ball used in most of our evaluation.
7

---

Published as a conference paper at ICLR 2021
FGP
ERAN+MIP
GeoCert R
Model
Time (s)
R
NR
U
TO
Time (8)
NR
TO
Time (8)
NR
TO
0.004
94
6
0
0.017
95
5
0
0.360
95
5
0
mnist20x6
0.016
95
0.054
0.988
mnist20x9
0.021
84
8
4
0.080
92
8
2.799
89
8
mmist4003
0.094
91
5
2
0.040
2,843
fmmist100x6*
0.012
85
8
0.982
0.750
1m
0.021
92
7
2.104
1,308
Table 3: Comparison of for local robustness certification (FGP vs. ERAN GeoCert) on 100 arbitrary test instances with a time budget of 120 seconds, including the median runtime and the certification result: either robust (R), not_robust (NR), unknown (U), or a timeout (TO). Results are for e 0.01.
We refer to each model by the dataset it was trained on, followed by the architecture of the hidden layers. For example, "mnist20x3" refers to model trained MNIST with 3 hidden layers of 20 neurons each. Models marked with an asterisk were trained with MMR (Croce et al. 2019); other models were trained using PGD adversarial training (Madry et al. 2018).
We observe that we consistently outperform GeoCert by about two orders magnitude, both on models trained with MMR and using adversarial training. On models trained for robustness (upper rows of Table B), FGP is 0.5x to 5x faster than ERAN. particular, FGP seems to scale better to deeper networks, while ERAN performs better wider networks. Interestingly, ERAN does not benefit as much from MMR training as FGP and GeoCert. On large models trained with MMR, our tool one two orders of magnitude faster than ERAN, and ERAN only about 2x faster than GeoCert.
Finally, while FGP is able determine robustness for almost all inputs deemed robust by GeoCert or ERAN, it struggles to find adversarial examples for non-robust points, which results in higher number of unknown cases compared the l2 variant. This not highly surprising, as projections are better-suited to the Euclidean space than to fox. space. While the projection in Euclidean space is unique, this not always the case in l.x space; we pick one arbitrary projection which thus might not lead to an adversarial example.
4 RELATED WORK
Our work can be grouped with approaches for verifying neural networks that aim to check local robustness exactly (Jordan et al. 2019 Katz et al. 2017: 2019 Tjeng& & Tedrake (0077;; the primary difference is that our approach avoids expensive constraint sol solving at the price of incompleteness.
GeoCert (Jordan et al. 2019) the closest work to ours; aims to exactly compute local robustness of deep neural networks for convex norms. Unlike approach, GeoCert computes the largest &p ball centered at an input point within which the network is robust. Our experimental comparison with GeoCert shows that our approach scales much better. This is not surprising as GeoCert relies on projections to polytopes, which are solved by quadratic program (QP) with linear constraints. This enables compute exactly the distance from point to an activation constraint, instead of an underapproximation as our approach does. In contrast, our approach uses projections to affine subspaces, which have a simpler, closed-form solution. [Lm al. (2020) builds on GeoCert, but reduces the number of activation regions to consider by exploring the network in a hierarchical manner. Although Lim al.) reduce the number of QPs required for verification, their variant still relies on constraint solving. While they improve on GeoCert by up to single order of magnitude, our approach consistently outperforms GeoCert by 2-4 orders of magnitude. MIP (Tjeng & Tedrake 2017) is an alternative to GeoCert based on mixed-integer programming; it also requires solving QPs for the l norm. We could fall back on similar techniques to provide a slower, but complete variant of algorithm when our projections cannot reach conclusion about decision boundary.
Reluplex (Katz et al. (017) and its successor, Marabou (Katz et al. 2019) are complete verification tools based on SMT solving techniques. Unlike our approach, Reluplex and Marabou do not support the l2 norm. A12 (Gehr et al.) 2018)) and its successor, ERAN (Singh et al., 2019b), are based on abstract interpretation (Cousot & Cousot 1977), using conservative over-approximations to perform
8

---

Published as a conference paper at ICLR 2021
their analysis, which leads to false positives, i.c. robust inputs incorrectly classified not robust. A mode of ERAN enables complete verification by falling back on a constraint solver when an input is classified not robust; however this tool does not support the &g norm either.
FastLin Weng et al. 2018) exploits the special structure of ReLU networks to efficiently compute lower bounds minimal adversarial distortions. CROWN (Zhang al., 2018) later expanded this to general activation functions. Although FastLin has been shown to be very scalable, our experiments indicate that the computed bounds may be imprecise.
Recently, quite different approach has been proposed for robustness certification. Randomized Smoothing (Cohen et al., 2019 Lecuyer al., 2018) is post-processing technique that provides stochastic robustness guarantee at inference time. This approach differs from our approach in that it (1) modifies the predictions of the original model (increasing the complexity of making predictions), and (2) provides probabilistic robustness guarantee that is quantified via confidence bound. As such it provides an alternative set of costs and benefits as compared to static verification approaches. Its complexity also differs from that of FGP, as it is dependent primarily the number of samples required to perform its post- post-processing of the model's 's output. We find that our experimental setup, achieving the same probabilistic guarantee the experiments described in (Cohen et al., (011)) requires 10t samples, taking approximately 4.5 seconds per instance. Thus, for the models in our evaluation, FGP is average faster or comparable in performance.
CONCLUSION
In this paper, we presented a novel approach for verifying the local robustness of networks with piecewise linear activation functions, that relies neither on constraint solving nor conservative over- approximations, but rather on geometric projections. While most existing tools focus on the & and fo norms, provide an efficient, highly parallel implementation implementation outperforms existing exact tools by multiple orders of magnitude, while empirically maintaining the same or better precision under a time constraint. Additionally, we show that our approach is particularly suited to scale up network verification to deeper networks-a promising step towards verifying large, offte-of-the-art models.
certify fg-robustness. Our
The work described in this paper has been supported by the Software Engi- neering Institute under its FFRDC Contract No. BA8702-15-D-000 with the U.S. Department of Defense, Bosch Corporation, an NVIDIA GPU grant, NSF Award ENS-1801391, DARPA GARD Contract HR001 12020006, Google Faculty Fellowship, and the Alfred P. Sloan Foundation.
Acknowledgments.
REFERENCES
Mislav Balumovic, Maximilian Baader, Gagandeep Singh, Timon Gehr, and Martin Vechev. Certifying geometric robustness of neural networks. In Advances in Neural Information Processing Systems (NIPS). 2019.
Chih-Hong Cheng, Georg Nührenberg, and Harald Ruess. Maximum resilience of artificial neural networks. In Automated Technology for Verification and Analysis (ATVA), 2017.
Jeremy Cohen, Elan Rosenfeld, and Zico Kolter. Certified adversarial robustness via randomized smoothing. International Conference on Machine Learning (ICML), 2019.
P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of pro- grams by construction or approximation fixpoints. In Symposium on Principles of Programming Languages (POPL), 1977.
Francesco Croce, Maksym Andriushchenko, and Matthias Hein. Provable robustness of ReLU networks via maximization of linear regions. In International Conference on Artificial Intelligence and Statistics (AISTATS), 2019.
Souradeep Dutta, Susmit Jha, Sriram Sankaranarayanan, and Ashish Tiwari. Output range analysis for deep feedforward neural networks. In NASA Formal Methods Symposium (NFM), 2018.

---

Published as a conference paper at ICLR 2021
Rüdiger Ehlers. Formal verification of thse linear ferward neural networks. In Conference on Logic in Computer Science (LICS), 2017.
Matteo Fischetti and Jason Jo. Deep neural networks and mixed integer linear optimization. Con- straints, 23(3):296-300 3096,,0990000 Jul 2018.
Timon Gehr, Matthew Mirman, Dana
Petar Tsankov, Swarat Chaudhuri, and Martin Vechev. A12: Safety and robustness certification of neural networks with abstract interpretation. In Symposium Security and Privacy (S&P), 2018.
Sven Gowal, Krishnamurthy Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Uesato, Relja Arandjelovic, Timothy A. Mann, and Pushmeet Kohli. On the effectiveness of interval bound propagation for training verifiably robust models. CoRR, abs/1810, 12715, 2018.
Matt Jordan, Justin Lewis, and Alexandros G. Dimakis. Provable certificates for adversarial examples: Fitting a ball the union of polytopes. In Advances in Neural Information Processing Systems (NIPS), 2019.
Guy Katz, Clark W. Barrett, David L., Dill, Kyle Julian, and Mykel J. Kochenderfer. Reluplex: An efficient SMT solver for verifying deep neural networks. In Computer Aided Verification (CAV), 2017.
Guy Katz, Derek A. Huang, Duligur Ibeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah, Shantanu Thakoor, Haoze Wu, Aleksandar Zeljić, David L. Dill, Mykel J. Kochenderfer, and Clark Barrett. The marabou framework for verification and analysis of deep neural networks. In Computer Aided Verification (CAV), 2019.
Mathias Lecuyer, Vaggelis Atlidakis, Roxana Geambasu, Daniel Hsu, and Suman Jana. Certified robustness to adversarial examples with differential privacy. In Symposium on Security and Privacy (S&P), 2018.
Cong Han Lim, Raquel Urtasun, and Ersin Yumer. Hierarchical verification for adversarial robustness. In International Conference on Machine Learning (ICML), 2020.
Aleksander Madry. Aleksandar Makelov, Ludwig Schmidt, Dimitris Tsipras, and Adrian Vladu. Towards deep learning models resistant to adversarial attacks. International Conference on Learning Representations (ICLR), 2018.
N. Papernot, P. McDaniel, Jha, M. Fredrikson, Z. B. Celik, and Swami. The limitations of deep learning in adversarial settings. In European Symposium on Security and Privacy (EuroS& PP) 2016.
Jérôme Rony, Luiz G. Hafemann, Luiz S. Oliveira, Ismail Ben Ayed, Robert Sabourin, and Eric Granger. Decoupling direction and norm for efficient gradient-based adversarial attacks and defenses. In Conference Computer Vision and Patter Recognition (CVPR), 2019.
Gagandeep Singh, Rupanshu Ganvir, Markus Püschel, and Martin Vechev. Beyond the single neuron convex barrier for neural network certification. In Advances in Neural Information Processing Systems (NIPS). 2019a.
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. Robustness certification with refinement. In International Conference on Learning Representations (ICLR), 2019b.
Christian Szegedy, Wojciech Zaremba, llya Sutskever, Joan Bruna, Dumitru Erhan, Ian J. Goodfellow, and Rob Fergus. Intriguing properties of neural networks. International Conference on Learning Representations (ICI.R) 2014.
Vincent Tjeng and Russ Tedrake. Verifying neural networks with mixed integer programming. CoRR, abs/171 2017.
Shiqi Wang. Kexin Pei, Justin Whitehouse, Junfeng Yang. and Suman Jana. Formal security analysis of neural networks using symbolic intervals. In USENIX Conference Security Symposium, 2018.
10

---

Published as a conference paper at ICLR 2021
Lily Weng, Huan Zhang, Hongge Chen. Zhao Song, Cho-Jui Hsieh, Luca Daniel, Duane Boning, and Inderjit Dhillon. Towards fast computation of certified robustness for ReLU networks. In International Conference Machine Learning (ICML), 2018.
Eric Wong and Zico Kolter. Provable defenses against adversarial examples via the convex outer adversarial polytope. In International Conference on Machine Learning (ICML), 2018.
Kai Xiao, Vincent Tjeng, Nur Muhammad Shafiullah, and Aleksander Madry. Training for faster adversarial robustmess verification via inducing relu stability. In International Conference on Learning Representations (ICLR), 2019.
Hongyang Zhang. Yaodong Yu, Jiantao Jiao, Eric Xing, Laurent El Ghaoui, and Michael Jordan. Theoretically principled trade-off between robustness and accuracy. International Conference Machine Learning (ICML), 2019.
Huan Zhang, Tsui- Weng, Pin-Yu Chen, Cho-Jui Hsich, and Luca Daniel. Efficient neural network robustness certification with general activation functions. In Advances in Neural Information Processing Systems (NIPS). 2018.

---

Published as a conference paper at ICLR 2021
A CORRECTNESS PROOFS
A.1 PROOF OF THEOREM 1
We show that when FGP returns not_robust, there exists an adversarial example, and when it returns robust, the model is locally robust at æ, with radius e. However, the algorithm may also return unknown, in which case we do not claim anything about the robustness of the model.
Proof. In the first case, where FGP returns not_ rot_robust, the proof of Theorem iis trivial: we exhibit point, p, such that || pl S and for which F(x) # F(p).
The interesting case is when FGP returns robust. We prove by contradiction that in this case, x is in fact locally robust with radius
Let us assume for the sake of contradiction that FGP returns robust, but there exists point, p. such that || p|| I and F(x) F()). Let Ar and Ap be the activation regions associated with æ and p respectively.
We define path of activation regions as sequence, Ap. Ap,..., Ag, of activation regions such that the underlying activation patterns A; and Ai+1 differ in exactly one neuron for all i, and there exists least one input, 3g, that has activation pattern A, for all i. For instance, in a network with three neurons, if Ao = (true, true, (alse), A1 (true, false, false), and A (true, false, true), and there exist inputs, 2g, F2. and Ø2 with activation patterns Au, A1. and A2, then (Ag, A1, Ag) is path.
Our proof relies on three facts, that we prove hereafter:
1. There exists path, P. from Ag to Ap where each region in the path contains at least one input at distance less than e from I, and either Ag = Ap or all A,, Aj in the path are different.
2. Our algorithm visits all regions in the path, P.
3. If a visited activation region contains an adversarial input, our algorithm either detects it, returning not_robust, or returns unknown.
Together, 7. and (3) imply that if an adversarial point, p. exists, it resides in an activation region that would have been checked by FGP, which would have resulted in the algorithm returning not_robust or unknown, contradicting the assumption that it returned robust.
Existence of a Path Consider the segment going from x to p in straight line. As || p|| < all points on this segment are also distance less than c. As f is a neural network with ReLU activations, f is a continuous function, are the activation functions, fu for each of its internal neurons, u. Furthermore, input points at the boundary between two activation regions (i.e., z, such that (z) = 0) belong to both activation regions. Therefore, listing all activation regions on the segment between and p yields path, P, from Ag to Aps with each region on the path containing an input point, Tt. on the segment, such that || x.Il <.
That each A,, Ag in is unique follows from the convexity of activation regions: there exist A, A, P such that there exists an A, in between, then A, A, cannot be convex, as there exists line segment with its end points in A, and A, that is not entirely contained within the region A, Az. This ensures that paths are of finite length.
2 Exploration by the Algorithm Given the existence of the path, P. from A. to Ap, we now prove that FGP would visit all activation regions in P if it returns robust. We proceed by induction the length paths induced (similarly to as above) by a line segment included in the c-ball centered on
In the base case, if the path is of length one, then it contains only A,, and the claim holds trivially since FGP starts by visiting Ag.
12

---

Published as a conference paper at ICLR 2021
In the inductive case, let us assume that for any path with length at most k induced by segment, 8, beginning at x with ||||| $ e, FGP visits all regions in the path. Now consider a path. P Ag...., Ag.. of length k + 1, induced by segment, s', beginning at z with ||s']| S e. Since A is on the path, there exists a point, 11-1, on s' such that the sub-segment from x to 2k-1 induces a path of length k; thus can apply our induction hypothesis to conclude that FGP visits Ag. ..... A Now, since A and A₁ are neighbors in P", they must share some boundary, C, that is intersected by s'. Thus, since ||>']] S 6, d(xx S E; thus when FGP visits Ag- it will add A₃ the queue via C. Therefore, since FGP returns robust only when all regions in the queue have been visited, FGP will visit Ag. concluding the proof of (2).
Detection of Adversarial Examples We conclude by proving that if there exists adversarial example in a region visited by FGP, then we either return not_ not_robust or unknown.
If p in Ap is adversarial example, then F(x) # F(p). By continuity of f. this means that there exists an input, p' on the segment from x to p that is exactly on a decision boundary, C. As || r'll S I pl S e, C must have been analyzed when exploring Ap-
However, when analyzing a decision boundary, FGP always returns either not_robust or unknown.
Thus, the decision boundary in the activation region containing p would have been analyzed by FGP; this yields a contradiction, as the algorithm must have returned not_robust or unknown rather than robust.
A.2 PROOF OF LOOP INVARIANT
The proof of lower-bound variant is similar to the proof of FGP in Scction A.1 It relies on the following loop invariant.
Proof. Loop Invariant I Juriiallly holds on entry of the loop since bound is initialized to O. Proving that the invariant is mantained is more interesting. Suppose that bound increases to bound'. must then be shown that there is unvisited activation region at distance less than bound'. We proceed again by contradiction: assume there was such a region, A, containing a point, p, such that |pll < bound'. Again, let consider the segment from x to p. and the path, P. induces. Let us consider A,, the first region of P at distance greater than bound that was not previously visited. If no distance less than bound from æ, and so by our induction hypothesis,
such region exists, then it was already visited. otherwise, A,- was visited, and the activation constraint, C, between A;- and A, is such that d(x, C) < bound' S e. Therefore, C' (which leads to A.) was already added to the queue with priority less than bound', and by virtue of the priority queue, it was explored before the current iteration, which yields a contradiction.
If bound does not increase, the invariant still trivially holds. This case can happen because our computation of the distance to constraints an underapproximation of the true distance to the feasible portion of the constraint.
B COMPUTING ACTIVATION CONSTRAINTS AND DECISION BOUNDARIES
Recall that an activation constraint, Cu, which is satisfied when fa(r) 2 0 - A(u), is a linear constraint with coefficients Wa, and intercepts, by. The computation of these weights and intercepts does not depend on particular point in À - -onnly on the activation pattern, A. Thus, we compute the boundaries of an activation region, A, knowing only the corresponding activation pattern, A.
In practice, the coefficients, Wa. correspond to the gradient of fu with respect to its inputs, evaluated at point in A. However, frameworks that perform automatic differentiation typically require a concrete point for evaluation of the gradient. Thus, we compute the gradient via backpropagation with the activation vectors, a, where the position in a, corresponding to neuron, u, takes value A(u) is true and 0 otherwise. The intercepts, bys are computed via forward computation using the activation vectors, with z set to 0. These operations can easily be implemented to run efficiently on a GPU.
13

---

Published as a conference paper at ICLR 2021
Decision boundaries in activation region, A. are computed similarly to internal activation con- straints; we take the linearization of the network in A. Since the network is piecewise linear, and linear within each activation region, this linearization is exact for the region being considered.
C HYPERPARAMETERS
Here, we provide details on the hyperparameters used to train the models used in our evaluation and to conduct the PGD (Madry et al. 2018) attacks used to obtain the upper bounds on the verified robust accuracy (VRA).
CNN Architecture We used a CNN architecture that has been used for benchmarking verification by (Wong Kolter 2018) and (Croce al.) (209).. It contains convolutional layers, each using 4 x 4 filters with a 2 x 2 stride, with 16 and 32 channels respectively, followed by dense layer of 100 nodes.
PGD Adversarially-trainee Models. To train models for robustmess, used PGD adversarial training (Madry et al., 2018). For training, we used the &g norm, and let = 2.5-10 times the e we verify with in order have higher fraction of verifiably-robust points. We trained each model for 20 epochs with batch size of 128 and 50 PGD steps.
Models. To train models for both robustness and verifiability, we used maximum margin regularization (Croce et al. 2019) (MMR). MMR has several hyperparameters including 7/ and yD, which correspond points from the internal boundaries and decision boundaries respectively (these can be seen acting similarly to the choice of e in PGD training); ng and nD, which specifyy the number of internal and decision boundaries to be moved in each update; and X, which specifies the relative weight of the regularization as opposed to the regular loss. See (Croce et al. 2019) for more details on these hyperparameters. We set 7B "/D = 2.5, ng 100, nn and X 0.5, and trained each model for 20 epochs with a batch size of 128.
Serimuu--Margin-eeen
the desired distance of the training
ReLU-Stabiltty-raaime Models. We also used ReLU stability (RS) (Xiao al. 2019) to regularize models for verifiable robustness. We trained using RS with PGD adversarial loss and & weight regularization, as was done by Xiao et al.] We weighted the RS loss by a 2.0, using an (i.e., the distance over which the ReLU activations should remain stable) of 8/ 8/255, and weighted the PGD adversarial loss by the & regularization decay from 10 to 10 over the course of training, and trained for 100 epochs with a batch size of 128.
1.0, using an e (i.e., the target robustness radius) of 36/255
scheduled
PGD Attacks. We obtained an upper bound on the VRA by performing PGD attacks on all the corsecty--lassifeed points for which every method either timed out or reported unknown; the upper bound the best VRA plus the fraction of points that were correctly-classieet which the PGD attack did not successfully find an adversarial example. We conducted these attacks with an l bound of 0.25 with 1,000 PGD steps.
undecided, and for
Arbitrary Test Instances To arbitrarily pick the 100 test instances, we used the random. randint
function from Numpy, setting the initial seed to 4444. The indices of the test instances are 8361, 7471, 8091, 4275, 5205, 6886, 5341, 4026, 4554, 5835, 8181, 6124, 6309, 1875, 7910, 6018, 1985, 6912, 8676, 2376, 9143, 5527, 5540, 4661, 1910, 7498, 2190, 789, 1672, 3393, 1925, 841, 8333,
4644, 5648, 138, 7872, 5204, 441, 3951, 3812, 3983, 8598. 8334. 5666, 5, 1014, 9148, 5993, 2182,
4141, 5385, 2774, 9927, 7507, 9097, 7047, 7319, 1638, 9535, 8889, 1196, 4992, 9223, 6525, 9577,
2266, 1748, 6462, 2969, 4866, 271, 9890, 2814, 9848, 8513, 289, 9002, 1103, 506, 1576, 1035, 9808,
8059, 2424, 6072, 6577, 1463, 5573, 8995, 100, 1457, 8103, 7835, 2491, 9481, 8053, 2478, 8132,
7033.
14

---

Published as a conference paper at ICLR 2021
D BREAKDOWN OF RUN-TIMES FOR DECIDED POINTS
92-
50-
23
02-
intanca
(a)
miii200
mnterated
miik2ts9
155
2222
6.15
3359
20
46
90
26
46
20
00 13
0 66
66
(b)
Figure 2: Cactus plots showing the time taken for each instance that decided as either robust or not_row rob_ro. The instances ordered by increasing time-per-instance. Results shown for the PGD adversarially-trainee models for both the & norm (a) and the &oo norm (b)
15


Reviews:
[{"review_id": "pZq_3cPb1Jm", "reviewer": "AnonReviewer1", "summary": "", "questions": "", "limitations": "", "rating": 6, "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_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "The paper proposes Fast Geometric Projections (FGP), a method to certify the robustness of neural networks with ReLU as activation exploiting the fact the such networks are piecewise affine functions. FGP can verify whether in an $\\ell_p$-ball around an input $x$ adversarial examples exist or not. Since it's not guaranteed to find a conclusive solution, it has the option of returning \"unknown\" if the given point could not be certified. FGP aims at computationally efficiency at the price of incompleteness. Finally, it can provide lower bounds on the norm of the smallest adversarial perturbation.\n\nPros\n1. Verifying efficiently the robustness of (large) neural networks is an interesting task and most of the research has primarily focused on the $\\ell_\\infty$-threat model. A fast methods which is effective in particular wrt the $\\ell_2$-norm is valuable.\n2. The proposed methods is geometrically justified and benefits from many heuristics to optimize efficiency.\n3. In the experimental evaluation, for the $\\ell_2$-threat model, FGP outperforms the methods for exact verification (GeoCert, MIP) with a timeout in terms of both verified robust accuracy and runtime (with a large margin). Moreover, it scales better than other methods to larger and deeper architectures when tested  on models trained for verifiability (MMR, RS).\n4. When comparing lower bounds on the size of the minimal adversarial perturbations, it provides better bounds than FastLin, although with higher computational cost.\n\nCons\n1. To achieve good provable robustness, it is necessary to train specifically for it and then usually the best bounds are given by the same technique deployed at training time (e.g. IBP training). An evaluation of FGP in such scenario seems to me particularly meaningful (and at the moment missing). If the proposed FGP outperformed the bounds given by the technique of, for example, (Wong & Kolter, 2018) on a model trained as in (Wong & Kolter, 2018), this would strengthen the proposed method.\n2. The $\\ell_\\infty$ version doesn't seem as competitive the $\\ell_2$ one. Moreover, in that case $\\epsilon=0.01$ is used, which is very small for MNIST or F-MNIST (e.g. Zhang et al. (2019) have guaranteed up to $\\epsilon=0.4$).\n3. It seems that CROWN (Zhang et al., 2018) slightly improves upon FastLin, so it might make sense to include it in the comparison.\n\nOther comments\n1. Only one value for $\\epsilon$ is tested for each dataset. It would be interesting to see how FGP scales to larger values.\n2. The clean accuracy of the models used in the evaluation should be reported (it would be helpful to know whether they achieve reasonable performance).\n3. Also, for completeness, using the different types of models (naturally trained, MMR and RS) for all the datasets (and also for the comparison to FastLin) would be good.\n\nOverall, the method is clearly presented and achieves good empirical results. As mentioned above, further experiments could show its effectiveness and applicability on models with state-of-the-art provable robustness.\n\nZhang et al., \"Towards Stable and Efficient Training of Verifiably Robust Neural Networks\", 2019\n\n---\nUpdate after rebuttal\n\nI thank the authors for their response. After reading it, the revised version and the other reviews, I think that there's evidence of the effectiveness of the proposed method.\n\nAs I tried to convey in the initial review, I consider the main weakness of the paper not showing the performance on models achieving state-of-the-art verified robustness. I think the case of $\\ell_\\infty$ is emblematic, where $\\epsilon=0.01$ is used. Since there exist models achieving provable robustness >90% for $\\epsilon=0.3$ (on MNIST), the scenario considered in the evaluation doesn't seem interesting, regardless of how FGP compares to the other methods.\n\nWhile I agree with the authors that training for provable guarantees sacrifices clean accuracy in most of the cases, as far as I know that is currently the way to achieve good VRA at meaningful thresholds. Along this line, also the authors used FGP on larger models when those were trained with MMR or RS. In my opinion the most interesting application of a (incomplete) verification method like FGP is to provide better VRA than current methods for training (IBP, CROWN-IBP, Wong & Kolter's method), for example using less heavily regularized models which can retain higher clean accuracy. I think this is the missing piece in the current version of the paper.\n\nFor these reasons, I keep my initial score.", "extra_scores": {}, "extra_text": {}}, {"review_id": "IjQdc3kmvz", "reviewer": "AnonReviewer2", "summary": "", "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": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "Summary:\nThis paper proposes an algorithm to verify whether or not there exists an adversarial example in an Lp ball of size espilon around a given training sample. As opposed to the more common used bound propagation method (Crown, fastlin, IBP...), it does not do so by overapproximating bounds on the output, but instead by exploring neighbouring activation patterns to the one where the sample to verify lie, in a form of exhaustive search. As opposed to previous similar algorithm (Geocert), it sacrifices completeness in order to gain efficiency. \nIn addition, the authors explain how to take advantage of the Neural network structure to make the algorithm more efficient. Experimental results are very convincing, showing strong improvements in term of runtimes of the method with the proportions of \"unknown\" sample remaining moderate.\n\nMain comment:\nIt would be beneficial for the authors to make explicit the difference between the Fast Geometric Projections algorithm and the GeoCert algorithm. As it is, it seems obvious to me that the two algorithms are clearly related but it would be beneficial to make the difference more apparent. There is a short mention in the Related Work section but I found it pretty lacking. Why does GeoCert need to rely on projection to polytope solved by quadratic program and FGP does not? \nAs it is, my understanding of the difference is that GeoCert, when computing the projection, computes it only to the actual existing part of the decision boundary/activation constraint, rather than to its infinite prolongation as is done by FGP. Is that correct?\nIs there a intuition or a result that could be given of when GeoCert and FGP are going to return the same result? Or equivalently, a characterization of FGP incompleteness? Is it something like \"There exists an activation pattern A intersecting with the epsilon ball, with the decision boundary Ca going through it, but the projection of the center point onto the (extended to an infinite line) decision boundary Ca does not belong to A\"\nI think that this would make the paper significantly stronger, if things were formulated in the way of \"We perform this change, which leads to the loss in completeness due to not handling those cases well, but in exchange the computation that needs to be done becomes much simpler leading to X orders of magnitude improvement.\", rather than \"here is an algorithm that works X order of magnitude better\". The first allows the reader to get an insight into the trade-off and the structure of the problem.\n\nSmaller comment:\nIt would be nice to have an ablation study / experimental evaluation of the benefits brought by 2.2 and taking advantage of the network structure if it's an experiment that could easily be run.\n\nExperiment Section comments:\n- I'm unclear as to what the upper bound on the verified robust accuracy tells. For FGP on cifar-CNN, why isn't the robust accuracy 86%? It seems like all samples have been successfully handled and 86 out fof the 100 have been found robust?\n- Fastlin has mostly been superseded by Crown, which usually give tighter bounds. I assume that the tightness comparison would still go the same way but it would be a more appropriate baseline. It would also be good to provide the runtime for Fastlin/Crown for the benefit of the reader. FGP takes 60s on those networks , but I doubt that Fastlin takes more than 1s. There is even a lot of space on the side of Table 1.b to add a runtime column!\n\nMinor Notes:\n- In 2.1, \"if A0 contains a decision boundary\" -> \"contains a decision boundary C\", maybe? C doesn't seem to be introduced anywhere (there is C_u for activation constraints).\n- In 2.1,  at the end, it is not clear if the enqueued neighbouring activation regions will also potentially enqueue their neighbouring regions? I think that I figured out that it is based on the rest of the paper but it would be nice to make it more explicit.\n- In 2.2, it would be nice, even if the proof is not there to have the intuitions behind it be in the main paper. The appendix sentence \"To prove the correctness of our treebased exploration, we only need to prove that the additional regions we filter out either are unreachable, or are explored through a different path.\" is perfectly sufficient to convince the reader of the idea.\n\nRecommended Related works:\nThe authors may potentially add a reference to \"Measuring Neural Net Robustness with Constraints\", by Bastani et al., NeurIPS 2016,   for context, although the method in that paper was only looking in a single linear piece of the network. Not really necessary though.\n\n\nOpinion:\nThe algorithm is great and its presentation from a point of view of \"what is done\" is quite clear but the paper would in my opinion be much better if it contextualize its contribution better in comparison to other algorithms. I would be happy to raise my rating if this was the case.\n\n\n###########################################\nUpdate after discussion with the authors and reading the updated version:\n\nThe authors have clarified the points that were unclear. I'm happy to raise my score.\n", "extra_scores": {}, "extra_text": {}}, {"review_id": "BmuNy44zITk", "reviewer": "AnonReviewer4", "summary": "", "questions": "", "limitations": "", "rating": 8, "confidence": 5, "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_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "Title before Rebuttal: _Novel idea for accelerating verification hampered by concerns on correctness of algorithm_\n\n# Summary of Contributions\nThe paper proposes a method to verify local robustness networks with piecewise-linear activation functions, providing tighter bounds than existing approximate verification approaches while scaling to deeper networks than existing complete verifiers. \n\nFurthermore, unlike other approximate verification techniques, the method is able to show the existence of adversarial examples (in some cases). \n\nThe method works by exhaustively checking each of the activation regions (that is, the convex polytopes on which the network is linear) that are fully or partially within the ε-ball for the presence of a decision boundary. \n- If there exists a region containing a decision boundary for which the projection $p$ of $x$ to the decision boundary is within the ε-ball:\n  - An adversarial example exists if $p$ is in the activation region\n  - The robustness status is unknown if $p$ lies outside of the activation region\n- Otherwise, if no such region exists, the sample is robust to local perturbations.\n\n# Score Recommendation\nThe method in this paper is novel and the results presented are compelling. However, it is currently marginally below the acceptance threshold (5) for me, as I am concerned about the correctness of the optimized tree-based exploration variant of FGP presented. Notwithstanding the other issues identified, if my concerns around the correctness are addressed and the presented results stand, this paper would be among the top 50% of accepted papers (8). Otherwise, it would be a reject (3).\n\nFor the tree-based exploration approach to be correct, we need to prove that regions filtered out are unreachable or explored through a different path. The proof in A.2 needs to be expanded upon, and does not currently provide sufficient detail to demonstrate that this is the case.\n\nSpecifically, consider the potential counterexample in the image linked: https://www.geogebra.org/geometry/ajzcrves. We have four polytopes A_prev, A, A_next, A bounded by ECG, DCE, FCD, GCF respectively. Every region that differs by one neuron is adjacent to each other. A_next is discarded when exploring from A, it will not be reached by any other path since A' will not be explored from A_prev (the boundary GC does not pass inside the ε-ball). I expect that some other property of the network means that this is not an actual counterexample, but do not see which specifically.\n\n# Strengths\n*Novelty*: The paper presents a novel approach for verification that can be accelerated on GPUs. While other work to accelerate verification on GPUs exist (e.g. [predicting dual variables for optimization using a neural network](https://arxiv.org/pdf/1805.10265.pdf) or [expressing SDP solver algorithms as passes through the network being verified](https://arxiv.org/pdf/2010.11645.pdf)), the method presented simply exhaustively searches (very efficiently) each activation region.\n\n*Results*: To the best of my knowledge, the method:\n- Advances the state-of-the-art in certifying local stability over perturbations of bounded $l_2$-norm, with significant improvements in runtime (1-2 orders of magnitude) over GeoCert.\n- Advances the state-of-the-art in providing tight certified lower bounds (up to 2 orders of magnitude) on $l_2$-robustness radius\n\n*Overall Clarity*: This paper was a pleasure to read, and I wanted to make special note of this. I appreciated that thought had been put in in naming and defining terms (e.g. activation pattern, activation region), and found the diagrams in particular helped me understand the algorithm. Results were organized clearly \n\n*Reproducibility*: The authors took pains to provide details that make their results more reproducible (architecture, training hyperparameters and method, time budget, computational setup for verification). \n\n# Weaknesses\n_(The relative length of this section should not be taken as an indictment of this paper.)_\n\nIn addition to the issue with the optimized variant of FGP, here are some additional weaknesses that should be addressed. \n\n## Clarity of Algorithm Description\n- With reference to Figure 2b and focusing on $C_1$, the penultimate paragraph of page 3 says “For each constraint at distance less than ε from x, we enqueue the corresponding activation region if it has not been searched yet”. It would be helpful to emphasize in the paper that we are checking if the *line* $C_1$ intersects the ε-ball, not just the line _segment_ between $A_{11}$ and $A_{01}$.\n- I could not find an explanation in the paper for how the decision boundaries are computed; this seems core to the efficiency of the approach. As far as I can tell, the method described linearizes the network $f$ about the activation region (obtaining $f’$), and computes the decision boundary in $f’$ (not $f$), and then checks the distance to $x$. If this is the case, it should be explicitly specified, and a concise proof that this is correct added.\n\n## Generalization to Other Norms\n- The time comparison (“up to 5x faster than ERAN on models trained with PGD, and one to two orders of magnitude faster than ERAN on models trained using MMR”) is misleading without noting that the FGP returns “unknown” for a significant proportion of samples (6-15%) while ERAN+MIP returns a result in all cases. This should be noted in Section 3.3, rather than readers having to head to the appendix to determine this.\n- While ERAN is a reasonably competitive verification method, I’d be interested to see a comparison with nnenum (CAV ‘20: https://github.com/stanleybak/nnenum) if possible, as I expect that nnenum may provide stronger results than ERAN.\n  - I would also love to see a comparison with [VeriNet](https://vas.doc.ic.ac.uk/software/neural/) (ECAI ‘20 but this is not necessary as ECAI ‘20 did occur after Aug 2, 2020.\n\n## Certified Lower Bounds\n- Given that FastLin is designed to be quick but provide loose bounds, it would be reasonable to provide the mean runtime for FastLin (presumably ~1s) and FGP_LB (60s) in Table 1b, so that someone scanning the paper can understand that FGP provides better bounds at the cost of longer runtime)\n- CROWN provides better certified lower bounds than FastLin without a significantly higher cost to runtime (see, for example, Table 4 of the original paper). Computing the mean bounds in Table 1b using CROWN (rather than FastLin) would be a better comparison of FGP to the state of the art.\n\n## Reproducibility\n- The first paragraph of page 6 states that “measurements are obtained by evaluating on 100 arbitrary instances”. It would be helpful for reproducibility to provide the indexes of these instances.\n- It would be nice to have the relevant code released.\n\n# Questions for Authors\n- With reference to Figure 1b: it seems possible to distinguish between the left and right cases by computing the projection of point $p$ onto the ε-ball, $p’$, and checking whether $p’$ is within the activation region. This would allow the algorithm to avoid returning `unknown` in cases like the right. Is this incorrect, or was it merely challenging to implement?\n- How did you handle the presence of multiple decision boundaries within a single activation region (e.g. one between category 1 and 2, and one between category 1 and 3) or does this provably not occur?\n\n# Additional Feedback\n \n- Figure 1 combines two related but different ideas (an illustration of the basic FGP algorithm, and an example of a case requiring FGP to return unknown when analyzing a boundary constraint) into a single figure. As a result, the figure was slightly confusing for me when I initially looked at it. I understand that this is probably done for space constraints, and the authors do attempt to use the spacing between the squares to distinguish between the two groups of squares, but perhaps a light vertical line (or some other visual aid) would help to distinguish more clearly. (I have a similar recommendation for Figure 2 is even less clear).\n- The use of “enriched” in third paragraph of Page 5 is slightly confusing (is the queue somehow enriched, or is it the regions that are?). What about “Instead, it is sufficient to use a regular queue of regions, augmenting _each region_ with a field storing the layer the last flipped neuron belongs to”?\n- The paragraph on “depth scalability” discussing Figure 3 seems to emphasize the _ratio_ of regions searched between FGP and GeoCert. Given this, showing the y-axis of regions searched on a log scale might be appropriate since it enables readers to do the comparison themselves.\n- The layout of the paper means that the first introduction in text of verified robust accuracy occurs after its use in Table 1. Given that it looks like there is enough space in the caption, it might be worth it to spell out what VRA is in the caption.\n- For reproducibility, it would be helpful to indicate which commit / [release](https://github.com/vtjeng/MIPVerify.jl/releases) of the MIP code you used to obtain the results.\n\n# Post-Rebuttal Comments\nI've increased the rating for the paper from 5 -> 8 as the authors have addressed all my substantive concerns.\n\n- Most critically, the authors demonstrated that, even without the tree-based exploration variant, FGP's performance improves significantly over the state of the art particularly for $l_2$ networks. \n- The authors have also significantly improved the clarity of the algorithm description, made the comparison in the section on generalization to other norms more clear, provided information in the paper allowing readers to understand that FastLin is significantly faster (but also significantly looser), and provided details that make reproducing these results far simpler. ", "extra_scores": {}, "extra_text": {}}, {"review_id": "6POeD7QDvXS", "reviewer": "AnonReviewer3", "summary": "", "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": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "The authors propose a systematic search over the convex polyhedral regions on which the network is linear, to find the decision boundary, so to certify local $\\ell_p$ robustness. The method is fairly general and evaluated for $p = 2$ and $p = \\infty$. A key point that makes the method feasible is leveraging of the compositional structure. \n\nThe proposed verification method is incomplete and returns, given an input either one of 2 certificates (robust or not_robust) or abstains from certification. In the case of $\\ell_2$ robustness, significant speed ups are gained compared to prior work. Certifying local $\\ell_p$ robustness is in general an important problem. The scalability to large networks seems to be an issue, although the proposed method significantly outperforms prior work. \n\nSuggestions:\nA potential improvement for Section 2 would be to include a simple running example, that showcases the algorithm step by step. Ideally, the same example would then also be used for Figure 2. \n\nQuestions:\n- What would it take to make the proposed method complete? What would the complexity / runtime be?\n- How large can the networks be grown for a more generous time budget (i.e. 5 min or 10 min instead of 2 min) so that the proposed method still performs well?\n\nGiven the generality of the approach and the speed up gained compared to prior work, i give this paper an accept. \n\n===\n\nI thank the authors for providing the answers to my questions. I will not change my score. ", "extra_scores": {}, "extra_text": {}}]

Author rebuttal:

Meta-review: The paper presents a sound and efficient (but not complete) algorithm for verifying that a piecewise-linear neural network is constant in an Lp ball around a given point. This is a significant contribution towards practical protection from adversarial attacks with theoretical guarantees. The proposed algorithm is shown to be sound (that is, when it returns a result, that result is guaranteed to be correct) and efficient (it is easily parallelizable and can scale to large networks), but is not complete (there exist cases where the algorithm will return "I don't know"). The experiments show good results in practice. The reviewers are positive about the paper, and most initial concerns have been addressed in the rebuttal, with the paper improving as a result. Overall, this is an important contribution worth communicating to the ICLR community, so I'm happy to recommend acceptance.
Decision: Accept (Spotlight)