1、Certifying Geometric Robustness of Neural Networks Mislav Balunovi c, Maximilian Baader, Gagandeep Singh, Timon Gehr, Martin Vechev Department of Computer Science ETH Zurich mislav.balunovic, mbaader, gsingh, timon.gehr, martin.vechevinf.ethz.ch Abstract The use of neural networks in safety-critical

2、 computer vision systems calls for their robustness certifi cation against natural geometric transformations (e.g., rotation, scaling). However, current certifi cation methods target mostly norm-based pixel perturbations and cannot certify robustness against geometric transformations. In this work,

3、we propose a new method to compute sound and asymptotically optimal linear relaxations for any composition of transformations. Our method is based on a novel combination of sampling and optimization. We implemented the method in a system called DEEP G and demonstrated that it certifi es signifi cant

4、ly more complex geometric transformations than existing methods on both defended and undefended networks while scaling to large architectures. 1Introduction Robustness against geometric transformations is a critical property that neural networks deployed in computer vision systems should satisfy. Ho

5、wever, recent work 1,2,3 has shown that by using natural transformations (e.g., rotations), one can generate adversarial examples 4,5 that cause the network to misclassify the image, posing a safety threat to the entire system. To address this issue, one would ideally like to prove that a given netw

6、ork is free of such geometric adversarial examples. While there has been substantial work on certifying robustness to changes in pixel intensity (e.g., 6,7,8), only the recent work of 9 proposed a method to certify robustness to geometric transformations. Its key idea is summarized in Fig. 1: Here,

7、the goal is to prove that any image obtained by translating the original image by somex,y 4,4 is classifi ed to label3. To accomplish this task, 9 propagates the image and the parametersx,ythrough every component of the transformation using interval bound propagation. The output regionIis a convex s

8、hape capturing all images that can be obtained by translating the original image between4and4pixels. Finally,Iis fed to a standard neural network verifi er which tries to prove that all images inIclassify to3. This method can also be improved using tighter relaxation based on Polyhedra 10. Unfortuna

9、tely, as we show later, bound propagation is not satisfactory. The core issue is that any approach based on bound propagation inherently accumulates loss for every intermediate result, often producing regions that are too coarse to allow the neural network verifi er to succeed. Instead, we propose a

10、 new method based on sampling and optimization which computes a convex relaxation for the entire composition of transformations. Convex relaxations of translation (x, y,) x, y 4, 4 +x I +y P G NEURAL NETWORK VERIFIER Robust Not robust Interval 9PolyhedraDEEPG Figure 1: End-to-end certifi cation of g

11、eometric robustness using different convex relaxations. 33rd Conference on Neural Information Processing Systems (NeurIPS 2019), Vancouver, Canada. The key idea of our method is to sample the parameters of the transformation (e.g.,x,y), obtaining sampled points at the output (red dots in Fig. 1), an

12、d to then compute sound and asymptotically optimal linear constraints around these points (shapeG). We implemented our method in a system called DEEP G and showed that it is signifi cantly more precise than bound propagation (using Interval or Polyhedra relaxation) on a wide range of geometric trans

13、formations. To the best of our knowledge, DEEPG is currently the state-of-the-art system for certifying geometric robustness of neural networks. Main contributionsOur main contributions are: A novel method, combining sampling and optimization, to compute asymptotically optimal linear constraints bou

14、nding the set of geometrically transformed images. We demonstrate that these constraints enable signifi cantly more precise certifi cation compared to prior work. A complete implementation of our certifi cation in a system called DEEPG. Our results show substantial benefi ts over the state-of-the-ar

15、t across a range of geometric transformations. We make DEEPG publicly available at 2Related work We now discuss some of the closely related work in certifi cation of the neural networks and their robustness to geometric transformations. Certifi cation of neural networksRecently, a wide range of meth

16、ods have been proposed to certify robustness of neural networks against adversarial examples. Those methods are typically based on abstract interpretation 6,7, linear relaxation 8,11,12, duality 13, SMT solving 14,15,16, mixed integer programming 17, symbolic intervals 18, Lipschitz optimization 19

