Venue: ICLR 2023 Conference

Reviews:

final_score: rating: 8: accept, good paper
review_content: summary_of_the_paper: The paper introduces a novel GPU-optimized verifier (FGV) for geometric transformations [1]. This verifier enables training using a sampling-based [2] robust classification loss leading to robust networks that are efficiently verifiable with the FGV. For small datasets (MNIST / CIFAR10), the proposed algorithm is orders of magnitude faster with comparable or better certified accuracy when compared to the state of the art. It also demonstrates non-trivial certification results on larger datasets (Tiny-ImageNet/Udacity self-driving car) for the first time.

[1] Rotations, translations, scaling, shearing, changes in contrast and changes in brightness
[2] Rather than computing the robust loss across the full input domain, the method computes the worst-case loss for a small subset of the input domain.
strength_and_weaknesses: Well written paper with all the details required to reproduce the result. Improves verification runtime by several orders of magnitude while matching or improving on robust accuracy, via a novel GPU-accelerated verifier.

A minor concern I have is around the hyperparameter $\nu$. The schedule of values for these hyperparameter are provided in the Appendix, but it's not clear to me how the work arrives at these values in the first place. Referencing Table 5, $\nu$ does not have a clear relationship to the size of the original domain. If hyperparameter tuning was used to determine the appropriate value of $\nu$, this should be reflected in the main body - since that would increase the amount of time actually required for training and verification.
clarity,_quality,_novelty_and_reproducibility: ### Clarity
Well written overall, with good flow and clear definitions.

Some questions:

Q: How do we define the output for geometric transformations (any rotation, any translation, shrinking, any shearing) that move some parts of the image out of the frame and leave some areas of the frame with no corresponding source pixel in the image? This does not have a bearing on your method per se, but doesn't seem to be defined either in the main body or the Appendix.

Q: Are interpolated transformations bijective? Otherwise, how do you handle this? My toy example are the following matrices:

```
1 0
0 1

0 1
1 0
```

When 'rotated' by 45 degrees, they seem to yield the same output:

```
0.5 0.5
0.5 0.5
```

When rotating this output matrix by another 45 degrees, which of the original matrices should you obtain?

Again - this is not necessarily an issue with your method (but it does complicate checking that the math is correct)

### Quality

Improves on the state of the art by several orders of magnitude in runtime (for a problem that is of interest to the community) and matching or improving on certified accuracy.

### Novelty

Clearly novel verifier, and novel loss (albeit one that is a variation on existing robust losses).

### Reproducibility

The evaluation section (and additional details in the Appendix) provides all the information necessary to reproduce the results. (For example, the work specifies the exact hardware used and the architecture of the networks verified).

---

Separately from the comments above, a minor nit: I don't think that the (low probability) susceptibility of probabilistic guarantees to false negatives for verification is so serious to be 'not permissible'. What's a real-world use case under which such false negatives would cause a problem? Some thoughts:

- In the case of offline evaluation on a dataset, the low rate of false negatives should not be a problem.
- In the case of determining online for a particular scene (say, validating stop sign detection in the driving context), having a deterministic method that verifies at a low rate that the stop sign detected is robust to adversarial examples seems just as bad as a probabilistic method that verifies at a high rate ...

Perhaps I'm missing something here. I'd be interested to hear your thoughts

summary_of_the_review: This paper is a clear accept. It introduces a novel GPU-accelerated verifier FGV for geometric transformations (the idea of using the GPU for verification is not novel, but applying it to geometric transformation is), allowing for a certifiable training approach that results in networks that are robust and verifiable via FGV. My only concern is that there does not seem to be a principled way to select the domain-splitting hyperparameter $\nu$; this may be something that has to be selected on a dataset-by-dataset basis.
review_title: null

final_score: rating: 8: accept, good paper
review_content: summary_of_the_paper: This paper deals with training neural network to be robust to geometric transformations of the inputs. Here, robustness is taken to mean *certified* robustness, which can be formally proven, even in the worst case scenario.

