Venue: ICLR 2021 Conference

Reviews:

final_score: rating: 7: Good paper, accept
review_content: Summary:
This 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. 
In 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.

Main comment:
It 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? 
As 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?
Is 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"
I 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.

Smaller comment:
It 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.

Experiment Section comments:
- 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?
- 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!

Minor Notes:
- 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).
- 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.
- 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.

Recommended Related works:
The 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.


Opinion:
The 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.


###########################################
Update after discussion with the authors and reading the updated version:

The authors have clarified the points that were unclear. I'm happy to raise my score.

review_title: Interesting algorithm, but the paper could be much better by situating itself better compared to existing work.

final_score: rating: 8: Top 50% of accepted papers, clear accept
review_content: Title before Rebuttal: _Novel idea for accelerating verification hampered by concerns on correctness of algorithm_

# Summary of Contributions
The 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. 

Furthermore, unlike other approximate verification techniques, the method is able to show the existence of adversarial examples (in some cases). 

The 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. 
- If there exists a region containing a decision boundary for which the projection $p$ of $x$ to the decision boundary is within the ε-ball:
  - An adversarial example exists if $p$ is in the activation region
  - The robustness status is unknown if $p$ lies outside of the activation region
- Otherwise, if no such region exists, the sample is robust to local perturbations.

# Score Recommendation
The 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).

For 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.

Specifically, 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.

# Strengths
*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.

*Results*: To the best of my knowledge, the method:
- 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.
- Advances the state-of-the-art in providing tight certified lower bounds (up to 2 orders of magnitude) on $l_2$-robustness radius

*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 

*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). 

# Weaknesses
_(The relative length of this section should not be taken as an indictment of this paper.)_

In addition to the issue with the optimized variant of FGP, here are some additional weaknesses that should be addressed. 

## Clarity of Algorithm Description
- 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}$.
- 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.

## Generalization to Other Norms
- 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.
- 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.
  - 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.

## Certified Lower Bounds
- 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)
- 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.

## Reproducibility
- 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.
- It would be nice to have the relevant code released.

# Questions for Authors
- 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?
- 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?

# Additional Feedback
 
- 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).
- 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”?
- 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.
- 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.
- 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.

# Post-Rebuttal Comments
I've increased the rating for the paper from 5 -> 8 as the authors have addressed all my substantive concerns.

- 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. 
- 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. 
review_title: Novel idea for accelerating verification

final_score: rating: 6: Marginally above acceptance threshold
review_content: 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.

Pros
1. 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.
2. The proposed methods is geometrically justified and benefits from many heuristics to optimize efficiency.
3. 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).
4. When comparing lower bounds on the size of the minimal adversarial perturbations, it provides better bounds than FastLin, although with higher computational cost.

Cons
1. 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.
2. 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$).
3. It seems that CROWN (Zhang et al., 2018) slightly improves upon FastLin, so it might make sense to include it in the comparison.

Other comments
1. Only one value for $\epsilon$ is tested for each dataset. It would be interesting to see how FGP scales to larger values.
2. The clean accuracy of the models used in the evaluation should be reported (it would be helpful to know whether they achieve reasonable performance).
3. 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.

Overall, 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.

Zhang et al., "Towards Stable and Efficient Training of Verifiably Robust Neural Networks", 2019

---
Update after rebuttal

I 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.

As 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.

While 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.

For these reasons, I keep my initial score.
review_title: Interesting method which could benefit from further experiments

final_score: rating: 7: Good paper, accept
review_content: 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. 

The 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. 

Suggestions:
A 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. 

Questions:
- What would it take to make the proposed method complete? What would the complexity / runtime be?
- 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?

Given the generality of the approach and the speed up gained compared to prior work, i give this paper an accept. 

===

I thank the authors for providing the answers to my questions. I will not change my score. 
review_title: General method for certifying l_p robustness 

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)