The Fundamental Limits of Neural Networks for Interval Certified Robustness
Authors: Matthew B Mirman
Maximilian Baader
Martin Vechev
Venue: Accepted by TMLR ()

Abstract: Interval analysis (or interval bound propagation, IBP) is a popular technique for verifying and training provably robust deep neural networks, a fundamental challenge in the area of reliable machine learning. However, despite substantial efforts, progress on addressing this key challenge has stagnated, calling into question whether interval analysis is a viable path forward.

In this paper we present a fundamental result on the limitation of neural networks for interval analyzable robust classification. Our main theorem shows that non-invertible functions can not be built such that interval analysis is precise everywhere. Given this, we derive a paradox: while every dataset can be robustly classified, there are simple datasets that can not be provably robustly classified with interval analysis.


Published in Transactions on Machine Learning Research (8/2022)
The Fundamental Limits of Neural Networks for Interval Certified Robustness
Matthew Mirman
natthew.mirmanten etha. ch
Maximilian Baader
musincilian. buader@inf,ellie ch
Martin Vechev
martin, www.tiiieeceeeiiifffoo wtheee
Department of Computer Science, ETH Zurich
Reviewed on OpenReview: https: // openreview. net/ forum? id- fsacLLU35V
Abstract
Interval analysis (or interval bound propagation, IBP) is popular technique for verifying and training provably robust deep neural networks, a fundamental challenge in the area of reliable machine learning. However, despite substantial efforts, progress on addressing this key chal- lenge has stagnated, calling into question whether interval analysis is a viable path forward.
In this paper present a fundamental result on the limitation of neural networks for interval analyzable robust classification. Our main theorem shows that non-invertible functions can not be built such that interval analysis is procise everywhere. Given this, we derive paradox: while every dataset can be robustly classified, there are simple datasets that can not be provably robustly classified with interval analysis.
1 Introduction
As neural networks are increasingly used in safety critical environments, ensuring their behavior with formal verification has become a highly active research direction (Liu et al., 2019a; Huang et al., 2020). Because neural networks are often too large for complete verification methods, incomplete analysis techniques are frequently employed (Gehr et al., 2018) these can scale to larger models though may fail to prove property that actually holds (as demonstrated in Fig. 1). Indeed, recent progress in constructing provable neural networks has been achieved thanks leveraging incomplete methods, and particularly interval (box) bound propagation (Mirman et al., 2018). However, while many improvements to provable defenses have been published (Gowal et. al., 2018; Zhang et. al., 2018; 2020; Xiao et. al., 2019; Wong et. al., 2018; Liu et al., 2021; Boopathy et al., 2021; Shi et al., 2021; Xu et al., 2021) (most building on IBP), progress remains far from satisfactory: the state-of-the-art certified robust accuracy is roughly 60% on CIFAR10 (Balunovic & Vechev, 2020), compared to state-of ofee----tthhhtttt standard accuracies of above 95%. The stagnation of progress in constructing provably robust neural networks has led to fundamental theoretical question:
Do efficiently verifiable neural networks exist?
(Fundamental Theoretical Question)
The first result addressing this question was investigated by Baader et al. (2020) which proved analog to the universal approximation theorem (Cybenko, 1989; Hornik et al., 1989) for interval-analyzable networks. Wang et al. (2020) further showed that two hidden layer networks could also be interval-analyzabll approximators. moonymous (2022) also demensttrated that training with interval propagation converges with high probability. While is helpful to know that searching for networks which can be easily analyzed might not be futile, these results do not explain, and even contradict the provable training gap that observed practico. A preliminary negative result was shown by Wang al. (2020): verifying the robustness of arbitrary neural networks in general and thus translating arbitrary neural networks into interval-nnalyablle forms is NP-hard.

---

