Generalized Universal Approximation for Certified Networks
Authors: Zi Wang
Aws Albarghouthi
Somesh Jha
Venue:  (2021)
Keywords: adversarial deep learning
neural network verification
interval analysis

Abstract: To certify safety and robustness of neural networks, researchers have successfully applied abstract interpretation, primarily using interval bound propagation. To understand the power of interval bounds, we present the abstract universal approximation (AUA) theorem, a generalization of the recent result by Baader et al. (2020) for ReLU networks to a large class of neural networks. The AUA theorem states that for any continuous function $f$, there exists a neural network that (1) approximates $f$ (universal approximation) and (2) whose interval bounds are an arbitrarily close approximation of the set semantics of $f$. The network may be constructed using any activation function from a rich class of functions---sigmoid, tanh, ReLU, ELU, etc.---making our result quite general. The key implication of the AUA theorem is that there always exists certifiably robust neural networks, which can be constructed using a wide range of activation functions.

Under review as a conference paper at ICLR 2021
GENERALIZED UNIVERSAL APPROXIMATION FOR CERTIFIED NETWORKS
Anonymous authors Paper under double-blind review
ABSTRACT
To certify safety and robustness of neural networks, researchers have successfully applied abstract interpretation, primarily using interval bound propagation. To understand the power of interval bounds, we present the abstract universal ap- proximation (AUA) theorem, a generalization of the recent result by Baader et al. (2020) for ReLU networks to large class of neural networks. The AUA theorem states that for any continuous function S, there exists a neural network that (1) approximates (universal approximation) and (2) whose interval bounds are arbitrarily close approximation of the set semantics of f. The network may be constructed using any activation function from rich class of sunctions-sigmod tanh, ReLU, ELU, etc.- etc.-making our result quite general. The key implication of the AUA theorem that there always exists certifiably robust neural networks, which can be constructed using a wide range of activation functions.
INTRODUCTION
With wide adoption of neural networks, new safety and security concerns arose. The most prominent property of study has been robustness (Goodfellow et al., 2015): small perturbations the input of network should not change the prediction. For example, small change to an image of stop sign should not cause a classifier think it is a speed-limit sign. A number of researchers have proposed the use of absiract interprelution (Cousot & Cousot, 1977) techniques to prove robustness of neural networks (Gehr et al., 2018; Wang et al., 2018; Anderson al., 2019) and train robust models (Mirman et al., 2018; Gowal et al., 2018; Huang et al., 2019; Wong & Kolter, 2018; Wong et al., 2018; Balunovic & Vechev, 2020).
Suppose want to verify robustness of neural network small changes in the brightness of an image. We can represent large set of images, with varying brightness, as an element of some abstract domain, and propagate it through the network, effectively executing the network intractably large number of images. If all images lead to the same prediction, then we have a proof that the network is robust the original image. The simplest abstract interpretation technique that leads to practical verification results is interval analysis- also referred to as interval bound propagation. In our example. if each pixel in a monochrome image is real number r, then the pixel can be represented as an interval [r- r + e]. where denotes the range of brightness we wish to be robust on. Then, the box representing the interval of each pixel propagated through the network using interval arithmetic operations.
The interval domain has been successfully used for certifying properties of neural networks in vision (Gehr et al., 2018; Gowal et al., 2018), NLP (Huang et al., 2019), as well as cyber- physical systems (Wang et al., 2018). Why does the interval domain work for certifying neural networks?
To begin understanding this question, Baader et al. (2020) demonstrated a surprising connection between the universal approximation theorem and neural-network certification using interval bounds. Their theorem states that not only can neural networks approximate any continuous function (universal approximation) as we have known for decades, but we can find a neural network, using rectified linear unit (ReLU) activation functions, whose interval bounds are arbitrarily close approximation of the set semantics of f, i.c., the result of applying f to a set of inputs (c.g., set of similar images).

---

Under review as a conference paper at ICLR 2021
AUA theorem (semi-formally): For continuous function f R - R that wish to approximate and error å > 0, there is neural network N that has the following behavior:
minxEB f(x)
maxxe B f(x)
Let B C IR" be box. The red interval (top) is the tightest interval that contains all outputs of f when applied to B.
8
If we propagate box B through N using interval bounds, we may get the black interval (bottom) (B). whose lowerlupper bounds are up to ó away from the red interval.
NB(B)
Figure 1: Semi-formal illustration of AUA theorem. (Right is adapted from Baader et al. (2020).)
The theorem of Baader et al. (2020) is restricted to networks that use rectified linear units (ReLU). In this work, we present a general universal approximation result for certified networks using a rich class of well-behaved activation functions. Specifically, we make the following contributions.
Abstract universal approximation (AUA) theorem. We prove what we call the abstract universal approximation theorem, or AUA theorem for short: Let f be the function we wish to approximate, and let 8 > 0 be the tolerated error. Then, there exists neural network N, built using any well bell-behaved activation function, that has the following behavior: For any box of inputs B, we can certify, using interval bounds, that the range of outputs of N is ō close to the range outputs of f. If the box B of inputs is single point in Euclidean space, the AUA theorem reduces to the universal approximation theorem; thus, AUA generalizes universal approximation. Fig. further illustrates the AUA theorem.
Existence of robust classifiers. While the AUA theorem is purely theoretical, it sheds light on the existence of certifiable neural networks. Suppose there is some ideal robust image classifier f using the loo norm, which is typically used to define The classical universal approximation theorem tells us that, for any desired precision, there a neural network that can approximate f. We prove that the AUA theorem implies that there exists a neural network for which we can automatically certify robustness using interval bounds while controlling approximation error. In addition, this neural network can be built using almost any activation function in the literature, and more.
of images in the neighborhood of a given image.
Squashable functions. We define rich class of activation functions, which we call squashable functions, for which our abstract universal approximation theorem holds. This class expands the functions defined by Hornik et al. (1989) for universal approximation and includes popular activation functions, like ReLU, sigmoid, tanh, ELU, and other activations that have been shown to be useful for training robust neural networks (Xie et al., 2020). The key feature of squashable activation functions is that they have left and right limits (or we can use them to construct functions with limits). We exploit limits to approximate step (sign) functions, and therefore construct step-like approximations of f. while controlling approximation eтror 8.
Proof of AUA theorem. We present a constructive proof of the AUA theorem. Our construction is inspired by and synthesizes range of results: (1) the work of Hornik et al. (1989) squashing functions for universal approximation, (2) the work of Csáji (2001) for using the sign (step) function to construct Haar (wavelet) functions, and (3) the work of Baader et al. (2020) the specialized AUA theorem for ReIUs.. The key idea of Baader et al. (2020) is to construct an indicator function for box-shaped regions. We observe that squashable functions can approximate the sign function, and therefore approximate such indicator functions, while carefully controlling precision of abstract interpretation. Our proof uses a simpler indicator construction compared to Baader et al. (2020), and as a result its analysis is also simpler.
2 RELATED WORK
The classical universal approximation (UA) theorem has been established for decades. In contrast to AUA, UA states that a neural network with one single hidden layer can approximate any continuous function compact domain. One of the first versions goes back to Cybenko (1989); Hornik et al. (1989), who showed that the standard feed-forward neural network with sigmoidal or squashing activations is universal approximator. The most general version of UA was discovered by Leshno et al. (1993), who showed that the feed-forward neural network is a universal approximator if and only if the activation function is non-polynomial. Because AUA implies UA, this means AUA cannot
2

---