The contribution are two-fold:
- Improvements in terms of speed of evaluating bounds on the output of the network given that the input is subject to geometric transformations.
- Using the speed-up in verification, it becomes feasible to include the robust loss into the training objective, in order to train the network to be certifiably robust, which will make it easier to verify.

The speed up of the verification is achieved by:
- Relying on input splitting to only consider *small* perturbations, such that for each pixel, only a small number of original image pixels can contribute to the interpolation. This has two impacts: the bounds produced are tighter (because the bound is taken over only a small number of pixel), and the transformation can be represented using a very sparse representation, which can make it efficient.
- Batching. During training, the sampled transformation range is applied to *all* of the elements in the batch (it's not a different transformation per sample), which means that the computation of the interpolation coefficients is amortized over the batch. I assume that the same is done at verification time, where a batch of test samples are verified at the same time, and the same "slice" of the input domain is verified for all the images at the same time.


strength_and_weaknesses: # Strength
The problem studied is quite an important one as geometric perturbations are a more realistic specifications than $\mathcal{L}_p$ bounds.
The paper is clearly written, with proper background being given for the problem studied (geometric perturbations, robust objectives), which makes it easy to follow along. The annotated Algorithm 1 is easy to follow, allowing for easy re-implementation by other people, and the running example of Appendix B is also useful for understanding.
The empirical results are quite convincing, and evaluated on a wide range of datasets and specification.


# Weakness - Things to improve.
- There is a lack of precision as to how bounds are propagated through the network. The authors describe very clearly how to propagate bounds through the geometric transformation, but then only describe that they use auto_lirpa to propagate through the network, without describing which algorithm they are using. The text after Definition 5 seems to indicate that this might be IBP, but it would be good to be clear on whether that's the case (is it the same both at training and verification time?)
- This is only a suggestion, but after reviewing the paper, I think what one of the things that the authors should highlight more is how different their method is from the most comparable works (Balunovic et al.) and (Mohapatra et al.). Both of these work go through the trouble of deriving bounds that are **explicitly dependent on $\theta$**, so that they can propagate linear bounds that are dependent on $\theta$. This paper completely circumvents that problem by using worse bounds which do *not* depend on $\theta$. It seems to me like this is an integral part of what makes things so efficient: given that you're going to chop up the input space in such tiny sub-intervals anyway, there is no reason to have super representative bounds.
- More generally, I think that the ablation study in 5.3 is the weakest part of the paper. The speedup number presented are impressive, but it seems to me that the comparison is a bit unfair, if the baseline method is not batched and operates on CPU rather than GPU. By all means, the author should provide these results but they also should include a runtime for their method under similar conditions (batch size of 1, running on CPU). I think that these would highlight clearly what the contribution is (parallelizing, vectorizable). As it is, this ablation study is not ablating anything, it's just comparing to a baseline. I'll clarify that even if the severely handicapped version of their algorithm is not outperforming Semantify-NN, that is still an acceptable result and that highlighting what choices need to be made to enable certified training is very interesting.
- I think the authors are missing a more detailed discussion of the verifiable robustness to rotation of (Singh et al.,  2019). It is cited as verifying the robustness against norm-based adversarial perturbations, but that paper actually also contains discussion of robustness to rotation, using exactly the same type of bounding through adversarial transformation.
clarity,_quality,_novelty_and_reproducibility: ## Quality
The paper achieves great empirical results, on an important problem, by proposing a simple solution. 

## Clarity
The paper is very clear in its explanation of their algorithm, and presents itself correctly in the context of the existing literature.

## Originality
The idea is relatively simple, combining the concept of certified training with the specification of robustness to geometric transformation, but the solution proposed to enable this combination is definitely novel.

## Minor note:
- In Algorithm 1, I assume that line 17 should be a call to the `MakeInterpGrid` procedure defined above?

summary_of_the_review: The paper provides a good solution to enable fast propagation of bounds through geometric transformations at training time, enabling certified training against geometric transformation. This simple idea, which is well explained and thoroughly evaluated leads to good empirical results.
review_title: null

final_score: rating: 6: marginally above the acceptance threshold
review_content: summary_of_the_paper: This paper introduces a framework to improve and certify robustness against certain geometric perturbations. The main contribution lies in the parallelization of geometric transformations and their inverses. These improvements enable efficient training as proposed in the paper, as well as efficient LiRPA verification. The conducted experiments demonstrate speedup up to multiple orders of magnitude. 
strength_and_weaknesses: It is an interesting idea to improve the scalability of the formal verification algorithms by accelerating / parallelizing perturbations. The appendices have also provided some additional insights. 
Weaknesses: 

1. The algorithm 1 as a core contribution would perhaps need more motivation and explanation. For instance, one could further modularize the big chunks of the algorithm into smaller functions with better defined purposes and input/output. Furthermore, it is not clear to me how this algorithm is better parallelizable than the standard methods. The paper could have been much stronger if this point had been highlighted. But since I'm no expert in algorithm efficiency and have probably missed certain aspects, I'm open to other reviewers' opinion. 

2. To be more self-contained, perhaps one could include a small recap of the LiRPA. 

3. I’m wondering why PGD+DeepG is expected to produce SoTA performances, since PGD is gradient based and DeepG geometric. The authors might want to include references that also make use of / explain this specific design. 

clarity,_quality,_novelty_and_reproducibility: The paper is well structured and easy to follow.
The novelty, to the best of my knowledge, lies in the parallelization of geometric perturbations that rely on interpolation operations. The proposed training loss is however straightforward and the certification is performed using auto LiRPA. 
The authors promise that the codes will be made available upon publication. 

summary_of_the_review:  In general this is a sound paper with an interesting idea but limited novelty. This could be improved, however, if the main contribution, the parallelization, could be elaborated.
review_title: null

final_score: rating: 6: marginally above the acceptance threshold
review_content: summary_of_the_paper: This paper certifies the robustness of the neural network under geometric transformations. While L2 norm bounded certification has been used in training to further improve the certification bound, no one has used this in geometric transformations. Following the established GPU accelerated certification method, this paper can speed up the geometric robustness.
strength_and_weaknesses: Strength:
1. This paper is the first one that uses GPU accelerated training for certified robustness against geometric transformations. 

2. The paper conducts an extensive study for certifying different models and datasets.


clarity,_quality,_novelty_and_reproducibility: The paper is clear, of good quality. The novelty is fair. Code is not provided, thus it is a little questionable that the paper can be reproduced.
summary_of_the_review: I do not work in the certification of neural networks, the results read solid in speed up and improving the geometric transformation certification. Thus I recommend for acceptance.
review_title: null

Meta-review: metareview:_summary,_strengths_and_weaknesses: The authors develop a technique to obtain certified robustness against geometric transformations (like rotations) of inputs to image classifiers, developing an accelerated verified that can run on a GPU.

Strengths:
1. Paper is well written and experiments are convincing.
2. The technique has efficient GPU implementations and clear psuedocode.

Weaknesses:
1. Details of the bound propagation procedure were unclear in initial versions as pointed out by some reviewers. However, these were adequately addressed in the rebuttal phase.

Hence, I recommend acceptance and encourage the authors to incorporate the (minor) comments from the reviewers in the final version.
justification_for_why_not_higher_score: While the technique developed is clearly effective, it is not yet demonstrated to be effective on SOTA models/datasets.
justification_for_why_not_lower_score: The problem of certified robustness to geometric transformations is well motivated, and the authors develop a rigorous solution backed up by several clever ideas for speeding up verification, enabling efficient implementation.
Decision: Accept: notable-top-25%