17、, semi-defi nite relaxations 20 and combining approximations with solvers 21,22 . Certifi cation procedures can also be extended into end-to-end training of neural networks to be provably robust against adversarial examples 23,24. Recent line of work 25,26,27 proposes to construct a classifi er base

18、d on the smoothed neural network which comes with probabilistic guarantees on the robustness againstL2 perturbations. None of these works except 9 consider geometric transformations, while 9 only verifi es robustness against rotation. The work of 28 also generates linear relaxations of non-linear sp

19、ecifi cations, but they do not handle geometric transformations. We remark that 1 considers a much more restricted (discrete) setting leading to a fi nite number of images. This means that certifi cation can be performed by brute-force enumeration of this fi nite set of transformed images. In our se

20、tting, as we will see, this is not possible, as we are dealing with an uncountable set of transformed images. Neural networks and geometric transformationsThere has been considerable research in em- pirical quantifi cation of geometric robustness of neural networks 2,3,29,30,31,32. Another line of w

21、ork focuses on the design of architectures which possess an inherent ability to learn to be more robust against such transformations 33,34. However, all of these approaches offer only empirical evidence of robustness. Instead, our focus is to provide formal guarantees. Certifi cation of geometric tr

22、ansformationsPrior work 9 introduced a method for analyzing rotations using the interval propagation and performed certifi cation using the state-of-the-art verifi er DEEPPOLY. It is straightforward to generalize their interval approach to handle more complex transformations beyond rotation (we prov

23、ide details in Appendix A.4). However, as we show experimentally, interval propagation loses precision which is why certifi cation often does not succeed. To capture relationships between pixel values and transformations, one would ideally use the Poly- hedra relaxation 10 instead of intervals. Whil

24、e Polyhedra offers higher precision, its worst-case running time is exponential in the number of variables 35. Hence, it does not scale to geometric transformations, where every pixel introduces a new variable. Thus, we extended the recent DeepPoly relaxation 9 (a restricted Polyhedra) with custom a

25、pproximations for the operations used in several geometric transformations (e.g., translation, scaling). Our experimental results show that even though this approach signifi cantly improves over intervals, it is not precise enough to certify robustness of most images in our dataset. In turn, this mo

26、tivates the method introduced in this paper. 2 (a) Original image 35 1 3 A1,1 A1,3 A3,1 A3,3 A5,1 A5,3 (b) Interpolation(c) Rotated image Figure 2: Image rotated by 4 degrees. Here, (a) shows the original image, while (b) shows part of (a) with a focus on relevant interpolation regions. Finally, (c)

27、 shows the resulting rotated image. 3Background Our goal is to certify the robustness of a neural network against adversarial examples generated using parameterized geometric transformations. In this section we formulate this problem statement, introduce the notation of transformations and provide a

28、 running example which we use throughout the paper to illustrate key concepts. Geometric image transformationsA geometric image transformation consists of a parameterized spatial transformationT, an interpolationIwhich ensures the result can be represented on a discrete pixel grid, and parameterized

29、 changes in brightness and contrastP,. We assumeTis a composition of bijective transformations such as rotation, translation, shearing and scaling (full descriptions of all transformations are in Appendix A.1). While our approach also applies to other interpolation methods, in this work we focus on

30、the case whereIis the commonly-used bilinear interpolation. To ease presentation, we assume the image (with integer coordinates) consists of an even number of rows and columns, is centered around(0,0), and its coordinates are odd integers. We note that all results hold in the general case (without t

31、he assumption). InterpolationThe bilinear interpolationI: R2 0,1evaluated on a coordinate(x,y) R2is a polynomial of degree 2 given by I(x,y) := 1 4 X i,j0,2 pi+i,j+j(2 |i + i x|)(2 |j + j y|).(1) Here,(i,j)is the lower-left corner of an interpolation regionAi,j:= i,i + 2 j,j + 2which contains pixel(

32、x,y). Matrixpconsists of pixel values at corresponding coordinates in the original image. The functionIis continuous onR2and smooth on the interior of every interpolation region. These interpolation regions are depicted with the blue horizontal and vertical dotted lines in Fig. 2b. The pixel value p

