Venue: ICLR 2022 Conference

Reviews:

final_score: rating: 8: accept, good paper
review_content: summary_of_the_paper: This paper presents a novel algorithm for identifying "provably robust adversarial examples": large regions in the input space that provably contain only adversarial examples.

Each region corresponds to a single adversarial example $\tilde{x}$ found in the center of the region, along with all the points that can be generated by applying a sequence of transformations to $\tilde{x}$. The transformations considered in the paper are semantically meaningful changes to the original image. Critically, we can be guaranteed that $\tilde{x}$ will be misclassified even if _it_ is perturbed.

The paper demonstrates that the algorithm can generate regions of non-trivial size on networks of non-trivial size. For example, for a CIFAR10 classifier with 6 layers and ~62k neurons, it finds axis-aligned regions containing a median of $10^{573}$ adversarial examples. In addition, the paper shows that provably robust adversarial examples can be used to create adversarial examples to $L_2$-smoothed classifiers that are more robust to $L_2$ noise as compared to adversarial examples generated directly via PGD attacks.
main_review: # Strengths

- **Originality**: The paper presents a novel algorithm to generating provably robust adversarial examples corresponding to semantically meaningful regions.
- **Quality**:
  - The paper demonstrates that the algorithm can scale to generate provably robust adversarial examples of non-trivial size on networks of non-trivial size.
  - The experiments in the paper have clearly been carried out with an attention to detail.
- **Clarity**:
  - The paper describes the algorithm in sufficient detail to enable reproducibility. (In particular, the appendix explains important details that would be required to re-implement the approach.)
- **Significance**:
  - The approach presented is modular, using existing certification algorithms as a subroutine. This has two key benefits:
    - Improvements to existing certification algorithms can be used to improve the search efficiency for provably robust adversarial examples
    - Certifiers which handle new classes of transformations could be used to generate provably robust adversarial examples for these classes of transformations.
  - While this paper focuses on adversarial examples, the approach can be used in any setting where we are interested to find large regions of input space with a constant classification (or, more generally, where a linear function of some neuron activations exceeds a threshold). I can imagine this being applied to better understanding/visualizing how the output of a neural network varies as the inputs change.

# Areas for Improvement

## Originality

- In the introduction, the paper states that "our regions are guaranteed to be adversarial while prior approaches are empirical and offer no such guarantees". Section B.2. mentions Liu et al., which "is also capable of generating provably robust hyperbox regions". Is the statement in the introduction wrong?

## Quality

- The baseline used seems to be a straw man, since it is simply "our method" but with uniform rather than adaptive shrinking; I would always expect "our method" to outperform the baseline. I would prefer to see the comparison to Liu et al. (and any other methods that produce provably adversarial regions if they exist) in the main body of the paper instead.
- In Table 2, the transforms selected appear quite arbitrary; in particular, they appear like they could have been cherry-picked to flatter the presented approach. Some detail on how the transformations were selected would alleviate this concern.

## Clarity

- Experimental setup for Section 5.3:
  - I struggled to understand what experiment was run in this section and what the results in Table 3 show. I understand that the goal of this section is to show that robust adversarial examples are significantly more effective against defenses based on randomized smoothing, but the setup for the experiment is still not clear to me. I'd be happy to discuss this with the authors, but some preliminary questions:
    - What are the units of 'robustness'?
    - Is the result for "Ours" normalized to 1?
    - Table 3:
      - Are the results for "baseline" and "ours" mean, or some other summary statistic?
      - What result exactly is shown for "individual attacks"? Were multiple attacks generated for each image, or was the individual attack the attack that was used to determine the value of $R'$?
- Reporting # of concrete examples:
  - In Table 1, the SizeO column reports an _upper bound_ on the number of concrete examples in the polyhedral region. This is not immediately clear from the description; a reasonable reader might expect that this is just the number of concrete examples. I would request that the authors either:
    - Estimate the actual number of concrete examples
    - Clearly indicate in the table description that this is an overestimate
    - Remove the SizeO column.
  - I have a similar concern with the "Over" column in Table 2; I don't see how an overestimate of the number of concrete examples in the region is relevant.

# Additional Comments

## Clarity