Under review as a conference paper at ICLR 2021
Squashable activation functions that satisdy Eq. (1)
softsign(a)
(a))
tanb(2)
Ite=
++e* e
Squashable activation functions that do directly satisty Eq.
= 0 ReLU(x)= = 0, <<
ELU(E)
6t
x 2
softplus(x)) lo + e*)
RooothReLU.. x- log(az + 1), a 2220
Examples of squashable activation functions, including popular functions, and more recent ones: sigmoid, tanh, rectified linear units (ReLU) (Nair & Hinton, 2010), exponential linear unit (ELU) (Clevert et al., 2016), seftplus (Glorot et al., 2011), softsign (Bergstra et al., 2009), and smooth ReLU (Xie al., 2020), which is parameterized by a >> 0.
Figure 2:
hold beyond non non-pol polynoooll activation functions. There are also other variants of UA. Some of them study the expressiveness of neural networks with structural constraints, such as restricted width per layer Lu al. (2017); Kidger Lyons (2019), or specific neural network architectures Lin Jegelka (2018). Another line of work focuses specific functions that one wants to approximate rather than arbitrary continuous functions, such as Anil et al. (2019); Cohen et al. (2019), who study approximation of Lipschitz functions.
Neural-network verification has received a lot of attention in recent years. Most techniques are either based decision procedures, like SMT solvers Ehlers (2017); Katz al. (2017) and integer linear programming (ILP) solvers Tjeng et al. (2019), or abstract interpretation. The former class can often provide sound and complete verification neural networks with piecewise-linear operations, like ReLU,, but is not scalable due to the complexity of the problem and the size of the networks. techniques sacrifice completeness for efficient verification. We have considered the simplest non-trivial numerical domain, intervals, that has been shown to produce strong results, both for robustness verification and adversarial training Gehr al. (2018); Anderson et al. (2019); Huang et al. (2019); Mirman et al. (2018); Wang et al. (2018); Zhang et al. (2020). Researchers have considered richer domains Singh et al. (2018; 2019), like zonotopes Ghorbal et al. (2009) and forms of polyhedra Cousot & Halbwachs (1978). Since such domains are strictly more precise than intervals, the AUA theorem holds for them.
Abstrrct-intterprettton----
FOUNDATIONS AND SQUASHABLE ACTIVATION FUNCTIONS
3.1 NEURAL NETWORKS AND SQAUSHABLE ACTIVATIONS
A neural network N is a function in Rm - R. We define network N following a simple grammar, a composition of primitive arithmetic operations and activation functions.
Definition 3.1 (Neural network grammar). Let E I be the input the neural network. A neural network N is defined using the following grammar: N = c x; Nı + N₂ c N1 t(NN), where E IR, x; is the ith element of x. and t RR - IR is an activation function. We will always fix single activation function t to be used in the grammar.
We now present general class of activation functions that will call squashable activation functions. Fig. 2 shows some examples.
Definition 3.2 (Squashable functions). t: ER-- - I. is squashable (1) there a < <b R such that t(x) = a,
lim Dc
lim t(x) = b, and Va < y. t(x)= < t(yy 200
(I)
or (2) we can construct a function t' that satisfies Eq. (1) as affine transformations and function compositions of copies of i, i.e., following the grammar in Def. 3.1. E.g., t'(x) ((1((x)))
Informally, an activation function is in this class we can use it to construct monotonically increasing function that has limits in the left and right directions, oo and oo. Squashable activation
In our construction and proof, we do not need the function to be monotonic; however, in practice, most
activation functions monotonic and abstractly interpreting arbitrary functions impractical.
3

---

Under review as a conference paper at ICLR 2021
-2-1
(a) ReLU(1 - ReLU(-x))
(b) softplus(1 - softplus(-zz)
Figure 3: Two activation functions after applying construction in Proposition 3.3. Observe that the resulting function satisfies Eq. (1), and therefore ReLU and softplus are squashable.
functions extend the squashing functions used by Hornik al. (1989). All of the activation functions in Fig. 2 are squashable.
Fig. 2 (top) shows activation functions that satisfy Eq. (I), and are therefore squashable. For example, sigmoid and tanh easily satisfy Eq. (1): both have limits and are monotonically increasing.
What about activation functions like ReLU, ELU, softplus, etc., shown in Fig. 2 (bottom)? is easy to see that they do not satisfy Eq. (1): none of them have a right limit. However, by point (2) of Def. 3.2, given an activation function i, if we can construct new activation function that satisfies Eq. (1), using the operations in the grammar in Def. 3.1, then t is squashable. We give a general and simple construction that works for all activation functions in Fig. (bottom).
Proposition 3.3. Let t E (RcLU, softplus, smoothReLU. ELU). The function f'(x) t(1 t(-x)) satisfies Eq. (1). Therefore, ReLU, softplus, Smooth ReLU, and ELU, are squashable.
Example 3,4. Fig. 3 shows t(1 - t(-x)), (())), for t = ReLU and t = softplus. Both have left/right limits and are monotonic. Thus, they satisfy Eq. (1) and therefore ReLU and softplus are squashable.
3.2 INTERVAL ANALYSIS OF NEURAL NETWORKS
Given f R +
and set C IR,,, we will use f(S) to denote (f(x) x E S}.
We now define interval versions of the operations of a neural network, which are known abstract transformers. This was first introduced in Cousot & Cousot (1977), which also proved the soundness of the interval domain. An m-dimennional box B is tuple of intervals [4, un] x ... [m, um All our operations are over scalars, so we define abstract transformers over ID boxes.
Definition 3.5 (Arithmetic abstract transformers), Let B be an m--dimensional box impul to the neural network. We follow the grammar in Def. 3.1 to define the abstract transformers.
tlt
[c, cl
x [4, u.], where 4, us are the ith lower and upper bounds of
[1, [1] C,
##
U2, 11
U2
111 + U1 + [z]
c)
[min(c I, c u), max(c c* u)]
Definition 3.6 (Abstract transformer for activations). Let = [1, u]. Then, t# (B) =[t(1,, t(w)).
This transforer was introduced in (Gehr et al., 2018).
4 ABSTRACT UNIVERSAL APPROXIMATION THEOREM & ITS IMPLICATIONS
In this section, we state the abstract universal approximation (AUA) theorem and its implications.
Assume fixed continuous function f C R2 with compact domain C C Rmm. that wish to approximate.
Definition 4.1 a approximation). Let 8 > 0. A neural network N 8-abstractly approximates iff for every box B C C, we have + 8, 8) C N# (B) [ 5, u + 6), where I = min (B) and u = max (B).
5-abstract approximation says that the box output of abstract interpretation N (B) is up to away from the tightest bounding box around the set semanties f(B). It was developed in Baader et al. (2020). Observe that the standard notions of approximation is a special case of 5-abstract approximation, when the box B is point in C.
4

---

Under review as a conference paper at ICLR 2021
We now state main theorem:
Theorem 4.2 (Abstract universal approximation). Let f C - IR be a continuous function on compact domain C' C R", Let be squashable activation function. Let 8 > There exists neural network N, using only activations that 8- b-abstractly approximates f.
Informally, the theorem says that is arbitrarily close to the set semantics of the approximated function. Note also that there exists such a neural network for any fixed squashable activation function the appendix, we give generalization of the AUA theorem to functions and networks with multiple outputs.
always find neural network whose abstract interpretation
As we discuss next, the AUA theorem has very exciting implications: We can show that one can always construct provably robust neural networks using any squashable activation function (Thm. 4.5).
We begin by defining robust classifier in & norm. We treat f C R as binary classifier, where an output < 0.5 represents one class and > 0.5 represents another.
Definition 4.3 (e-Robustness). Let x E R M C and c > O. The e-ball of Rx((x) = {z ||z - x < c). We say that f is c-robust on set M iff. for all x E M and z E (x),). we have f(x) < 0.5 iff f(z) 0.5.
Definition 4.4 (Certifiably robust networks). A neural network N is e-certifiably robust on M iff for all E M, we have N# (B) S (-20,0.5) 0.5) or N# (B) S [0.5, o0), where B Re Rx(xx (Note that an c-ball is box in Iem.)
From an automation perspective, the set M is typically a finite M, the verifier abstractly interprets N on the e-ball of x, deriving a lower bound and upper bound of the set predictions ((R.(x) (x)). If the lower bound is > 0.5 or the upper bound < 0.5, then we have proven that all images in the e-ball have the same classification using N.
points, e.g., images. For every
Assuming there is some ideal robust classifier, then, following the AUA theorem, we can construct a neural network, using any squashable activation function, that matches the classifier's predictions and certifiably robust. Refer to the supplementary materials for an extension to n-ary classifiers.
Theorem 4.5 (Existence of robust networks). Let CC R be e-robust on set M C. Assume that Vx E M, E R. (x). f(z) & 0.5.² Let t be a squashable activation function. Then, there exists neural network N, using activation functions i, that (1) agrees with M, i.e., Vx E M. Nxx) < 0.5 iff (xx < 0.5, and (2) is c-certifiably robust on M.
PROOF OF AUA THEOREM: AN OVERVIEW
We now give an overview of our proof of the AUA theorem, focusing on its novelty. Our proof is constructive: we show how to construct a neural network that 6-abstractly approximates a function f.
Approximating indicator functions (Sec. 6). The key element, and primary novelty of our proof, is the construction indicator functions from squashable functions. Our construction is motivated by Csáji (2001), who used sign functions to construct the Haar function, which can be used to uniformly approximate any continuous function. See Fig. 5b for an example of the indicator function's 's approximation with sigmoid.
1.2
1.6
Ja
0.4
S0
Sliced sin(2.) with
a classical idea to use indicator functions to approximate a con- tinuous function piccewise fashion-see Nielsen (2015, Ch.4) for an interactive visualization of universal approximation. However, for AUA, the input to the function is box, and therefore we need make sure that our indicator- function approximations provide tight abstract approximations (Def. 4.1), as will be shown in Thm. 6.2.
range of size 0.4
0.4
(b) Example slice
Figure 4: Slicing example
This assumption eliminates the corner case where point sits exactly the classification boundary, 0.5.
5

---

Under review as a conference paper at ICLR 2021
Composing indicator functions (Sec. 7). Once we have approximated
indicator functions, we need to put them together to approximate the entire function f. The remainder of the construction is an adaption of one by Baader et al. (2020) for ReLU networks.
The construction starts by slicing f into a sequence of functions fi such that f f= - f.. Each f; captures the behavior of f on small interval of its range. See Fig. 4 for example of slicing. Next, we approximate each fi using a neural network N, Slicing ensures that 5-abstract approximation tight for large boxes. Because f(B) = Es fi(B), when approximating (:(B) using (B), we can show that for most i, [t( x (B). The smaller the range of slice fi. the tighter the abstract approximation of using indicator functions.
Our construction and analysis are different from Baader et al. (2020) in the following ways:
Baader et al. (2020) focus exclusively on ReLU activations. In our work, we consider squashable functions, which contain most commonly used activation functions. Compared to ReLU, which has rigid values, we only know that squashable functions have limits at both sides. This makes the class of functions more expressive but also harder to quantify. When analyzing the interval bounds of the whole network construction, we need to take into account the extra imprecision, which propagates from the indicator function the whole neural network.
2.
The key construction of Baader et al. (2020) is to build min (21, ..,......mm using ReLUs. The depth of the construction depends on m, and the analysis of its interval bounds is rather complicated. Our construction uses only layers of activations, resulting in a much simpler analysis. Because ReLU is squashable function, a by-product is that if we only consider AUA for ReLU, our construction and its analysis are simpler than that of Baader al. (2020).
ABSTRACTLY APPROXIMATING INDICATOR FUNCTIONS
We begin by showing the crux of our construction: how to approximate an indicator function. Recall that our goal is to d-abstractly approximate continuous function f : C. -
+ R.
Grid of boxes. Fix e O. Consider standard grid of vertices over C. where any two neighboring vertices are axis-aligned and of distance we will call this an e-grid. Let (a1, bi] x... [um: bm] be a box on the grid, where [a;, b.] is the range of at dimension i. other words, b, 0z is
multiple of e. The neighborhood v(G') of G is [a E, b1 + ... X (am e, 6m + e]. Our goal to construct an indicator function whose value is close to within G, and close to 0 outside G's neighborhood vG). The idea of using grid is similar to the nodal basis in He et al. (2018).
Indicator- approximation intuition. Given any activation function f that satisfies Eq. (1), key observation is that if we dilate properly, i.e., multiply the input with large number μ to get t(ux), we will obtain an approximation of the sign (or step) indicator function a function that indicates whether an input is positive or negative: sign(x) 1 if > 0 and 0 otherwise. A sign function can be used to construct an indicator function for 1-dimensional boxes. For example, sign(x)) sign(x 1) returns I for x E (0, 1]. and otherwise. In what follows, we will use the above ideas to approximate the sign function and the indicator function for m-dimensional boxes.
6.1 APPROXIMATING A ONE-DIMENSIONAL INDICATOR FUNCTION
We will first show how to construct an indicator function for a ID box, using a squashable function. The main challenge is choosing the dilation factor that results in tight abstract approximation.
Without loss of generality, assume we are given a squashable function that (1) satisfies Eq. (1) and (2) has left and right limits of 0 and 1, respectively."
Loss of precision from limits. The activation function t has limits at both sides, but the function might never reach the limit. For example, the right limit of the sigmoid function, a, is 1, but Vr. (x) * 1. This will lead to a loss of precision when we use / to model a sign function. However, we can carefully apply mathematical analysis to rigorously bound this imprecision.
P 'The vertices of the grid form natural e/2-net on C equipped with to metric.
'If (1) is not satisfied, by Def. 3.2, we can construct i' that satisfies Fq. (1) from t. If (2) is not satisfied, we can apply affine transformation to the results of t make the left and right limits 0 and 1.

---

Under review as a conference paper at ICLR 2021
0.5
0.5
0.5
0
-4 -2
2
4
-4 -
2
(a) o102))
(b) (102z) -0000)))>(1())) 1))
(c) Plot of Ng on = [0, 1] x [0. using
the activation (μ = 10, 20 = 0.05, e = 1).
Figure 5: Approximating indicator functions on [0, oo), [0, 1] and [0, 1] x [0. 1] using the sigmoid activation functions
Dilation to approximate sign function. We now discuss how to dilate get sign-function- like behavior. By definition of limit, we know the following lemma, which states that 40 > 0 by sufficiently increasing the input of t. we can get close to the right limit of and analogously for the left limit. Figs. 5a and 5b show how sigmoid can approximate an indicator function.
Because the grid size e, we want the sign-function approximation to achieve a transition from to = I within c. Let μ be the dilation factor. We would like the following (Fig. 6 illlustrates the loss of precision incurred by our construction):
Lemma 6.1. V0 > 0, 3p > 0 such that: (1) if 7 0.5e, then t(ux) (1 0, 13; (2) if x & -..5e then t(uz)= E (0, 8).
Indicator function on dimension i. Recall that the projection of box G on dimension is (as; bi]. We want build an indicator function that has value close to 1 on [a,, bx). and value close to O on \ [a, c, bç + c]. Notice that our approximation may not be able to exactly tell if we are in G or its neighborhood.
Inspired by how to construct an indicator function from a sign function, we will take the difference between two shifted sign functions. Let
-0.5e 0.5c
Figure 6: Loss of precision @ due to use of squashable activation approximate sign function. Length of red arrows is < A.
4(x)) t (x 0.5e))) t (μ (b, 0.5e))) (2)
We choose the two points a; 0.5c and b, + 0.5c, which lie in the middle of the [as, by] and its neighborhood, so that 4s' value of is close to 1 within [as, b:). and 0 outside (a,, by]'s neighborhood.
6.2 APPROXIMATING AN II-DIMENSIONAL INDICATOR
We saw how to construct indicator approximation for a 1-dimensional box. We will now show how to construct an indicator function approximation Ng for an m-dimensional box.
Constructing NG- We want construct indicator function whose value within box G is close to 1, and outside the neighborhood v(G) close to O. In the multi-dimensional case, m 2 2, we do not know which, if any, dimension j of an input outside the neighborhood of G. The I-dimensional indicator approximation. i, which we constructed earlier, can be used to tell us, for each dimension j. whether zj within the bounds of the neighborhood of G. Therefore we can construct a logical OR approximation that applies f to each dimension and takes the OR of the results. Specifically: (1) we will construct function that applies f to each dimension, and sums the results such that the answer > 0 if x E G, and < if x & v(G). (2) Then, we can use the sign-function approximation to indicate the sign of the answer.
Formally, we define the neural network No as follows:
m
No(x) = 11
Σ
H((a:)++ 0.5c
where Hz(x) = (x) (1 11-220 20). Eq. (3) has similar structure to the m-dimensional indicator in Baader et al. (2020). i.e., both of them use the activation function to evaluate the information from all dimensions.
7

---

Under review as a conference paper at ICLR 2021
The term Ei= (z;), evaluates to positive value if x E G and to negative value if x & v()). Observe that we need to shift the result of i by (1 22)) ensure negative answer if one of the dimensions is outside the neighborhood. Then, we use to approximate the sign function, as we did in the I-dimensional case, giving 1ff G, and 0f v()). Fig. 5c shows plot of a two dimensional No.
Abstract precision of indicator approximation. The following key theorem states the precision of the abstract interpretation of Ng: if the input box is in G, then the output box is within @ from 1; if B is outside the neighborhood of G, then the output box is within from 0.
Theorem 6.2 (Abstract interpretation of NG). For any box B C C, the the following is true:
1. N (B) S [0.
2. If B S G. then (B) (1 10, 1].
3. If S C v(),, then ( C (0.
Complexity of construction. To construct single indicator function, we use 2m + activation functions, with depth and width 2m. If we restrict ourselves to ReLU neural network, we use 4m + neurons, with depth and width 2m;; in contrast, Baader al. (2020) used 10m - ReLu functions, with depth 3 + logg(m) and width 4m.
7 COMPLETE PROOF CONSTRUCTION OF AUA THEOREM
We have shown how to approximate an indicator function and how to control the precision of its abstract interpretation (Thm. 6.2). We now complete the construction of the neural network N following the technique of Baader et al. (2020) for ReLU networks. Because we use an arbitrary squashable function approximate the sign function, this introduces extra imprecision in comparison with ReLUs. We thus need a finer function slicing to accommodate it, i.e., we use slicing size of 5/3 instead of 8 8/2 in Baader et al. (2020). We provide the detailed analysis the appendix. In what follows, outline how to build the network N that satisfies the AUA theorem.
Slicing f. Let f C + be the continuous function we need to approximate, and d be the approximation tolerance, per AUA theorem statement (Thm. 4.2), Assume min f(C) = 0. Let u = max (C). In other words, the range of f is [0, u].
Let r 3- We will decompose f into sequence of function slices fa. whose values are restricted to [0, r.. Let K [//T]. The sum of the sequence of function slices is f. The sequence of functions f C + [0, r]. for E (O....,Au K) is:
f(x) it, iT f(x) < si++1 1)7 0,
f(()) =
f(x) ir ir (1+1)<< f(x)
Approximating f. We will use the indicator approximation NG (Eq. (3)) to construct neural network N, that approximates ft. Let G be the set of boxes whose vertices are in the grid. Because C' is compact, [g] is finite. Consider f((();;
roughly similar to an indicator function for the set S = {x E C f(x) > (i 1)7), i.e., indicating when f(x) is greater than the upper bound of the ith slice. To approximate (x),, we will consider all boxes G that are subsets of S, and construct
indicator function to tell us whether an input is in those boxes. Let G, (G E G (()) > (i 1)r}.
Now construct (x) that approximates fx) as Ní(x) t (μ (Eoeg, Nc(x) - 0.5)).
Sum all N,. Because ΣK fi(x) f(x), and (x) approximates f(()),, we will construct the neural network N as N(x) = T " N2(x).
N 8-abstractly approximates f; therefore, the AUA theorem holds.
'Oteewwise, we can shift such that min f(C)- 0.
8

---

Under review as a conference paper at ICLR 2021
8 CONCLUSION
We have shown that the AUA theorem holds for most practical neural networks, and demonstrated that in theory interval analysis might be interested in reducing the size of the neural network constructed in course of our proof, for example, by allowing the use of richer domains, like zonotopes and polyhedra.
certify the robustness of neural networks. In the future, one
REFERENCES
Greg Anderson, Shankara Pailoor, Isil Dillig, and Swarat Chaudhuri. Optimization and abstraction: A synergistic approach for analyzing neural network robustness. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 731-744, 2019.
Cem Anil, James Lucas, and Roger Grosse. Sorting out Lipschitz function approximation. In Kamalika Chaudhuri and Ruslan Salakhutdinov (eds.). Proceedings of the 36th International Conference on Machine Learning, volume 97 of Proceedings of Machine Learning Research, pp. 291-301, Long Beach, California, USA, 09-15 Jun 2019. PMLR. URL httttttt/ppccceeeeeeee mlr. press v ani119a html.
Maximilian Baader, Matthew Mirman, and Martin Vechev. Universal approximation with certified networks. In International Conference on Learning Representations, 2020. URL https:// openreview n Sett//ooroe forum? Lorumm?ddBBLgxXBEEE..
Mislav Balunovic and Martin Vechev. Adversarial training and provable defenses: Bridging the gap. In International Conference on Learning Representations, 2020. URL httts::/ net/ / forum? id=SJxSDxrKD=
James Bergstra, Guillaume Desjardins, Pascal Lamblin, and Yoshua Bengio. Quadratic polynomials learn better image features. Technical report, 1337, 2009.
Djork-Aréé Clevert, Thomas Unterthiner, and Sepp Hochreiter. Fast and accurate deep network learning by exponential linear units (elus). Yoshua Bengio and Yann LeCun (eds.), Inter- national Conference on Learning Representations, ICLR 2016, San Juan, Puerto Rico, May 2-4, 2016, Conference Track Proceedings, 2016. URL http: / www...oog/abs.s....eooeeeee /t//ab//11111 5111 0.2889..
Jeremy Cohen, Todd Huster, and Ra Cohen. Universal lipschitz approximation bounded depth neural networks, 2019.
Patrick Cousot and Radhia Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL '77, pp. 238-252, New York, NY, USA, 1977. Association for Computing Machinery. ISBN 9781450373500, doi: 519973. URL https: doi. org/ 10. (ttpr/g...114.... 10.....1151111911 512973.
Patrick Cousot and Nicolas Halbwachs. Automatic discovery of linear restraints among variables of a program. In Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pp. 84 96, 1978.
Balázs Csanád Csáji. Approximation with artificial neural networks. 2001.
George Cybenko. Approximation by superpositions of a sigmoidal function. Mathematics of Control, Signals and Systems, 2:303-314, 1989.
Ruediger Ehlers.
Formal verification of piece-wiss wise linear feed forward neural networks. In Interna- tional Symposium on Automated Technology for Verification and Analysis, pp. 269-286666 286.. Springer, 2017.
Gehr, M. Mirman, D. Drachsler-Coher Tsankov, S. Chaudhuri, and M. Vechev. Ai2: Safety and robustness certification of neural networks with abstract interpretation. In 2018 IEEE Symposium on Security and Privacy (SP), pp. 3-18, 2018.
Khalil Ghorbal, Eric Goubault, and Sylvie Putot. The zonotope abstract domain taylor1+. In International Conference Computer Aided Verification, pp. 627-633. Springer, 2009.

---

Under review as a conference paper at ICLR 2021
Xavier Glorot, Antoine Bordes, and Yoshua Bengio. Deep sparse rectifier neural networks. In Proceedings of the fourteenth international conference on artificial intelligence and statistics, pp- 315-323, 2011.
Goodfellow, Jonathon Shlens, and Christian Szegedy. Explaining and harnessing adversarial examples. In International Conference on Learning Representations, 2015. URL http:// arxiv. org/ abs 1412. 6572.
Sven Gowal, Krishnamurthy Dvijotham, Robert Stanforth, Rudy Bunel, Chongli Qin, Jonathan Uesato, Relja Arandjelovic, Timothy Mann, and Pushmeet Kohli. the effectiveness of interval bound propagation for training verifiably robust models. arXiv preprint arXiv:1810.12715. 2018.
Juncai He, Lin Li, Jinchao Xu, and Chunyue Zheng. Relu deep neural networks and linear finite
elements. arXiv preprint arXiv: / 1807 807.03973, 2018.
Kurt Hornik, Maxwell Stinchcombe, Halbert White, al. Multilayer feedforward networks are universal approximators. Neural networks, 2(5):359-360 366, 1989.
Po-Sen Huang, Robert Stanforth, Johannes Welbl, Chris Dyer, Dani Yogatama, Sven Gowal, Krishna- murthy Dvijotham, and Pushmeet Kohli. Achieving verified robustness to symbol substitutions via interval bound propagation. Proceedings of the 2019 Conference on Empirical Methods in Natural Language Processing and the 9th International Joint Conference on Natural I. Language Processing, EMN.P--JCNLLP 2019, Hong Kong, China, November 3-7, 2019, pp. 4081 4091, 2019. doi: 10.18653/v1/D19- 1419. URL https: http//iiiorggg//// www.orggg//... 1861186633118 30//////1/D/333 1419.
Guy Katz, Clark Barrett, David Dill, Kyle Julian, and Mykel Kochenderfer. Reluplex: An efficient smt solver for verifying deep neural networks. In International Conference on Computer Aided Verification, pp. 97- Springer, 2017.
Patrick Kidger and Terry Lyons. Universal approximation with deep narrow networks. arXiv preprint 1905::9905.8800 2019.
Moshe Leshno, Vladimir Ya. Lin, Allan Pinkus, and Shimon Schocken. Multilayer feed- forward networks with nonpolynomial activation function can approximate any func- tion. Neural Networks, 6(6):861 867, 1993. ISSN 0893-6080. doi: https//doi.org/ URL http: www.://w.eeeeeeeeeteeee.eeeeeee. com/ science/ atticclee/11/0003300000000
Hongzhou Lin and Stefanie Jegelka. Resnet with one-neuron hidden layers is universal approximator. In S. Bengio, H. Wallach, H. Larochelle, K. Grauman, N. Cesa-Bianchi and R. Garnett (eds.), Advances in Neural Information Processing Systems 31, pp. 6169 6178. Curran Associates, Inc., 2018. URL http: httppaaapeeseeeeeeeeeeeeeeeeeees pwapprrs.nipp.... nips. cc/ cc/paper//////c/ceee/eeep heti--oo--nuuoo--iieeeeeeee
7855-resnes pdf.
is waw.llyyrs-i--nnvvrrers---sees www.iiveeaal-ppppoiimtatttt.
Zhou Lu, Hongming Pu, Feicheng Wang, Zhiqiang Hu, and Liwei Wang. The expressive power of neural networks: A view from the width. In Proceedings of the 31st International Conference on Neural Information Processing Systems, NIPS' 17, pp. 6232-6240, Red Hook, NY, USA, 2017.
Curran Associates Inc. ISBN 9781510860966
Matthew Mirman, Timon Gehr, and Martin Vechev. Differentiable abstract interpretation for provably robust neural networks. In International Conference Machine Learning (ICMI), 2018. URI. https: www. i icml. cc/ Con frronneeeeee/ 2208 8 2tt////21///////// /eshhchheeeeeeeeee 2echeddll22hooEEeett=2277
Vinod Nair and Geoffrey E Hinton. Rectified linear units improve restricted boltzmann machines. In ICML, 2010.
Michael A Nielsen. Neural networks and deep learning, volume 2018. Determination press San Francisco, CA, 2015.
W. Rudin. Principles of Mathematical Analysis. McGraw - Hill Book C., 1986. URL https:
//books. google l ctm http://oooo.....oooaaaaaaaaaaaaa
10

---

Under review as a conference paper at ICLR 2021
Gagandeep Singh, Timon Gehr, Matthew Mirman, Markus Püschel, and Martin Vechev. Fast and effective robustness certification. In Advances in Neural Information Processing Systems, pp. 10802-10813, 2018.
Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin Vechev. An abstract domain for certifying neural networks. Proceedings of the ACM on Programming Languages, 3(POPL):1-30, 2019.
Vincent Tjeng, Kai Y. Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net, 2019. URL https: // //pperevieww net. fest/forre forum? Hd-HyGddiRqtm.
Shiqi Wang, Kexin Pei, Justin Whitchouse, Junfeng Yang, and Suman Jana. Formal security analysis of neural networks using symbolic intervals. 27th USENIX Security Symposium (USENIX Security 18), pp. 1599-1614 2018.
Eric Wong and Zico Kolter. Provable defenses against adversarial examples via the convex outer adversarial polytope. volume 80 of Proceedings of Machine Learning Research, pp. 5286-5295, Stockholmsmässan, Stockholm Sweden, 10-15 Jul 2018. PMLR. URL MRRLhttp://rroceedeii mlr. waa..press/// v80 //wo///wlggl 8a html.
Eric Wong, Frank Schmidt, Jan Hendrik Metzen, and Zico Kolter. Scaling provable adversarial defenses. In Proceedings of the 32nd International Conference Neural Information Processing Systems, NIPS' 18, pp. 8410-8419, Red Hook, NY, USA, 2018. Curran Associates Inc.
Cihang Xie, Mingxing Tan, Boqing Gong, Alan Yuille, and Quoc Le. Smooth adversarial training. arXiv preprint ar arXiv:2006. 145.6 2020.
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 International Conference on Learning Representations, 2020. URL https: http::::////peeeeeeeee net/ fortmm?rmm iddskxuk1 FFWB.
A VECTOR-VALUED NETWORKS AND ROBUSTNESS
In this section, extend the AUA theorem to vector-valued functions. We also extend our robustness results to n-ary classifiers.
A.1 HIGHER
DIMENSIONAL HIGHER-DIMENSIONN
FUNCTIONS
Vector-valued neural networks. So far we have considered scalar-valued neural networks. We can generalize the neural-network grammar (Def. 3.1) to enable vector-valued neural networks. Simply, we can compose a sequence scalar-valued neural networks construct neural network whose range is R". Formally, we extend the grammar as follows, where E; are the scalar-valued sub-neural networks.
Definition A.1 (Vector-valus neural network grammar). A neural network N R - R" is defined as follows
N
E.)
E
c
Ej + E2
Es
t t(E....., Ex)
where e RR I, is one of the m inputs to the network, and & an activation funnctooonfuuccionn
Example A.2. Consider the following neural network N _g222 R²
N(x) = (a(x) + 0.5x2), (0.12 + 0.3rz))
which can pictorially depict as the following graph:
11

---

Under review as a conference paper at ICLR 2021
41
0.5
J2
Generalized AUA theorem. We now generalize the AUA theorem to show that we can 8-abstractly approximate vector-valued functions.
Theorem A.3. Let C - Re be a continuous function with compuct domain C R Let Then, there exists neural network N =R + IRm such that for every box C C, and for all i m.
[4: + us S N S C 6,u 5
where
N (B)s is the ith interval the box N# (B), and
2. 4 = min St and u4 = max S₁, where S fBB) (recall that S; is the set of ith element of every vector in S).
Proof. From the AUA theorem, we know that there exists a neural network N; that 6-abstractly
approximates Ji : C - R, which is like but only returns the ith output. We can then construct
network N = (N1 N,). Since each N, satisfies Eq. (4) separately, then N 6-abstractly approximates f.
A.2 ROBUSTNESS 7-ARY CLASSIFICATION
We now extend the definition of e-robustness to n-ary classifiers. We function f C. + R" to denote an n-class classifier. returns a value for each of the n classes; the class with the largest value is the result of classification. We assume there are ties. Formally, for given C, denote classification by f as cx)ss(f(x)), where
class(y) = arg max m
Definition A.4 (n-ary robustness). Let M C. We say that f is e-robust on M, where >> 0, for all x E M and x' E (x), we have class = (lass(f(x')).
We now extend the certifiably robust neural networks definition to the n-class case. Recall that R. (x) (x' ||x- x'|l e).
Definition A.5 (Certifibly robust networks). A neural network N is c-certifiably robust on M if. for all x E M, for all y, E #N (X.(x)), we have class(y) class(y').
Existence robust networks. We now show existence of robust networks that approximate some robust n-ary classifier f-
Theorem A.6 (Existence of robust networks). Let C R be continuous function that is e-robust on set M. Then, there exists a neural network that
1. agrees with on M, i.e., Vx M. class(N((x)) class (f())) and
2. is c-provably robust on M.
Proof. First, we need to post-process the results of f as follows: For all x C,
(0...., (0x)=((.....ll....
where y f(x and (lass((()) In other words, f is just like f. but it zeroes out the values of all but the output class i. This is needed since the interval domain is non-relational, and therefore it cannot capture relations between values of different classes, namely, keeping track which one is larger. Note that if f is continuous, then f is continuous.
12

---

Under review as a conference paper at ICLR 2021
Let 8' be the smallest non-zero element of any vector in the set (f(x) x C}. Following the AUA theorem, let N be a neural network that d-abstractly approximates f. where 0.56'.
STATEMENT (1): Pick any E M. Let the ith element of f(x) & 0; call it By construction i = class( class(((x)) (x)). Let N(x) = (yi....; Vv). By AUA theorem, we know that V5 < 0.58', for j * i, and 2 c 0.56'. Since 2 8', class( N (x)) = class(f(x)) =i.
STATEMENT (2): Let x E M. Let S = (x)... Let S; be the projection of all vectors in S on their ith element, where i = class(f(x))) (x)). We know that min S; > 8'. min S; exists because (x) is compact,
S and S;. By construction of and the fact that is robust, all other elements of vectors of S are zero, i.e., Sj = {0}, for j + i.
Let N# (x)) = [ıj ug] By AUA theorem and its proof, for j * i, we have Uy] C [0, 0.58". Similarly. [4, uz] S [min S: - 0.56', uz] S [0.55", uz]. It follows that for all y,y' E N (R, we have class(y) class(y') i. This is because any value in [8' 0.58', uz] larger than any value in [0, 0.56").
Notice that Thm. 4.5 is special case, it also holds.
B APPENDIX: ELIDED PROOFS
B. PROOF PROPOSITION 3.3
It is easy to see that all the activation functions t are monotonically increasing with lim t(x) =1 and
lim t(x)
for some / E R.
Because is increasing, ((=x) and ((1 - x) are both decreasing: thus, their composition ((1 - ((-x))
increasing.
lim t(1 t(-x)) = E( lim (1 t(-x))) = 2--00
-
lim t(1 - t( x)) = 1(1
lim f(-x)) = t(1 -
x0000
2100
ReLU.: 1 0, and ((1 1) = ReLU(1 - 0) = 1.
ELU.: 1 = 1, and ((1 1) FLU((2 2
softplus.: O, and f(1 I) softplus(1) log(1 +e).
smoothReLU.:: / 0, and t(1 - 1) = smoothReLU, =1 log(a + 1). (One can easily verify that 1 log(a + 1) < 1 for + 0).
B.2 CHOICE OF PARAMETERS 0 AND
Because the our construction works for any fixed 0 and e, we will choose 0 = min( K+1 4m+2' 4| )
where K and G are defined in Sec. 7; and < 0.5 be such that if ||x yll & then [f(x). f(y) < т. The latter is achievable from the Ceine-Cantor Theorem (see Rudin (1986),, so f is uniformly continuous on C.
B.3 PROPERTIES OF É
The following lemmas show that f, roughly behaves like an indicator function: its value within a box's ith dimension (as, bi] is ss its value outside of the neighborhood is z O; its value globally is bounded by 1. We will analyze the values of the terms in f.
13

---

Under review as a conference paper at ICLR 2021
The following lemma states that if is within the box's ith dimension, then the first tenm is close to 1 and the second term is close to O, resulting in (x()) ss
Lemma B.1. If [as, bi], then the following true:
1. t(u(z 0.5c a:)) E (1 8, 1].
2. t(u(æ 0.5c - b.)) E (0,
Proof. STATEMENT (1): Because x 3 04 ++0.c-- a; > 0.5e. From Lem. 6.1, (.1, E 0,1].
STATEMENT (2): Because b-, < -0.5c. From Lem. 6.1, b.)) [0, 0).
The next two Jemmas state that if x is outside the neighborhood, then the two terms are similar, resulting in (x) x O. Lemma B.2. If & a; 6, then the following true:
(((( 0.5c a:)) E (),
2. t(u(z 0.5c - b,)) E (),
Proof. STATEMENT (1): Because < - x 0.5c a, & -0.5e. From Lem. 6.1, t(u(x + 0.5c a4) E (0,0). a:))
STATEMENT (2): Because x & 0; 6 and a; b, & c. Then x 0.5c h E -0.5c. From Lem. 6.1, f(u(x - 0.5c - b.)) E ().
Lemma B.3. If > b; + e, then the following is true:
1. t(u(x + 0.5c - a;)) E (1 -1-60 0, 1].
2. t(u(x - E (1 0, 1]
Proof. STATEMENT (1): Because 3 b, + and b, > a, x 2 + Then + 0.5c a, 0.5e. From Lem. 6.1, t(μ(I + 0.5c a;)) (1 10--0,1 0, 0,
STATEMENT (2): Because x 3 b, + 6, x- - 0.5c by 3 0.5c. From Lem. 6.1, t(u(x - 0.5c - b:)) E (1 1.1].
B.3.1 ABSTRACT PRECISION OF f
We are ready to prove properties about the abstract interpretation of our 1-dimensional indicator approximation, f, The following lemma states that the abstract interpretation of i,2 1,4h (B), is quite precise: if the I-dimensional input box B is outside the neighborhood of G, on G's ith dimension, then the output box is within 0 from O: if the input box B is within the ith dimension of G. then the output box is within 20 from 1.
Lemma B.4 (Abstract interpretation of f.). For 1-dimensional box B, the following is true:
1. 2 (B) C (-00, 1].
2. 1f B (- B C [b. to, then 1 (B) C (-0,0).
3. If B (as, bi), then 1.1 (B) C (1 20,
14

---

Under review as a conference paper at ICLR 2021
Proof. We begin the proof by simplifying the expression e (B). Recall that 8(x) t(f(1r + 0.5c a.)) [((( 0.5e b4)). Let B [a, b]. By applying abstract transformer 8# (Def. 3.6) and
subtracting the terms, get e (B) [Ti T4, T2 Tal, where
Ti = t(p(a + 0.5c 0 - a;))
T2 = t(u(b + 0.5c - a.;))
73 U(p(a 0.5e b:))
Ta uu(b 0.5e - -bi))
We now ready prove the three statements.
STATEMENT (1): By the definition of i, Vv. f(x) [0, 1). T,, T3, T4 [0, 1). Therefore, the upper bound of f# (B) is T2 T3 < 1.
STATEMENT (2):
Case B C (-oc, 04 - c). From Lem. B.2, 7, 72, T3, T4 E [0, then T2 - T3 < 0, and
- > -0.
Case 2: B C [b; + 6, 00). From Lem. B.3, T3, T4 E (1 - 0, 1J. then T/ T3 < 0, and
T4 -0.
In either case, 1.t (B) ] (-0,0).
STATEMENT (3): If B [ (a,, b,]. a, la,, by). From Lem. B.1(1), T1, T2 (1 0] From Lem. B.1(2), T3, T4 E [0,0). Then Ti - T4 > 1- 20 and T2 - T3 & 1. Therefore, i (B) C (1 20, 1].
B.4 ABSTRACT PRECISION OF NG
We are now ready to analyze the abstract precision of No. We first consider H; in the following lemma. For any box B C C, let B, be its projection on dimension which is an interval.
The following lemma states that if B in the box G, then E, H is positive; otherwise, if B is outside the neighborhood of G. then E, _1 is negative.
Lemma B.5 (Abstract interpretation Hj), For any box C C, the following is true:
1. If B G. then Σm H (B,) S 20,
2. 1f B CC (GG), then - H (B:) C (-00,-e)
Proof. STATEMENT (1): B C G, then Vi. B; C (ag bi]. From Lem. B.4 (3), 8 (B:) S (11 - (1-220 thus,
120,
(B.)
1th (B:) +# -(1 - -
C
(0, 20
(0, 00)
Sum over all m dimensions, E 11 (B:) C EE (0, -0) = 0o).
STATEMENT (2): If B (G), then there is dimension j such that either B, S (-0c, ec] or B, C bb +, 0o). From Lem. B.4 (2), we know that {# (B,) (-0,0) 0). Therefore,
H
i# (#(B) +# - 20)#
(5)
C - 1,-1,30-1)
For the remaining m dimensions, from Lem. B.4 (1), we know that { (B,) (-00, 1] when i f j. Therefore.
H (B:)
f BB) # -(1 200)#
(6)
C (-00 20
15

---

Under review as a conference paper at ICLR 2021
Take the sum of all the dimensions,
Cie(I...m) H, (B,)
$ m)...m.. ()) (-00, (m 1,m *# (-00, 20]
(substitute Eq. (6)) (turn sum into *#)
(7)
(-00, 2(m - 1)0]
(apply **)
Now, take over all the m dimensions,
E H (B:)
= Eie(I,...m) (M. 11tht (B;) +# H1th (B,) S (-00, 2(m - 1)0 +# (0 1, 30 1)
(decompose sum)
(substitute Eqs. (5) and (7) (apply #
(-00, (2m + 1)0 - 1)
Because of our choice of 0, 0 < ām+z (see Appendix B.2). Then (2m + 1)0 < therefore
2m+11 0.5, and
4m+42
m
Σ
(B:) (B,) (-00, -0.5)
Also we have assumed that < 0.5 (see Appendix B.2); therefore
(B.) S (c)
B.4.1 PROOF OF THM. 6.2
Proof.
STATEMENT (1): See definition of NG in Eq. (3). The outer function of NG is t, whose range is [0, 1] by the definition of squashable functions and our assumption that the left and right limits are and 1. Therefore, N (B) C [0, 1].
STATEMENT (2): C G. from Lem. B.5, we know that Σm H (B.) S (0, oo). Then,
Σ H (B.) + (0.5c)* C (0, (0) +* (0.5c) C
(0.5e, oo)
From Lem. 6.1, we know that x 2 0.5c, then 0 < t(ux) & 1. Therefore,
N (B) = # (1+ # # (0.5e, oo)) S 0,
STATEMENT (3): If B C v(G), from Lem. B.5, we know that Em H (Bi) S (-o0,- -t).
Then.
E (B.) # (0.5c) # C (-o0, -c) ## (0.5c)# S (-00,-0.5r) -0.56)
From Lem. 6.1, we know that x < -0.5e, then 0 < t(Ux) < 0. Therefore,
N (B) = # (n # 1-00,-0.5e 3 [0,0)
B.5 ABSTRACT INTERPRETATION OF N
Observe how for any box B C from the abstract domain, it overapproximated by larger box G 2 B from the finitely many boxes in the e-grid. Intuitively, abstract approximation of N; incurs an сгтоr when the input B is not in the grid. We formalize this idea by extending the notion of neighborhood (Sec. 6) to boxes from the abstract domain. For box B C C, if B G, then B's neighborhood GB = v( (B); otherwise, let GB be the smallest G E g, by volume, such that B C G. Note that GB is uniquely defined.
The following lemma says that considering the neighborhood of B only adds up to 7 of imprecision to the collecting semanties of f.
16

---

Under review as a conference paper at ICLR 2021
Lemma B.6 (Properties of GB). The following is true:
1. fBB) > B, then f(Gn) 3 B T.
2. 1f f(B) & then f(GB) 3
Proof. Both of the statements follow from our choice of in constructing the grid (see Appendix B.2). If ||x - xx < c, then [x(x - f(y)] < т. Consider the B and its neighborhood Gg. By definition
of neighborhood, Vx E GB, By E B, such that ||x yll E e.
STATEMENT (1) Because [(B) > 8, then f(y) > 3, [(x) 2 f(y) - > B --.. т. Then Vx GB.
f(x) > B T.
STATEMENT (2) Because f(B) < B, then f(y) < 80 f(x) & f(y) + x 3 T. Then VX GB.
f(x) & B +T
Theorem B.7 (Abstract interpretation of No). For any box B S C, let max fBB). and 1 min f(B). The following is true:
1. No C 10.
2. Ifl > (i (i+ 2)T, then Bu, (1 0, 1] such that [u, u.] S N (B) S (1 (1-0,1}
3. Ifu & (i 1)r, then 30, (0,0) such that [4,4] S N (B) S (0,0).
Proof. We begin by noting that in Statement (2), [u,, us] S N (B) for some uN (1 1 -8,
direct corollary of N (B) S (1 0, 1]. Because if N (B) S (1 0, 1]. and N (B) * then
N (B) contains at least one point in (1 0, 1]. Similarly, in Statement (3), (4, 4] C N (B) for some 4 E [0,6 0) is direct corollary of N (B) S [0, 0).
In Appendix B.2, we have chosen that 0 < 4 fact we will use later in the proof.
STATEMENT (1): The outer function of N, is t, whose range is [0, 1]. by the definition of squashable function and construction, N (B) C [0, 1].
STATEMENT (2): Because f(B) (i + 2)r, by Lem. B.6, f(GB) (i 1)T, GB Gi. Thus, we can break up the sum as follows:
Σ Nx(x) =
Σ
No(x)
+ +N)
GEG
GE(D.)(GN))
From Thm. 6.2, N (B) C (1-0, 0, 1], and (B) S [0, for G e 9, (GB). Therefore, we can conclude the following two facts:
Σ (B) (1-,,00) and GEG.
(B) 0.5,, 0.5) S (0.5 0, oc) (0.5c, oo) GEG.
The second inequality follows from the fact that we assumed 0 < (see Appendix B.2). Therefore, 0.5 >> 0.25 0.5c.
4|0 & 0.25 (above) and < 0.5
1
follows from Lem. 6.1 that
N (B) t# (at (u****
# Σ (B) + 1-0.5, -0.5 ))
c c (1- (1-08 0,1]
GEG.
STATEMENT (3): If u & 1)T, will show that VG G.. B B (C)
17

---

Under review as a conference paper at ICLR 2021
Pick any G 9r, then we have f(G) > (1 1)T. Thus, from Lem. B.6, f(Gg) > it. Recall that if
B E G. then G3 = v BB). Hence, f(v(G)) > ir. However, f(B) < u & (1- 1)T, T.. so BBv(G)
Equivalently, B C C ((((G))
From Thm. 6.2, YG E G;.
(B) - 00 so
Σ ( (B) - [0, 1000) (9,
GEG.
We assumed that 0 < बशश and < 0.5 (see Appendix B.2), so | < 0.25, and |g]0 0.5 <
-0 0.25 & -0.5c. Hence,
Σ
00,025)
and
[+ _ [-0.5, -0.25) E (-00,-0050 -0.5e)
GES.
GEO.
It follows from Lem. 6.1 that
(B) 00.. 0.5) -0.5 )) c 10
N (B) 1
1nth *
Σ GE9
B.6 ABSTRACT INTERPRETATION OF N
Before proceeding with the proof, we give a general lemma that will be useful in our analysis. The lemma follows from the fact that, by construction, K+I
Lemma B.8. If fo...... ... 7K [-6,0], 0). then Ex T [-1,]]
Proof. This simply follow from the choice of 0
K+I'
Proof outline of Thm. 4.2. Our proof involves three pieces, outlined below:
(A) Because N (B) 7 # Ex N+( need only analyze E N (B). We will decompose the sum into five sums and analyze each separately, arriving at five results the form:
[Lu 0 S Σ
N, (B)
[1en) U2y
iES,
for j E 5J. where U, = tO...., K} and S are mutually disjoint sets.
(B) Then, we sum over all five cases, getting
5
K
5
Σ
Lıj.
Σ
Un
S
> N (B) S
Σ
Lej.
U2i
j=l
(C) L,= Les and U/ = - Uzj. Then, we get the bound U1. S AN (B)
[L2 U2].
Finally, we show that [L2, U2] [ - 8, 5) and [ + 6, u 8) [4. Equivalently, we will show that
1- 1- < L2 & L & l 5 and u 5 < U1 & U2 < a +
Proof assumptions. We will assume that e [pr, (p + 1)r) and u [gT, (q + 1)T), for some P & g & K. Additionally, let c, e be such that f(c) = and f(d) = u.
Step A: Decompose terms.
and analyze separately. We begin by decomposing the sum into five
This is the most important step of the proof. We want to show that most N,'s 's in Σ N (B) (almost) precise. By almost we mean that their values are ss 1 and ss 0. The motivation is then to extract many precise terms possible. The only tool used in the analysis is Thm. B.7.
18

---

Under review as a conference paper at ICLR 2021
Consider the function slices represented by Term and 5; for example, Term represents
abstractions N₂" of function slices fi, for E [0. p 2]. The function slices of Term 1 and 5 are referred to in Thm. B.7 (Statements 2 and 3): they have an (almost) precise abstract
interpretation. That is, the abstract semantics of N (B) and the collecting semantics of (B) agree. For Term the abstract interpretation of all N (B) [1,1] and fB) [T] For Term 5, the abstract interpretation of all N," (B) R [0,0] and [B) = 0j.
Now consider function slices St. where i Ip + 2. - 2]. The abstraction of these function slices is also (almost) precise. We can see [(c) 1 is below the lower bound of the slices and
(dd is above the upper bound of the slices. Hence, f((d) and N ((d3) [1, 1]. Similarly, f((c) = 0 and N (fc)) ~ [0. 0]. Because e, d E B, and due to continuity of f. we have fB) = [0, 1). and N (B) = [0. 1].
The remaining function slices are those in Term 2 and Term 4, and they are at the neigh- borhood of the boundary of [2, ul.. Most precision loss of N (B) comes from those two terms.
This drives us to decompose the sum as follows:
K
g+l
Σ N (B) 1=0
Σ (B)
Σ
(B)
Σ bp+2
(B)
(B)
#
Σ N
(B)
Σ N b
(B)
Term 2
Term 3
Term 4
Term
(8)
We will analyze the five terms in Eq. (8) separately, and then take their sum to get the final result. For now, assume that q 3 p 3; the q & p + 2 case will follow easily.
(i) Term 1: Vi < p- we have pr > (i ( 2)r. Because = min (BB and I e [pT, (p+ 1)r).
then [BB > pr > (i+ 2)T.
From Thm. B.7, 3mg E (1 0, 1] such that [us, ui] S N2 (B) S (1 - 0.1 Then
E [ui, uz] C E N, (B) C 2 (1 0, 1].
p 2
2
Σ k=0
Ju, uz]
S
Σ i=u
N (B) S (p-1) # (1 0, 1]
(ii) Term 5: Vi > + 2, we have (4 + 1)7 < (i - 1)7. Because u = max ((B) and
u E (yT, (q + 1)r). then ((B) < (4+ 1)7 < (i - 1)7.
From Thm. B.7, 34 (0, such that (4, 4] C N (B) S (0, Then ΣK Eispeeli [i] S K
Ei N# (B) C E K
200++10,00) 10, 0).
K
Σ kmq+2
41
C
N
C (K q - 1)# *# (0.0)
2mq+2
(ii) Term 3: Vi E [p + 2,q - 2]. we have (p + 1)r < (i 1)7 and qu > (i + 2)T.
f(c) = < (p + 1)r & (i - 1)T, and (d) = u 2 q7 > (i+
From Thm. B.7, N (fc)) S 0) and N ({d)) S (1 - 21-0,11 1). Because e, d E B,
[0, 10,1-0 0] S N, (B).
Also by Thm. B.7, (B)
(B) C [0, 1]. Hence, Σズ 10.1 0 S E. N. (B) S
Σe-22 10,1] 1].
4-2
9-2
Σ 2=p+2
10,1- - 0
Σ
N (B) c (q-p-3)- 3) # [0.1]
imp+2
(iv) Term 2: vi E [p- 1,p 1). since we have assumed that q 2/ p 3, then 9 > p+p 3 > i
19

---

Under review as a conference paper at ICLR 2021
Because f(d) > 9r > (i+ 2)7, from Thm. B.7, Bu, (1 0, 1] such that [u,, Us] S
(1d3) E (1 0, 1].
Because E B, [u, uil S N (B). Hence, ju, ui] S N (B) S [0, 1] and
EiELi [2: u,] S Ei N (B) S 10pp110,11 [0,1] 1].
p+1
p+1
Σ i=p-1
Lu us]
Σ (B) i=p-1
C
3 * [0,1]
(v) Term 4: For Vg- < < q+gl111 1, because q p 3. we have p ++1 < q 2 & i - 1.
Then f(c) = < (p + 1)r < (i - 1)T. From Thm. B.7, 31, E [0, f) such that [1,44]] S
N (1ct) C [0,0).
Because c E B, [4, 4.] S N (B). Thus, 14,4 S N. (B) _ [0.1].
9+1
4,4
Σ (B) 3 * [0.1]
1=4-1
Step B: Sum all five cases. We now sum up all five inequalities we derived above derive an overall bound of the sum in the form [1, U1]
E.
N (B) S [I/2, U2]. For example.
p-2
2
K
p+1
11
Σ U4
+
Σ
4+
E
0
1++
Σ
4
1=0
i=9+2
1=p+2
==p-1
ビ=タ-1
Recall that, by Thm. B.7, Vi E {O..... K}. u, E (1- - 0, 1] and 4 E [0,0), Let 7 = U2s So 1, E (0,0).
We simplify Li L22, Ui and U3 as follows:
L.
EE u, + Ei=gt24 4 Ex 9 Ei 14 E
(sum of the left bound)
(1 - i,) + Σ K
4 ンリー 2 1 1pt1 (1 [.) Σ
- 4
9+1
(substitute u, with i.)
(E-3) + - (1) + E1 + Σズ 4 + + 0 +
==p- 1 (-4) + Σi 4
p+1
(Rearrange the terms)
(D+2) + Entol (-1) + ΣKك 4 + プリー 0
(Sum all the 1's)
From Lem. B.8, ( + Σi 0 + Σ K
- [1,1] by plugging in -4, 4. 0 to 17. So.
E 1, p+3
Ul = Σ ui + E 4 + E/ 8) - U4 + - 9+1
2-
-
(sum of right bound)
E - 1,) + E
E 21
4
2
0)
M+ 1pppp11 - 4,) Di
4
(substitute u; with i,)
= (q 1) + Eet
-i=--
+ 9- 19ー2 (-0)
(sum all the 1's)
From Lem. B.8, 22 (-()) + 2-
Dispt2
(-0) + +
4 E
1.. Thus,
U E [g 2, g]
1/2 (p-1) 10-1)(1-0) (p ()(-0)
(sum of left bound) (rearrange terms)
20

---

Under review as a conference paper at ICLR 2021
Because 8 & K+I and K & p
K, we have (p 1)(-0) [-1, 1]. Hence,
I2 E ip - 2, pl
U/2 = (p (p-1 1 -- 3) + (K - --
1) (
3) 3
(sum of right bound)
(rearrange terms) (sum all the 1's)
q+2+ q
Because < I and -K & 9 1) < K, we have (K q E [[-,, Then,
R4T
U/2 E + 1, 9
Step C: Analyze the bound. It remains to show that - 8 & L2 & L1 & &1+ and u 8 < U1 <
U2 & uut+ 8.
Recall that we have set that 5 = 3r. Also I E [pr, (p+ 1)7), then
1- 8 (p 2)r
and
1+ > (p+
Since E [gr, (q 1)r), then
- (q 2)
and
u u 5 > (g 3)r
We have just analyzed E, L2 U/ and U/2 above. Now we have:
I = T < (p + 3)T
La = 212 > (p 2)
U1 = T (g 2)T
Up = TU/ & (q + 3)T
follows from the above inequalities that
(p 2)
L2
L
& (p+
< I+
and
21 (1 2
U1
U2
& (g + 3)
u 6
This concludes the proof for the case where 9 > p + 3.
and 5 are almost precise. The imprecise terms can only come from Terms and 4. If g < + 2, the only analyses that will be affected are those of Terms 2 and 4. Since q < p + 2, we have p > q - which means Terms 2 and 4 have potentially less sub-terms in this case. Thus imprecise terms are less than the q > + case and we can apply the same analysis as above and derive the same bound.
Excluded case. Previously,
have shown that Terms
We have thus shown that the neural network N that we construct d-abstractly approximates f. and therefore the AUA theorem true.
21


Reviews:
[{"review_id": "f1cpuFCm1O", "reviewer": "AnonReviewer1", "summary": "", "questions": "", "limitations": "", "rating": 5, "confidence": 3, "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 studies the universal approximation of robust networks called the abstract universal approximation. While the traditional universal approximation aims to approximate the single output corresponding to each input value, abstract universal approximation studies the output interval generated by the input interval (or box) and the interval value propagation. The main contribution of the paper is to extend the result of Baader et al., 2020 to networks using general squashable activation functions.\n\nI think that the main weakness of this paper is its novelty. The main idea of the proposed result seems very similar to that by Baader et al., 2020: approximate a target function using a summation of indicator functions. This idea and using a squashable (or sigmoid) activation function to approximate the indicator function have been widely used in the universal approximation literature. Hence, I think that the result of this paper (Theorem 4.2) can be viewed as a simple extension of the result by Baader et al. 2020. \n\nThe authors additionally claim that their construction and analysis are simpler than those by Baader et al., 2020. However, I think that this is only a minor improvement as the main focus is to show the 'existence' of networks, approximating functions under constraints.\n\nDue to these reasons, my decision tends to reject.", "extra_scores": {}, "extra_text": {}}, {"review_id": "PL3kJCEiRY", "reviewer": "AnonReviewer2", "summary": "", "questions": "", "limitations": "", "rating": 4, "confidence": 5, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "This paper proposes to extend the techniques of Baader et al. [2020], demonstrating that interval analysis provable ReLU networks are universal approximators, to a larger class of activation functions, which they call squashable functions.    Furthermore, they claim that their proof of this theorem is simpler due to using a bounded depth construction.  \n\nPros:\n\n* Their theorem does reduce the depth of the necessary construction.\n\n* Expanding the theorem to more activation types is a potentially useful contribution.\n\n* Technically, the paper appears to be correct.\n\nCons:\n\n* The proposed method mostly follows the same proof technique ad Baader et al. [2020] and thus is not particularly novel.\n\n* The authors claim that their method uses the most commonly used activation functions, yet ReLU is by far the most relevant activation function and is already included in the original theorem.\n\n* The number of ReLUs they use for an indicator function (they might need to use intractably many indicator functions) is asymptotically identical to Baader et al [2020]. They have only reduced the number of neurons used per indicator by a constant.  However, it is unclear whether this is an advantage, since the method appears to use more slices as well.  How do the two methods compare in terms of number of neurons for the entire net when considering the same function, delta, and epsilon?\n\n* The title “Generalized Universal Approximation for Certified Networks” is claims a significant improvement in generality over the original paper, Universal Approximation with Certified Networks (Baader et al. [2020]), yet the addition of other activation functions is hardly a significant enough difference to warrant such a claim of generality.\n\n* Care is not taken when introducing concepts from prior work:  Section 3.2 discusses concepts introduced first by Cousot et al. [1992] and then brought to neural networks by Gehr et al. [2018], but is presented as if it were new.  Definition 4.1 is an idea developed by Baader et al [2020] yet this is also not made clear.  Section 6.2 proposes an idea that is very similar to Def 4.2 from Baader et al and uses concepts introduced as the nodal basis function in He et al [2018] but does not make this clear. \n\nFinal Review:\n\nIn summary, while technically the paper does not appear to have flaws, its contributions are incremental, and its similarity to prior work is such that it is hard to recommend acceptance.   I am thus giving this paper a rejection. \n\n[1] P. Cousot and R. Cousot. Abstract interpretation frameworks. Journal of Logic and Computation, 2(4):511–547, 1992.\n[2] Gehr, T., Mirman, M., Tsankov, P., Drachsler Cohen, D., Vechev, M., and Chaudhuri, S. Ai2: Safety and robustness certification of neural networks with abstract interpretation. In Symposium on Security and Privacy (SP), 2018.\n[3] Juncai He, Lin Li, Jinchao Xu, and Chunyue Zheng. ReLU Deep Neural Networks and Linear Finite Elements. arXiv preprint arXiv:1807.03973, 2018.\n", "extra_scores": {}, "extra_text": {}}, {"review_id": "Ku-avEH4XM", "reviewer": "AnonReviewer3", "summary": "", "questions": "", "limitations": "", "rating": 4, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "The paper shows an \"augmented\" universal approximation (UA) result for neural networks that the authors call Abstract UA (AUA for short) and the motivation comes from understanding expressivity and certifiability of NN. Their result holds for NN with a wide variety of activation units and this is the main point of the paper, which directly extends the same result for ReLU networks (Baader et al. 2020).\n\nTypically, results in UA state that any continuous function f on a bounded domain can be expressed as a combination of activation units, sometimes even with only one hidden layer and one output layer, which is the classical result by Cybenko (1989), Hornik (1989) and more.  Their augmented version asks what if we want to have a more robust version of those statements, where we want to certify that any given box in the domain of f is mapped through the NN in such a way so that the NN values always stay close to the values of f. More formally, for some given accuracy \\delta, we want to have |NN(x) - f(x)| < \\delta for all x in the box. Furthermore, we would like to be able to certify this property and to do so we can use the technique of interval propagation. (To put it differently, the image of any interval of f is basically \"sandwiched\" between two close-by surfaces that are output by the NN.)\n\nThe result is of theoretical nature and this is fine as expressivity and certifiability are not yet well-understood. The major issue with the paper is the lack of novelty. The most related paper in terms of techniques and ideas (Baader et al.) proved the exact same result when the activations are ReLUs instead of the wider variety of activation units considered in the paper. The units considered here, are basically monotone functions that have upper and lower cut-offs or can be phrased as such after a simple transformation. The main ideas for approximating functions via step functions and indicators on intervals or boxes has been used for decades (even starting with the folklore results in approximation theory) and there seems to be lack of substantially new ideas. The reviewer feels that given the previous work on ReLUs (Baader et al.), the proof for the more general activation units can be reverse-engineered. Finally, of secondary importance the authors state some simplifications over Baader et al.\n\nA minor issue that the reviewer is ok with, is that for a more practice-oriented person, it is hard to buy the motivation from adversarial robustness/certifiability as in many settings the adversary will not just choose an attack bounded in \\ell_infinity by some small parameter. It is nice to have certifiable NN and know their behaviour if the inputs slightly change, however the motivation also needs to address what happens when a few large perturbations are allowed like the single-pixel attack (\"One pixel attack for fooling deep neural networks\").\n\nOverall, conditioned on the immediate prior work,  the result itself simply extends AUA from ReLU activations to more general units, and is not surprising. \n\nOne quick suggestion: Can the authors clarify how the lipschitzness of f or of the NN can affect the statements? Otherwise, the theorem may be misinterpreted as a consequence of continuity.\n\nSuggestions for future improving:\nDid the authors consider proving something along the lines of depth separation results for such kinds of AUA? The reviewer believes this could give a new dimension to the AUA theorems and draw another connection with certifiability and depth/width tradeoffs. Depth is usually preferred in practice over width, and a formal way for proving this is to show the power of depth in representing functions: for example, relevant works here are Telgarsky's (Benefits of depth in neural networks) and later improvements (Better Depth-Width Trade-offs for Neural Networks through the lens of Dynamical Systems) that show exponential separations in depth vs width by constructing highly oscillatory functions. However these works do not consider certifiability which may be an opportunity for your techniques.\n\nAnother quick question: Is there a formal comparison of your squashable activation units to the semi-algebraic units considered in Telgarksy? Maybe your results can also capture such activations?\n \nOther comments:\n\nTheorem 3.3:  Do the authors consider this one of the main contributions of the paper? Wouldn't it be better to be stated as a proposition, as it is quite straightforward for the activation units stated there?\n\np1: \"Their theorem states that not only can neural networks approximate any continuous function f\n(universal approximation)\" ... the reviewer believe that this first part of the sentence is a bit misleading as universality has been known since the 80s. The sentence starting with \"but...\" is the extension presented in Baader et al. and that is the contribution, right?  \n\nFig.1: When one takes interval bounds and considers a superset of box B, shouldn't the output be superset of f(B)? Maybe the figure is a bit confusing? What does it mean:  \"(Right is adapted from Baader et al. (2020).)\"\n\np2: When Abstract universal approximation (AUA) theorem is stated: Again f is continuous so it should be clarified. Also: Line 5 of this paragraph: interval bounds are stated but if the parameters are not given (is it \\eps?) like it was done in the intro, then the result is not meaningful as it would be a consequence of the continuity of f and Lipschitzness of NN (please discuss).  Maybe another way to phrase the same thing, is to say that whenever the input is changed to B+\\eps, the network follows f(B)+\\delta for appropriate parameters? The point is just that the NN will not do anything \"too wild\" correct? In other words, there is a NN that will map intervals of f to not-much-wider intervals correct?\n\nTypos/Inaccuracies:\np2: the AUA theorem implies us that \np2: while controlling approximation error δ\np2: a bounded number of layers --> just one hidden layer was proved in Cybenko. What is the \"standard\" feedforward NN?\np2: an universal -> a (several places)\np6: has rigid values --> rigid? (meaning relu is fixed everywhere?)\n\n", "extra_scores": {}, "extra_text": {}}, {"review_id": "FsMsLUhPFIN", "reviewer": "AnonReviewer4", "summary": "", "questions": "", "limitations": "", "rating": 5, "confidence": 2, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "", "summary_of_the_review": "", "strength_and_weaknesses": "", "limitations_and_societal_impact": "", "review_text": "This work studies the task of universally approximating continuous functions by (certain classes of) neural networks. The paper shows that for a continuous function $f$ there exists a neural network $N$ such that for any box $B$ the range of outputs of $N$ is close (in a parameter $\\delta$) to the range of outputs of $f(x)$, $\\forall x \\in B$.\nThis proof is constructive and applies to $N$ using ReLU, sigmoid, tanh or ELU activation functions. (The result actually includes an even larger class of activation functions, that the authors call _squashable_.)\n\nA previous work, Baader et al., shows the same result when neural networks use ReLU activation functions. The authors of this paper provide a result applicable to a broader class of networks. They also improve the size of neural networks constructed in Baader et al. (as discussed in the last paragraph of Section 6), but at many points in the paper this result feels to be incremental.\n\n-- Minor comments about the paper:\n\nFigure 1, which assumes Eq (1), could be moved to the top of Page 4, after Eq (1) is stated.\n\nSections 3 and 4 have lots of text in bold. Many paragraphs are named, and then they have definitions with the same name. It reduces readability.\n\nThe bottom of Figure 6 and the text are too close to each other.\n\n**Updates**:\n\nAfter carefully reading comments of the other reviewers as well as the authors' response, I change my score from 6 to 5.", "extra_scores": {}, "extra_text": {}}]

Author rebuttal:

Meta-review: The authors extend prior work showing that networks trained to be certifiably robust using interval bound propagation are universal approximators. They extend prior results applicable to ReLU networks to a much broader class of networks with general activation functions. 

The paper makes an interesting contribution to the literature relative to prior literature showing that one need not sacrifice universal approximation guarantees while training networks with IBP to be certifiably robust to l_inf attacks.

Since the paper is primarily theoretical, the main concern raised by the reviewers was around novelty and the theoretical significance of ideas presented relative to prior work. While proof techniques may be novel, the extension of AUA results to alternate activation functions is not surprising and do not substantially contribute to the field's understanding of learning certifiably robust networks particular since most SOTA results for IBP-based training have been achieved with ReLU based networks. The authors' rebuttal did not providing convincing arguments for the reviewers to revise their scores. Hence I do not feel that the contributions of the paper justify acceptance at this time.
Decision: Reject