Published in Transactions on Machine Learning Research (8/2022)
2
x
f(x
3
(a) Network. The circles
which represent ReLUs contain their biases.
(b) Network values f f(x) for x E [-4,4]
1
(c) 1st affine
(d) 1st ReLU
(e) 3)2nnd affine
(1) 2nd ReLU
(g) 3rd affine
(b) 3rd ReLU
Figure 1: An example of a neural network which is in fact robust, yet which interval arithmetic fails to prove is robust. The three intervals L = [-3, 1--3-11 -1] (w), M [--,, 1] (a) and R = [1.3] (m) are depicted using dashed lines Fig. 1b. The interval propagation through the network shown using the rectangles. The conerete values are shown by the dashed lines. After the 2nd affine layer (Fig. 1e) the orange and green box overlap while the orange lines do not overlap, demonstrating loss of precision. The output Interval is [-1,1] for all three input intervals L, M and R. In graphs (c) through (h) the vertical axis corresponds to the outputs of the upper set of neurons in (a) and the horizontal axis corresponds to the outputs of the lower set of neurons.
In our work, we provide a strong negative answer, thus explaining the provable training gap: we demonstrate that non-trivial datasets can not be classified by interval-provable networks.
Formally, given a neural network, or more generally any program, fi X + +, the goal of verification is to algorithmically prove that maps an imput spec (specification); Sy S X, to a subset of an output spec, So V where the spec So) is member of a spec-sel 8 C P(X) P()). Interval analysis in particular replaces the basic operations of f with interval arithmetic (Moore, 1966; Hickey et al., 2001), producing an Intervals()). of such that every element of S₁ is mapped by f to an element of f (Sr). As representing and computing intervals is efficient, f is proven to meet the spee So) by proxy of proving f S So. Here we consider interval robustness classification specs where the input specs are closed intervals, and the output specs are either Ry0 or Reo-
interval extension, f#; Intervals(
Main contributions. In this paper, we present the first proofs capturing key limitations (incompleteness) of using ReLU based neural networks to build robust classifiers that can be certified with interval analysis:
Fundamental Imprecision of Interval Analysis (Thcorem 4.10): In this theorem we identify for the first time the highly general conditions under which interval analysis looses precision. Specifically, we show that non non-invertible functions can not be built using affine transformations and ReLUs such that over-approximation using interval analysis is precise everywhere. To make proving this theorem possible, we need to keep track of a strict interior relationship even when the dimension of the network increases in irrelevant ways. To do this, we develop the relative subset. relation (Definition 4.2) and prove various useful properties in Section 4.1.
Impossibility of Interval-Provabll Robust Classifiers (Section 5): Here we show that classi- fiers in particular can not be built such that they are provable robust with interval analysis in two key ways. We first demonstrate Corollary 5.2 how this theorem can be immediately applied show that it is impossible to construct a feed-forwant ReLU-neural network of any shape (e.g., residual, convo- lutional, dense, fully-connected) that is perfectly provably robust (Definition 5.1) with interval analysis for even unrealistically simple dataset with only three points. Informally, perfect here describes the property that the spec-set is maximal in that it includes as many valid robustness spees describing the dataset as possible without including any input specs which might render the spec-set unsatisfiable, including those that touch the shared border between two points. We then show in Theorem 5.8 that even when the requirement for perfect provability is relaxed to regions that are distant from cach other (a-inte (a-interval provable with a < 1 as in Definition 5.3), there are datasets with O(a=1) points that can not be provably robustly classified with one-hidden layer networks using interval analysis.
2

---

Published in Transactions on Machine Learning Research (8/2022)
Possibility of Interval-Agnostic Robust Networks (Proposition 5.10 and 5.11): Here we demonstrate the paradox that in both of the previous two cases, perfectly robust classifiers (Definition 5.1) can always be constructed, even if they are not necessarily provably robust using interval analysis. In the case of 1-d datascts, these can furthermore be constructed to be one-layer deep. Together with Theorem 5.8 and Corollary 5.2 this implies that the restriction that a network be analyzable with interval-arihhmetic is severely limiting.
2 Problem Motivation
Studying the robustness of artificial neural networks has become an important area of rescarch as they are increasingly deployed in safety-critical applications such as self-driving cars (Bojarski et al., 2016). Szegedy et al. (2013) first demonstrated that neural networks classifying images can be fooled into misclassificatiin by imperceptible pixel changes in an otherwise correctly classified image.
Many of these looling techniques, known as adversarial allacks, have been developed (Carlini & Wagner, 2017; Goodfellow et al., 2015; Kurakin et al., 2016; Shaham et al., 2015; Croce & Hein, 2019b; Papernot et al., 2016a; Wong et al., 2019b). To defend against these attack, mothods strengthening models have been proposed (Papernot et al., 2016b; Tramèr et al., 2017: Wong et al., 2019a; Stutz et al., 2020; Bastani et al., 2016; Croce & Hein, 2020). A particular line of research aims to provide formal guarantees (i.e., verify) that neural networks behave correctly (Katz et al., 2017; Singh et al., 2018; 2019; Boopathy et al., 2019; Liu et al., 2019b; Wang et al., 2018: Balunovic et al., 2019; Zhang et al., 2021; Lin et al., 2021; Croce & Hein, 2019a; Croce et al., 2018). As complete verification of a neural network is NP-Hard (Katz et. al., 2017), the majority of modern techniques are incomplete and based on over-approximaatig the behavior of a network (Gehr et al., 2018). While incomplete methods can be highly efficient, a correct classification of a network might not be provably correct, as illustrated in Fig. 1. In fact, for naturally trained neural networks, only a small percentage of non-attackable input images are verifiable.
To improve verification rates, techniques to train networks amenable to verification (Raghunathan et al., 2018; Mirman et al., 2018; Wong & Kolter, 2018; Wong et al., 2018) have been developed. While this has been an active area of research, the state-of-the-art developed by Balunovic & Vechev (2020) achieves a certified robust accuracy of 60.5% on CIFAR10, which is low given that state-of-the-art standard accuracy is over 95%.
The recent plateau of progress in closing this gap has raised concerns on whether there are theoretical limitations to neural network analysis (Salman al., 2019). In this work, we prove fundamental limitations, which help explain the significant gap between certified robust accuracy, and standard accuracy. We focus interval analysis, as some of the most successful and widely used methods are based on this relaxation (Mirman et al., 2018; Gowal et al., 2018).
3 Background
We now introduce key concepts and notation, a reference to which can be found in Appendix C.
3.1 General Notation
We begin with some general notation. For some positive natural & E N we write [K] = RR.. Given sets Ti....,yy Th and a set Y T x... x Th we write Y|: for the restriction to the dimension i, or Y|, = {u:: y E Y}.
Many of our proofs require spaces with slightly richer structure than d-dimensional real vector spaces. We will call these real binary-tree tensor-spaces, the class of which can be defined inductively as F (Ti x T2: Tı, T3 I {.). Given a space S E IT, we can inductively define the set L8 of closed, non- empty, axis-aligned boxes over S: If Ti T2 for Ti, T2 T then 3² = (B, B2: B1 E "h B2 "h and if S R then Φ {[a, b) laa b E RA < b) or Ø³ = II the set of real intervals.
In cases where this richer tree structure is unnecessary, we consider Rd e T for d E N>1 to be real binary- tree tensor space by assuming a canonical ordering: T = R x Rd-1, We abuse notation and say 3d is specifically the set of closed, non-empty, axis-aligned boxes on the d-dimensional real vector space. We note that gg = xd
3

---

Published in Transactions on Machine Learning Research (8/2022)
We write the box with center E Ie and radius 1220 (,(c) = {x: Vi [d] E [-1,1].=; c, + fra). We also write B (²((()= = {y E R²: || - ylls= < <e} for a E Rd and e E Rs0 for an open box. For given box Be Ødt let CBB) denole its center and R(B) denote its radius vector such that B (C(B)
For any bounded and non-empty set C C for E J, the lhull, written Hos (C), is the smallest axis aligned box containing C, which we formally define inductively: (C) for S1, S2 E I and Hox(C) (C) = [in[(C)) sup(C)) if S = R.
(Cl2) if = X1
For any set S we write P(S) to mean the powerset of S. A- and S S A we write f[S] or (S) to mcan {f(s): 8 E S): but sometimes abuse notation and write f(S) == f[S] to avoid clutter. Similarly, we also occasionally write f o even when I and g are non invertible to mean (go f)-
3.2 Robustness and Interval Certification (IBP)
is some function (i.e., neural network). We say that this network assigns a label E {-1,1} to a point a E R if sign f(x) = L. In our case, we discuss lo0 -adversaaaa region specifications. In this case, we say that f is c-robust around x with label I if Va' E Bz)x). f(x)) =1.
Suppose f: Rd +
The goal of robustness certification is to provide guarantee that neural network is robust at some point. However, an analysis not producing proof of robustness at point does not mean that the neural network is non-robust at that point. This leads to efficient methods in terms of over-approzimation, originally described as abstract-innerppeelan (Cousot & Cousot, 1977) and applied to neural networks by Gehr et al. (2018).
Interval Analysis In this paper, we focus on the Interval (or Box) relaxation, and in particular, Interval Bound Propagation (TBP) (Gowal al., 2018), also known as interval analysis, or the Interval domain for interaattntterpretatiion. An interval, B ød can either be represented as center c e Rd and radius RR50
as before, or as lower-bound and upper bound, 4,44 la E F respectively such that for each dimension j E [d].
we have 4, Σ lu.j- The two representations are related as follows: 4 = c r and la = c or c = 2 (4 + (.) and r= - 1..-4) 14).
Analyzing Neural Networks The application of IBP to neural networks with ReLU-activations is straightforward. In this paper, we consider (feed forward) neural networks defined inductively as follows:
Definition 3. A o-(neural) network with o-activations is a program, J, inductively defined by the grammar f = fo fl Sump///Dpl loo for n E R and n' + 0, and interpreted as function with domain I I F and codomain O E T as follows:
Sequential Computation: Given f = 91 92 and g1. 92 are interpreted as functions 91: B + O and 92: I B, we say f: - O computes f(xx) = (92(z)).
Parallel: Given f (g1.92) and g1, 92 are interpreted functions 91: I O₂ and g2 In O2 and we say f: T x 12 > O₁ x O2 computes [(x) = (gi
Addition: Given f Sum we say f: 2 R computes ((x) = x1 x2.
Duplication: Given f = Dup, we say f: I I2 computes f(x) = (x, x).
Constant: Given f = K we say : I + R computes f(x) =
Multiplication by a Constant: Given f k- we say f: ER + computes f(x) x.
Activation: Given f = a we say f: R + R computes f(x) = ozx)
We nole that duplication and addition are the only relational operations here.
For the purposes of exploring its limits, we view IBP as a method that implicitly constructs a transformed function which acts on intervals. We describe this transformed function inductively as well:
Definition 3.2 (Interval Analysis). The interval transformation, f#, of a ReL.U-network is as follows:
4

---

Published in Transactions on Machine Learning Research (8/2022)
(a) A
(b) A = B
(c)
(d) A zZ B
Figure 2: Visualization of the relative interior relation. Green (n) boxes are A and purple (1) boxes are B.
Sequential Computation: If f = 91 92 then ft (B) = of (gf (B)).
Parallel: If f (91,92) then f* = şl [ x 92 # (B)2).
Addilion: Tf f
Sum then (*(B) = {a a E B/1 A Bl2)
Duplication: If f Dup then f (B) B x B.
Constand: If f = k. for K E R then (BB == {n}
Multiplication by a Constant: If f K- for some non-zero R, then (B( {n- (R- B}.
Aclivalion: If ReLU, then f (B) = (ReL.((x): x BJ.
Proposition 3.3. The interval transformer, , over-approximates f, meaning that (
4 Fundamental Imprecision of Interval Analysis
Here we show our main result, that no neural network can be perfectly provably robust with interval analysis for simple functions. We first introduce the necessary machinery (in particular, the concept of relative interior outlined Fig. 2) and lemmas that allow us to show a relationship between whether the network represents an invertible function, and where there is an approximation error.
Counterintuitively, rather than being able to show that the transformed network is imprecise for specific input box (i.e,, that for specific box B, we know [[B] Ç. I# (B)), we must, for any input box B containing non-invertible points on its surface, find an input box, A, that is a strict subset of B (via a particular notion of strict defined below), such that f[B] S (A). The fact that A is a strict subset of the relative interior of B implies that interval analysis is imprecise enough on the network such that can not be used to prove desired properties of B (such that f is perfectly robust for B). is however crucial that A not be required to be too strict a subset of B. One might be tempted find subsets of the topological interior of B. This however leads to significant technical issucs: need to have notion of strict subset that applies even when some of the neurons in the network are unused (and zero). One can imagine the set representing the possible activations of those neurons as lower dimensional surface embedded in a higher dimensional space, as in the case of Fig. 2(c) and (d). In this case, the interior of B would be empty, even though we might have identified a subset of it that induces imprecision.
4.1 The Relative Subset Relation
We begin by formalizing the intuitive concept from Fig. 2 using the known notion of relative interior, and demonstrating some useful lemmas related to it. First, recall for a set S C gd that the affine hall of S, written (S) the smallest linear-uusppace of Rd that contains S.
Definition 4.1. We recall the standard definition of relative interior:
relint(S) = for E S: Fe 1a (x) af)((S) C).
5

---

Published in Transactions on Machine Learning Research (8/2022)
We note that if S E H we can restate the relative interior relint(S) = {r S: Vi [d] ((CU where 5Iß is the interior of S's restriction to dimension i.
Definition 4.2 (Relative Subset). A is a relative subset of B, written AC B, if and only if A C relint (B).
We note that if A, B E Hd we can rephrase C B as follows: A S B and for each dimension, i, where B is not empty, Ali S BE or more concisely, Vi E [d]. (B) # = Al. S Blj). In particular, in one dimension, for real intervals [a, b] and [a', bJ] we have [a, bj c [a', 8] if and only if a' <a D' or a' 8' = b.
Let A, A', can be found in Appendix B.1):
, B, B', C. be bounded and non-empty subsets of Rd in the following lemmas (the proofs of which
Lemma 4.3 (Respects Projection). AC B implies Al [ B/.-
Lemma 4.4 (Respects Cartesian Product). AC B and A' B' implics A A'C B
Lemma 4.5 (Downward Union). AC C and B C C. implies AUBEC
Lemma 4.6 (Downward Hull). C E gd and A C C implies Ho (A) CC
The following two lemmas are trivial and we frequently use them without mention:
Lemma 4.7 (Singleton Reflezivity). {a} {a}. Lemma 4.8 (Center-Singleton is Always a Relative Subset). A e 3d implics {C(A)) c A.
It is important to note that some simple related properties counterintuitively do not always hold. Namely, if AE and C C it is not always the case that ACG C. Furthermore, if A C and A' E B' it is not always the case that Hos (A U A') C ('U
4.2 Inversion With Respect to The Relative Subset Relation
Here we demonstrate that neural networks can loosely invert sets with respect to the relative subset relation. More formally, for any neural network f with ReLU-activations, one can essentially always find a strict subset, X' of the relative interior of box X that the neural network maps to superset of a specified subset Y of the relative interior of the hull of f(X).
Lemma 4.9 (Concrete Relative Inversion). Suppose is food-forward network with ReLU-activations and Y,X' E nd and X is compact and non-emply. Then C (fx(() = AX' (
PROOF OVERVIEW. (Full Proof in Appendic B.2) The proof is by structural induction on the construction of f. We the lemma itself the induction hypothesis. Below outline three key cases of the structural induction: sequential computations, relational parallel computations, and ReLU:
Case: = g h.
(Sequential Computation) Subproof. By definition, Y H h(X)). Thus, there is some H H (h(X) such that Y C (H) by the induction hypothesis on g. Applying the induction hypothesis again with the network h, we get set X'E Hxx such that H C (X')... Thus, Y C g (H) S c o li#t (x*())= f (X').
Case: Dup. Subproof. We know Y11 (X) and (X) by Lemma 4.3. By Lemma 4.5 and Lemma 4.6, know X' == (Y UYk2 is relative subset of Hox (X), and thus Y C X' x x'= f (X').
(Duplication)
Case: = (91,
(Parallel)

---

Published in Transactions on Machine Learning Research (8/2022)
Figure 3: A visualization of the claims of Theorem 4.10. The neural network, I classifies three imputs 2 = 2, to respective labels y -1,1, as in Corollary 5.2. Here, 0 is the non-invertability and (y) = 1).
y
These two points mapping to y, which constitute N (y), are marked in red (n). The bs-
8*h (M)
hull, (N), is marked in green (=). The perfect approximation of f on Hoa (N) (i.e., ((u,f(v) f(u)): E N)) is marked in blue (-). We can see that the interval approximation of the relative interior box M C Ho (N) looses precision by looking at the orange region (s).
-2
2
M
Hoo (N)
Subproof.
We know both that 1/1 C Hoo (X)(() and Y (x) hypothesis twice to produce L [ Hox (Xl1) and R C Hos (X12) such that Y1 S. of (L) and 1|2 S of (R). We choose X' = x R. By Lemmaa 4.4, we have X' C HX)()). Then x 92 (X'2)) f* (X').
apply the induction
Y S g (X)
Case: f = ReLU.
(Aclivalion) Subproof. We know that f: I3 + R, which simplifies the proof. In this case, loo-hull of S(X) must either be a subset of R20 so either Y is the singleton set containing zero, or a subset of Rso. In the first case, we pick X' to be an casy-to-pick (the singleton set containing conter as in Lemma 4.8) relative subset of the hull of X. Otherwise, we can pick Y itself, since ReLU(Y)) = (X).
Case: f for e # O.
(Mult. by a Conslant)
Subproof. Let X' = ())))) Ø = inf X, x, = sup X, 31 = inf Y and Vu = sup Y. We note that 21 = C(Hso (X)) (Ho (X)). Similar expressions can be derived for Ja Vt and Vu- Supposing c > 0 (the other case is analogous) and ø < xa (the proof is similar when equal), we have cri < V S ya cæ by Hox
Then clearly, Y C f(X)). Because we know that = 1 we can write
Then we know xn < |e- ly- Fu, and thus X' Hoo (X).
(Further Cases in Appendir B.2)
4.3 Impossibility for Non-Invertibility
We now prove central result, that non-invertible neural networks necessarily induce approximation imprecision. Essentially, visualized in Fig. 3, we show that there is box, M which is relative subset (i.e., usually very strict subset) of the -bull of any region for which the network is entirely not injective, such that analyzing the network with M includes any of the non-invertible points in the inferred approximation.
The key idea that while there may be non-invertibilities on the boundary, M does not include these, as it is a relative subset. Thus, we can use this thcorem to infer areas where analyzing the network produces approximations that include points that not in the concrete, or true, set of possible network outputs.
Theorem 4.10 (Fundamental Imprecision of Interval). Suppose f:S +T with S.T e T is a ReLU-network and y E T. and N C (y) is compact and non-empty. Then assuming M E 28.
3M H.. (M))
PROOP OVERVIEW. (Full Proof in Appendir B.2) Again, the proof by structural induction on the construction of f, using the theorem itself as the induction hypothesis. Below we outline three key cases: sequential computations, relational parallel computations, and addition:
7

---

Published in Transactions on Machine Learning Research (8/2022)
Cose: f = g h h
(Sequential Computation)
Subproof. We know that N S -h- o and thus can use the induction hypothesis on h to produce Hoo (N))) such that E (M'). By Lemma 4.9, we know that there is some M F (N)(NN such that M' C h## (M) and thus that y E g*t o h# (M).
Case: = Dup.
(Duplication)
Subproof. N = {yr} because N S (uz). By singleton reflexivity, N C (N).N). Thus, E (N).
Case: 92)-
(Paralell) Subproof. First know N/1 S 9i (v)) and N|2 S 92 (y2) by projection and that M1 and N|2 still compact and non-empty, Thus, by the induction hypothesis twice we see that there are boxes M1 C Hoo (N) and M2 C Ho (N12) such that y1 E of (M1) and 32 # (M2). Then Mj x M2 E Hoo (N) by Lemma 4.4. Then y1 E f (M1 x M2)1 and y2 E J#M x M2)12 by
soundness. Thus, there is some box M C (N) such that y E (M).
Case: f = Sum.
(Addition)
Subproof. Because f: R22 + R, we know (w) = {(a, y -
We can pick M = [C)HH) and
demonstrate that M E Hoo (N) and that E (MM).
Case: f = ReLU.
(Activation)
Subproof. In this case, y RcLU(x)) can either be zero or greater than zero. y > 0, then N N = {v} by the definition of ReLU, and thus that {y} C Hox(N) and E f ((v)). Otherwise, y = 0 and thus N = (-oo,0, 0j. We thus know (C(H))(N))) E (N) and finally y E f (IC(Hsc(N)))
(Further Cases Appendie B.2)
5 The Paradox of Interval Provable Network Construction
In this section we first demonstrate a varicty of unexpectedly and problematically simple scenarios (although Theorem 4.10 implies many more) that appear in a dataset, imply the impossibility of constructing an interval-provably robust network. We then show the paradox that in each of these cases, and further for every dataset, it is possible to build perfectly robust classifier without consideration of interval analysis.
5.1 Impossibility of Perfect Provable Robustness of Unconstrained Networks
Here we demonstrate an immediate application of Theorem 4.10: there are simple datasets that no neural network can perfectly (as defined below), and provably robustly with interval classify.
Definition 5.1. We say that neural network f: Idd - R is perfectly v-(provable) robust classifier with E (0, 1] for points II, E RRd and labels I In E (-1,1) if given 5 = 2 mingzz ||,; xylloo then Ve < Pō. Vi E (zB. > O. If it is provable then we also have that Vi E [m]. (B. > O.
We note that the specification-set induced by this definition is perfect as described in the introduction, in that it inchudes every valid robustncss specification describing the dataset (æ1, 4....., (x); every robustness specification (Sr,,, So.:) where æ; E S1,; and 4 So,: and Sr, Ç Ba(x;) is part of the specification-sel, but not robustness specifications for different (and possibly differently classified) points that would be touching.
Corollary 5.2 (Perfectly Provably Robust Classifiers are Impossible). There is no feed forward ReL.Unctwork that is a perfectly 1-provably robust classifier for the dataset D = ((-2, - 1), (0, (2, -1)}
PROOF. Suppose f: RR a perfectly 1-provably classifier for this dataset. Then by continuity we know that f(-1) f(1) = 0, and thus that {-1,1} S f-) (which is a compact non-empty set). Then by application of Theorem 4.10, there is some set M Hoo (1),,1)) such that 0 E f# (M). Rephrased, this
8

---

Published in Transactions on Machine Learning Research (8/2022)
L+
L
R+
R-
(a) ReLU(-x)
(b) -eeU((>))
(c) ReLU(z)
(d) -ReLU(x)
Figure 4: The orientations of neurons captured by the sets Lt, L-, R+, and R-
means that there are a, b E (-1,1) such that e f# (Ia, b)). This contradicts the definition of a provably I-provable robust classifier however.
5.2 Impossibility of Imperfect Provable Robustness for One-Layer Networks
In this section wo show a impossibility rosult for the case where the robust regions around inputs in the dataset do not overlap one another, and are thus imperfectly robust. To do this, we focus on single layer neural networks, as prior work shows possibility results here for deeper networks (Baader al., 2020). Specifically, we present an upper-bound on the number of points that can be proven to be robustly classified with interval for single-layer network. We do this by constructing worst-case dataset, which we call flips. We begin by formalizing this dataset, and the notion of robust and provable robustness for classifier this dataset.
Definition 5.3. We say:
A d-flip is a point &, Idd with 2t,1 and ž., with label 1, = (-1)'. If d is unspecified, is taken to mean 1-flip.
f: R IR classifier for k flips Vi (b). ((x,) = 1,
F: x ((R) an a-classifier for k flips Vi E [k:. Vy F( - a, 2; + aal). sign 1, F. {i.}.
If fP (the perfect transformation) an a-classifier for is flips, we say an a-robust classifier for k flips.
If ft (the interval transformation from Definition 3.2) an a-classifier for k flips, then we say that f is provably a-robust classifier for k. flips.
We now specify the notion of single-layer network for which we demonstrate bounds:
Definition 5.4. single-layer o-network, f: R + R, with n--eurons and a r-activations a function with pre- activation weights, N E R", pre-activation bias, E R", post-activation weights, M E R., and post-activation bias, d IR (the weights and biases are known as parameters), such that f(x) M (Nx +d.
We note that while Definition 3.2 defines ordering of addition, the above definition does not. While concreto-addition is associative, this does not necessarily hold for abstract addition. However, thankfully, for the interval Iransformation, it is, and the bounds we demonstrate apply to any ordering of the operations.
Definition 5.5. Given a single-layer ReLU-network, f with n neurons and pre/post-activation weights N, M, impreccison-ccotributtionn (respectively) of f at x are:
the absolute and standard imprecision- contributions
AD,((=)
Σ
M,N.).
Ni
and ID.s(x)
Σ
M,N,
20M..EENE
where can be the set. L = Rgo, the set R == R20 or R and S can be + = B20, the set - := Rço or R.
Intuitively, L+,L-, R+. R correspond to the orientations that a neuron can take, as visualized in Fig. 4. L (resp. R) results in contributions from neurons that activate as the argument x of the impredsioon-oontibttion function decreases (resp. increases). Note that f'(x)) In. (x) if the derivative of f is defined at
9

---

Published in Transactions on Machine Learning Research (8/2022)
Lemma 5.6 (End-Neuron Imprecision-Boundy For all and single-layer ReLU-networks that classify k-flips for k= = [x]] + 5, we have K < max (x. An,
PROOF OVERVIEW. We prove this by induction on c c= [k], using two simultancous inductive invariants:
cs AL,+((22 An,+(22) An,+ (8x) Au,+ (Ste,,
and
S AL,-(81) An,-(81) + (8k-1 (2x-(2x-1).
This proof involves two key observations: (i) once
in a direction has accumulated, it will only be larger for points further in that direction, (ii) one must measure not just the accumulated growth of the impreeciion-
at the ends of the approximated data (&1 and εt) in the out-wards directed neurons, but the growth of the relative imprecision--cottribttiin excluding contribution from in-wards directed neurons. We make these observations more precise in the full proof in the appendix.
(Full proof in Appendir A)
Before demonstrating the result for single layer networks, we require one further lemma, used to find a specific data-point with enough accumulated imprecision contribution to cause a violation:
Lemma 5.7 Blower-Bound on Imprecision- Contribution). For any a S 1 and k k [2] 5 and single-layer ReLU-network that classifies & flips, there is some point [R]] such that
a + a) + f(2)- a))
a))
< ( + An,((R) - a) Ax, a.)
PROOF OVERVIEW. By using c == we can apply Lemma 5.6 (with c), to show bounds for either the left right-most & (i.e., j or j = k). For this point, use the knowledge that the function is contimuous, piecewise differentiable, to find points E [&g - 2, and u E [zy. + a] such that (())))()aaa)) f() and (u) f(8)+0)-f(1)) so we can use that
f'(1) f'(u) Is,R(() - IR.x(u)
S AL, - a) - An, + a
that -c, An,n(2)), and that
1,a (f(2) aa) + +[(z - a))
= -1, -(x))-((,, f(x,
-( + i,e
to produce the final upper bound.
(Full proof in Appendir A)
We are now ready to show our main theorem, an upper bound on the number flips that can be provably robustly classified with a single layer network.
Theorem 5.8 Songle-Layer Limit). No single-layer ReL can provably a-robustly classify [ more flips for any (0, 1].
PROOF OVERVIEW. The proof is by direct application of Lemma 5.7, and expansion of the definition of the derivative. We demonstrate that for the found by Lemma 5.7, the center of the box must be strictly closer (Full proof in Appendix A)
to than its radius.
Corollary 5.9 (Single-Laye) Limit in Multiple Dimensions). No single-layer ReLU-networt can provably a-robustly classify [ + 5 or more d-flips for any a 10.
10

---

Published in Transactions on Machine Learning Research (8/2022)
PROOF. Suppose f: R² + R is single-layer network that can provably a-robustly classify 2 [ d-flips for some a E (0, 1]. Then we construct a function f"; R + R mapping x f(Mx) where M E R is defined as having M1,1 and M,1 0 for > Then f can provably a-robustly classify flips for some and is only 1-layer which contradiets Theorem 5.8.
5.3 One-layer strong interval-agnosee possibility
Proposition 5.10 (Single-Layer Perfectly Robust Classifiers Always Erist). For any dataset of n points E R and labels I 1- there is one-hiddene ReLU-network that perfectly robustly (but not necessarily provably) classifies it.
PROOF. present the construction explicitly. Let = min(/æ; - xz/: i f1 in
f(u) =
Σ 1m1
4 ReLU [3 - (x) 5)}]
-ReLU 13 - m;)]
+ +RLLU
[1 - (xq + 5))]
One check that this works by plugging in 2z, although full proof is by induction. While this is not immediately of the form described for one-hidden layer networks, one can see casily how to algebraically convert this into that form. Because we only care about robustness, and not interval provability of S, this is sufficient.
Proposition 5.11 (Perfectly Robust Multi- Sulti-DDimensioal Classifiers Always Erist). For any datasct n points v, Rd and labels E (-1, there ReLU-network that perfectly robustly (but not necessarily provably) classifies it.
PROOF. Here present special case of the proof shown by Baader et al. (2020), and do not worry about the number of layers or implicit projections involved. Again, we present the construction explicitly. Let = min{]1æ;- xy]loc: : i # j}. We define a neural indicator function Bump, for each dimension k [d]:
Bump, (v) ReLU [1 (2r,, - 6))]
-ReLU [3 m(,k)]]
+ReLU [ (3x - (Zi + 8))]
We furthermore inductively define neural implementation of d-value minimum:
1 nming(a,b) b) = (ReLU(a + b) - ReLU(-a - b) - ReLU(a b) - ReLUU-a +b) 2
uming(at...... == nmin (a1, mmina-mie... (qi.._)(
given d > 2
Finally, bring this all together in function:
f(v) =
B,,m,,
We can first see that amina(a1...... aa) ming dg Given that Bump,, & (v) is in (0, 1] if lly 2i 8 and is 0 otherwise, can see that sign f sign 1 if byy zilloo 8.
]
11

---

Published in Transactions on Machine Learning Research (8/2022)
6 Discussion and Future Work
While we limited the scope of our discussion to Reltiivvi,, we note that our theorems extend trivially to any monotone bounded aclivation. However, we observe that non-monotonic activations functions (such as absolute value) do not admit the same forms of theorems. Our preliminary experiments however indicate that substituting ReLU with these activation functions does not result casier training or provability. This suggests that there are more general versions of the theorems presented here, in particular relating the difficulty of program synthesis with the relational expressiveness of the relaxation used to verify the specification.
7 Conclusion
In this work we proved two theorems that demonstrate fundamental limitations on the expressiveness of interval provable neural networks. We showed that no ReLU-network can perfectly provably classify simple one-dimensional datasets containing only three points. This indicates a fundamental loss of precision whenever ReLU-networks are analyzed using interval arithmetic, which can not be regained, no matter the network. Further, we showed that a single hidden layer ReLU-network can not provably classify simple datasets even without the requirement for nerfectness, which is in stark contrast to classical universal approximation theorems, where single hidden layer is sufficient. This shows that the approximate capabilities of interval provable networks are lower compared to standard neural networks.
References
Anonymous. On the convergence of certified robust training with interval bound propagation. In Submilled to The Tenth International Conference on Learning Representations, 2022. URL https: //openreview
under review.
Maximilian Baader, Matthew Mirman, and Martin Vechev. Universal approximation with certified networks. ICIR, 2020.
Mislav Balunovic and Martin Vechev. Adversarial training and provable defenses: Bridging the gap. In ICLR, 2020.
Mislav Balunovic, Maximilian Baader, Gagandeep Singh, Timon Gehr, and Martin Vechev. Certifying geometric robustness of neural networks. In NewrIPS, 2019.
Osbert Bastani, Yani Ioannou, Leonidas Lampropoulos, Dimitrios Vytiniotis, Aditya V. Nori, and Antonio Criminisi. Measuring neural net robustness with constraints. In NeurIPS, 2016.
Mariusz Bojarski, Davide Del Testa, Daniel Dworakowski, Bernhard Firner, Beat Flepp, Prasoon Goyal, Lawrence D. Jackel, Mathew Monfort, Urs Muller, Jiakai Zhang, Xin Zhang, Jake Zhao, and Karol Zieba. End to end lcarning for self-driving cars. arXiv preprint 1rri::664.07999 2016.
Akhilan Boopathy; Tsni-Wei Weng, Pin-Yu Chen, Sijia Liu, and Luca Daniel. Cnn-cert: An efficient framework for certifying robustness of convolutional neural networks. In AAAI, volume 33, 2019.
Akhilan Boopathy, Tsui-Wei Weng, Sijia Liu, Pin-Yu Chen, Gaoyuan Zhang, and Luca Daniel. Fast training of provably robust neural networks by singleprop. arXie preprint (XXi:2102.001000 2021.
Nicholas Carlini and David A. Wagner. Towards evaluating the robustness of neural networks. In Symposiun Security and Privacy (SP), 2017.
Patrick Cousot and Radhia Cousot. Abstract interpretation: unified lattice model for static analysis of
programs by construction approximation of fixpoints. In Symposium on Principles of Programmingg Languages (POPL), 1977.
Francesco Croce and Matthias Hein. Provable robustness against all adversarial ly berttuurrations for p >> In ICLR, 2019a.
12

---

Published in Transactions on Machine Learning Research (8/2022)
Francesco Croce and Matthias Hein. Sparse and imperceivable adversarial attacks. In Proceedings of the IEEE/CVF International Conference on Computer Vision (ICCV), 2019b.
Francesco Croce and Matthias Hein. Reliable evaluation of adversarial robustness with an ensemble of diverse parameter-free attacks. In JCML, 2020.
Francesco Croce, Maksym Andriushchenko, and Matthias Hein. Provable robustness of relu networks via maximization of linear regions. arXiv preprint arXtt:1810.07488,, 2018.
George Cybenko. Approximation by superpositions of a sigmoidal function. Mathematics of Control, Signals and Systems (MCSS), 1989.
Timon Gehr, Matthew Mirman, Petar Tsankov, Dana Drachsler Cohen, Martin Vechev, and Swarat Chaudhuri. Ai2: Safety and robustness certification of neural networks with abstract interpretation. In Symposium on Security and Privacy (SP), 2018.
Ian J Goodfellow, Jonathon Shlens, and Christian Szegedy. Explaining and harnessing adversarial examples. In ICLR, 2015.
Sven Gowal, Krishnamurthy Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Uesato, Timothy Mann, and Pushmeet Kohli. On the effectiveness of interval bound propagation for training verifiably robust models. arXiv preprint 1rXi::1800. 12715, 2018.
Timothy Hickey, Qun Ju, and Maarten H Van Enden. Interval arithmetic: From principles to implementation. Journal of the ACM (JACM), 48(5):1038- 1068, 2001.
Kurt Hornik, Maxwell B. Stinchcombe, and Halbert White. Multilayer feedforward networks are universal approximators. Neural Networks, 1989.
Xiaowei Huang, Daniel Kroening, Wenjie Ruan, James Sharp, Youcheng Sun, Emese Thamo, Min Wu, and Xinping Yi. A survey of safety and trustworthiness of deep neural networks: Verification, testing, adversarial attack and defence, and interpretability. Computer Science Review, 37:100270, 2020.
Guy Katz, Clark Barrett, David L Dill, Kyle Julian, and Mykel J Kochenderfer. Reluplex: An efficient smt solver for verifying deep neural networks. In International Conference on Computer Aided Verification (CAV), 2017.
Alexey Kurakin, Ian J. Goodfellow, and Samy Bengio. Adversarial examples in the physical world. arXiv preprint 1oni::607.000 02533, 2016.
Wan-Yi Yi Lin, Fatemeh Sheikholeslami, Leslie Rice, J Zico Kolter, et al. Certified robustness against physically- realizable patch attack via randomized cropping. In ICLR, 2021.
Changliu Liu, Tomer Arnon, Christopher Lazarus, Christopher Strong, Clark Barrett, and Mykel J Kochenderfer. Algorithms for verifying deep neural networks. arXiv preprint (rXim:1903.06777 2019a.
Chen Liu, Ryota Tomioka, and Volkan Cevher. On certifying non-uniform bound against adversarial attacks. In ICML, 2019b.
Chen Liu, Mathieu Salzmann, and Sabine Süsstrunk. Training provably robust models by polyhedral envelope regularization. IEEE Transactions on Newral Networks and Learning Systems, 2021.
Matthew Mirman, Timon Gehr, and Martin Vechev. Differentiable abstract interpretation for provably robust neural networks. In ICML, 2018.
Ramon E Moore. Interval analysis. Prentico-Hall Englewood Cliffs, NJ, 1966.
Nicolas Papernot, Patrick McDaniel, and Ian Goodfellow. Transferability in machine learning: from phenomena black-box attacks using adversarial samples. arXiv preprint 6665:660077771 6a.
13

---

Published in Transactions on Machine Learning Research (8/2022)
Nicolas Papernot, Patrick D. McDaniel, Xi Wu, Somesh Jha, and Ananthram Swami. Distillation as defense to adversarial perturbations against deep neural networks. In IEEE Symposium on Securily and Privacy (SP), 2016b.
Aditi Raghunathan, Jacob Steinhardt, and Percy Liang. Certified defenses against adversarial examples. In ICLR, 2018.
Hadi Salman, Greg Yang, Huan Zhang, Cho-Jui Hsieh, and Pengchuan Zhang. convex relaxation barrier tight robustncss verification of neural networks. In NewrIPS, 2019.
Uri Shaham, Yutaro Yamada, and Sahand Negahban. Understanding adversarial training: Increasing local stability of neural nets through robust optimization. arXiv preprint urzio:1511.05432, 2015.
Zhouxing Shi, Yihan Wang, Huan Zhang, Jinfeng Yi, and Cho-Jui Hsieh. Fast certified robust training with short warmup. Advances Neural Information Processing Systems, 2021.
Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin Vechev. Fast and effective robustness certification. In NewrIPS, 2018.
Gagandcep Singh, Timon Gchr, Markus Püschel, and Martin Vechev. An abstract domain for certifying neural networks. In POPL, 2019.
David Stutz, Matthias Hein, and Bernt Schicle. Confidence-calibrateed adversarial training: Generalizing to unseen attacks. In ICML, 2020.
Christian Szegedy, Wojeiech Zaremba, Ilya Sutskever, Joan Bruna, Dumitru Erhan, Ian J. Goodfellow, and Rob Fergus. Intriguing properties of neural networks. arXiv preprint (rXio:131..6199 2013.
Florian Tramer, Alexey Kurakin, Nicolas Papernot, Ian Goodfellow, Dan Bonch, and Patrick McDaniel. Ensemble adversarial training: Attacks and defenses. orXiv preprint Xrx::17755. 705.07204. 2017.
Shiqi Wang, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. Efficient formal safety analysis of neural networks. Tn NewrIPS, 2018.
Zi Wang, Aws Albarghouthi, Gautam Prakriya, and Somesh Jha. Interval universal approximation for neural networks. In POPL, 2020.
Eric Wong and Zico Kolter. Provable defenses against adversarial examples via the convex outer adversarial polytope. 2018
Eric Wong, Frank Schmidt, Jan Hendrik Metzen, and J Zico Kolter. Scaling provable adversarial defenses. In NewrIPS, 2018.
Eric Wong, Leslie Rice, and J Zico Kolter. Fast is better than free: Revisiting adversarial training. In ICLR, 2019a.
Eric Wong, Frank Schmidt, and Zico Kolter. Wasserstein adversarial examples via projected sinkhorn iterations. In ICML, 2019b.
Kai Xiao, Vincent Tjeng, Nur Muhammad Shafiullah, and Aleksander Madry. Training for faster adversarial robustness verification via inducing rehu stability. International Conference on Learning Representations, 2019.
Kaidi Xu, Huan Zhang, Shiqi Wang, Yihan Wang, Suman Jana, Xue Lin, and Cho-Jui Hsich. Fast and Complete: Enabling complete neural network verification with rapid and massively parallel incomplete verifiers. In International Conference on Learning Representations, 2021. URL https://openreevie.. net/ torum7id-mV2cB116...
Huan Zhang, Wei Weng, Pin-Yu Chen, Cho-Jui Hsich, and Luca Daniel. Efficient neural network robustness certification with general activation functions. In Advonces in Neural Information Processing Systems (NuerIPS), dec 2018.
14

---

Published in Transactions on Machine Learning Research (8/2022)
Huan Zhang, Hongge Chen, Chaowei Xiao, Sven Gowal, Robert Stanforth, Bo Li, Duane Boning, and Cho-Jui Hsieh. Towards stable and efficient training of verifiably robust neural networks. In TCLR, 2020.
Yuhao Zhang, Aws Albarghouthi, and Loris D'Antoni. Certified robustness to programmable transformations in Istms. In EMNLP, 2021.
15

---

Published in Transactions on Machine Learning Research (8/2022)
A Extended Proofs for Single Hidden Layer Network Results
Here we restate the theorems and show the full proofs for the results in Section 5.2.
Lemma 5.6 (End-Neuron Imprecision- Borrridsioo-Buundd.... For all x 2 and single-layer ReLU-networks f that classify k-flips for [ + 5, we have R < max ma.())..(21)) An, An.
PROOF OF 3.6. We prove this by induction on c.
Induction Hypothesis: Given c E (0, -1, -2} there some even natural number S ReLU(( + 2) + such that for any single-layer ReLU-nctwork, f that classifies & flips we have
Ac, - An,+ (82) + An, (8x) - AL.+ (8t)), and e < (x1) - (R1)(21) + AR. (xx-() AL,- ($x-1))
Base Case: Suppose S 0. Subproof. Pick k = 2. Then
AL, (82) (R2) + AR,+(80) AL,+( = 0 2 C, and
ARR (81) ) + - ($2-1) - AL, (8g-1) = 2
4
Induction Step: Supposc > 0, and the induction hypothesis holds for -- 2.
Subproof. Then there some even natural k < ReLUU(c-2-222 such that for any single-layer ReL U-network, f. that is a classifier for k'' flips we have
c 2 A (82) - AR, (82) + AR,((RN)) - AL (8x),
and c c- 2
A (x1) - AR.-($8 + AR. (x - AA. (2
Pick k = + Then k is even, and k < RcLU(c) + 4 < ReLU + 2) + since 0.
Let f any single-layer ReLU-network that classifies flips. Then f also classifies flips. We only show the positive bound, that c S AL,+ AR,+ + AR+(#ts) AL,+ The proof for the negative bound is analogous.
There must be some point I E [& x such that ('()) _ -1 by the mean value theorem (since UeLt-wowwsrks are continuuus) and because f(2x) = = -f($*+1).
Similarly, there must be some point u E [& such that 1 f'(u). Thus,
(') - ((( 2
< Ir,t (1) + Ir,-- (u) - In,+ + In, (u)
(1) II,-(1) IR.+(1) -I).-II).
We know It.-(u) (1) < 0 and [R)- - II,-(1) < and Iz,+ = -A (1) and
In.t (1) = An,+(t) (t) for any 80
2 < A1,+((4 (u)+ + (R)
+ Ar.+ (1) - AR.+ (1)-
We also know (r, increases as / decreases and AR,S(!) increases / increases,
2 < Ar,, AR, ($x))
+ AL.+ AR, (8xr),
16

---

Published in Transactions on Machine Learning Research (8/2022)
By combining with the positive inductive bound, we get
- ( Ar, (x2) An, + (82) + An,+ (8x) Ar.+ (2x) ( + AR,+ (3x) + Ar., (3w) )- An, (3x) - AL,+ - AR,+ (82) - AL,+ (3x) + AR. (3x))
which proves the positive bound of the induction hypothesis for c.
Thus, by induction, we find that there some S [c] + such that, after removing the negative terms and increasing by swapping &2 with & and ă with &y:
c 1 S AL,+ (81) + AR.+ (8x), and c 1 S Ar,- (81) + Ar.- (2x))
Summing these oquations together gives us:
2c 2 S (x1) + AR,+ (Rx) + (1x) + (Rx-(xx) (x
and thus that a < An.
Lemma 5.7 Klower-Bound on Imprecision--Cnntiiuuie Contribution.). For any a S 1 and k 2 [21 + 5 and single-layer ReLU-network that classifies k flips, there is some point [k] such that
- a)) i (f(x) + a) + -(t;-
< AR + An,R(Rj a) Ar, + aa)
PROOF OF 5.7. Let k 2 12a 12 +5, and define c c= 2. Because 2 [|c|] +5, can Lemmna 5.6 to get that |c| < (x. (.
For convenience, we define fL(x) = a- (f(x) - f(x - a)) and = a + - f(x)).
We only show the proof when le| < (x))( the other case analogous, but picking j = In this case we know 0 < AL1 and thus,
i + a) + f(z - a)) S f(()) Fn((1)) +
There must be point [ x. such that F((1) s f(() and point u [,, + al such that ('(u) s fn(u).
We can thus derive, in manner similar to what is seen in Lemia 5.6:
- - fa(21) f( (u) s II++ + II, (1) (1) + IR,+ + +I,
- (I,+(u) II,-(uu) In.+ (u) - IR.-(W)
5 Ir,- (1) - IIR--(u)
< A - a) ARR( +a).
fx())) - FR(X1) + Aa,((2)) + ALx(RI
a) AR, + as c lel < ALLR(8)) (a.)(21).
17

---

Published in Transactions on Machine Learning Research (8/2022)
Theorem 5.8 (Single-Lager Limit). No single-layer ReL can provably a-robustly classify [ + 5 more flips for any E (0, 1].
Suppose E (0, 1], and assume, for the sake of contradiction, that ʃ is a single-layer ReL.U-network with weights N, .M and biases b, d that provably a-robustly classifies [ + 5 flips.
PROOF OF 5.8.
We begin the proof by labeling the intermodiate states of interval analysis for point &, with interval radius a of the network f:
aaj = ReLU( + [N]a)
va. ReLU(N&, + (N]a)
Wa o/a Vjaa
Ca.j = jja + V1j00
8 ((2) = 2 Mca. + d, 2 |M]wss)
where the notation |X| means the point-wise absolute value (i.e., |1|; = (Xil).
Then our assumption for contradiction tells us that for any j E [kt], we have that not in (*2), a)) and thus that (-I) 2d) 2 WWa...
Let j be such that Lemma 5.7 tells has I,a (f($)+ ( aa)) AR,R ( + (z)+
We note that by expanding the definitions, sums, and meaning of absolute value, can derive that Mca, + 2d = M(r + vaj) + 2d = f(2, + a) + f(2, a). so our assumption for contradiction thus implics [M & (-1y + 2d) = (-1) + a [(2 a).
We perform the following deduction:
(-1)(f((3) + aa) + f(z) - a))
Σ
M + 6, + a(NN - [M
2,
Σ
MM + b, +o|Ns) - |M
N12,
M
Σ a|M,N,
2b
Σ
|M by a/N:)
Σ
a|MNI+ +
Σ
a|MN
b2
2.
M.N. +
Σ
M.N.
+b,20
Niky 22
2 a(AAR((2)) An, -a) + AL.R( + a))
2 (,(s( +a) + f(2, -a))
which is a contradiction.
18

---

Published in Transactions on Machine Learning Research (8/2022)
B Extended Proofs for General Impossibility Results
Here we restate the theorems and show the full proofs for the results in Scction 4.
B.1 Proofs for Relative Interior Lemmas
In the following lemmas, let A',', B', be bounded and non-empty subsets of R
Lemma 4.3 (Respects Projection). A C B implies Ale C B/c.
PROOF OF 4.3. Let y E Al.. Then there is some E A such that = y. Then relint( by ACB B. Then there is some e > 0 such that (z) n af S B. Then N,(x)); n af(()) S B), We know (B) S aB)( given 2 E (B. it must be an affine combination of the i'th dimension of elements of B. Letting z' be the same affine combination those elements, 2 = 2, so E af) Then N₂ (x1h) n (B)) Bl; and thus E relint(B|,))
Lemma 4.4 (Respects Cartesian Product). AC B and A' C B' implies Ax x A B'.
PROOF OF 4.4. Let (x,x") E A x A'. Then because x E A we know x E relint and respectively x' E relint Then there is some 6 > such that (x) n (B) S B, and é > such that (2(x') n aff (B') S B'. We know (An A') x (Bn
(A B) n (A' x B'): (a, E (An A' x (B)B) implies A and b E BOB' (a, E A x B and (a, X'x (a, b) E (AX
Then, know (B x B") S BB) af(()") (b, E af B") implies (b, b') is affine combination of elements of B x B' which implics b is an affine combination of elements from B and d' is an affine combination of elements from B', so (b,b") E (B) x (B'(
Thus for = min we know Nx(a,x²) naff B') CB Thus (x,z') E relint (B x B').
Lemma 4.5 (Downward Union). AEC and B C implies AUBCC.
PROOF OF 4.5. Suppose x E A. Then I E A or x E B. Either way, we know x E relint(C)..
Lemma 4.6 (Dounward Hull). CE Ld and AC C implies (A)
PROOF OF 4.6. CE Le implies Cli E B, and thus Cl2 is convex so relint(Cl)) is convex. We know A) C C)2 by Lemma 4.3, so Hoc (A)) E Cla by convexity Cl and that How is the convex hull in one dimension. Thus, by Lemma 4.4, we know Hx,11) x ... Hox = Ch x... x Cla- Because C E 3dd we know Ch1 x..xX x Cla and similarly that Hoo (A) = Hox (Ah1) ... Hoc (Ala). Thus, (3) CC c
19

---

Published in Transactions on Machine Learning Research (8/2022)
B.2 Proofs for Inversion and Impossibility Theorems
Lemma 4.9 (Concrele Relative Inversion). Suppose is leed-forward network with ReI.U-activations and Y' E 2dd and X is compact and non-empty. Then
Y C Hoo(f(() = X.K c Hox (X). f
PROOF OF 4.9. The proof is by structural induction on the construction of the network f, assuming the lemma itself as the induction hypothesis for any network with fewer operations than f. First, assume Y C (X()).
Case: f = g h.
(Sequential Computation)
Subproof. By definition, Y C by the induction hypothesis on g. Applying the induction hypothesis again with the network h, we get a set X' C (X) such that C h## (X'). Thus, Y S g (H) 9* o (X*) f (X').
Thus, there exists some H C Hoo (X)) such that Y C g (H)
Case: f = Dup.
(Duplication)
Subproof. Then 1/1 C (X) and Y/2 C (X) by Lemma 4.3, We choose X' (Y UY22 which we know by Lemma 4.5 and Lemma 4.6, is such that X'c (X). Thus, Yh S X' and Y/2 S so
Y X x X*
Case: f = (g1, 92)-
(Parallel)
Subproof. Then Y/1 E (91 (X1)) and Y/2 C Hoo (92((12) by definition. Then applying the induction # (L) and Y12 S 92
hypothesis twice produces LC Hox (Xl1) and RCHx (X12) such that Y1 S Then we choose X' L x R which we know by Lemma 4.4, is such that X' c (X). Then C ot (X'l)) _ (X'l2) -
# (R).
Case: f ==0 C.
(Conslant)
Subproof. Here, any subset X' X will suffice. Then we can let X' (C(X)).
Case: f e- for e + 0.
(Multiplication by a Conslant)
Subproof. Let X' B (CY). Then clearly, Y C f(X). It remains to show that X'c Hoo (X). For the remainder of this subproof, because we know that Y and Vu sup We note that I C(Hoo (X)) R(H (X)) and on. Supposing y1 > (the other case is analogous) and zι < zu (the proof is similar when they equal), we have сεı < S The < cr. by Y Hoo (f())).
we will write x; = inf X, J, = sup X,
Then we know x < - y1 < |c- yu < In, and thus X' C Hoo (X).
Case: ReL.U.
(Activation)
20

---

Published in Transactions on Machine Learning Research (8/2022)
Subproof.
Again, because know that d = 1 we will write 2t = inf X, 2u sup and y == inf and sup We know that inf Hx (X()) = ReLU(()) and sup (((())) = ReI.U(x... Thus by
Y c Hoo((f()) we know ReLU(az) S y1 S ya S ReLUU(z). We then have two cases we need to
address:
Suppose: Ta > 0.
Subproof. Here we define X' 1yt Vul. We thus have 2 S RcLU(()) yt S Un <RL(((.)) I. provided Hi < Tu. Otherwise we know ø ReLU(()) y1 yı ReLU((z)) = Iu we have X' [ Hoo(X)
Suppose: Iu O.
Subproof. Define X' = (uttar) ). ReI.U (u = 0 = y1 yn implies X' c Hx)(X).
Thus, in both cases we can find X' C (X) such that Y S (
Case: - Sum.
(Addition)
Subproof. Conveniently again, Y is one-dimensional. Either How (f())) is single point or it is not:
Assume: Hox (f(X)) is single point.
Subproof. Then inf Y = sup Y = inf H.c (f(X)) = sup Hox (f()). Let Y. , In this case, we know there is some compact and non-empty set Z C R such that X [(x',' -y=z)) x' E Z). Then we can pick X' = ((C( (
which is the singleton-set containing the center of the -hull of X and thus X' Hxx(X) by Lemma 4.8.
Otherwise: (f)( not a single point.
Subproof.
We know inf (((())) inf S sup sup HJ))) Because Y is one- dimensional and relative subset of the non-singular Hoo (f(X)) know Y C Ho (HHoo)))
Let a, b, Ta, Th, T. be as follows:
((H)))
ra R(Ho (x(1)): = R(Ho (X12)).
b = C(Hoo
y = C(Y),
and
ry = R(Y).
Then Hos (X) Br, (a) Br, (b) and thus Y C f(B,. (a) B,, (6)) Biratro) 6).
Choose X'= = =B,(x)) for x and r defined as:
a b + = a To
T1 = T TyTa
To Tb
y- b
Ty
22 b + mb
and 12
Na + Tb
ra + Tb
Then clearly, œ1 x2 y, and 1ı + = Tv Y C f(X).
Thus ry < ra + rb by Y C B (a + b).
This also tells us that y + ry < a + b + ra + ro and y - ry > a b ro - Tb. If r. *
we can derive I1 +r, < <a +r and x - ri > a ra. Similarly, if r, + we can derive
Ø2 + r2 b+ Tb and 22 12 b Tb. Thus, X1 B,, (a) and X₂ E B,, and thus by Lemma 4.4 we have X' C B,, (a) B,, (b) (X).
21

---

Published in Transactions on Machine Learning Research (8/2022)
Thus, in both cases, there exists an X' (X) such that Y f(') S fx))).
As any feed forward neural network (without input-value dependent loops) can be expressed using these operations without modifying the result under interval analysis, by induction 3X' C (X). Y S f# (X').
22

---

Published in Transactions on Machine Learning Research (8/2022)
Theorem 4.10 (Fundamental Imprecision of Interval). Suppose f: T with S.T E I is ReLU-network and y E I and N S (y) is compact and non-empty. Then assuming M E y
3M C Hxx (
PROOF OF 4.10. The proof is by structural induction on the construction of the network J, assuming the theorem itself as the induction hypothesis for any network with fewer operations than f.
Let f: R" + Rm a feed forward network with ReLU activations, and let y E RR" and let N S fy) be compact and non-empty. Then f one of the following cases:
Case: f = h
(Sequential Computation)
Subproof. We first know that S h-1 (v) by the definition of f. We then infer that h(N) S Hox Hox(N) is compact and non-empty by application the continuous function h. Thus, by induction on h(N) and g there some M' c (xo(hN)) such that y E 9* (M"). Thus, by Lemma 4.9, we know that there is some M Hoo(N) such that M' C h## (M). Thus, y E ** h (M) (*MM..
Case: f = Dup.
(Duplication) Subproof. We have N C (313 n {12) so N = tn By singleton reflexivity, C (N) Thus, y E f (NN..
Case: f = (g1, 92).
(Parallel)
Subproof. First we know Nı S (1)) and N/2 S 92 (U2) by projection and that N|1 and N|2 are still compact and non-emply. Thus, by the induction hypothesis twice we see that there are boxes Mi E (N))) and Ma E Hox (Nl2) such that yı of (M1) and v2 E I (M2). Then M1 M2 Hoa by Lemma 4.4. Then yn f# (M1 M2)h and y2 8# (M1 x M2)l2 by soundness. Thus, there is some box M C Hoc (N) such that f (M).
Case: f == C.
(Conslant)
Subproof. We know y = e and thus f-1 = R. let M (N)) c Ho), then y E f# (M).
Case: f(v)= = c. for c 0.
(Mulliplication by a Conslant)
Subproof. We know (y) = fc-1 1. .y] = NE HN)(N) by N being non-empty and thus E f (N).
Case: f ReLU,
(Activation)
Subproof. Then ReLU(x) can either be zero or greater than zero.
Case: > 0
Subproof. N = {8} by def. of ReLU, and we know {8} C (N) and y e f ((v)).
4
23

---

Published in Transactions on Machine Learning Research (8/2022)
Case: y
Subproof. N = (- by def. of ReLU, Thus (M))) E (N) and y e f* (1C(H
Because y the result of a ReLU, must have been one of these two possibilities, and in both cases we could find some M C (N) such that y E (+(M).
Case: f = Sum.
(Addition)
Subproof. In this case, we know N C (v) {(a,8) a): a a RJ. We pick M = [C(H>x t (N). Given N bounded, we know:
inf N/1 + sup sup.N] N| inf N|2 sup N/2
C(Hoo(N))
2
inf M/1 + sup N|1 2y inf N/1 sup N/1
2
We can rewrite f(C(H.so(N))
inf N/1 sup sup.Ni N/1
2y inf N|1 sup N/1 y.
((C(Hoo(N))
2
Thus, y= [(C(Hx((N)) E (M(M
Thus, 3M C. Hos (N). E f# (M).
24

---

Published in Transactions on Machine Learning Research (8/2022)
C Reference of Symbols and Notation
General Notation (Sec. 3.1)
Notation for Analysis (Sec. 3.2)
[k] The inder set {I....,k) k} for EEN
:P:P(S P(T)
The perfect transformer, defined the mapping S + (f(x): E
Y/: The restriction of Y C Ti .... x Tk to dimension i, or formally, the set {y: y e Y
f B H
The interval transformation of a a- network f: S
The powerset operator
[[s]
The lifted application of f to a subset S of its domain. Formally, the set [ 8}
Relative Subsets (Sec. 4.1)
aff(S)
The smallest linear- sinear-susppcee of IRd containing S
5
The topological interior of S
ReLU
The function mapping x E R to max
relint(S)
The relative interior. Formally, the set {o E S: 3e > 0. (² n aff S S}
Ar B The relative subset relation, defined formally, as C relint(B)
Spaces and Domains (Sec. 3.1)
N The set of natural numbers The set of real numbers
Single-Layer Networks (Sec. 5.2)
x; An input point in Fa defined 81,1 2i and &, for j >
T The class of binary-tree tensor-spaces defined (T1 T2: T2,Th T) {R)
1, An output label equal to (-1)*
Φ The set of closed, non-empty, axis axis-aligned bozes over S E T
An,s(#)
The absolute imprecision-contribuuiio
Dd For d E N, this is the set of closed, non- empty, axis-aligned boses over Rd
In,s(#)
The standard imprreisionn-comriiutiion
Notation for Boxes (Sec. 3.1)
(c) The closed bor with center E Rd and radius E 20
R(B) The radius the box B
C(B) The center of the box B
(S) The Loe -hull, smallest axis aligned box containing S
25


Reviews:
[{"review_id": "EXR55tIcSy", "reviewer": "Reviewer_f5Ug", "summary": "", "questions": "", "limitations": "", "rating": null, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "Strength:\n- Proved theorems and lemmas \n- Figures which helped to follow the paper context\n- Interesting results with trivial examples in the end to show problems with interval networks in context of robustness (this could be a reason of worse results for interval networks compared to classic ones)\n\nWeakness:\n- Changing notation and mixing different use cases throughout the paper make it hard to read and follow\n- Some notations in Figures hard to follow\n- Consideration of mainly 1d input space and problems with theorems for multi-dimensional inputs (here some clarification is needed from authors on comments below to be sure that everything holds in $\\mathbb{R^n}$)\n- Absence of any comments on flips dataset and paradox in multi-dimentional case (or how to inherit it from 1d case)", "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": "", "paper_topic_and_main_contributions": "", "excitement": null, "reproducibility": null, "ethical_concerns": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "summary_of_contributions": "In this paper authors investigate robustness (adversarial robustness / math context of stable solution in well-posed problems) on interval neural networks. The main contributions of the paper:\n- theorem and its proof \"Fundamental imprecision of intervals\": for the feed forward network with ReLU activation $f: \\mathbb{R}^n\\to\\mathbb{R}^m$ under some conditions there could exist some input interval where the network produces approximation which includes values that are not possible / true / concrete network outputs. This means that interval network looses precision.\n- based on this theorem and introducing definition of provably robust classifier authors show simple 1d binary classification dataset with 3 points for which there is no feed forward ReLU network which is perfectly 1-provably robust.\n- if we relax definition to have $\\alpha$-interval provable robust classifier, authors showed that datasets with $O(\\alpha^{-1})$ points from $\\mathbb{R}$ (binary classification task) cannot be $\\alpha$-provable robust classified by a single-layer ReLU network (definition of this kind of network see in def 5.4)\n- finally authors demonstrate paradox by showing that any dataset with points from $\\mathbb{R}$ can be perfectly robustly classified by a single-layer ReLU network while from above it is impossible for interval case.", "claims_and_evidence_yn": "", "claims_explanation": "", "audience_yn": "", "audience_explanation": "", "requested_changes": "General:\n- I never saw notation for \"for $\\forall x.f(x)>0$\" with dot between expressions. For me personally it is very annoying to read. Maybe use comma, or space or $\\Rightarrow$\n\nAbstract\n- \"there are there are\" -> \"there are\"\n\nFigure 2\n- Add transparency for squares to make visible intersection between squares of different color. Or use different hatching for them without fill. Without this it is very unclear for \"after the 2nd affine layer ...\" statement in the caption.\n- Specify axis for (c)-(h) pictures, that x axis correspond to the upper path in (a) and y axis corresponds to lower path in (a). Maybe it is good to show how input interval to the NN is mapped into 2D plane first to make it clear.\n\nSec. 3.1\n- I propose to remove notation $\\mathbb{B}$ as it messes things with $\\mathbb{R}$ and simply use $B$, in context either we use $B$ or $B_r(c)$. I don't think there should be any differences in notation here.\n- definition of $H_\\inf(C)$ seems messed sup and inf, should be changed in left and right inequalities.\n- Move $[k]:=\\\\{1,..k\\\\}$ notation to the beginning.\n\nSec 3.2\n- first paragraph: $\\mathbb{B}_\\epsilon(x)$ -> $\\mathbb{B}^0_\\epsilon(x)$. Even I think everywhere we can skip $0$ in the superscription as it is not used in any other context.\n- second paragraph second sentence - it is needed to rephrase it as very hard to read and follow.\n- Maybe I missed, but I think Def 3.1 and 3.2 are given only for 1d input in the end, it cannot give us definition on multi-dimensional inputs. The way we can get multi-dim is duplication, which doesn't create different coordinates. With this I think all proofs and theorems / results cannot be extended to the most interesting case of multi-dimensional inputs.\n- Usage of $x_1$, $x_2$ is not clear and the whole notation is messed between 1d and nd cases. So it should be clarified, e.g. if $x$ is a vector or not, from which space it is.\n- Def 3.2 Parallel: maybe add that $B=(x_1, x_2)$?\n- Def 3.2 Constant: what is $m$, $n$? what is the notation for $\\\\{k\\\\}$\n- Proposition 3.3 - what does it mean over-approximate? maybe have footnote or definition on that?\n\nSec. 4\n- Harder to read when notation on $f[B]$ and $f(B)$ is used in the same sentence but no any reason why to mix it.\n\nSec. 4.1\n- Are notes for both definitions 4.1 and 4.2 given in case of one box or in case $S, A, B$ are set of boxes? It is not clear from the text. For the def 4.1 note why do we need to have center point in the relint$(S)$? Also here $x\\in S|^0_i$ should be $x_i\\in S|^0_i$. In note of def 4.2 seems a lot of typos in the $[a,b]$, $[b,c]$ and $a'$, $b'$ usage.\n- last paragraph - could authors add any examples for both cases?\n\nSec 4.2\n- In Lemma 4.9 \"By Lemma 4.5\" -> \"By Lemma 4.5 and 4.6\" (same in Appendix)\n- In Lemma 4.9 $f(x_1, x_2) = (g_1(x_1), g_2(x_2))$ case: $Y|_2$ should be relative interior of $H_\\inf(g_2(x_2))$, samy $Y|_2$ should be subset of $g^\\\\#_2(R)$. Same fixes are needed in Appendix\n- Lemma 4.9 no any proof for multi-dimensional inputs and results cannot be simply extended to multi-dimensional case.\n\nSec 4.3\n- I found it is hard to read with changed notation on $x$ where it is not input anymore and now used in the context of function value with $f^-1(x)$.  This also creates difficulties to read Fig. 3 as took time to understand what is x-axis and what is y-axis. Also notation on points introduced later - also hard to parse earlier.\n- th. 4.10: \"using the lemma itself\" -> \"using the theorem itself\"\n- th. 4.10: function takes $\\mathbb{R}^n$ but in proof there is no any justification for this, only for $\\mathbb{R}$\n- th. 4.10: case $f(x_1, x_2) = (g_1(x_1), g_2(x_2))$: fix notation as we swtiched to $y$ here as input space. Same in Appendix. Also \"$x_1\\in g_1^\\\\#(M_1\\times M_2)$ and $x_2\\in g_2^\\\\#(M_1\\times M_2)$\" should be $x\\in g_1^\\\\#(M_1) \\times g_2^\\\\#(M_2)=f^\\\\#(M)$\n- I like here example of fig. 3 to demonstrate the outcome from the theorem, but it is not clear how to use this theorem in general, and why it is about imprecision of interval? Maybe some extended comment / clarification, or even abstract explanation in case $N$ is some set of the points which is mapped to the same $x$ (so non-invertible on this point).\n\nSec. 5:\n- Corollary 5.2 what about other $\\nu$?\n- Def. 5.3 for $F$ is given not clearly.\n- the whole section seems weak to me as results only for 1d input which is not much interesting. Can we inherit anything for 2d case at least that similar properties / paradox will be there?\n\nAppendix B2\n- proof 4.9 $f=gh$: $g(H)$ -> $g^\\\\#(H)$ in the last sentence\n- proof 4.9 $f(x)=cx$: $X'$ should be internal interior of $H_inf(X)$ not \"equal or internal interior\".\n- proof 4.9 relu: why ReLU$(m)$?\n- proof 4.9 $x_1+x_2$: please polish sentence \"Then $H_\\inf(X)=$...\" There is some typos as hull is not used in some places and strange notation on 2d case is used for the box with $r_a + r_b$ - this we cannot sum.", "broader_impact_concerns": "The paper has analysis of robustness for interval networks. The whole paper is abstract math analysis and abstract examples. One suggestion maybe is to have one-two sentences why robustness is important and what is the practical relation could be of the theory in the paper for those who is using interval networks in practice.", "additional_comments": "", "extra_scores": {}, "extra_text": {}}, {"review_id": "TG0xUqQHEg", "reviewer": "Reviewer_ubCf", "summary": "", "questions": "", "limitations": "", "rating": null, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "Strengths\n---\n\nKnowing limitations of verifiable neural networks is an interesting problem. This paper reports on deficiency of interval propagation as a means of verification.\n\nWeaknesses\n---\n\nThe definition of “relative” interior is central to the paper, but I could not get an intuition about the significance of it. What is a “non-relative” interior and what difficulty does it pose?\n\nThe writing is sloppy and has many mistakes.\n\n* Sect. 3.2: The definition of $r$ is missing.\n* What do $m$ and $n$ refer to in Def. 3.2?\n* How can multiplication by a constant in Def. 3.2 be a singleton set?\n* In Def. 4.1, what is $\\mathbf{B}_\\epsilon^o$? \n* Def. 4.1 seems to admit points lying on the hyper-planes of a box (so that $aff(S) = S$). But isn’t this supposed to define an \"interior\"? Not clear if the paragraph following the definition is meant to take care of this case.\n* The last sentence in the paragraph after Def. 4.2 has many mistakes.\n* Lemma 4.6: What is $H_\\infty$?\n* Def. 5.1: Why does $i$ range over the dimensions?\n\nThe claim below is stated in more general terms than demonstrated in the paper.\n\n“Given this, we derive a paradox: while every dataset can be robustly classified, there are there are (sic) simple datasets that can’t be provably robustly classified with interval analysis.” – The term “every dataset” is misleading. The claim (Proposition 5.9) is stated for 1D datasets.\n\nI did not understand the following statements.\n1. We note that while Definition 3.2 defines an ordering of addition, the above definition does not.\n2. This suggests that there are more general versions of the theorems presented here, in particular relating the difficulty of program synthesis with the relational expressiveness of the relaxation used to verify the specification.\n\nThe authors need to proofread the paper to fix grammatical and typographic mistakes.\n", "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": "", "paper_topic_and_main_contributions": "", "excitement": null, "reproducibility": null, "ethical_concerns": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "summary_of_contributions": "Analysis of neural networks for robustness has become an active research topic. This paper argues that even if robust classifiers exist, they may not be provable by interval propagation. Interval propagation is a scalable but imprecise method to abstractly analyse programs and neural networks. It is therefore not surprising that there exist robust classifiers that cannot be proved to be robust using interval propagation. The paper identifies a class of neural networks (non-invertible networks with ReLU activations) interval propagation loses precision on and shows a concrete example of a dataset for which an interval-verifiable robust classifier cannot be constructed. It considers a less strict definition of robustness ($\\alpha$-robust) and constructs another example dataset (called flips) for which a single layer network verifiable with intervals is not possible. These datasets do admit robust classifiers.", "claims_and_evidence_yn": "", "claims_explanation": "", "audience_yn": "", "audience_explanation": "", "requested_changes": "The paper needs a significant rewrite to address the points raised above.\n\nDo not use contractions like “can’t” in formal writing.\n\nUse \\citep for citing related work.\n", "broader_impact_concerns": "None", "additional_comments": "", "extra_scores": {}, "extra_text": {}}, {"review_id": "PvqiAa964v", "reviewer": "Reviewer_N9Hb", "summary": "", "questions": "", "limitations": "", "rating": null, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "A negative result is presented that non-invertible functions can’t be built using affine transformations and ReLUs such that over-approximation using interval analysis is precise everywhere. Further, the paper claims that even when the requirement for perfect provability is relaxed to regions that are distant from each other (\\alpha-interval provable with < 1), there are datasets with O(1/alpha) points that can not be provably robustly classified with one-hidden layer networks using interval analysis. Finally, the paper establishes that perfectly robust classifiers can always be constructed with just one-hidden layer networks, even if they are not necessarily provably robust using interval analysis. \n\nThe reviewer has not yet gone over the proofs in detail, but the overall results appear to be consistent. \n\nTypos and minor comments:\nAbstract has repeated \"there are\" in the last sentence. ", "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": "", "paper_topic_and_main_contributions": "", "excitement": null, "reproducibility": null, "ethical_concerns": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "", "summary_of_contributions": "The paper attempts to investigate the class of neural networks for which precise interval analysis/interval bound propagation, for verifying robustness of deep neural networks, is feasible. A negative result is established. ", "claims_and_evidence_yn": "", "claims_explanation": "", "audience_yn": "", "audience_explanation": "", "requested_changes": "The proofs can be made more tractable by introducing a symbol table earlier in the paper. ", "broader_impact_concerns": "There are no broader impact concers. ", "additional_comments": "", "extra_scores": {}, "extra_text": {}}]

Author rebuttal:

Meta-review: The paper received positive feedback from the reviewers and the authors have responded to earlier concerns of the reviewers. The authors are strongly advised to take into account detailed feedback from Reviewer f5Ug for preparing the final version. 

All reviewers view the paper positively and therefore, the paper can be accepted with minor revision. Congratulations to authors on a solid work and I look forward to receiving the final version of the paper. 


Best,

Decision: Accept (poster)