Here are some issues with clarity that do not constitute major issues, but would still improve the paper significantly if addressed. At the high level, he paper appears to be trying to squeeze too many results in, leading to important details being omitted.

### Missing Details

- Section 5.3: "We exclude images whose radius is too big" - what constitutes too big? For these images, what is the robustness to $L_2$ smoothing defenses of adversarial examples generated by your method?
- Table 1 / Table 2: Is the time reported here a median or average, and is it only for instances where the methods succeed?
- Table 2: The value of #Splits is listed but no guidance is provided to the reader as to how to interpret the result. I would recommend moving this information to the appendix or adding an interpretation.
- Definition 2: "whose $L_2$ ball is certified as adversarial" - I didn't find a definition in the paper of what it means for the $L_2$ ball to be adversarial. (I would have assumed that this means that every sample in the ball has a different classification as compared to $x$, and not that every sample has to have the same classification as $\tilde{x}$, but the rest of the paper seems to suggest the latter definition.)

### Miscellaneous Points

- Section 3 (Overview): "... assumes an algorithm $\alpha$" - the variable $\alpha$ is already used above to indicate the probability that `CERTIFY` fails. I'd recommend using a different variable here.
- Section 3.2 (Computing an Underapproximating Region): "sacrificing a few pixels where the network is not very robust" - did you mean where the _adversarial example_ is not very robust here? If the network is not robust for a certain pixel, it doesn't make sense to me to sacrifice _those_ pixels ...
- Section 5.1: "Column #Regions" is referenced, but it is "#Reg" in both tables.

## Spelling / Grammar

- Section 2.2 (Geometric Certification): "creates overapproximation of the region" -> "creates an approximation of the region"
- Figure 1: "repred crosses" -> "red crosses"?

# Questions

This is out of the scope of this paper, but the result in Section 5.4 suggests that it might be possible to find perturbations to empirically robust adversarial examples (empirically verified by an EoT approach) that result in a correctly classified image. Do you have any sense whether it would be possible to consistently find such "dis-adversarial attacks" on empirically robust adversarial examples?
summary_of_the_review: Overall, I recommend accepting the paper. The paper presents a novel approach to finding large regions of adversarial examples, with strong experimental evidence that it scales well. The details provided would enable other researchers to reproduce the presented approach. Most importantly, this approach is likely to be something that other researchers can use and build upon.

Having said that, the paper has some issues with clarity. Details are provided in the main review, but I'd like to highlight in particular Section 5.3, which I found particularly hard to parse.

N.B. My current recommendation for this paper as-is is 6, but I'd be quite happy to upgrade the recommendation to 8 if the bulk of my concerns around clarity are addressed.

--- 

## After Paper Discussion Period
During the paper discussion, the authors addressed the bulk of my concerns around clarity, and I've upgraded my recommendation to 8 as a result.
review_title: null

final_score: rating: 6: marginally above the acceptance threshold
review_content: summary_of_the_paper: The manuscript introduces a definition of provablely-robust adversarial examples, a set of examples that are verified to be classified as different labels compared with the input of interest. The main idea of the technique is to shrink a box-like region from an over approximation to a verifiable smaller sub-region such that a robustness verifier will return robust for all points in that particular sub-region. In the evaluation part, the author demonstrates the effectiveness of the approach with several experiments, i.e. robustness against intensity transformation and randomized smoothing defense. 

main_review: ### Strength

This paper has clearly stated its objective, the approach and the corresponding evaluations. The proposed technique is designed for a concrete objective, generating provably-robust adversarial examples. The approaches are well-documented in the paper and evaluations are conducted over several datasets and models. 
The paper has spent a lot of space explaining the technique from a high-level perspective down to its implementation details, which helps the reader to better understand the algorithm. 

### Weakness

My concerns of the paper mainly focus on the following three aspects: 

