Universal Approximation with Certified Networks
Authors: Maximilian Baader
Matthew Mirman
Martin Vechev
Venue:  (2020)
Keywords: adversarial robustness
universal approximation
certified network
interval bound propagation

Abstract: Training neural networks to be certifiably robust is critical to ensure their safety against adversarial attacks. However, it is currently very difficult to train a neural network that is both accurate and certifiably robust. In this work we take a step towards addressing this challenge. We prove that for every continuous function $f$, there exists a network $n$ such that:
(i) $n$ approximates $f$ arbitrarily close, and (ii) simple interval bound propagation of a region $B$ through $n$ yields a result that is arbitrarily close to the optimal output of $f$ on $B$. Our result can be seen as a Universal Approximation Theorem for interval-certified ReLU networks. To the best of our knowledge, this is the first work to prove the existence of accurate, interval-certified networks.

Published as a conference paper at ICLR 2020
UNIVERSAL APPROXIMATION WITH CERTIFIED NETWORKS
Maximilian Baader, Matthew Mirman, Martin Vechev
Department of Computer Science ETH Zurich, Switzerland
[mbaader, matthew. mi rman, ma martin, r wtw.ii...eethccccc..e..
ABSTRACT
Training neural networks to be certifiably robust critical to ensure their safety against adversarial attacks. However, it currently very difficult train neural network that is both accurate and certifiably robust. In this work we take a step towards addressing this challenge. We prove that for every continuous function f. there exists a network n such that: (i) approximates f arbitrarily close, and (ii) simple interval bound propagation of a region B through yields result that is arbitrarily close to the optimal output of f on B. Our result can be seen as a Universal Approximation Theorem for interval-certifeer ReLU networks. To the best of our knowledge, this is the first work to prove the existence of accurate, interval-certifedd networks.
INTRODUCTION
Much recent work has shown that neural networks can be fooled into misclassifying adversarial examples (Szegedy et al. 2014), inputs which are imperceptibly different from those that the neural network classifies correctly. Initial work defending against adversarial examples revolved around training networks to be empirically robust, usually by including adversarial examples found with various attacks into the training dataset (Gu and Rigazio| 2015 Papernot al., 2016 [Zheng et al.) 2016, Athalye et al.) 2018 Eykholt et al. 20118 Alloosvi--eztllee However, while empirical robustness can be practically useful, it does not provide safety guarantees. As a result, much recent research has focused on verifying that a network is certifiably robust, typically by employing methods based on mixed integer linear programming (Tjeng et al., 2019).
et al.) 2017 Xiao et al. 2018).
SMT solvers (Katz et al.) (2017), semidefinite programming (Raghunathan et al.) (0). duality
(Wong and Kolter| 2018 Dvijotham al., 2018b), and linear relaxations (Gehr et al. 2018 Weng et al. 2018 Wang et al. 2018b) /Zhang al. 2018 (ingh et al. 2018 (Salman et al.] 2019).
Because the certification rates were far from satisfactory, specific training methods were recently developed which produce networks that are certifiably robust: Mirman et al. (018) 20 et al. (2018b); Wang et al. (2018a); Wong and Kolter (2018); Wong et al. (2018); Gowal et al. (2018) train the network with standard optimization applied an iverrapproximation of the network behavior on a given input region (the region created around the concrete input point). These techniques aim to discover specific weights which facilitate verification. There is a tradcoff between the degree of the over-approximation used and the speed of training and certification. Recently, (Cohen et al. 2019h) proposed statistical approach certification, which unlike the non-rrobaiilistic methods discussed above, creates a probabilistic classifier that comes with probabilistic guarantees.
So far, some of the best pon-probabiilittc results achieved on the popular MNIST (Lecun al. 1998) and CIFAR 10 Krizhevsky 2009) datasets have been obtained with the simple Interval relaxation Gowal et al. 2018 Mirman et al.) 2019), which scales well at both training and verification time. Despite this progress, there are still substantial gaps between known standard accuracy, experimental robustness, and certified robustness. For example, for CIFARIO, the best reported certified robustness is 32.04% with an accuracy of 49.49 99.99 when using fairly modest lox region with radius 8/255 (Gowal al. 2018). The state-of-the-an non-robust accuracy for this dataset > 95% with experimental robustness 50%. Given the size of this gap, key question then is: can certified training ever succeed or is there a fundamental limit?

---