33、x,yof the transformed image can be obtained by (i) calculating the preimage of the coordinate(x,y)underT, (ii) interpolating the resulting coordinate usingIto obtain a value, and (iii) applying the changes in contrast and brightness viaP,() = + , to obtain the fi nal pixel value px,y= I,(x,y). These

34、 three steps are captured by I,(x,y) := P, I T 1 (x,y).(2) Running exampleTo illustrate key concepts introduced throughout the paper, we use the running example of an MNIST image 36 shown in Fig. 2. On this image, we will apply a rotationRwith an angle . For our running example, we set P,to be the i

35、dentity. Consider the pixel p5,1in the transformed image shown in Fig. 2c (the pixel is marked with a red dot). The transformed image is obtained by rotating the original image in Fig. 2a by an angle = 4. This results in the pixel value p5,1= I R1 4 (5,1) = I(22,32) 0.30 Here, the preimage of point(

36、5,1)underR 4 produces the point(22,32)with non-integer coordinates. This point belongs to the interpolation regionA1,3and by applyingI(22,32)to the original image in Fig. 2a, we obtain the fi nal pixel value 0.30for pixel(5,1)in the rotated image. 3 Neural network certifi cationTo certify robustness

37、 of a neural network with respect to a geometric transformation, we rely on the state-of-the-art verifi er DeepPoly 9. For complex properties such as geometric transformations, the verifi er needs to receive a convex relaxation of all possible inputs to the network. If this relaxation is too coarse,

38、 the verifi er will not be able to certify the property. Problem statementTo guarantee robustness, our goal is to compute a convex relaxation of all possible images obtainable via the transformationI,. This relaxation can then be provided as an input to a neural network verifi er (e.g., DeepPoly). I

39、f the verifi er proves that the neural network classifi cation is correct for all images in this relaxation, then geometric robustness is proven. 4Asymptotically optimal linear constraints via optimization and sampling We now present our method for computing the optimal linear approximation (in term

40、s of volume). MotivationAs mentioned earlier, designing custom transformers for every operation incurs preci- sion loss at every step in the sequence of transformations. Our key insight is to defi ne an optimization problem in a way where its solution is the optimal (in terms of volume) lower and up

41、per linear constraint for the entire sequence. To solve this optimization problem, we propose a method based on sampling and linear programming. Our method produces, for every pixel, asymptotically optimal lower and upper linear constraints for the entire composition of transformations (including in

42、ter- polation). Such an optimization problem is generally diffi cult to solve, however, we fi nd that with geometric transformations, our approach is scalable and contributes only a small portion to the entire end-to-end certifi cation running time. Optimization problemTo compute linear constraints

43、for every pixel value, we split the hyper- rectanglehrepresenting the set of possible parameters intossplitshkks. Our goal will be to compute sound lower and upper linear constraints for the pixel valueI(x,y)for a given pixel(x,y). Both of these constraints will be linear in the parameters = (,) hk

44、. We defi ne optimal and sound linear (lower and upper) constraints for I (x,y) to be a pair of hyperplanes fulfi lling wT l + bl I(x,y) hk(3) wT u + bu I(x,y) hk,(4) while minimizing L(wl,bl) = 1 V Z hk ?I (x,y) (bl+ wTl ?)d (5) U(wu,bu) = 1 V Z hk ?(b u+ wTu) I(x,y) ? d.(6) HereVdenotes the normal

45、ization constant equal to the volume ofhk. Intuitively, the optimal constraints should result in a convex relaxation of minimum volume. This formulation also allows independent computation for every pixel, facilitating parallelization across pixels. Next, we describe how we obtain lower constraints

46、(upper constraints are computed analogously). Step 1: Compute a potentially unsound constraintTo generate a reasonable but a potentially unsound linear constraint, we sample parameters1,.,Nfromhk, approximate the integral in Eq. (5) by its Monte Carlo estimate LNand enforce the constraints only at t

