Provable Defense Against Geometric Transformations
Authors: Rem Yang
Jacob Laurel
Sasa Misailovic
Gagandeep Singh
Venue: ICLR 2023 notable top 25% (2023)
Keywords: Certified robustness
geometric transformations

Abstract: Geometric image transformations that arise in the real world, such as scaling and rotation, have been shown to easily deceive deep neural networks (DNNs). Hence, training DNNs to be certifiably robust to these perturbations is critical. However, no prior work has been able to incorporate the objective of deterministic certified robustness against geometric transformations into the training procedure, as existing verifiers are exceedingly slow. To address these challenges, we propose the first provable defense for deterministic certified geometric robustness. Our framework leverages a novel GPU-optimized verifier that can certify images between 60$\times$ to 42,600$\times$ faster than existing geometric robustness verifiers, and thus unlike existing works, is fast enough for use in training. Across multiple datasets, our results show that networks trained via our framework consistently achieve state-of-the-art deterministic certified geometric robustness and clean accuracy. Furthermore, for the first time, we verify the geometric robustness of a neural network for the challenging, real-world setting of autonomous driving.

Published as a conference paper at ICLR 2023
PROVABLE DEFENSE AGAINST GEOMETRIC TRANSFORMATIONS
Rem Yang', Jacob Laurel', Sasa Misailovic', Gagandeep Singh 1.2 University of Illinois Urbana- Sibana-Champaign VVware Research (remyang2, jlaurel2, mi sailo, sgnds]@iiil edu
ABSTRACT
Geometric image transformations that arise in the real world, such as scaling and rotation, have been shown to casily deceive deep neural networks (DNNs). Hence, training DNNs to be certifiably robust to these perturbations is critical. However, prior work has been able to incorporate the objective of deterministic certi- fied robustness against geometric transformations into the training procedure, as existing verifiers exceedingly slow. To address these challenges, we propose the first provable defense for deterministic certified geometric robustness. Our framework leverages novel GPU-optimized verifier that can certify images be- tween 60x to 42,600 faster than existing geometric robustness verifiers, and thus unlike existing works, is fast enough for use training. Across multiple datasets, our results show that networks trained via our framework consistently achieve state-of-the-art deterministic certified geometric robustness and clean ac- curacy. Furthermore, for the first time, verify the geometric robustness of neural network for the challenging, weal-world setting of autonomous driving.
INTRODUCTION
Despite the widespread success of deep neural networks (DNNs), they remain surprisingly suscep- tible to misclassification when small adversarial changes are applied to correctly classified inputs (Goodfellow et al. 2015 Kurakin et al. 2018). This phenomenon is especially concerning as DNNs are increasingly being deployed in many safety-critical domains, such autonomous driving (Bo-
jarski al. 2016 Sitawarin al. 2018) and medical imaging (Finlayson et al., 2019).
As result, there have been widespread efforts aimed at formally verifying the robustness of DNNs against norm-based adversarial perturbations (Gehr et al.) 2018; [Singh et al.) [209 [Weng et al. 2018 Zhang et al. 2018) and designing novel mechanisms for incorporating feedback from the verifier to train provably robust networks with deterministic guarantees (Gowal et al.) 2019 Mirman et al.,
2018 Xu et al. 2020 Zhang al. 2020). However, recent works (Dreossi et al. 2018; Engstrom ct al. 2019: Hendrycks & Dietterich [2019] Kanbak et al. 2018) Liu et al. 2019] have shown that geometric transformations which capture real-world artifacts like scaling and changes in contrast can also easily deceive DNNs. No prior work has formulated the construction of a deterministic provable defense needed ensure DNN safety against geometric transformations. Further, existing deterministic verifiers for geometric perturbations (Balunovic et al. 2019 Mohapatra et al., (2020) severely limited by their scalability and cannot be used during training for building provable de- fenses. Probabilistic geometric robustness verifiers (Fischer et al. 2020 Hao et al., 2022 Li et al., 202T) are more scalable but may be inadequate for safety-critical applications like autonomous driv- ing, since they may falsely label an adversarial region as robust. These limitations have prevented the development of deterministic provable defenses against geometric transformations thus far.
Training networks to be certifiably robust against geometric transformations carries multiple challenges that do not arise with norm-based perturbations. First, geometric transforma- tions are much more difficult to formally reason about than é, perturbations, unlike an b,lbal the adversarial region of a geometric transformation is highly nonuniform and cannot be directly rep- resented symbolic formula encoding convex shape. Computing this adversarial input region for geometric perturbations is indeed the main computational bottleneck faced by existing geomet- ric robustness verifiers (Balunovic et al. 2019 Mohapatra et al. 2020), thus making the overall
Challenges.

---

Published as a conference paper at ICLR 2023
verification too expensive for during training. Hence, training DNNs for deterministic certi- fied robustness against geometric perturbations requires not only formulating the construction of a provable defense, but also completely redesigning geometric robustness verifiers for scalability.
This Work. To address the outlined challenges, we propose Certified Geometric Training (CGT), framework for training neural networks that are deterministically certified robust to geometric transformations. The framework consists of (1) the Fast Geometric Verifier (FGV), a novel method perform geometric robustness certification that orders of magnitude faster than the state-of-the- art and (2) computationally efficient loss functions that embed FGV into the training procedure.
We empirically evaluate our method the MNIST (LeCun al. 1998). CIFARIO (Krizhevsky 2009). Tiny ImageNet (Le & Yang 2015), and Udacity self-driving car (Udacity) 2016) datasets to demonstrate CGT's effectiveness. Our results show that CGT-trained networks consistently achieve state-of-the-an clean accuracy and certified robustness; furthermore, FGV is between 60 x to 42,600 faster than the tfateoof-the-ar verifier for certifying each image. We also achieve several breakthroughs: (1) FGV enables to certify deterministic robustness against geometric transfor- mations on entire test sets of 10,000 images, which is more than 50x the number of images over existing works (100 in Balunovic et al. (2019) and 200 in Mohapatra et al, (2020)); (2) we are the first to scale deterministic geometric verification beyond CIFARIO; and (3) we are the first to ver- ify neural network for autonomous driving under realistic geometric perturbations. Our code is publicly available at
2 RELATED WORK
Geometric Robustness Certification. Certification of geometric perturbations (such as image ro- tations scaling) going beyond f--norm attacks have recently begun to be studied in the literature. There are two main approaches to formally verifying the geometric robustness neural networks: deterministic and probabilistic. Most recent works geometric robustness verification use ran- domized smoothing-base bbased techniques to obtain probabilistic guarantees of robustness (Fischer et al.) 2020 Hao al., 2022, Li et al. 2021). While these approaches can scale to larger datasets, their analyses are inherently unsound, i.c., they may falsely label an adversarial region as robust. For safety-critical domains, this uncertainty may be undesirable. Furthermore, such guarantees are ob- tained over smoothed version of base network, which at inference time requires sampling (i.e., repeatedly evaluating) the network up to 10,000 times per image, thereby introducing significant runtime memory overhead (Fischer et al.) 2020). Our work focuses on deterministic verification, whose analysis is always guaranteed to be correct and whose certified network incurs no overhead during inference. In particular, this type of certificate always holds against any adaptive attacker. However, the existing deterministic geometric robustness verifiers (Balunovic et al. 2019 [Mhha patra et al. 2020) exceedingly slow and thus unsuitable for training, due to the high cost of abstracting the geometric input region (even before propagating it through the network). [Singh et al. (2019) study deterministic robustness against rotations, but their results are subsumed by Balunovic et al. 2019). While some works have focused on scaling verifiers (Müller et al. 2021 2020 they have not targeted geometric robustness as we do.
Xu et al.
Provable Defenses Against Norm-based Perturbations. Prior works (Gowal et al. 2019 Mirman
al., 2018 Xu et al.) (2020] Zhang et al., 2020) incorporate verification explicitly into the training loop so that the trained networks become easier to verify. Typically, this task is accomplished by formulating a loss function that strikes a balance between the desired formal guarantees (i.e., high certified robustness) and clean accuracy (i.e., the network's accuracy on the original dataset). To ensure quick loss computation over a large set training images, interval bound propagation (IBP) (Gowal et al. 2019; Mirman et al. 2018) is the most popular technique. However, previous perturbations, which do not capture the highly nonuniform
IBP works mainly consider adversarial input regions that characterize geometric transformations.
BACKGROUND
We denote neural network as function f: Cx R from H W image with C channels to n, real values. We focus on feedforward networks, but our approach is general and equally applicable to other architectree. Let or CxxH denote input image and y denote its
2

---

Published as a conference paper at ICLR 2023
corresponding label. For the remainder of the paper, write interval variables with tilde: e.g., [2, Ø = {I : x S x I Ø} is an interval with x and as lower and upper bounds, respectively. First, we detail the geometric transformations that our work considers.
3.1 GEOMETRIC TRANSFORMATIONS
A geometric image perturbation is a function P: RC x R + RCCHHW which takes an input image I and parameters (e.g,, angle of rotation, amount of brightness), then produces the geometrically perturbed image z'. We consider interpolated transformations rotation, translation, scaling, and shearing and pixelwise transformations - contrast and brightness. For ease of expres- below) apply independently to each image channel, we write Zi to denote z's pixel in the 7th row and شHh column of an arbitrary channel.
sion, since these transformations (Eqs. and [
Interpolated Transformations. Interpolated transformations involve an affine transformation on each pixel's s row and column indices, followed by an interpolation operation. As these operations are performed in the 2D plane, first interpret the row and column indices (i, as points (u, v) IR? where the u-axis is the horizontal axis and the v-axis is the vertical axis. Here, we define functions which convert zero-indexed i. indices
(n(()) j (W 1)/² and (i) (H- 1)/2 to u, U coordinates with respect to the center of an H x W image. Let Tg: : R2 + TR. be an in- vertible affine transformation (e.g., rotation, translation) parameterized by 0 (e.g., rotation angle, amount of horizontal shift). The equations for each affine transformation are given in Eqs. [3 in Appendix A To compose multiple perturbations, we compose their respective affine transforma- tions; for example, scaling by A. rotating by ş, then shearing by y results in the transformation To u) (IThear Trrotate Txele)(u, v) where 0 (X, T
(p, 7). Having converted row-column indices to IR??, we compute for each location (ou()), (i)) the (real-valued) coordinate that maps T ((..(i) & (i)), where Th is the inverse transformation. Since these transformed coordinates may not align exactly with integer-valued pixel indices, must interpolate. We consider the bilinear interpolation kernel of Jaderberg et al. (2015), given as:
to this location under TG; we can obtain this coordinate as (u',v')
H-1W-1
(u v)
Σ
Σ
In.m max 1,10-111111111 1 1 max(0, 1 1-1v -/w (dn(m))
(1)
n= m=0
The value of each pixel in the interpolated image is then:
2/. (T, (.
Pixelwise Transformations. The cumulative effects of contrast and brightness acting on the pixel Fify given by the respective contrast and brightness perturbation parameters a, E IR, as de- scribed in Balluoovic et al. (2019;; et al. (2020):
2 = min (1, max (0, (1 + a) Fij + B))
3.2 INTERVAL BOUND PROPAGATION
For each pixel in the input and each neuron in the DNN, verification with interval bound propaga- tion (IBP) (Gowal et al. 2019) associates an interval bounding its minimum and maximum values. A sound verifier propagates intervals through the network from the input the output layer by evaluating the network's 's layers using interval arithmetic; we detail these operations Appendix
3.3 CERTIFYING GEOMETRIC ROBUSTNESS USING IBP
We now show how to certify the geometric robustness of classification and regression networks.
Certified Classification Robustness Against Geometric Transformations. Given an interval f enclosing the set of possible perturbations on the input and classifier f, we denote the worst-case output vector as (ā)), where (interpreting all operations via interval arithmetic) the correct class's entry is the lower bound and all other entries are the upper bounds of the network's output:
(0) (z) and f5(8) = (+) Vj E 2,,2,... ... n.o \ {v)
3

---

Published as a conference paper at ICLR 2023
We say that f is certifiably robust for ă if, even in the worst case, network classification is correct: y arg max; fz()). To certify geometric robustness image requires computing its bounds the range of geometric perturbation parameters. and the geometric perturbation P is interpreted over interval arithmetic. However, for a given range of perturbation parameters 0 for which we wish to verify robustness, the interval width 0 2 may be too large for the direct evaluation of (z(zz, 0)) to yield bounds that are precise enough for successful certification. Hence, like other geometric robustness verifiers (Balunovic et al. 2019 Mohapatra et al. 2020), we employ parameter splitting.
still guarantee that the
- P(x, 0), where 0 [ 0) is an interval vector bounding
We subdivide the entire range of parameters 0 into K smaller disjoint intervals {01,02 .2. 0x) where 0 U 0g. and certify each split 0g independently. If verifying all splits succeeds, then certification holds on the entire parameter range 0. As interval bounds are constants and not symbolically depend the input parameters (unlike DeepG (Balumovic et al., 2019)), propagating these bounds is highly efficient and can be done on large number of parameter splits for improved precision. Accounting for splitting, we say that f is certifiably robust for P(x. 0) if:
arg max f((((r, Ak E ( K)
(5)
Certified Regression Bound Against Geometric Transformations. Distinct from classifiers, as regression tasks do not have strict notion of correctness, our goal is to verify whether network's outputs are within range close to the ground truth. Hence, our certification problem is to directly bound the network outputs. For regression network f (interpreted over interval arithmetic), the certified output range over the input P(x,0 0) is the smallest interval containing the union of all splits' output bounds:
k U (((((((,0))) k=1
(6)
CERTIFIED GEOMETRIC TRAINING
We now describe the formulation of our provable defense and fast geometric verifier (FGV) that comprise our training framework for certified geometric robustness.
4.1 ROBUST LOSS FOR CLASSIFICATION AND REGRESSION NETWORKS
Training Classification DNNs. The key to incorporating geometric robustness guarantees into training lies in formulating certification as part of the loss function. Since represents the worst- case classification output under range of perturbed inputs, the parameter updates toward obtaining provably robust DNNs. To account for parameter splitting during certification (which is unique to our geometric setting), formulate enforce local robustness at the level of individual input splits. To certify the network across the entire desired range = [0. 0). we enforce this local property across all splits. Furthermore, similar other works on certified training, we also need enforce high clean accuracy. This yields the following formulation for the ideal robust classification loss:
use it in the training loss to guide
training loss to
Σ - (f((((,)))))
Le((,,)) = k- - +
where é can be any classification loss function (we use the cross-entropy loss) and E [0, 1] governs the relative weighting between the clean accuracy and geometric robustness terms (with higher k prioritizing clean accuracy).
In practice, the loss in Eq. is too computationally expensive, since the runtime scales linearly with the number of splits, which often needs to be large to ensure precise certification. As remedy, we instead enforce the robustness property stochastically using data augmentation in conjunction with randomized sampling of interval splits. We uniformly sample scalar perturbation amount
0 (1,00) 0) and compute local interval split 0,
v. + v). where is hyperparameter (0
4

---

Published as a conference paper at ICLR 2023
vector governing the interval size of each perturbation parameter. We then compute the tractable robust classification loss as:
[= = (( ()), + -x) ( ((f(P(s)))))))))))))) 01)).)
(8)
Since we sample different 0 for each mini-batch of training samples, this approach will, on av- erage, effectively enforce local robustness over the entire parameter range (hence leading to global robustness). As in prior works (Gowal et al.) 2019 Xu et al.] 2020; Zhang et al.] 2020). we can vary x with the training iteration, temporally changing the weighting between clean accuracy and robustness. The hyperparameter vector is akin to in the loo -orm case, but it governs the size of a geometric ball P(x, 0t) rather than an e-ball; note that is vector, since the interval size corresponding to each geometric transformation may be different. We show that this hyperparam- eter is easy determine. Finally, while this loss function incorporates only IBP propagate the geometric region through the network, it can be easily adapted to other provable training methods like CROWN-IBP (Zaag et al. 2020 by substituting the e-balls in their loss functions with our formulation of local geometric balls.
Training Regression DNNs. Since our goal is minimize both the width of the certified output bound as well as its distance to the ground truth, the ideal scenario would be when the certified lower and upper bounds coincide at the ground truth. Hence, we can essentially treat the certified bounds as worst-case network outputs and minimize both the lower and upper bounds' distances to the label. With similar insights gleaned from the classification loss function, we thus formulate the robust regression loss as:
(z. =K ((.(:))=x(((((((t.))) 0)). + (1- (1)))(,)))).)) + (((((((x))))
(9)
2
where l can be any regression loss function (we use the mean squared error).
While we experimentally focus on the more common interpolated transformations, our loss for- mulations can also be used for other parameterized semantic perturbations on which interval over- approximations for each pixel can be computed, such as Gaussian blur or color space perturbations.
4.2 FAST GEOMETRIC VERIFIER
A key technical challenge arises during the computation of the loss functions in Eqs. g and we need to perform geometric robustness certification on images at every iteration of traiing. Certi- fication against geometric transformations requires two key steps: (1) obtaining bounds on the set of perturbed images obtainable after applying geometric perturbation P and (2) propagating these bounds through a neural network. The key bottleneck of existing geometric verifiers, which renders them unusable for training, lies in the first step (which we show Section (5.3). This bottleneck stems from the fact that when computing the interpolation, the sequence of arithmetic computa- tions performed at each pixel can be drastically different depending on the pixel location, which has precluded existing approaches from leveraging parallelism. Thus, core part of our contribution is designing a novel and efficient GPU-parallelizabl method for computing interpolated transfor- mations over interval bounds: serving the dual purpose of speeding up verification and being able to utilize these bounds during training. Algorithm presents the pseudocode. Additionally, we also show rumning example in Appendix C.I By default, areas of interpolated image with no corresponding source pixel will be padded with zero, as in Balunovic et al. (2019). However, our algorithm is agnostic to the particular padding mode: we discuss how to handle other padding strategies (e.g., replicating the border pixel values) in Appendix C.2
We mathematically decompose the interpolated transformations (Eqs. [Eqs.[and22 into three parts which are all GPU-parallelizable: computing the coordinates of each pixel location under inverse transfor- mation To calculating the interpolation distances max(0, 1- 10- (n)))maa))) -max(0, 1-lu--lo ou (m))). and fimally obtaining the resulting interpolated images. Our key insight is that the first two steps are solely dependent on the transformation To and the height and width of the images, but not the image pixel values themselves. Hence, these computations need only be done once for a given transforma- tion range, amortizing the cost for any number of images in batch. We now detail each part.
Inverse Coordinates ①. We first determine the inverse coordinates (ū', 8*) T7 (9u(() (1)) for each (i,j) pixel index, where 0 S < H and < < W for images with height H and
5

---

Published as a conference paper at ICLR 2023
Algorithm Fast interval interpolated transformation.
Input: X E [0, 1| a batch N images with dimension x H x W
Tg. an interpolated transformation with interval parameters 0
Output: X' [[0, 1I xxx [o. XXXXXXXX W1. a batch of transformed interval images
I: procedure MAKFINTERPGRIDD H, W. W
2:
(1.7) + (00, 1 :.... H 1]. ,.... W 1])
(u,u) - ( (W 1)/2,
1)/2
① 4:
(U, + (lu u² uu IT
11 tmes
W times
5:
(0', + TT
6:
(U,,V:) (0" wws.eape V rr.sehhaeee 1))
7:
G+ max(0, IV. - VI) O max 1 10, U)
8:
+ count nonzeros dim = (1,2))
- flatten(G)
3
10:
+ gel.nonzero.iddies///
11:
12:
(r,c) (Lía mod HW)/W), mod HW) mod W)
13:
return G2 + (r, (r,,,,0a)
14:
end procedure
15:
procedure INTERPOLATE(K, G.)
17:
(r,c, (, + G2 S (--00 [[.
18:
④
19:
X; < aplit_and S, dim 2, sizes = 2)
20: return X' rey.resh CN, C.H.W)
21:
end procedure
width W. The inverse transformations (shown in Appendix A Eqs. TO 13 are pixelwise, hence this step can immediately be parallelized by defining the matrices U, V (i) and (i, = (1), then applying T over this whole grid of coordinates. Since T is parameterized by an interval range of parameters 0, this inverse transformation and all subsequent arithmetic operations are interpreted via interval arithmetic.
l where (i. =
Interpolation Grid ② and Exploiting Sparsity 3. For each (ū', 8'), we next calculate the terms max(0, (8/ (n))) max - j Φu (m))) in Eq. [ we call these terms interpolation distances and denote them du',s' Here lies key difference between our interpolation formulation and that sequential implementations.
the sequential case, one need only compute _6' for where /' < (n) < Jt and yn where 7' S dm(m) < ūi; this is because all other values of n, m will evaluate to a distance of O. Yet since these ranges of n, ma can be vastly different for each (ū', E'), the only way parallelize the simultaneous computation of these distances for all inverse coordinates to, for each (w', F'), compute di. v for all <
H. S m W. We term these computed distances the interpolation grid G. However, since most of the entries in & will be 0 (i.c., the degenerate interval [0, 0)) typicalyy more than 99% of them we design a custom sparse tensor representation G so that when interpolating, only the nonzero entries will be multiplied Jud n,m only when the distance is nonzero). First, for each nonzero du' .e' we must know its location (i.e., n. m) so that we can multiply its value with the corresponding image pixels in the same location. To do so, we convert Ō to COO (coordinate) format, a 3-tuple of vectors: which stores the nonzero values of G, and r, e which store the nonzero values' row and column indices n, m. However, once actually interpolate across images and obtain the summands zä', Fn.m dii 5 we need to know which summands contribute to the same pixel (i.e., have the same ií' and ε') and should thus be added together; this is challenging since the grid values have been flattened. To solve this issue, we store an additional vector z that records the number of nonzero interpolation distances for each ( i').
with image pixel values (i.e., computing Fn,m

---

Published as a conference paper at ICLR 2023
Obtaining Interpolated Images 4 After calling MAKEINTERPGRID (which only needs to be done once for given set of transformations) and obtaining G. (r, 2), interpolate across any batch of images X. For all batch and channel dimensions, we obtain the pixel values at locations corresponding to the interpolation distances in i (by indexing the last two dimensions of X with r, and elementwise multiply with 인 to obtain S, which contains the values of all summands across all pixels. To recover the final pixel values, we sum the terms belonging to the same pixel (i.e., the gä',E' that have the same i', (') together. To do so, we split the last dimension of Š into HW chunks {he H where each h2 has length 2;; then, each chunk's sum is exactly the final pixel value. Since this last dimension has been flattened to take advantage of sparsity, we reshape it back to dimension x W obtain the final interpolated images.
now efficiently
Finally, we use IBP (during both training and certification) to propagate the computed geometric bounds through the neural network.
5 EVALUATION
We evaluate the effectiveness of CGT over multiple datasets, network architectures, and transforma- tions. We implemented CGT atop PyTorch (Paszke et al., 2019) and use auto_LiRe LPRPA (Xu et al.) 2020) to propagate our computed geometric perturbation bounds through neural networks.
Datasets and Architectures. We evaluate our approach on the MNIST, CIFARIO, Tiny ImageNet, and Udacity self-driving car datasets. The first three are image classification tasks, while the last is regression task that predicts a steering angle given a driving scene image. On MNIST and CIFAR 10, use the same architectures from DeepG (Balunovic et al. 2019) to compare directly with their results. On Tiny ImageNet, we use the 7-layer convolutional network (CNN7) and WideResNet architectures from Xu et al. (2020). On Udacity, we use the classic Nvidia architecture from (oojasik iet al. 2016). Details are in Appendix[D.I
Metrics. Our primary metrics for classifier are (1) its clean accuracy, (2) its certified robustness under geometric transformations, and (3) the certification time on the test set. For a regression network, utilize the analogous metries of (1) mean absolute error (MAB), (2) certified MAE, i.e.. the larger of the certified lower and upper bounds' MAEs, as well as (3) certification time. We also measure per-epoch runtime and GPU memory usage during training (shown in Appendix
Baselines. To the best of our knowledge, training a DNN via PGD (Madry et al. 2018) combined with data augmentation (denoted PGD/A) and certifying with DeepG produces the current state- of-the-art deterministic geometric robustness and accuracy. However, the DeepG verifier does not scale beyond CIFARI0; hence, we compare our approach theirs on just the MNIST and CI- FARI0 datasets, using the sets of transformations from their work. Notably, DeepG only certifies 100 images (due to long runtimes). while we certify full test sets of 10,000 images. The work of Semantify-NN (Mohapatra et al.) (220)) is strictly less precise than DeepG and also only handles a single interpolated transformation (rotation); thus, we only compare certification with DeepG. However, they propose an algorithm compute the interval over-approximation of images under rotation, and we provide an ablation study comparing the speed of Algorithm D to theirs.
Hyperparameters. We show the training and certification hyperparameters in Appendices D.2 and D.3 and explain how to tune these hyperparameters in Appendix D.4
machine with 2.40GHZ 24-core Intel Xeon Silver 4214R CPU with 192GB of main memory and one Nvidia A100 GPU with 40GB of memory. All baseline results were also run on the same hardware for fair comparisons. For WideResNet, we used the same CPU with four A100 GPUs.
Hardware. We trained and certified all networks (except WideResNet)
5.1 MNIST AND CIFARIO
Table I presents the comparison of our approach with DeepG; asterisks denote DeepG certification results over a subset of 100 images (since their approach takes too long to run on the full test set). Over variety of challenging transformations on MNIST and CIFAR10, achieves state-of-the performance. On all MNIST experiments, our certified robustness is sub- stantially higher than DeepG, while attaining comparable clean accuracy. Furthermore, our verifier
approach consistently
7

---

Published as a conference paper at ICLR 2023
Comparison of network certification time and accuracy with the prior state-of-the-art on MNIST and CIFAR1O. We denote R(p) rotation of typ degrees; Tu(Au) and T. (Av)) translation of + pixels horizontally and =vv pixels vertically, respectively; Sc(A) scaling of =X%; Sh(?) shearing of +7%; C(a) contrast change of =a%; and (B3 brightness change of +3 Asterisk denotes that certification was measured on subset of 100 test images.
Table I:
Training Certification Method
Accuracy (%)
Certified (%)
Cert. Time per Image (s)
FGV Speedup
Dataset
Transformations
PGD/A DeepG
99.1
86.0"
19.12
R(30)
CGT + FGV
99.1
94.2
0.00045
42623x
PGD/A DeepG CGT + FGV
99.1
77.0"
367.82
T2(2)
MNIST
99.2
89.8
0.0090
40949 x
Sc(5), R(5),
PGD/A DeepG CGT + FGV
99.3
34.0"
155.24
C(S), B(0.01)
99.1
92.6
0.0048
32563
Sh(2), R(2), Sc(2), C(2), B(0.001)
PGD/A DeepG CGT + FGV
99.2
72.0"
71.72
99.1
96.3
0.024
x
PGD/A + DeepG
71.2
65.0"
78.18
R(10)
CGT + FGV
80.5
63.2
0.465
168x
CIFARIO
PGD/A DeepG CGT + FGV
68.5
39.0"
18.92
R(2). Sh(2)
70.1
51.0
0,263
72x
Sc(1), R(). C(1), B(0.001)
PGD/A DeepG CGT + FGV
73.2
43.0"
163.26
71.3
42.3
2.725
60x
several orders of magnitude faster. On CIFARIO, we achieve significantly better tradeoff between certified robustness and accuracy than the baseline for the first two cases, while obtaining similar results the third transformation set; certification time considerably lower than DeepG. For the first and third CIFAR10 110 experiments, we attain 65% and 49% on the subset of 100 images used by DeepG (which are equal or better than their results), while the certifiability evaluated over the whole test set (presented in the table) is slightly lower. These results show that rather than using the input set to certify networks not trained to be provably robust, is more effective to explicitly train networks to be certifiably robust and verify them with less pre- cise but faster verifier (with large number of parameter splits). Using our custom loss formulation in Eq. [ yields the best results on our verifier; Table 6 in Appendix F. shows that other existing lo based training methods (which cannot incorporate geometric bounds) do not perform as well.
more precise abstractions
5.2 SCALABILITY TO LARGER DATASETS AND MODELS
Our work can scale to larger datasets like Tiny ImageNet and real-world tonomous driving dataset where previous approaches do not.
Table 2: Certified geometric robustness and accu-
racy on Tiny ImageNet networks. Certification is performed with FGV.
Table presents our results on Tiny- ImageNet networks trained for the shear, scale, and rotation transformations. For both networks, proach preserves a relatively high clean ac- curacy while obtaining substantial robust- ness guarantees. For context, in Xu et al.) (2000) for robuustess with e 1/255, they attain 21.6% accuracy and 12.7% cer- tified robustness on CNN7 and 27.8% accu- racy and 15.9% certified robustness WeteResNet. Certification time is still fast, even though the images are much higher-definitie than MNIST and CIFAR1O, showcasing FGV's scalability. We also that our approach scales well to large state-of-the models like NeteResNet.
Network
Transforms
Acc. (%)
Cert. (%)
Cert. Time per Image (s)
Shear (2%
27.3
18.7
0.059
observe that our ap-
CNN7
Scale (2%)
26.1
15.2
0.057
Rotate (5%)
26.0
13.1
0.285
Shear (2%)
35.5
25.7
0.214
Wide ResNet
Scale (2%)
33.1
21.3
0.205
Rotate (5")
32.2
17.4
1.006
8

---

Published as a conference paper at ICLR 2023
Figure I:
Visualization of standard and certified steering angles for the CGT-trained network on test-set driving scenes. Green line is the ground truth, blue line is the network prediction, and red hue is the certified bound on the network's 's prediction within =2 rotation of the input.
Next, we demonstrate, to the best of our knowledge, the first study of provable defense in real-world setting against realistic geometric transformations on the Udacity dataset. The neural network takes as input high-definition RGB 3 66 x 200 images, and our task is accurately predict the correct steering angle and tightly and provably bound the range of angles under geometric transformations. Specifically, we consider a transformation of =2 rotation.
While there is an inherent tradeoff be- tween certified robustness and network per- formance on the previous datasets, we find that, surprisingly, here we can scale our ap- proach to obtain both high certifiability and improve network performance at the same time. To demonstrate this phenomenon, train a network with (1) just the regular mean-squared error loss and input data aug- mentation of +-20 rotation (Regular), (2) the first method with the addition of dropout on linear layers (Dropout), and (3) our CGT for- mulation in Eq.
Table 3: Mean absolute error and certified bounds (lower is better) for rotation range of 2 on self- driving networks.
Training Method
Std.
Cert. MAE
Cert. Width
Cert. Time per Image (s)
MAE
Regular Dropout CGT
6.07
97.56"
180"
0.11
4.85
96.65
178"
0.12
5.36
8.05
5.43
0.11
Table 3 presents our results for the standard and certified errors of these training methods (lower is better). An interesting observation is that this task is prone to overfitting: we can observe that adding dropout significantly improves the standard error of the network. In this case, training with CGT's interval bounds actually acts as an effective regularizer that serves the dual purpose of combatring overfitting and enforcing certifiability. Training without CGT leads to trivial certification bounds (i.e., the certified steering angle can be anywhere in +90%); conversely, training with CGT yields very tight certified bounds. Fig. T shows visualizations of the CGT-trained network's predictions and certified bounds.
5.3 ABLATION STUDIES
Algorithm for Interval Interpolated Transformation. In Appendix E.3 we compare Algorithm to Semantify-NNi -N''s algorithm for computing interval rotation bounds. We show that our algorithm is orders of magnitude faster, hence enabling our scalable training and verification approaches.
Effect of Parameter Split Size. We train CIFAR10 and Tiny ImageNet network with various sizes of the hyperparameter and discuss how it affects certified and clean accuracy in Appendix E.2
6 CONCLUSION
We proposed Certified Geometric Training (CGT), provable defense that leverages novel fast geometric verifier to improve the deterministic certified robustness of neural networks with respect to geometric transformations. Our experiments across multiple datasets and perturbation sets showed that CGT consistently attains state-of-ther the-art certified deterministic geometric robustness and clean accuracy, while being highly scalable.

---

Published as a conference paper at ICLR 2023
ACKNOWLEDGMENTS
This research was supported in part by NSF Grants No. CCF-1846354, CCF-1956374, CCF-220888,, CCF-2238079, USDA Grant No. AG NIFA 2021-67021-33449, Sloan UCEM Graduate Scholarship, and a Qualcomm Innovation Fellowship.
REFERENCES
Mislav Balunovic, Maximilian Baader, Gagandeep Singh, Timon Gehr, and Martin Vechev. Certi- fying geometric robustness of neural networks. In Proc. Neural Information Processing Systems (NeurIPS), pp. 15287-15297, 2019.
Mariusz Bojarski, Davide Del Testa, Daniel Dworakowski, Bernhard Firner, Beat Flepp, Prasoon Goyal, Lawrence Jackel, Mathew Monfort, Urs Muller, Jiakai Zhang, et End end learning for self-driving cars. arXiv preprint arXiv: 1604.07316, 2016.
Tommaso Dreossi, Somesh Jha, and Sanjit Seshia. Semantic adversarial deep learning. In Proc. International Conference Computer Aided Verification (CAV), pp. 3-26, 2018.
Logan Engstrom, Brandon Tran, Dimitris Tsipras, Ludwig Schmidt, and Aleksander Madry. Explor- ing the landscape of spatial robustness. In Proc. International Conference on Machine Learning (ICML), pp. 1802-1811, 2019.
Samuel G Finlayson, John D Bowers, Joichi Ito, Jonathan L Zittrain, Andrew L Beam, and Isaac Kohane. Adversarial attacks on medical machine learning. Science, 363(6433) 2019.
Mare Fischer, Maximilian Baader, and Martin Vechev. Certified defense to image transformations via randomized smoothing. Proc. Neural Information Processing Systems (NeurIPS), pp. 8404 8417, 2020.
Timon Gehr, Matthew Mirman, Dana Trachsler-Cohen, Petar Tsankov, Swarat Chaudhuri, and Mar- tin Vechev. Ai2: Safety and robustness certification of neural networks with abstract interpreta- tion. In Proc. IEEE Symposium on Security and Privacy (SP), pp. 3-18, 2018.
Ian J Goodfellow, Jonathon Shlens, and Christian Szegedy. Explaining and harnessing adversarial examples. In Proc. International Conference on Learning Representations (ICLR), 2015.
Sven Gowal, Krishnamurthy Dj Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Uesato, Relja Arandjelovic, Timothy Mann, and Pushmeet Kohli. Scalable verified training for provably robust image classification. In Proc. IEEE/CVF International Conference on Computer Vision (ICCV), pp. 1842-4851, 2019.
Zhongkai Hao, Chengyang Ying, Yinpeng Dong, Hang Su, Jian Song, and Jun Zhu. Gsmooth: Certified robustness against semantic transformations via generalized randomized smoothing. In Proc. International Conference on Machine Learning (ICML), pp. 8465-8483 2022.
Dan Hendrycks and Thomas Dietterich. Benchmarking neural network robustness to common corruptions and perturbations. In Proc. International Conference on Learning Representations (ICLR), 2019.
Max Jaderberg, Karen Simonyan, Andrew Zisserman, and Koray Kavukcuoglu. Spatial transformer networks. In Proc. Neural Information Processing Systems (NeurIPS), pp. 2017-2025, 2015.
Can Kanbak, Seyed- Moosavi-Dezfooli,, and Pascal Frossard. Geometric robustness of deep networks: analysis and improvement. In Proc. IEEE/CVF Conference on Computer Vision and Pattern Recognition (CVPR), pp. 4441-4449, 2018.
Diederik Kingma and Jimmy Ba. Adam: A method for stochastic optimization. In Proc. Interna- tional Conference on Learning Representations (ICLR), 2015.
Alex Krizhevsky. Learning multiple layers of features from tiny images. Technical report, 2009.
10

---

Published as a conference paper at ICLR 2023
Alexey Kurakin, Ian J Goodfellow, and Samy Bengio. Adversarial examples in the physical world.
In Artificial intelligence safety and security, pp. 99-112. Chapman and Hall/CRC, 2018.
Ya Le and Xuan Yang. Tiny imagenet visual recognition challenge. CS 23/N, 2013.
Yann LeCun, Léon Bottou, Yoshua Bengio, and Patrick Haffner. Gradient-based learning applied to document recognition. Proc. of the IEFE, 86(1 11:2278-2222 1998.
Linyi Li, Maurice Weber, Xiaojun Xu, Luka Rimanic, Bhavya Kailkhura, Tao Xie, Ce Zhang, and Bo Li. Tss: Transformatioon-peecffi smoothing for robustness certification. In Proc. Conference on Computer and Communications Security (CCS), pp. 535-557, 2021.
Hsueh-Ti Derek Liu, Michael Tao, Chun-Liang Li, Derek Nowrouzezahrai, and Alec Jacobson. Beyond pixel norm-balls: Parametric adversaries using an analytically differentiable renderer. In Proc. International Conference on Learning Representations (ICLR), 2019.
Aleksander Madry, Aleksandar Makelov, Ludwig Schmidt, Dimitris Tsipras, and Adrian Vladu. Towards deep learning models resistant to adversarial attacks. In Proc. International Conference on Learning Representations (ICLR), 2018.
Matthew Mirman, Timon Gehr, and Martin Vechev. Differentiable abstract interpretation for prov- ably robust neural networks. In Proc. International Conference on Machine Learning (ICML), 2018.
pp.
Jeet Mohapatra, Tsui-Wei Weng, Pin-Yu Chen, Sijia Liu, and Luca Daniel. Towards verifying robustness of neural networks against family of semantic perturbations. In Proc. IEEE/CVF Conference on Computer Vision and Pattern Recognition (CVPR), pp. 244-252, 2020.
Christoph Müller, François Serre, Gagandeep Singh, Markus Püschel, and Martin Vechev. Scaling polyhedral neural network verification on GPUs. In Proc. Conference on Machine Learning and Systems (MLSys), pp. 733-746, 2021.
Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, Alban Desmaison, Andreas Köpf, Ed- ward 7. Yang. Zachary Vito, Martin Raison, Alykhan Tejani, Sasank Chilamkurthy, Benoit Steiner, Lu Fang, Junjie Bai, and Soumith Chintala. Pytorch: imperative style, high- performance deep learning library. In Proc. Neural Information Processing Systems (NeurIPS), pp. 8024-8035, 2019.
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. An abstract domain for certi- fying neural networks. Proc. ACM Program. Lang., 3(P0PL):1-30, 2019.
Chawin Sitawarin, Arjun Nitin Bhagoji, Arsalan Mosenia, Mung Chiang, and Prateek Mittal. Darts: Deceiving autonomous cars with toxic signs. arXiv preprint arXiv:1802.066430, 2018.
Udacity. Using deep learning to predict steering angles. self-driving car 2016.
Tsui-Wei Weng, Huan Zhang, Hongge Chen, Zhao Song. Cho-Jui Hsich, Luca Daniel, Duane S. Boning, and Inderjit S. Dhillon. Towards fast computation of certified robustness for relu net- works. In Proc. International Conference on Machine Learning (ICML), pp. 5273-5282, 2018.
Kaidi Xu, Zhouxing Shi, Huan Zhang, Yihan Wang, Kai-Wei Chang, Minlie Huang, Bhavya Kailkhura, Xue Lin, and Cho-Jui Hsieh. Automatic perturbation analysis for scalable certified robustness and beyond. In Proc. Neural Information Processing Systems (NeurIPS), pp. 1129- 1141, 2020.
Huan Zhang, Tsui-Wei Wei Weng, Pin-Yu Yu Chen, Cho-Jui Hsieh, and Luca Daniel. Efficient neural network robustness certification with general activation functions. In Proc. Neural Information Processing Systems (NeurIPS), pp. 4944-4955 2018.
Huan Zhang, Hongge Chen, Chaowei Xiao, Sven Gowal, Robert Stanforth, Bo Li. Duane Boning, and Cho-Jui Hsich. Towards stable and efficient training of verifiably robust neural networks. In Proc. International Conference Learning Representations (ICLR), 2020.
11

---

Published as a conference paper at ICLR 2023
A EQUATIONS FOR INTERPOLATED TRANSFORMATIONS
For each interpolated transformation, we present the equation for its inverse transform T which used instantiate Eq.
Rotation. Parameterized by an angle yp E [0, 27]:
(u, = cos yp
sin yp cos
uu
cos pp + v sin yp
(10)
sin yp
cos yp - u sin [p]
Translation. Parameterized by an amount of horizontal shift Au E and an amount of vertical shift Ao E R:
1u Au Av
Tu.su v)
(11)
1
Scaling, Parameterized by scaling factor X E
TRAS -1:
[w/(+>)) w/(1+
T (u, v)
I+1
(12)
Shearing. Parameterized by a horizontal shearing factor 7 E R:
1
(u,
(13)
0
B INTERVAL BOUND PROPAGATION ABSTRACT TRANSFORMERS
Interval bound propagation (IBP) is a special case of linear relaxation based perturbation analysis (LiRPA), where each neuron's bounds are hyperrectangles. Below, we give recap on how com- pute the bounds for affine (i.e., convolutional and fully connected) layers and monotonic activation functions from Gowal et al. (2019). For a more detailed discussion, we refer the reader Gowal et al. (2019) and Xu et al. (2020).
For neuron (or pixel) [2, z). its bounds after applying an affine layer with weights W and bias b are computed as:
mnt jur
r, 14 +
(14)
where μ = W (3+22 2 + b and r [WI(
For neuron = [2, z]. its bounds after applying a monotonic activation function h: R - R (e.g., ReLU) are computed as:
ient [a{))
(15)
We can obtain final bounds on network's outputs by composing the operations above and propa- gating intervals from the input layer to the output layer.
C ADDITIONAL DETAILS ON FAST INTERVAL INTERPOLATED TRANSFORMATIONS
C.I RUNNING EXAMPLE
We present running example of Algorithm 1 Here, we consider applying scaling of á +.2% 3 images. Per Eq. [2 the inverse transform function for this perturbation is:
T (u,
0.02, 0.02 1+ 0.02 0.02]
[0.98, 1.02 00.98 1.02
We color code the diagrams below, so that information belonging to the same pixel location has the same color.
12

---

Published as a conference paper at ICLR 2023
Lines 2-4: First, create meshgrid of (u, v) coordinates that the inverse transform of all coordinates can be computed in parallel. We obtain:
-1
0
and V
0
0
1
-1 -1
Line 5: Now, apply T to each entry in U, V. Note that since T produces interval coordi- nates, all subsequent operations need to be interpreted via interval arithmetic. We have:
[-1.02, -0.98]
[0. 0]
[0.98. 1.02]
U
Ú'=
[-1.02, -0.98]
[0, 0]
[0.98, 1.02]
[0.98, 1.02]
1-1.02, 00.88
[0. 0J
[0.98, 1.02]
[0.98, 1.02]
[0.98, 1.02]
[0.98, 1.02]
V
[0. 0]
[0. 0]
[0, 0]
[0.98, 1.02]
[-1.02, -0.98]
1-1.02, -0.98]
1-1.02, -0.98]
Lines 6-7: We can now compute the bilinear interpolation grid (i.e., all interpolation distances). For each (ñ', 5') coordinate, we compute 7' U and J' -V, which are both 3 3 interval matrices. As there are 9 inverse coordinates, we end up with two 9 x interval tensors Us and Va (where the ordering of the first dimension is according to row-major order of ū', ě¹). The rest of the operations to compute the interpolation distances are all elementwise; we can thus obtain G max(0, 1
Val) @ max 1 - [Ū2)), shown below. We omit writing entries that are zero (i.e., the degenerate interval [0, 0)).
[0.96. 1.00]
[0.00, 0.02]
[0.98, 1.00]
[0.00, 0.02)
[0.96, 1.00]
[0.00, 0.02]
(0.00,
[0.00, 0.02]
[0.00,
[0.00, 0.02]
[0.98, 1.00]
[0:00, 0.02]
[1.00, 1.00]
[0.00, 0.02]
[0.98, 1.00]
10.00. 0.02)
[0.00, 4c-4]
[0.00, 0.02)
[0.00, 4c-4]
[0.00, 0.02)
[0.96, 1.00]
[0.00, 0.02]
[0.98, 1.00]
[0.00, 0.02]
[0.96, 1.00]
As discussed in Section 4.2, we can see that the region of interpolation is significantly different for each pixel, hence order to parallelize the entire computation across all inverse coordinates, we must interpolate over the entire x 3 range of (u, v) coordinates for each ,'). However, doing so leads to a lot of sparsity in G. which we can now exploit. (With larger images, typically more than 99% of G are zero entries; however, since the image dimension in this running example is small, the sparsity not as great.)
Lines 8-12: We now convert & to our custom sparse format before performing interpolation with image pixels, so that all zero- eroo-muliillications are eliminated. First, we count the number of nonzero entries in each inverse coordinate's matrix:
4
2
2
2
Then, we flatten & (in row-major order) and store it in COO (coordinate) format. We thus obtain an interval vector tē that stores all the nonzero interpolation distances, along with integer vectors r, c which, for each value of w, stores its corresponding row and column index:
10.96. 1.00)
10.00, 0.02]
[0.00, 0.021
10.00,
[0.98. 1.001
[0.00. 0.021
[0.00, 0.02]
[0.96. 1.00]
[0.00, 4e
[0.00. 0.02)
00.88, 1.00)
10.00, 0.02)
[1.00, 1.00)
[0.00. 0.02)
[0.98. 1.00)
[0.00. 0.02)
10.00, 4e
[0.96. 1.00)
[0.00. 0.02)
[0.00. 0.02)
(0.98
[0.00.
10.00 0.02]
(0.66
13

---

Published as a conference paper at ICLR 2023
0
1
0
0
2
1
2
0
O
1
1
2
1
2
0
2 0
0
1
2
1
2
This concludes the procedure Make InteeInterpae InteepGrii (). and we are now ready to use this infor- mation to compute actual interpolated images. Consider a batch of 1000 3 RGB images, X [0, 1]1000X3x3x3, Now, consider the first channel of the first image, {(0 0). which is a x matrix (whose values we randomly select for this example):
.55
.42
x =
.53
.49
.51
.56
.62
.45
Line 18: We multiply each interpolation distance with the pixel value of [0, 0] in the corresponding location; this will yield the values of all summands in Eq. [across all pixels. To accomplish this, we index the image according to the indices stored in (r, c) and elementwise multiply these pixel values
with w. obtaining S = ãē C X [0, 0, c]:
S = [0.53, 0.551
10.00. 0.01]
10.00, 0.01]
[0.00. 2c-1]
[0.19,0.50 0.500
[0.00. 0.011
[0.00, 0.01]
[0.10, 0.42]
[0.00, 2e-11
[0.00, 0.01]
[0.52, 0.53]
10.00, 0.011
[0.49, 0.491
10.00, 0.011
[0.50, 0.51]
[0.00, 0.01]
10.00. 2c-41
[0.54, 0.56)
[0.00. 0.011
[0.00, 0.01]
[0.51, 0.62)
[0.00, 2o-4]
[0.00, 0.01)
[0.00, 0.01]
[0.43, 0.45]
Line 19: Finally, we sum the terms in S that belong to the same pixel location. In the context of the diagram above, this is summing the entries in S that are of the same color. In practice, this color information is encoded in the vector z, which stores, for each pixel location, the number of nonzero interpolation entries; hence, we break S into contiguous chunks such that the length of chunk i (where 0 < 9) is given by 24, and sum all values each chunk, obtaining:
X 10.53, 0.57]
[0.49, 0.51]
[0.40, 0.44]
[0.52, 0.54]
[0:49,
[0.50,
[0.54, 0.58] [0.61, 0.63]
[0.43, 0.47]
Line 20: This vector is then reshaped to a 3 matrix, yielding the final pixel values of X 0] under transformation:
[0.53, 0.57]
[0.49, 0.51]
[0.40, 0.44]
X'
[0.52, 0.54]
[0.49, 0.49]
[0.50, 0.52]
[0.54, 0.58]
[0.61, 0.63]
[0.43, 0.47]
Finally, we remark that this interpolation process is completely independent for each batch and channel. Therefore, to parallelize across multiple images and channels, we simply need to index across all batch and channel dimensions when computing (i.c., let S = w O x(,,,rr))).
C.2 PADDING STRATEGY
To handle other padding techniques (e.g., replicating the border pixels of the in-frame part of the image), our core algorithm remains completely unchanged - all that is needed is a preprocessing step that pads the input image according to the desired padding strategy, and postprocessing step that crops the output back to the original dimensions. We describe these steps in detail below.
Let us assume we have a batch of H W images X, an interpolated transformation Tg. and a desired padding mode st strategy by which to fill in the areas of the interpolated images with no source pixel. First, we determine the number of pixels by which to pad the original H W images. To so, we compute the meshgrid (U, V) and the inverse coordinates (Ū', V") as in I Algorithm Then, the amount of padding required is = [max[] min Ú' min ], max Ú' - max U|, min V min VI, max V - max V- ). In other words, the padding amount is the integer just greater than the maximum distance from that after padding, none of the central H x W pixels will have a value zero after interpolation. Now, we pad X all sides by p pixels according to strategy. This padded batch of images can then be directly fed into Algorithm to obtain batch of transformed interval images X', Finally, to obtain transformed images in the original dimensions, we take central H W crop of X'.
coordinate the border its inverse counterpart; this ensures
14

---

Published as a conference paper at ICLR 2023
D ADDITIONAL EXPERIMENTAL DETAILS
D.1 NETWORK ARCHITECTURES
We detail the network architecture(s) used for each dataset below. We express a convolutional layer as a 4-tuple of (number of filters, kernel size, stride, padding).
MNIST: 2 conv layers 2, 2, {200, 10} neurons. All layers are followed by a ReLU activation, except for the final output layer.
(64, 4, 2, 1)} followed by 2 linear layers with
CIFARIO: 3 conv layers ((32,3, 1,1,, (32,4, 4, 1), 4,4,4,2,1) 1)) followed by linear lay- ers with (150, 10) neurons. All layers are followed by ReLU activation, except for the final output layer.
Tiny ImageNet:
CCNN7: conv layers {(64, 3, 1.),, (64, 1, (128, 3, 1), (128, 3, 1), (128, 3, 2,} followed by linear layers with {512, 200) neurons. Each conv layer is fol- lowed by a batch norm layer then a ReLU activation. The first linear layer is followed by ReLU activation.
WideResNet: Let (2 s) denote the output after feeding through this quence of layers: batch norm with p; features, ReLU, conv(p,, 3, 1),, batch norm with Po features, ReLU, conv(po,
1); let Sp Po; s) denote the output after feeding I into a conv(po, 1, 8, 0). Then, we define a wide basic block as the func- tion (P Po. s) Q= Po. s) + Sp s). The architecture of the network is then: a conv layer (16, 3, 1), W W161,, 160, 1), (160, 320, 2), W3230 640, 2), batch norm, ReL.U, average pooling with a x 7 kernel, then finally a linear layer with 200 neurons.
Driving: conv layers {(24, 5, 2, 0), (36, 5, 2, 0), (48, 5, 2, 0), (64, 1),,, (64, 3, 1, })} followed by 4 linear layers with {100, 50, 10, 1} neurons. All layers are followed by ReLU activation, except for the final output layer. For the Dropout network, we add a dropout layer with p 0.5 after the first linear layers.
D.2 ADDITIONAL TRAINING DETAILS
Training Schedule. We train the MNIST networks for 100 epochs with batch size 256, CIFARIO networks for 120 epochs with batch size 128, Tiny ImageNet networks for 160 epochs with batch size 128 (CNN7) or 400 (WideResNet), and the self-driving network for 50 epochs with batch size first train with only the cross-entropy loss during warm-up period;
128. For the classifiers, warm up for 15 epochs on MNIST and 30 epochs on CIFARIÓ 10 and Tiny ImageNet. For the self- driving network, we directly use Eq. from the start. In order to ensure convergence for the loss, we linearly decay k. from to Ki = 0.5 and employ a linear ramp-up up schedule to slowly increase the value of y from up to final parameter size of vy; we ramp up across 50, 60, 80, and 50 epochs for MNIST, CIFAR10, Tiny ImageNet, and self-driving, respectively. We explain how to tune the hyperparameter My and provide the values of vy for each experiment Section D.4
Data Preprocessing and Augmentation. For all networks, we augment the input images during training according to the set of transformations CIFAR10 and Tiny ImageNet, we also perform random horizontal flips and select random crops of 32 x 32 with padding (for CIFAR 10) and random crops of 56 x 56 (for Tiny ImageNet). At test time, we use a central crop of 56 x 56 for Tiny ImageNet. For the self-driving dataset, we first crop the top of the 480 x 640 input images to 280 x 640, then resize them with bilinear interpolation to 66 x 200; also perform random horizontal flips. For all datasets, normalize input images according to the channel statistics from the train set immediately before the first network layer.
which we want to be robust. addition, for
Optimizer. We use the Adam optimizer (Kingma & Ba 2015) across all networks. For MNIST and CIFAR1O, we use an initial learning rate of 10 3 which we decay by 0.1 at the 80th and 100th epoch, respectively. For Tiny ImageNet, by 0.1 after 120 and 150 epochs. For self-driving, we use an initial learning rate of 10-3, 10.3, which we decay by 0.1 after 20 and 40 epochs. For all networks, we clip gradients at norm of 8.
an initial learning rate of 5 x 10 which we decay
15

---

Published as a conference paper at ICLR 2023
Table Interval sizes of geometric transformation parameters used during training and certification. For experiments with compositions of transformations, the sizes are specified in the same order as the transformations.
Perturbation parameter interval size
Dataset
Perturhations
Training (2py)
Certification (0s- (c)
R(30)
0.5
0.25
T.(2). T,(2)
(0.1,
(0.05, 0.05)
MNIST
Sc(5), R(5), C(5), B(0.01)
(1,0.25, 5, 0.02)
(0.5, 0.125, 5, 0.02)
Sh(2), R(2), Sc(2), C(2), B(0.001)
(0.5, 0.125, 0, 0.002)
(0.25, 0.0625, 0.25, 4, 0.002)
R(10)
0.001
0.0002
CIFARIO
R(2), Sh(2)
(0.02, 0.05)
(0.01, 0.025)
Sc(1), R(I), C(1), B(0.001)
(0.005, 0.005, 0.5, 0.002)
(0.005, 0.005, 0.5, 0.002)
Sh(2)
0.01
0.002
Tiny
Sc(2)
0.01
0.002
ImageNet R(5)
0.005
0.001
Driving
R(2)
0.004
0.001
Table 5: Average and maximum pixel interval widths of geometrically transformed images used for training (for CGT networks) and certification (for all networks).
Training Interval Width
Certification Interval Width
Dataset
Perturbations
Average
Maximum
Average
Maximum
R(30)
0.019
0.234
0.010
0.124
T.(2). T,(2)
0.041
0.334
0.022
0.181
MNIST
Sc(5), R(5), C(5), B(0.01)
0.043
0.356
0.031
0.223
Sh(2), R(2), Sc(2), C(2), B(0.001)
0.022
0.253
0.015
0.153
R(10)
2.67 x 10
8.53
10
5.38 x 10
1.71 x 10
CIFARIO
R(2), Sh(2)
8.94 10
2.82
10
4.52 10-3
1.42 10
Sc(1), R(1), C(1), B(0.001)
6.37 x 10-3
1.26 x 10
6.37 x 10
1.26 x 10
Sh(2)
1.21 x 10-3
4.90 x 10-3
2.44 x 10-4
9.82 x 10
Tiny
ImageNet Sc(2)
2.39 10
8.76
10
4.81 10
1.76 10
R(5)
2.15 x 10 3
7.88 x 10
8.63 x 10
3,17 x 10
Driving R(2)
2.82 x 10 1.51 x 10
7.71 x 10
4.00 x 10
D.3
ADDITIONAL CERTIFICATION DETAILS
Batch Size. We batch size of 10,000, 10,000, 2,000, 400, and 3,000 during the certification of MNIST, CIFAR1O, Tiny ImageNet CNN7, Tiny ImageNet WeteResNet, and self-driving networks, respectively.
Parameter Splits. To ensure precise certification, select parameter splits that are 1-5x smaller width than those used during training. The certification configurations for each experiment can be found in Section D.4
D.4 PARAMETER INTERVAL. SIZES
In Table we show the interval sizes of the geometric perturbation parameters that we use during training and certification for all experiments. In the Training column, we present the final (i.e., after ramp-up) interval size of each perturbation parameter used during training. Since we enforce a local geometric ball of up łVy in Eqs. and the interval size of this ball is 2 (where v/ is the final parameter interval size after ramp-up. as discussed in Section D.2). In the Certification column, present the interval size of each split used during robustness certification. For experiments with
16

---

Published as a conference paper at ICLR 2023
multiple perturbations, the ordering of the sizes corresponds with the ordering of the transformations in the Perturbations column.
We describe below the procedure to obtain the values of My shown in Table 4
1. For a given set of n perturbations P with interval parameter ranges = = 8). we first start with an arbitrary V/y such that V/; < - f for all 1 s S n.
2. Then, we uniformly sample 10 random scalar parameter values {0x 1 (where each 0g U ((, 0) as in Eqs. [8 and 9 and compute, over all train set images X [0, 1jxxxxx>> the maximum pixel interval width of each image under perturbation of P with parameters 0g + vy:
Ms = {max X where X" = P(X, Oz + v2)
(16)
given X denotes the 7th perturbed image in the train set. Essentially, in this step converting interval sizes in parameter space to pixel space to gauge the amount of over- approximation in the computed bounds (as it the pixel's intervals that are ultimately propagated through the network). Now, we calculate the average maximum pixel interval width over all images and parameter samples, obtaining μ = mcan [mean M& k=1-
We find that selecting Vf such that is close to typical values of used in the -nom setting (e.g., 0.2 and 0.4 for MNIST, 4/255 and 8/ 6/255 for CIFARIO) yields both accurate and certifiable networks, If μr > e, then we reduce Vy (hence reducing the amount of over-approximation) and recompute this step until μ e. Note that this tuning requires no training, and can be computed in under minute for all the datasets that we consider.
3. Once appropriate values of V/y have been determined from step (2), we can proceed to use them in training. We perform a 80-20 rain-validation split of the train set, and use CGT to train a network to completion. If the validation accuracy and robustness are sufficiently high, then no further tuning is required. Else, we reduce "y and repeat this step. We only had to do this step a few times, as the calculation of the pixel widths already provided good heuristic for network performance.
After determining the appropriate parameter sizes during training time, selecting the certification split sizes is straightforward. We empirically find that selecting parameter sizes that are 2x smaller than those used during training yields good balance between certification rate and runtime. If faster certification time is desired, one can use the same parameter sizes at both training and certification time (as we do in the CIFAR10 10 experiment with scaling, rotation, certification rate is desired, one use parameter sizes that contrast, and brightness). higher smaller, the cost of higher runtime (e.g.. we find 5x to be effective for Tiny ImageNet, while using parameter sizes that are even smaller has diminishing returns and does not appreciably increase certification rate).
Table 5) shows the maximum pixel interval width during training and certification for each experi- ment. Additionally, we also show the average pixel interval width (i.e., Eq. [6] with the max oper- ation replaced by mean) to demonstrate that geometric transformations produce highly nonuniform bounds, further motivating why supplying precise geometric bounds during training is crucial to achieving networks that are both accurate and certifiable.
E ADDITIONAL RESULTS
E TRAINING METHODS
To demonstrate the benefit of our loss function, we compare CGT with three baseline training meth- ods: (1) data augmentation, denoted Augment.: (2) augmentation with PGD (Madry et al. (018)) denoted PGD+A; and (3) augmentation with IBP (Gowal et al. 2019), denoted IBP+A. We select these baselines because, to the best of our knowledge, they are the only training methods utilized in existing works on deterministic geometric robustness (as no work incorporates precise geometric regions into training as we do). For (1), the loss function simply the cross-entropy loss, with input images augmented according to the perturbations to generate adversarial examples of the augmented images. For (3), we employ the IBP loss, with interval e-balls placed around the augmented images.
are trying to certify. For (2), use PGD
17

---

Published as a conference paper at ICLR 2023
Table 6: Comparison of training methods on the MNIST translation (left) and CIFARIO rotation (right) benchmarks.
Training Method
Accuracy (%)
Certified (%%
per Egoch (8)
Training Method
Accuracy (%)
Certified (%)
per Epoch (s)
GPU
Mem. (MB)
Mem. (MB)
CGT
99.2
89.8
3.25
116.3
CGT
80.5
63.2
6,06
236.2
IBP+A
98.5
82.6
2,53
116.2
IBP+A
62.2
46.4
5.44
235
PGD+A
99.4
0
16.6
67.07
PGD+A
76.7
38.8
7.48
83,26
Augment.
99.4
0
1,50
64.76
Augmcut.
83.7
0.04
5.13
74,38
Table sshows these comparisons the MNIST translation and CIFAR rotation benchmarks. For the PGD and IBP-based baselines, we select e = 0.1 and = 2/ 2/255 for MNIST and CIFARIO 10, respectively, which are commonly used in the literature (Balunovic et al. 2019: Gowal et al. 2019 Zhang et al. 2020). For PGD, we use a step size of 0.005 and 40 steps for MNIST and a step size of 0.002 and steps for CIFARIO. When calculating the time and memory statistics for CGT and IBP+A, we only consider the epochs after warm-up (i.e., when we start computing the interval robustness loss term). We can observe that our approach, which can supply precise bounds that correspond to the geometric perturbations we are trying to certify, is able to attain the best certified accuracy while maintaining high clean accuracy and only using slightly more time and memory compared to the other approaches.
E.2 EFFECT OF HYPERPARAMETER
Table 7: Variation of clean and certified accuracy function of vy. c is the certification interval
size, Vo is the value of Vy used in our main results, and = Vo- c.
Benchmark
Accuracy
Vj
Type
c g
Vo
1. +
g
CIFARI0 R(2), Sh(2)
Certified
45.6
49.8
51.0
51.7
50.8
Clean
73.5
71.8
70.1
69.8
66.6
Tiny ImageNet
Certified
9.4
13.6
15.2
16.0
16.5
Sc(2)
Clean
28.5
26.9
26.1
25.4
25.2
As the size of the local geometric ball (controlled by v) a key training hyperparameter of our loss function in Eq. [8] we conduct ablation study CIFAR10 network and Tiny ImageNet CNN7 on how varying V/y (i.c., the final parameter interval size after ramp-up, as discussed in Section D.2p affects the certified and clean accuracies of -tainedd networks. Table 7 presents these results. In addition to the original value of Vy used in our benchmarks Sections 5.1 and 5.2 (denoted v,), select four additional settings for y and train with CGT for each of these values. We choose the smallest My to be equal to the interval size at certification time, c, and the largest Vy to be equal to c plus two times the difference between v, and We certify all networks with the original size of
We can observe that generally, larger values of vy lead to increased certified accuracy, at the cost of decreased clean accuracy. CGT thus allows one explicitly tune the tradeoff between these metrics by varying vy. The notable exception to this trend is the CIFARIO 10 network with the largest 1/y; in this case, using Dy that is excessively large actually decreases certified robustness (since the clean accuracy drops considerably). There are diminishing returns to using larger intervals during training: while the certified accuracy increases significantly when using V/ vo compared to V/ = c, further increasing the size to M/ + g/2 22 or above only slightly increases certifiability.
E.3 SPEED OF INTERVAL INTERPOLATED TRANSFORMATION ALGORITIIM
We demonstrate why FGV is necessary component of our framework. Table R presents the com- parison of Algorithm| to the state-of offte--f--he-aa art algorithm for computing interval geometric bounds in Semantify-NNN (Mohapatra et al., 2020), which is sequential and CPU-only. To compute interval rotation bounds for a batch of training images (256 for MNIST and 128 for CIFAR10 and Tiny ImageNet), we 3.00020,000- faster. Our end-to-end speedup when combining both the input
18

---

Published as a conference paper at ICLR 2023
Table Time compute interval rotation bounds and network outputs for one batch of images.
Time Compute Bounds (s)
Time to Propagate Bounds
End-to-End Speedup
Dataset
Our Speedup
Semantify-NN
Ours
MNIST CIFARIO
33.10
0.0029
11250x
0.0037
4974x
22.81
0.0026
8645x
0.0043
3293
Tiny ImageNet
62.83
0.0030
20610x
0.0179
3003
Table 9: Time compute interval rotation bounds for one batch of images, with method running on the CPU and with batch size 1.
Dataset
Semantify-NN (s)
Ours CPU (8)
Our Speedup
MNIST CIFAR10 Tiny ImageNet
33. 10
0.25
135x
22.81
0.11
200
62.83
0.28
221 x
geometric perturbation bound computation and the propagation of these bounds through the network 3,000-5,000x. For Tiny ImageNet, we use the CNN7 network in this experiment. These results show that without Algorithm [ the overhead during training is high functions Eqs. and
our proposed loss
As ablation study, CPU and with batch size of 1. As seen in Table g our runtime is still 100-200x faster than Semantify-NN's. These results show that our speedup is only due the ability to leverage GPU hardware, but also due to fundamental algorithmic improvements that allow the computation of interpolated transformations be efficiently parallelized.
algorithm under the conditions Semantify-NN's
the
E.4 TRAINING STATISTICS
Table 10 shows the training statistics of runtime per epoch and GPU memory usage for all of our When calculating the time and memory statistics, we only consider the epochs after warm-up (i.e., when we start computing the interval robustness loss term).
networks.
Table 10: Training runtime and GPU memory usage for all our benchmarks.
Network
Perturbations
Time per Epoch (s)
Max GPU Memory (MB)
R(30)
3.46
116.3
T2)2). T.(2)
3.25
116.3
MNIST
Sc(5), R(S), C(5), B(0.01)
3.46
116.3
Sh(2), R(2), Sc(2), C(2), B(0.001)
3.53
116.3
R(10)
6.06
236.2
CIFARIO
R(2), Sh(2)
236.3
Sc(1), R(1), C(1), B(0.001)
6.11
237.3
Sh(2)
4362
Tiny ImageNet
Sc(2)
48.9
4362
CNN7
R(S)
48.9
4361
Sh(2)
98.2
34143
Tiny ImageNet
Sc(2)
98.1
34143
WideResNet
R(S)
98.8
34143
Driving
R(2)
11.7
3428
19


Reviews:
[{"review_id": "tsna-qKWdJ", "reviewer": "Reviewer_Z6j5", "summary": "", "questions": "", "limitations": "", "rating": 8, "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": "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.\n\n[1] Rotations, translations, scaling, shearing, changes in contrast and changes in brightness\n[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.", "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.", "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.\n\nA 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.", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "3: Some of the paper’s claims have minor issues. A few statements are not well-supported, or require small changes to be made correct.", "technical_novelty_and_significance": "4: The contributions are significant, and do not exist in prior works.", "empirical_novelty_and_significance": "4: The contributions are significant, and do not exist in prior works."}, "extra_text": {}}, {"review_id": "lGuylVM2i3m", "reviewer": "Reviewer_XMPM", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": 2, "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": "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.", "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. ", "strength_and_weaknesses": "Strength:\n1. This paper is the first one that uses GPU accelerated training for certified robustness against geometric transformations. \n\n2. The paper conducts an extensive study for certifying different models and datasets.\n\n", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "4: All of the claims and statements are well-supported and correct.", "technical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work.", "empirical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work."}, "extra_text": {}}, {"review_id": "hrCz2X7uA4", "reviewer": "Reviewer_2P26", "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": "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.\n\nThe contribution are two-fold:\n- Improvements in terms of speed of evaluating bounds on the output of the network given that the input is subject to geometric transformations.\n- 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.\n\nThe speed up of the verification is achieved by:\n- 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.\n- 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.\n\n", "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. ", "strength_and_weaknesses": "# Strength\nThe problem studied is quite an important one as geometric perturbations are a more realistic specifications than $\\mathcal{L}_p$ bounds.\nThe 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.\nThe empirical results are quite convincing, and evaluated on a wide range of datasets and specification.\n\n\n# Weakness - Things to improve.\n- 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?)\n- 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.\n- 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.\n- 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.", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "4: All of the claims and statements are well-supported and correct.", "technical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work.", "empirical_novelty_and_significance": "4: The contributions are significant, and do not exist in prior works."}, "extra_text": {}}, {"review_id": "fIgV9CJcDVM", "reviewer": "Reviewer_56ik", "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": "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. ", "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. ", "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. \nWeaknesses: \n\n1. 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. \n\n2. To be more self-contained, perhaps one could include a small recap of the LiRPA. \n\n3. 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. \n", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "4: All of the claims and statements are well-supported and correct.", "technical_novelty_and_significance": "2: The contributions are only marginally significant or novel.", "empirical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work."}, "extra_text": {}}]

Author rebuttal:

Decision: Accept: notable-top-25%