Published as a conference paper at ICLR 2020
00 1
[o. i
[0,
[x)
0.5
[0.
0.0
[0,
+]
10.
[0, +
(a) Not certifiable network n1.
(b) The function f.
(c) Certifiable network 722.
Figure The ReLU networks n, (Figure 2ap and n2 (Figure 2c
encode the same function
(Figure 2b). Interval analysis fails certify that ni does not exceed 0. 1] on [0, 1] while certification succeeds for 112-
In this paper we take step in answering this question by prov- ing result parallel to the Universal Approximation Theorem (Cybenko) 1989 Hornik et al., 1989). We prove that for any con- tinuous function defined on a compact domain
[a.b]
Rd and for any desired level of accuracy 8, there exists a ReLU neural net- work n which can certifiably approximate f up to using interval bound propagation. As interval is a fairly imprecise relaxation, our result directly applies to more precise convex relaxations (c.g., Theorem
n²
Figure 1: Illustaaiion of
Zhang et al. 2018); Singh et al. 2019)).
Theorem 1.1 (Universal Interval-Certiffe Approximation, Figure D. Let r C RT be compact set and let : r IR be continuous function. For all d > O, there exists ReLU network such that for all boxes [a, b] in I' defined by points b E I' where a < by for all k the propagation of the box [a, b] using interval analysis through the network n. denoted n² ([a, b)), approximates the set [2, u] = min f( b)), max f(a,, b]]] S R up to 8,
+ 6, u 5) S n² ((a, b)) S -6, 6, 87.
(1)
We recover the classical universal approximation theorem (lf(x) - n(x) < 8 for all E r) by considering boxes (a, bj describing points (a
b). Note that here the lower bound is not u as the network n is an approximation of f. Because interval analysis propagates boxes, the theorem naturally handles &so norm bound perturbations to the input. Other I, norms can be handled by covering the Ip ball with boxes. The theorem can be extended easily to functions f: r + R² by applying the theorem component wise.
Practical meaning of theorem The practical meaning of this theorem is as follows: if we train a neural network n' on given training data set (e.g.. CIFARIO) and are satisfied with the properties of n' (e.g.. high accuracy), then because n' is a continuous function, the theorem tells us that there exists network which is accurate as n' and as certifiable with interval analysis n' is with a complete verifier. This means that if we fail to find such an n. then either n did not possess the required capacity the optimizer unsuccessful.
Focus on the existence of a network We note that we do not provide a method for training a certified ReLU network even though our method is constructive, question and thus we focus on proving that a given network exists. Interesting future work items would be to study the requirements on the size of this network and the inherent hardness of finding with standard optimization methods.
aim to answer an existential
Universal approximation insufficient We now discuss why classical universal approximation insufficient for establishing our result. While classical universal approximation theorems state that neural networks can approximate a large class of functions f. unlike our result, they do not state that robustness of the approximation of f is actually certified with scalable proof method (e.g.. interval bound propagation). one uses a non scalable complete verifier instead, then the standard Universal approximation theorem is sufficient.
2

---

Published as a conference paper at ICLR 2020
To demonstrate this point, consider the function f R - R (Figure 2b mapping all x v 0 to 1. all
x 2 to and all 0 < x < 1 to 1 - 2 and two ReLU networks n1 (Figure 2a and n2 (Figure 2c)
perfectly approximating f, that is (2) = f(z) n2(2) for all z. For = 4. the interval
certification that n maps all x E [0, 1] to [0, 1] fails because 1 3 C (10, 1D) = [0, [0. 2
7) However, interval certification succeeds for n2. because n 11) = [0. To the best of our knowledge, this is the first work to prove the existence of accurate, interval-certified networks.
2 RELATED WORK
After adversarial examples were discovered by Szegedy al. (2044), many attacks and defenses were introduced (for a survey, see Akhtar and Mian (2018). Initial work on verifying neural network robustness used exact methods (Katz et al.j 2017] Tjeng al. 2019) on small networks, while later research introduced methods based on aver-approximation (Gehr et al. 2018 Raghunathan et al. 2018a Singh et al., 2018 Salman et al. 2019) aiming to scale to larger networks. A fundamentally different approach is randomized smoothing (Li et al.) [2099] Lécuyer et al.) 2019 Cohen et al. 2019b), in which probabilistic classification and certification with high confidence is pertormed.
As neural networks that are experimentally robust need not be certifiably robust, there has been significant recent research on training certifiably robust neural networks (Raghunathan et al. 2018b
2018: WWan et al.) 20188a Gowal et al. 2018 Dvijotham et al. [2018a] Xiao et al. G00eenoheen et al. (019b). As these methods appear to have reached performance wall, several works have started investigating the fundamental barriers in the datasets and methods that preclude the learning of a robust network (Iet alone a certifiably
Mirman et al. 2018: 2019 Wong and Kolter (2018) Wong al.
robust one) (Khoury and Madnilld-Menell 2018 Schmidt et al. 2018 Tiippras al. 2019). In our
work, we focus on the question of whether neural networks are capable of approximating functions whose robustness can be established with the efficient interval relaxation.
Feasibility Results with Neural Networks Early versions of the Universal Approximation Theo- rem were stated by Cybenko (1989) and Hornik et al. (1989). Cybenko (1989) showed that networks using sigmoidal activations could approximate continuous functions in the unit hypercube, while Hornik et al. (1989) showed that even networks with only one hidden layer are capable of approxi- mating Borel measurable functions.
More recent work has investigated the capabilities of ReLU networks. Here, Arora et al. (2018). based on Tarela and Martinez (1999), proved that every continuous piecewise linear function in RT can be represented by a ReLU network. Later, He et al. (2118) reduced the number of neurons needed using ideas from finite elements methods. Relevant to our work, AArora et al. (2018) introduced a ReL.U network representations of the min function. Further, we use a construction method that is similar to the construction for nodal basis functions given in He et al. (2018).
Universal approximation for Lipschitz constrained networks have been considered by Anil et al. (2019) and later by Cohen et al. (2019a). A bound on the Lipschitz constant of network immediately yields a certified region depending on the classification margin. Anil et al. 2019) proved that the set of Lipschitz networks with the GroupSort activation is dense in the space of Lipschitz continuous functions with Lipschitz constant 1, while (ohhnn et al. 2019g) provide an explicit construction to obtain the network. We note that both of these works focus on Lipschitz continuous functions, more restricted class than continuous functions, which we consider in our work.
BACKGROUND
In this section we provide the concepts necessary to describe our main result.
Adversarial Examples and Robustness Verification Let n : Rm + IR be a neural network, which classifies input x to a label t if n(x), > n(x), for all j t. For correctly classified input x, an adversarial example is an input y such that x is imperceptible from to a human, but is classified different label by n.
Frequently, two images are assumed to be "imperceppible"" if there I, distance is at most e. The Ip ball around an image is said to be the adversarial ball, and network is said to be e-robust around if
3

---

Published as a conference paper at ICLR 2020
49
1 4/
4/3-
09
4/5
4/
-2
-2
0
2
x
I
(a) f
(b) Slicing of f. fo. ..........
(c) Networks n. approximating Ss-
Figure 3: Approximating f (Figure Ba using ReLU network Eu + Σx Rg. The ReLU networks
ng (Figure Beb approximate the N -slciing of (Figure 3b), as sum of local bumps (Figure 6).
every point in the adversarial ball around classifies the same. In this paper, we limit our discussion to lse adversarial balls which can be used to cover to all 1p balls.
The goal of robustness verification is to show that for neural network imput point and label t, every possible input in an lxc ball of size around x (written IB (x)) is also classified to t.
Verifying neural networks with Interval Analysis The verification technique we investigate in this work is interval analysis. We denote by B the set of boxes B [a, b] C IR" for all m, where a, S b; for all i. Furthermore for I' C RRT we define B(1)) := B n I' describing all the boxes in The standard interval transfratrrssoo for the basic operations and the ReLU function R (Gehr et al. (008)), Gowal et al. (2018) are
are considering, namely +, 7
ba +8 [c, d] {a+ c, +d] (*( b]) = [R(a), R(b)]
- laa, b] [-b, -a
. [a, b] = [Aa, Ab].
where (a, Ic, d E B(R). and À Rzo- Furthermore, used to distinguish the function from
its interval-transfommen transformation fa. To illustrate the difference between f and ft, consider f(x) ==
evaluated on x = [0, 1). We have [[0, 1]) = O, but (0. 1)) = [0, 1] - # [o, 1] = [0, 1] + [-1,0]
[-1,1] illustrating the loss in precision that interval analysis suffers from.
Interval analysis provides a sound over-approximation in the sense that for all function f. the values that f can obtain on [a, b), namely f(a, b)) == {f(x) x E [a, b]} a subset of f"( If is composition of functions, f = fi o ... o fk. then f ..... o f a sound intervaltrrassormee for f-
Furthermore all combinations f of +, - and R are monotone, that is for [a. b). [c. d| S B(R))) such that [a, b) S [c, d then f ([a, b)) C f ([c, d)) (Appendix Aj. For boxes [ar, a:] representing points I coincides with f. fR a:) = f fx). This will later be needed.
PROVING UNIVERSAL INTERVAL-PROVAT
APPROXIMATION
In this section, we provide an explanation of the proof of our main result, Theorem 4.6 and illustrate the main points of the proof.
The first step in the construction is to deconstruct the function f into slices {fx r [0, flossse such that that (xx Eo EN= fi(()) for all x, where to is the minimum of S(T). We approx- imate each slice fx by ReLU network nig. The network n approximating f up n(x) == Eo + / Σ. n4 (x). The construction relies on 2 key insights, (i) the output of 5 n can be confined to the interval [0, g. thus the loss of analysis precision is at most the height of the slice, and (ii) we can construct the networks ng using local bump functions, such that only 4 slices can contribute the loss of analysis precision, two for the lower interval bound, two for the upper one.
will be
4

---

Published as a conference paper at ICLR 2020
y
R(aa((2)
Figure 4: Neighbors / (x: (blue dots) and (ndd(() (red squares).
Figure 5: (1)
The slicing f Josk-c o of the function f: [-2, 2] (Figure 3a mapping f(x) = + 3x
is depicted in Figure 3b) The networks are depicted in Figure 3c In this example, evaluating the
of ni, namely n² on the box B [-1, 1] results into n² n1([1,1]] [-2, 6/5
lies is within the 5 = bound of ([] [-
Definition 4.1 (N-slicing (Figure (b)). Let r C RTT be a closed m-dimensional box and let f I be continuous. The N-slicing of
of functions {fuJoskeN defined by
0
if f(x) S Ex,
T I
f(x) - Ex
f < f(x) < St+11
Ak E (O..... N 1},
Ek-1 Ex
if Ek+11 I f()),
where & == Eo + (EN - Eo), K. [I....,N - 1}. to == min f(T) and EN max f(T).
To construct a ReLU network satisfying the desired approximation property (Equation ( if evaluated on boxes in B(T), need the ReLU network nmin capturing the behavior of min building block (similar to He et al. (2018)) It is given by
-1
nmin(x, v) = (1
R
With the ReLU network nmin, we can construct recursively ReLU network nminy mapping N arguments to the smallest one (Definition A.8) Even though the nnterval-rransoommattio loses precision,
establish bounds the precision loss of nmin'y sufficient for (Appendix A)
R(1 x)) clipping every value exceeding back to 1 (Figure 5) to construct the local bumps de w.r.t. a grid G. G specifies the set of all possible local bumps we can use to construct the networks ng. Increasing the finesse of G will increases the approximation precision.
Now, we the clipping function R:,.1]
Definition 4.2 (local bump, Figure 6). Let M E N, G x M x ... {
((
im i i zm) a grid,
C G be set of grid points describing the corner points of hyperrectangle in G. We define ReLU neural network Φ.: RTT [0. 1] C R w.r.t. G' by
l = 2 Togg 2m]+1 and let { +
2 M
M
M ) R l xR) + 11 #0+11))
R e. (xz
(x(x) = R nmingm
U LSk5m
We will describe later how M and get picked. graphical illustration of local bump for in two dimensions and d 2 (x) evaluates to for all r that lie within the convex hull of c, namely conv(c). after which (x( quickly decreases linearly to 0. d. has 1 2(2d 1) + 2d ReLUs and 1 1 [log (2d 1)1 layers.
d & M M fo" dd cad c is shown in Figure 6 The local bump
of M
5

---

Published as a conference paper at ICLR 2020
(c e
1/M
1/ME
Í/Me
1/M
cal, c The points in (conv(()) are Figure 6: Local bump 6., where e contains the points ell cal, depicted by the red squares.
By construction (x) decreases to before reaching the next neighboring grid points (Cconv(c) where (²x) : {g E
< {z} denotes the neighboring grid points æ and (r) x EEU U (Figure 4.. The / (ccov((c))) forms hyperrectangle
x
gllx
similarly for for ATU))= (N
in G' and is shown in Figure 6 using red squares. Clearly conv(c) C conv (c))..
Next, give bounds on the loss of precision for the interval-transforone transformaaooonnnn di. We can show that interval analysis can (i) never produce intervals exceeding [0, 0] and (ii) is precise if B does no intersect (c))(N(c)) conv(c).
Lemma 4.3. For all B E B(R"",, ). it holds that dE(B) [0, 1] E B and
[1,1] if C conv(c) (B) 10, if CT con((c)))))))
The formal proof is given in Appendix A The next lemma shows, how ReLU network ne can approximate the slice f& while simultaneously confining the loss of analysis precision.
Lemma 4,4. Let r C Rm be a closed box and let f: T - R be continuous. For all 5 >> there exists of ReLU networks (ng JoSK<NN of size N E IN approximating the N-slicing of (fuJokkeN (Ex as in Definition 4.1 such that for all boxes B E B(T))
[0,
if ( < & if f(B) 2 + 2'
n
[1
and n C [0, 1].
It is important note that in Equation the following, we discuss a proof sketch.
2 mean f and not ft. The proof for Lemma
4.4 given
in Appendix A
Because I is compact and is continuous, f is uniformly continuous by the Heine-Cantor Theorem. So we can pick M E N such that for all x E I satisfying ||y- S 3 holds (/))-/(()) <
We then choose the grid G = ( ym C Rm
Next, we construct for every slice a set Åş of hyperrectangles on the grid G: if a box B E B(T) fulfills f(B) 2 EK+1 + 5. then we add minimal enclosing hyperrectangle e G such that B C conv(c) to Az. where conv(c) denotes the convex hull of c. This implies, using uniform continuity of f and that the grid G fine enough, that fconv(()) 2 EK+1- Since there is only finite number of possible hyperrectangles in G, the set A is clearly finite. The network fulfilling Equation (2)
ny (2) = R
Σ de(x))
cEAL
where is in Definition 4.2 The ng depicted in Figure 3c

---

Published as a conference paper at ICLR 2020
Now, see that Equation ( holds by construction: For all boxes B E (TT such that f {
on B exists d' E As such that B [ conv(c') which implies, using Lemma 4.3 that o² (B) = [1, hence
(B) R (...)) (B) +
Σ
dB())
Ve d' : (B = [0, 1](Lemma 4.3
c
(1,.a](1,1] (21,P2))
[I.P1l] E ((R20)
(i + +11, 1 p2))
-11.1]-
Similarly, if (B) & - holds, then it holds for all As that B does not intersect (conv (c)). Indeed, a E As would violate this, then by construction, f(conv(c)) 2 Ex+1, contradicting f(B) & & - 1. Thus (BB = [0, 0j, and hence (BB = [0, 0). Theorem 4.5. Let T C RRm be closed box and let f: T R be continuous. Then for all d >> exists a ReLU network such that for all B E B(T)
| 6, u 8] C n² (B) C [ - 6, u +
where I := min f(B) and == max f(B).
Proof. Pick NN such that the height of each slice is exactly 5. if this is impossible choose a slightly
smaller 8. Let (na Io be series of networks as in Lemma 4.4 Recall that Eo min f(T). We define the ReLU network
n(x) Eo + 3
nx(x).
(3)
Let B E B(T). Thus we have for all k
f(B) 2 Ek+2 + f(B) 2 Ex+1 +
Lemmo 15
n²((B) = [1
(4)
J(B) S 1 f(B) $ E
Lemma
nB) = 00.0).
(5)
Let E to....,. N 1} such that
E, = min S(B) < Ep+1
(6)
En S max f(B) S Ex+1,
(7)
Thus by Equation 4 for all k E (0, P 2) it holds that n (B) [1, 1] and similarly, by Equation (5) for all & E {q 2,...,,, N 1} it holds that
as depicted in Figure 7
k slices
nx(B)
N-1
[0.0]
(B) 00, 0j. Plugging this into Equation sum into three parts leaves us with
3 after splitting the
g+22
[0.0]
n²(B)= = Eo Σ
(B) +
Σ
(B)
+ 1
Σ k=p+1
(B)
4
k=p-1
=o + (p (p-1))1)
Σ
(B)
9
10, 1]
k=p-1
p+2
10. 1]
Applying the standard rules for interval analysis, leads
4+1
P
nB( = ISp Ep-1 +1+
Σ
nB
p
k=p-1
where we used in the last step, that Eo R-g. Ex- For all terms in the sum except the terms corresponding to the 3 highest and lowest we get
p
(B) [0,
Vk E {p- 2, .....,
, q-
2}.
(8)
Figure 7: Illustration of the proof
for Theorem 4.5
7

---

Published as a conference paper at ICLR 2020
Indeed, from Equation 6 know that there is B such that f(x) 1 Ep+1 Ep+2 2 thus by
Lemma 4.4 ( [z., =z) = [0, 0] for all p p < - - 2. Similarly, from Equation ( we know, that
there is x E B such that f()) 2 E E--1 + 2. thus by Lemma 4.4 n (1x,, ax" [1, 1] for all
+ 2 v k - q 2. So n (B) at least [0, 1]. and by Lemma 4.4 also at most [0, 1|. This leads to
n²(BB= 1 11 Ep +
Σ
n
(B) + E((g 2) - 2000,
Σ
(B
k=p-1
k=q-1
p+1
= 1, 11
Σ
n (B) + 10. - Ep+2)
+ 5
Σ n (B).
k=p-1
k=q-1
We know further, that if p + 3 S than there is an E B such that f(x) 2 Ep43 fp+ + /.2 hence
similar as before n (1z, x|) = [1, 1] and similarly (1 æI) = [1,1] and n² ([z, x]) = [1, 1]. So
know, that Σ -k=p- n (B) includes least [3 3g) and the most [0, 3g Similarly, there exists x' e B such that n (1x1 x01) 0j. n ((x æ²)) [0, 0] and ((x', x')) [0.0].
This leaves us with
p+1
[39,3g]
Σ n [0.3g]
k=p-1
00.0 S
Σ
n (B) S 30.
k=--1
p + > y the lower bound we want to prove becomes vacuous and only the upper one needs to be
proven. Thus we have
1 5.5,u-o - 8) S (p22 Ep-11 S C S 15p-1,,,-2 [ 6, u + 8).
where 1 == min J(B) and = max ((B).
Theorem 4.6 (Universal Provvbel-Provablle Approximation). Let C Rm be compact and f: r + Rd be continuous. For all d E Rgo exists a ReLU network such that for all B e B(T)
| 8, 8] C (B) S - 6],
where I, E Rm such that 4 == min f(B)= k and ug == max x for all k.
Proof. This is a direct consequence of using Theorem 4.5 and the Tietze extension theorem to
produce neural network for each dimension d of the codomain of
Note that Theorem [.1 is a special case of Theorem 4.6 with d = 1 to simplify presentation.
5 CONCLUSION
We proved that for all real valued continuous functions f on compact sets, there exists ReLU network approximating f arbitrarily well with the interval abstraction. This means that for arbitrary input sets, analysis using the interval relaxation yields an over-approximation arbitrarily close to the smallest interval containing all possible outputs. Our theorem affirmatively answers the open question, whether the Universal Approximation Theorem generalizes to Interval analysis.
Our results address the question of whether the interval abstraction is expressive enough to analyse networks approximating interesting functions f. This is of practical importance because interval analysis is the most scalable non-trin trriiilial analysis.
8

---

Published as a conference paper at ICLR 2020
REFERENCES
Naveed Akhtar and Ajmal Mian. Threat of adversarial attacks on deep learning in computer vision: A survey. arXiv preprint arXiv:1801.000 00553, 2018.
Cem Anil, James Lucas, and Roger B. Grosse. Sorting out lipschitz function approximation. In International Conference on Machine Learning, (ICML), 2019.
Raman Arora, Amitabh Basu, Poorya Mianjy, and Anirbit Mukherjee. Understanding deep neural networks with rectified linear units. International Conference on Learning Representations, (ICLR), 2018.
Anish Athalye, Logan Engstrom, Andrew Ilyas, and Kevin Kwok. Synthesizing robust adversarial examples. In International Conference on Machine Learning, (ICML). 2018.
Jeremy E. J. Cohen, Todd Huster, and Ra Cohen. Universal lipschitz approximation in bounded depth neural networks. arXiv preprint arXiv:1904.04861. 2019a.
Jeremy M. Cohen, Elan Rosenfeld. and J. Zico Kolter. Certified adversarial robustness via randomized
smoothing. In International Conference on Machine Learning, (ICML), 2019b.
George Cybenko. Approximation by superpositions of a sigmoidal function. Mathematics of Control, Signals and Systems (MCSS), 1989.
Krishnamurthy Dvijotham, Sven Gowal, Robert Stanforth, Relja Arandjelovic, Brendan O'Donoguue, Jonathan Uesato, and Pushmeet Kohli. Training verified learners with learned verifiers. arXiv preprint 1rXiv::1005 10265, 2018a.
Krishnamurthy Dvijotham, Robert Stanforth, Sven Gowal, Timothy A. Mann, and Pushmeet Kohli. A dual approach to scalable verification of deep networks. In Uncertainty in Artificial Intelligence, (UAI), 2018b.
Kevin Eykholt, Ivan Evtimov, Earlence Fernandes, Bo Li, Amir Rahmati, Chaowei Xiao, Atul Prakash, Tadayoshi Kohno, and Dawn Song. Robust physical- worldd attacks on deep learning visual classification. In IEEE Conference on Computer Vision and Pattern Recognition, (CVPR), 2018.
Timon Gehr, Matthew Mirman, Dana Drachsler-Cohen, Petar Tsankov, Swarat Chaudhuri, and Martin T. Vechev. A12: safety and robustness certification of neural networks with abstract interpretation. In IEEE Symposium on Security and Privacy, (SP), 2018.
Sven Gowal, Krishnamurthy Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Uesato, Relja Arandjelovic, Timothy A. Mann, and Pushmeet Kohli. On the effectiveness of interval bound propagation for training verifiably robust models. arXiv preprint arXiv: 1800.1//10 2018.
Shixiang Gu and Luca Rigazio. Towards deep neural network architectures robust to adversarial examples. In International Conference on Learning Representations, (ICLR), Workshop, 2015.
Juncai He, Lin Li, Jinchao Xu, and Chunyue Zheng. ReLU Deep Neural Networks and Linear Finite Elements. arXiv preprint arXiv: 00397,3 2018.
Kurt Hornik, Maxwell Stincheombe, and Halbert White. Multilayer feedforward networks are universal approximators. Neural Networks, 1989.
Guy Katz, Clark W. Barrett, David L. Dill, Kyle Julian, and Mykel J. Kochenderfer. Reluplex: An efficient SMT solver for verifying deep neural networks. In Computer Aided Verification (CAV), 2017.
Mare Khoury and Dylan Hadfield-Menell. On the geometry of adversarial examples. arXiv preprint arXiv:1811.00525. 2018
Alex Krizhevsky. Learning multiple layers of features from tiny images. 2009.
Y. Lecun, L. Bottou, Y. Bengio, and P. Haffner. Gradient-based learning applied to document recognition. Proc. of the IEEE, 1998.

---

Published as a conference paper at ICLR 2020
Mathias Lécuyer, Vaggelis Atlidakis, Roxana Geambasu, Daniel Hsu, and Suman Jana. Certified robustness to adversarial examples with differential privacy. In IEEE Symposium on Security and Privacy, (SP), 2019.
Bai Li, Changyou Chen, Wenlin Wang, and Lawrence Carin, Certified adversarial robustness with additive noise. In Advances in Neural Information Processing Systems (NeurlPS), 2019.
Matthew Mirman, Timon Gehr, and Martin T. Vechev. Differentiable abstract interpretation for provably robust neural networks. In International Conference on Machine Learning, (ICML), 2018.
Matthew Mirman, Gagandeep Singh, and Martin T. Vechev. A provable defense for deep residual networks. arXiv preprini arXiv: /903/ 2019.
Seyed-Mohsen Moosavi-Dezfooli, Alhussein Fawzi, Omar Fawzi, and Pascal Frossard. Universal adversarial perturbations. In IEEE Conference on Computer Vision and Puttern Recognition, (CVPR), 2017.
Nicolas Papernot, Patrick D. McDaniel, Somesh Jha, Matt Fredrikson, Z. Berkay Celik, and Anan- thram Swami. The limitations of deep learning adversarial settings. IEEE European Symposium Security and Privacy, EuroS&P, 2016.
Aditi Raghunathan, Jacob Steinhardt, and Percy Liang. Semidefinite relaxations for certifying robustness to adversarial examples. In Advances in Neural Information Processing Systems (NeurIPS), 2018a.
Aditi Raghunathan, Jacob Steinhardt, and Percy Liang. Certified defenses against adversarial examples. In International Conference on Learning Representations, (ICLR), 2018b.
Hadi Salman, Greg Yang, Huan Zhang. Cho-Jui Hsieh, and Pengchuan Zhang. convex relaxation barrier to tight robustness verification of neural networks. arXiv preprint arXiv:1902.08722, 2019.
Ludwig Schmidt, Shibani Santurkar, Dimitris Tsipras, Kunal Talwar, and Aleksander Madry. Adver- sarially robust generalization requires more data. In Advances in Neural Information Processing Systems (NeurIPS), 2018.
Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin T. Vechev. Fast and effective robustness certification. In Advances in Neural Information Processing Systems (NeurIPS), 2018.
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin T. Vechev. An abstract domain for certifying neural networks. PACMPL, (POPL), 2019.
Christian Szegedy, Wojciech Zaremba. Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian J. Goodfellow, and Rob Fergus. Intriguing properties of neural networks. International Conference on Learning Representations, (ICLR), 2014.
J. M. Tarela and M. V. Martínez. Region configurations for realizability of lattice piecewise-linear models. Mathematical and Computer Modelling, 1999.
Vincent Tjeng. Kai Y. Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming. In International Conference on Learning Representations, (ICLR), 2019.
Dimitris Tsipras Shibani Santurkar, Logan Engstrom, Alexander Turner, and Aleksander Madry. Robustness may be odds with accuracy. In International Conference on Learning Representations, (ICLR), 2019.
Shiqi Wang, Yizheng Chen, Ahmed Abdou, and Suman Jana. Mixtrain: Scalable training of formally robust neural networks. arXiv preprint 1rXiv:1811.0262. 2018a.
Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. Efficient formal safety analysis of neural networks. In Advances in Neural Information Processing Systems (NeurIPS), 201 8b.
10

---

Published as a conference paper at ICLR 2020
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 networks. In International Conference on Machine Learning, (ICML), 2018.
Eric Wong and Zico Kolter. Provable defenses against adversarial examples via the convex outer adversarial polytope. In International Conference on Machine Learning, (ICML), 2018.
Eric Wong, Frank R. Schmidt, Jan Hendrik Metzen, and J. Zico Kolter. Scaling provable adversarial defenses. In Advances Neural Information Processing Systems (NeurIPS), 2018.
Chaowei Xiao, Bo Li, Jun- Yan Zhu, Warren Hc, Mingyan Liu, and Dawn Song. Generating adversarial examples with adversarial networks. In International Joint Conference on Artificial Intelligence, (IJCAI), 2018.
Kai Y. Xiao, Vincent Tjeng. Nur Muhammad (Mahi) Shafiullah, and Aleksander Madry, Training for faster adversarial robustness verification via inducing relu stability, International Conference on Learning Representations, (ICLR), 2019.
Huan Zhang. Wei Weng, Pin-Yu Chen, Cho-Jui Hsieh, and Luca Daniel. Efficient neural network robustness certification with general activation functions. In Advances Neural Information Processing Systems (NeurIPS), 2018.
Stephan Zheng, Yang Song, Thomas Leung, and Ian J. Goodfellow. Improving the robustness of deep neural networks via stability training. In IEEE Conference on Computer Vision and Pattern Recognition, (CVPR), 2016.

---

Published as a conference paper at ICLR 2020
A PROOFS FOR THE UNIVERSAL INTERVAL-CERTIHED APPROXIMATION
Lemma A.1 (Monotonicity). The operations
are monotone, that is for all [a2. by] and
(01, b1], (az, bul, [cr di), [02, d2] E B(R)) such that [01, b1] _
[ei, dzl S [oz, dzl
holds
[a1, b1] +8 [1, d1] _ [02, d2l +8 [c2, d2
[a1. b1] _ [c1 d1] [ [ag, d2] _ [c2, dg
[01, [1,b1]= [c1 d1] S [0g, dg]
_ [02, de).
Further the operation and R are monotone, that is for all (a, b], [c, d] E B(R) and for all À E Rgo such that (a, b] S [c, d] holds
A # [a, C [c, d] (F((a, bl) S ([c,
Proof.
[a1, bi] +3 [e,, di] = [ai + ci, bi + di] C [02 + 02, b2 + d2]
[u2, d2] 4 (02, d2]
[a) - [ei, di] (an di, b1 ai] C [02 d2, b2 c2] [02, d2]
_ [c2, d2)
[a. = Da Xb] C [A. Ad [Ac, Ad] ( b]) [R(a), R(b) C [(c), R(d)) (=([ed))
Definition A.2 (N-slicing). Let C. R be compact m-dimensional box and let f: r be continuous. The N-slicing of f is set of functions (ʃk Jossonn defined by
0
if f(x) S Ex.
Js: T-R ++
f(x)
Ex
if EN f(x) < Ex+1, Vk: E (O...., N.....N.. N 1}.
Ex+1 Ex otherwise,
where &s : (Smax - Emin), E (O....,NY Emin == min f(T) and Emax == max f(T).
Lemma A.3 (N-slicing). Let {fuloseNN-I be the N-slicing of f. Then for all x E we have f(x) = Eo + EN- ft(2)).
Proof. Pick I and let (O...., N 1) such that & s f(x) S E11 Then
N-1
1-1
N-1
1-1
Eo + Σ fx(x)) = Eu Σ fz(z) + f((z) +
Σ fa(x) = Eo + (SK42 - Ex) + f((x)
k=
k=0
k=1+1
k=0
E + f((x) f(x).
Definition A.4 (clipping). Let a, E E < b. We define the clipping function R. R + R by
(x)) = b- R(b x).
Lemma A.5 (clipping). The function R sends all æ < b to x, and all r > b to Further,
Rd Rf (la', (8) [().
12

---

Published as a conference paper at ICLR 2020
Proof. We show the proof for R| the proof for R(r.M] is similar.
x < b - [|, (3) b R(b x) = b b x x
x 2 b R(o.0) b R(b x) b b
Next,
R (T., = b - R² R²(b-+
b f R=(
= b = ( - -,
= b OF +|R(b - b), R(b -d'l
b bb+ 1+ d'), -R(b b')l
[b R(b -a'),b R(b b')]
[R(..)]aa') (1))
Definition A.6 (nmin). We define the ReLU network nmin: R² + by
nmin(x,8) = 2 -1 -
-
Lemma A.7 (nmin). Let 2; y R, then mmin(2, v) min(x, v).
Proof. Because nmin is symmetric its arguments, we assume w.o.lgg x 2 y.
nmin(x.8)
2 (1 -1 -
x x - - y 1 -
1 (1 -1 -1 -
x + !
If + y 2 0, then
nmin(x, (xr + v)
If + y < 0, then
nmin(x, = 7 (xr + x =
Definition A.8 (nminx). For all N E N21, define ReLU network nminy defined by nmin, (x)
nmin (I1,..... .NN == mmin (min (min (99 ,,n)).
Lemma A.9. Let (a, b), [c, d] E B(R). Then nmin" (ja, 6], d)) nmin' ([c, dI, [a, 6) and
+ d-6 d+ b-
if d S
mmin"((a, b), [c, d))
la 2
if < d and
[a + c
if S d and 2 c
13

---

Published as a conference paper at ICLR 2020
Proof. The symmetry abstract elements is immediate. In the following, omit some of to improve readability.
nminf((a, b), [c,
2(1 -1 -1 -1) R
-1
a. bj c, d
1 -1
[a, b) (c. d
-la, b) [c, d
-1 -1 -1) R
2
[a,b] cc, d
-la,b] + (c. d)
c. c. b d
1
[-b [-b 1o--d,aac a d
= - -1 -1 -1) 12
[a - b
(e- b, -
[R(a + c), R(b d)
1 [1 -1 -1 -1) 2
[R(-b d), R(-a c)
[R(a - d), R(( 0
RR(c b), R(d a)
= 2
(IR(a + R), [R(-b dd), RR -a - c)]
|A(a - (ila-d), R(b - c]] [R(c - b), R(d - a)])
(IR(a+ d()+ [-
c). - R( - d))
+ I-R((b- c). -R(a + a). - -R(c 6)])
(IR(a c) - R( aa - c), R( + - R - d))
2
+ R - c) R(d - a). R(a - d) R(c - b)])
Claim: R(a+c)- R(-a-R(-= a+c. Iatc> 0 then -ac 0 thus the claim in this case. Indeed: If + c 0 then -a - -c 0 thus +c) R(-a - c) = R( Similarly R(b d) R(-b-d)=
--a c) = a +
So the expression simplifies to
1 2
nmin' b). [c, +(a
R(d- a), R(a - d) - R(c - b))
We proceed by case distinction:
Case 1: b - c 0: Then 5bsc
2 (Ia + bb d, b c)
1
2 (Ia + c d,b
c))
la + and 1_
Case 2: d2 0: Then < d a b. By symmetry of nmin equivalent to Case 1. Hence
nmin" [c, d)) = le a -
Case 3: a a-d and b c>> 0:
mmin"((a, b), [c, d)) = 5 b d) + b b- d + a, 0)
- ([a c c b b
la + btd b+d
14

---

Published as a conference paper at ICLR 2020
Thus have
a + add
b+ d-
if S
2
nmin"([a, b), (c, d])
|c + a-b
d+ b-a
if d S
a
if d and
Definition A.10 (neighboring grid points). Let G be as above. We define the set of neighboring grid points of by
N(x) (g G Ig E || all #1 (z)-
For U Rm we define M(U) (M(x)) x xE EUE
Definition A.11 (local bump). Let M E E, G == (7r )m 2 2m]+1 and c
2 (
M
x
Fm M
S G. We define ReI.U neural network &e: Rmm + (0, 1] w.r.t. the grid G by
dc(x) R
nmingm
U 15
{R..n(MM(TT 11++ + 1), R xx) + 11}
Lemma A.12. It holds:
i
if x & conv(W(c))
= i
6c(x) min (O. [)++Ju(Me( -xx) -xx)+11 +1}
if æ E conv(c)
otherwise.
Proof. By case distinction:
Case x & N().. Then there exists k, such that either Ik
1 M
or
x >
+1 M
Then
Mf(xx
& M + 1 or M mx) + is less or equal to 0. Hence
(x(x)== O.
Case x E conv(c). Then for all h holds
4 M
S 2b I &
Thus ME(FR
11) +1 1 and
M
MeC xK) + 12 for all k Hence
(c)))=
where a 2 1.
Case otherwise: For all x exists a i such that Mf(#s smaller equal all other arguments of the function min and smaller or equal to If the smallest element smaller than O, then (x) will evaluate to O, otherwise it will evaluate
M) + or ME M
m3) + is
to M - M ) + or ME " ad xx) + 1. Thus we can just drop R and R from the equations and take the minimum also over O:
(x(x) min U
( $4) RG, Ix) + +11}
m U(MM $ - (=)
min
k=1
min
( + -zx) +1)
k=0
15

---

Published as a conference paper at ICLR 2020
Lemma A.13. Let [u1, 1]...., [uN, 1] be abstract elements of the Interval Domain B. Then nminf ([u1, 11, .....,.,...... [uN, 1]) |u
UN + N, 1].
Proof. By induction. Base case: Let N = 1. Then nmin ([u1, 1]) [uz, 1]. Let N = 2. Then (min 1), [u2, 1]) = [u1 + U2 1, 1].
Induction hypothesis: The property holds for N' s.t. 0< N' O Induction step: Then it also holds for N: amingy ((u1, Il...., [uN, 1]) nmin" (nmin NN/2 ([u1, ... /4/2/22, 1)},
IN/ (1u1N/2 -1, .l...., [uN, IJ)
nmin" + ....44 W/N/21 + [N/2] 1],
[upN/2]+1 + +.. uN + - N + [N/2]] 1])
Lemma A.9
[1 +... + uu + [N/2] - N + [N/2] - 1,1]
[u1
uN + 11 N,
Lemma A.14. Let [a, b), [u, 1] E B(Rg1). Then
nmin b), (u, 1]) S - [
Proof.
nmin"((a, [u, 1]) [a + 2 b+ 1-
if
[a + u b+1 b+1
if
If < u then b 1 b+ - ايط If u S b then -+u b+1 2 zatu-
u+1 a+
So
mmin"([a, b), [u, 1]) S Ja +
--1
b+ll
2 2
Lemma A.15. Let N N22, let [wi, 1,.1)....,,ue [uN - 11, luN, d E B(R) s.t. b 1 be abstract Then there exists E IR s.t.
1t elements of the Interval Domain B. Furthermore, let H(x) 2
nmin x ([uI, I)..... [wN-1, [un, S [u, H Ingo (
Proof. By induction: Let N = 2:
nmink 1], [u2, d))
Lemma A.14
a + 11-1 (d))
Let N 3:
mming((u 1], [u2, 1], [u3, d)) nmin"
(nmin=((un) mmin"(nmin' nmin"([us + u2 - 1, 1], [ug, d))
1], [12, 1)), [uz,
S [ug + a (d)]
nming ([u1, 1], [a, [uz, 1)) nming (lus, dI, [u1, [u, 1]) nmin (nmin² ([ua. d). [uy 1]), [u2, 1]) nmin ([u3 + -1
2- [d)], [u2, 1))
S [ug + tu 2
So aminj d]. [wr, 1], [u2, 1]) is always included in [ua + 41
(1)))))
2
Induction hypothesis: The statement holds for all < N' -
16

---

Published as a conference paper at ICLR 2020
Induction step: Then the property holds also for N:
mming d. [u1, ...... [uN- 1J) amin'(nmin) N/2 (LuN, [u, [u1, ...,.. (u10//1-111)
= (1upw/21 1], ... (uw-1, (4.
umin"([u', [ 1])
C nmin logg N/ (d),
nmin' , [ogg ( (00 (d)), [u", 1))
nmin ([u', (l0g (d)) (u") 1))
nmin' 1 [oRR2 (d)), [v", :1]
[u", H Dog, (
and similarly for other orderings of the arguments. Lemma A.16. Let (x) := 2
1+e
For all N E Nyo. we have that d < - 2 implies H (d) s 0.
Proof. By induction. N 1: Then H(1 2) 1=1-2 =0
Induction hypothesis. The statement holds for all N' such that < N' N.
Induction step: N + 1: d S 1 1%
HN+1 (d) < N+1(1 2 = H (H(1 - 22+1)) = H (1+1-2 = HN 2 0
Lemma A.17. For all boxes B B(RR), have
[1. 1]
if S conv(c)
(B = [0,0] oj
if TBCT | ccov((((c)
Furthermore, @t(B) S [0, 1].
Proof. Let d, be a local bump and let B [a B(RT).. Let [r/. sk), [r.. E B(R) such that o M + [rk s and M
M Me(lax, bx]
17 [ax, bx]) + 1 = 1r2, s
If (a, b] C conv(c): Then < r and 1 < r for all k: E m.. Thus
(ia b]) = R (mmin.... ( R i (x))==))))))))(())(())))........
= Rd (nmin ((1, 1) (1.)))))))))))
= [1, 1]
If [a, b) C r conv (c(c)): Then there exists (p',k') f1.2) {I,..., m) such that
&/' < 1 - 2 flog, No N1+1 Using Lemma An1 Lemma A.15 we now that there exists
"'
u E s.t.
@5( bl) Rd (nminn (Rf (1r (n
R²d (nmin
([Rx. (e
C Rº (nming
(LR (1R 4) U (1
C Rd ([u,0))
= [0,0] 0]
For any (a, b] (B() have (Ba b)) [0, by construction.
17

---

Published as a conference paper at ICLR 2020
Lemma A.18. Let I R be closed box and let f: I - IR be continuous. For all > exists a set ReLU networks (ng losks----- of size IN approximating the N-slicing of f. {ff fieoosgNN-1 (Ex in Definition A.2) such that for all boxes B E B(T)
(B) = [[0,0]
f( I & 2
[1,1] if f(B) 2 +
and (B) C 0,, I].
Proof. Let N E N such that N > 2 Smaee where Emin min f(T) and Emax max f(T). For simplicity we assume I [0, 1|. Using the Heine-Cantor theorem, we get that f is uniformly
continuous, thus there exists a 8' > 0 such that Vr, E r.lly x/|0c < 8' + llf(y) f(=)l < 2
Further, let M E IN such that M 2 and let G be the grid defined by G :- ( C R"
Let C(B) be the set of corner points of the closest hyperrectangle G confining B E B(T). We construct the set
A == {C(B) B B(T): f(B) 2 Ek+1 + 1
We claim that {NaJOSASN-1 defined by
ny (x) R(m,1)
Σ Ed(lo) dc(z)
CeE
satisfies the condition.
Case 1: Let B E B(T) such that f(B) Ek+1 + Then for all g (B)) holds fx(g) 82. By 27 construction exists a d' E As such that C conv(c). Using Lemma 4.3 we get
(B) = Rd [x.1]
Σ
(B{ = R
(B) +
Σ
(B
LEEA
OE c Vo
RR ([1, 1] + [p1. [1,
where Pp), E B(R2o). Indeed, by case distinction:
Case 2: Let B E B(T) such that J(B) < Ea - 5. Then for all E (BB) holds (g) = 0. Further,
B conn((((c) for all E Au because G fine enough. Using Lemma 4.3 we obtain
(B) I1f..11
Σ 22(13)) CE
( 0)) [0,0] 0).
By construction we have n (B) S [0.
18


Reviews:
[{"review_id": "SkenkkVpFB", "reviewer": "AnonReviewer3", "summary": "", "questions": "", "limitations": "", "rating": 3, "confidence": null, "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": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "The paper aims to show that there exist neural networks that can be certified by interval bound propagation. It claims to do this by showing that for any function f, there is a neural network g (close to f) such that interval bound propagation on g obtains bounds that are almost as good as one would get by applying interval bound propagation to f.\n\nThere are a couple issues with this paper. The first is that the main theorem does not imply the claimed high-level take-away in the paper in any practically relevant regime. This is because while the paper does show that there is a network that approximates f well enough, the size of the network in the construction is exponential (for instance, one of the neural network components in the construction involves summing over all hyperrectangles lying within a grid). The result is only plausibly practically relevant if there is a polynomially-sized network for which the bound propagation works.\n\nThe second issue is the comparison to related work, which omits both several key techniques in the literature and two related papers on universal approximation.\n\nOn universal approximation papers, see these two: https://arxiv.org/abs/1904.04861 and https://arxiv.org/abs/1811.05381. They consider a different proof strategy but more plausibly yield networks of reasonable size.\n\nOn key techniques in the literature: \"typically by employing methods based on mixed integerlinear programming, SMT solvers and bound propagation\" ignores several major techniques in the field: convex relaxations (SDP + LP), and randomized smoothing. Similarly, \"specific training methods have beenrecently developed which aim to produce networks that are certifiably robust\" again ignores entire families of techniques; Raghunathan et al. train SDP relaxations to perform well, while Cohen et al. train randomized smoothing to work well. Importantly, randomized smoothing is not about creating an over-approximation of the network but explicitly constructs networks that are smooth.\n\n\"some of the best results achieved on the popular MNIST (LeCun et al., 1998) and CIFAR10(Krizhevsky, 2009) datasets have been obtained with the simple Interval approximation (Gowalet al., 2018; Mirman et al., 2019)\"\n-Is this actually true? I just looked at Mirman et al. and it doesn't seem to explicitly compare to any existing bounds. My impression is that randomized smoothing (Cohen et al.) currently gets the best numbers, if we're allowed to train the network. If not allowed to train the network, Raghunathan et al. (Neurips 2018) performs well and is not compared to in the Mirman paper.\n\nThese omissions must be addressed as the introduction and related work is misleading in its current state.\n\nFinally, some writing issues:\n>>> While the evidence suggests \"no\", we prove that for realisticdatasets and specifications, such a network does exist and its certification can beestablished by propagating lower and upper bounds of each neuron through thenetwork\n\nOne cannot \"prove\" something for \"realistic datasets\", since \"realistic datasets\" is not a formal assumption. Please fix this.\n\n>>> \"the most relaxed yet computationally efficient convex relaxation\"\n\nWhat does most relaxed mean? Most relaxed would most straightforwardly mean outputting the entire space as the set of possibilities at each point, which is clearly not intended.", "extra_scores": {"experience_assessment": "I have published in this field for several years.", "review_assessment:_thoroughness_in_paper_reading": "I made a quick assessment of this paper.", "review_assessment:_checking_correctness_of_experiments": "N/A", "review_assessment:_checking_correctness_of_derivations_and_theory": "I assessed the sensibility of the derivations and theory."}, "extra_text": {}}, {"review_id": "Hkg_xk_TFH", "reviewer": "AnonReviewer2", "summary": "", "questions": "", "limitations": "", "rating": 8, "confidence": null, "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": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "Summary: \nThis paper proves a theoretical result, that for every continuous function f, there exists a ReLU network approximating f well, and for which interval propagation will result in tight bounds.\n\nThe proof is by construction: the function to approximate is decomposed into a sum of functions (slices) with bounded range, which will be approximable to the correct precision. Each slices is approximated as a sum of local bumps, who essentially approximates an indicator function over a grid.\n\nComments:\n* Equation (1) of Theorem 1.1, I assume that the left inclusion could be replaced by [l, u], given that interval propagation generate valid bounds? Or is the case that due to the approximating network being only an approximation, interval propagation on it might not give actual bounds on the real function?\n\nOpinion:\nThe paper is very technical and takes some effort to parse to understand the construction, but the authors do a good job of providing examples and illustrations to make it at least intuitive. The content is clearly novel and the result is far from trivial.\n\nThe only thing that i'm slightly wary is the significance of what is proven. The paper shows that approximating a continuous function with a network such that bound propagation works well on it is feasible.\nOn the other hand, the motivation given is \"given a dataset and a specification, is there a network that is both certified and accurate with respect to these\", which is a slightly different problem. If this was proven to be yes, then we would know that when our robust training fails, this is due to optimization not being good enough or our not network not having enough capacity. The result proven here does not suffice, because it pre-suppose the existence of a correct function, that would match the dataset and specification, which is not guaranteed (see for example the proofs that robustness and accuracy are at odds, or you can just imagine verification of robustness for too-large radius which would lead to infeasible specification). I still like the paper and I think it might just be a matter of framing the abstract and introduction.\n\nDo the authors have an implementation, even for only toy-size examples, of the generation of a Neural Network approximating a given function or is this purely theoretical? Especially when the proof is constructive like this, this can strengthen the confidence that no subtle mistakes have been made. If so, this should be mentioned.\n\nPotential typos:\nPage 4: \"Further\" -> \"Furthermore\"?\nPage 5: \"Increasing the fines\" -> \"Increasing the finesse?\"\nPage 6, just before Lemma 4.3, missing a mathcal before the N?\n\nDisclaimer:\nI carefully checked the derivations in the paper but only assessed the sensibility of the proofs in the appendix.\n", "extra_scores": {"experience_assessment": "I have published one or two papers in this area.", "review_assessment:_thoroughness_in_paper_reading": "N/A", "review_assessment:_checking_correctness_of_experiments": "N/A", "review_assessment:_checking_correctness_of_derivations_and_theory": "I assessed the sensibility of the derivations and theory."}, "extra_text": {}}, {"review_id": "HJgjoVkWcr", "reviewer": "AnonReviewer1", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": null, "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": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "This paper proves the universal approximation property of interval-certified ReLU networks. Such a network achieves the best certified accuracy against l_infty adversaries at large epsilons on MNIST and CIFAR10, but the certified accuracy is still far from satisfaction. With the results from this paper, we can at least make sure the interval-certified ReLU networks is able to fit the robust classifier with arbitrarily small error if it exists. \n\nI did not check the details of the proofs, but I think such a theorem is a great reference for future work. \n\nHowever, we cannot conclude whether a network with a moderate size exists to fit the robust classifier well from this paper. From the construction of local bumps (nmin), the number of neurons needed to represent a bump function grows exponentially with the input dimension, which makes the size of the network vacuously large when the input is images. We are not getting any closer to improving the certified robustness with this paper.", "extra_scores": {"experience_assessment": "I have read many papers in this area.", "review_assessment:_thoroughness_in_paper_reading": "I made a quick assessment of this paper.", "review_assessment:_checking_correctness_of_experiments": "N/A", "review_assessment:_checking_correctness_of_derivations_and_theory": "I assessed the sensibility of the derivations and theory."}, "extra_text": {}}]

Author rebuttal:

Meta-review: This work shows that there exist neural networks that can be certified by interval bound propagation. It provides interesting and surprising theoretical insights, although analysis requires the networks to be impractically large and hence does not directly yield practical advances. 
Decision: Accept (Poster)