1. Motivation of the “provable” part of the adversarial examples is missing. This paper relates to the prior work in generating robust adversarial examples [1, 2], where they can serve as a good motivation to generate “robust'' adversarial examples”: these papers discuss several physical distortions in applying the adversarial examples into the real-world cases for images and audio. In the other word, these distortions are real-world adversaries for artificial adversarial examples. However, the motivation for the “provable” part is missing to me. I understand the “provable” part can be related to a counter problem, probably-robust networks. The provably-robust network is motivated to build networks where the robustness can be guaranteed for all possible attacks and the evaluations are free from the choice of adversaries. To that end, can the authors explain more about the motivation for “provably”-robust adversarial examples? A follow-up question is: does the robust region proposed in this paper actually contain the physical distortions that may be encountered in the real-word cases [1, 2] and how often? It seems that the more important part we need to prove is that these regions are guaranteed to contain all or part of the distortions you can possibly encounter so that an adversary does not need to worry about that an adversarial example fails in practice. 

2. Important experimental setups and discussions are missing. 
- Unfortunately with some amount of time during my review I can not locate the concrete definitions and actual implementations of the intensity changes and geometric changes as mentioned in Table 1 and 2. This information should be helpful to understand the importance of the results. 

- How “provable” is evaluated? Table 1 and 2 seem to only evaluate how big the region is and Table 3 seems to use randomized smoothing as an attack to adversarial examples generated by the proposed approach. However, the motivation of the paper mostly relies on [1, 2], where the “robustness” of an adversarial example is actually not designed against a prediction defense, i.e. randomized smoothing, but transformations and distortions.

- Unless I misunderstand the results, Table 1 and 2 seem to only aggregate over less than 100 examples per dataset and it may take up to ~5000s for one example in CIFAR. I understand that the bottleneck is that the verifier is usually resource-consuming. If that is the case, the authors may need to convince the readers under what circumstances this trade-off between resource and probably-robustness is worthwhile compared to the fast empirical approaches. 

3. Writing. I find the writing of the method part is well-organized and polished, which makes me enjoy the reading of the approach. However, the experiment part is relatively dense and sometimes even difficult to read when a lot of notations and symbols appear in the paragraph without sufficient explanations to remind the reader what they refer to. Also, it would be best to add explanations to notations in the captions of figures and tables so the reader does not have to search for what is measured in the table. 

[1] Athalye, A., Engstrom, L., Ilyas, A., & Kwok, K. (2018, July). Synthesizing robust adversarial examples. In International conference on machine learning (pp. 284-293). PMLR.

[2] Qin, Y., Carlini, N., Cottrell, G., Goodfellow, I., & Raffel, C. (2019, May). Imperceptible, robust, and targeted adversarial examples for automatic speech recognition. In International conference on machine learning (pp. 5231-5240). PMLR.

summary_of_the_review: Overall I incline to a weak rejection at this stage of the reviewing process but I am open to any discussions. The reasons that prevent me from giving higher scores are the insufficient descriptions of the motivations and the current way the experiment sections are written with, which I have mentioned in my main review.
review_title: null

final_score: rating: 6: marginally above the acceptance threshold
review_content: summary_of_the_paper: The main contribution of the paper is a framework that will output a large batch of adversarial examples, assuming access to a few black-box mechanisms.
main_review: The term "provably robust" appears misleading; there is no theory showing that the examples must be adversarial.

While authors highlight that there are massive amount of adversarial examples (say $10^{573}$) produced by the algorithms, such number seems really dependent on particular problems while lacking a theoretical justification.

On the novelty of the algorithms, I feel it relies many black-box components and their properties; which lowers the technical contribution if the work.


**Updates after discussion**

I agree that the paper brings out interesting ideas and the experimental results are convincing. However, I also feel authors need to tune down the contributions on the theoretical part because many of the guarantees hinge on black-box components that are leveraged from prior works.
summary_of_the_review: See above.
review_title: null

Meta-review: In this paper, authors introduce and study provably robust adversarial examples. Reviewers had mixed thoughts on the work. One reviewer mentioned that the "provable" robustness is somehow overstated in the work: looking at the title and abstract, it sounds like the paper develops a new algorithm that is guaranteed to be robust, but in reality the robustness hinges on the black-box verifiers (which is acknowledged by the authors during discussion). I agree with this. This should be more clearly stated in the work. I strongly suggest authors to calibrate exaggerated statements of contributions in the revised draft. Having said this, reviewers liked the the experimental study of the paper and found it to be comprehensive and convincing.
Decision: Accept (Poster)