47、he sampled points: min (wl,bl)W LN(wl,bl) =min (wl,bl)W 1 N N X i=1 ?I i(x,y) (bl+ wTli ?), bl+ wT l i Ii(x,y)i N. (7) This problem can be solved exactly using linear programming (LP). The solution is a potentially unsound constraintb0 l+ w 0T l (it may violate the constraint at non-sampled points).

48、 For our running example, the region bounded by these potentially unsound lower and upper linear constraints is shown as orange in Fig. 3. 4 0 8 4 0 0.25 0.5 0.75 1 Angle Pixel value Interval bounds I R1 (5,1) Sound enclosure Unsound enclosure Random samples Figure 3: Unsound (Step 1) and sound (Ste

49、p 3) enclosures forI R1 (5,1), with respect to random sampling from 0, 4, in comparison to the interval bounds from prior work 9. Note that I R1 (5,1) is not piecewise linear, because bilinear interpolation is a polynomial of degree 2. Step 2: Bounding the maximum violationOur next step is to comput

50、e an upper bound on the violation of Eq. (3) induced by our potentially unsound constraint from Step 1. This violation is equal to the maximum of the functionf() = b0 l+ w 0T l I(x,y)over the hyperrectanglehk. It can be shown that the functionfis Lipschitz continuous which enables application of sta

51、ndard global optimization techniques with guarantees 37. We remark that such methods have already been applied for optimization over inputs to neural network 38, 19. We show a high level description of this optimization procedure in Algorithm 1. Throughout the optimization, we maintain a partition o

52、f the domain of functionfinto hyperrectanglesh. The hyperrectangles are stored in a priority queueqsorted by an upper boundfbound h of the maximum value the function can take inside of the hyperrectangle. At every step, shown in Line 6, the hyperrectangle with the highest upper bound is further refi

53、 ned into smaller hyperrectanglesh01,.,h0 k and their upper bounds are recomputed. This procedure fi nishes when the difference between every upper bound and the maximal value at one of the hyperrectangle centers is at most?. Finally, maximum upper bound of the elements in the queue is returned as a

54、 result of the optimization. We provide more details on the optimization algorithm in Appendix A.5. Algorithm 1 Lipschitz Optimization with Bound Refi nement 1:Input: f, h, k 2 2:fmax:= f(center(h) 3:fbound h := fbound(h,f) 4:q := (h,fbound h ) 5:repeat 6:pop (h0,fbound h0 ) from q with maximum fbou

55、nd h0 7:h01,.,h0 k := partition(h0,f) 8:for i := 1 to k do 9:fmax:= max(f(center(h0i),fmax) 10:fbound h0 i := fbound(h0i,f) 11:if fbound h0 i fmax+ ? then 12:add (h0i,fbound h0 i ) to q 13:end if 14:end for 15:until a maximal fbound h0 in q is lower than fmax+ ? 16:return fmax+ ? 5 The two most impo

56、rtant aspects of the algorithm, which determine the speed of convergence, are (i) computation of an upper bound, and (ii) choosing an edge along which to refi ne the hyperrectangle. To compute an upper bound inside of a hyperrectangle spanned between points hland hu, we use: f() f(h u+hl 2 ) + 1 2 ?

57、 ?hf?T(hu hl). (8) Here ? ?hf? can be any upper bound on the true gradient which satisfi es|if()| ? ?hf? i for every dimensioni. To compute such a bound, we perform reverse-mode automatic differentiation of the functionfusing interval propagation (this is explained in more details in Appendix A.2).

58、As an added benefi t, results of our analysis can be used for pruning of hyperrectangles. We reduce a hyperrectangle to one of its lower-dimensional faces along dimensions for which analysis on gradients proves that the respective partial derivative has a constant sign within the entire hyperrectangle. We also improve on standard refi nement heuristics instead of refi ning along the largest edge, we additionally weight edge length by an upper bound on the partial derivative of that dimension. In our experiments, we fi nd that these in