Year: 2020

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.

text: 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.

heading: 1 INTRODUCTION
text: 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 to the input of a network should not change the prediction. For example, a small change to an image of a stop sign should not cause a classifier to think it is a speed-limit sign. A number of researchers have proposed the use of abstract interpretation (Cousot & Cousot, 1977) techniques to prove robustness of neural networks (Gehr et al., 2018; Wang et al., 2018; Anderson et al., 2019) and to 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 we want to verify robustness of a neural network to small changes in the brightness of an image. We can represent a large set of images, with varying brightness, as an element of some abstract domain, and propagate it through the network, effectively executing the network on an intractably large number of images. If all images lead to the same prediction, then we have a proof that the network is robust on 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 a real number r, then the pixel can be represented as an interval [r− , r+ ], where denotes the range of brightness we wish to be robust on. Then, the box representing the interval of each pixel is 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 f (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 an arbitrarily close approximation of the set semantics of f , i.e., the result of applying f to a set of inputs (e.g., set of similar images).
AUA theorem (semi-formally): For a continuous function f : Rm → R that we wish to approximate and error δ > 0, there is a neural network N that has the following behavior:
Let B ⊂ Rm be a box. The red interval (top) is the tightest interval that contains all outputs of f when applied to x ∈ B. If we propagate box B through N using interval bounds, we may get the black interval (bottom) N#(B), whose lower/upper bounds are up to δ away from the red interval.
6 δ 6 δ
minx∈B f(x) maxx∈B f(x)
N#(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 δ > 0 be the tolerated error. Then, there exists a neural network N , built using any well-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 a single point in Euclidean space, the AUA theorem reduces to the universal approximation theorem; thus, AUA generalizes universal approximation. Fig. 1 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 `∞ norm, which is typically used to define a set of images in the neighborhood of a given image. The classical universal approximation theorem tells us that, for any desired precision, there is a neural network that can approximate f . We prove that the AUA theorem implies us 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.
Squashable functions. We define a 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 error δ.
Proof of AUA theorem. We present a constructive proof of the AUA theorem. Our construction is inspired by and synthesizes a range of results: (1) the work of Hornik et al. (1989) on 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) on the specialized AUA theorem for ReLUs. 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.

heading: 2 RELATED WORK
text: 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 on a 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 a 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
hold beyond non-polynomial 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 et al. (2017); Kidger & Lyons (2019), or specific neural network architectures Lin & Jegelka (2018). Another line of work focuses on 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 on decision procedures, like SMT solvers Ehlers (2017); Katz et 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 on 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. Abstract-interpretation-based 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 et 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.

heading: 3 FOUNDATIONS AND SQUASHABLE ACTIVATION FUNCTIONS

heading: 3.1 NEURAL NETWORKS AND SQAUSHABLE ACTIVATIONS
text: A neural network N is a function in Rm → R. We define a network N following a simple grammar, a composition of primitive arithmetic operations and activation functions. Definition 3.1 (Neural network grammar). Let x ∈ Rm be the input to the neural network. A neural network N is defined using the following grammar: N = c | xi | N1 +N2 | c ∗N1 | t(N1), where c ∈ R, xi is the ith element of x, and t : R→ R is an activation function. We will always fix a single activation function t to be used in the grammar.
We now present a general class of activation functions that we will call squashable activation functions. Fig. 2 shows some examples. Definition 3.2 (Squashable functions). t : R→ R is squashable iff (1) there is a < b ∈ R such that
lim x→−∞ t(x) = a, lim x→∞
t(x) = b, and ∀x < y. t(x) 6 t(y) (1)
or (2) we can construct a function t′ that satisfies Eq. (1) as affine transformations and function compositions of copies of t, i.e., following the grammar in Def. 3.1. E.g., t′(x) = t(1− t(x)).
Informally, an activation function is in this class if we can use it to construct a monotonically increasing function that has limits in the left and right directions, −∞ and∞.1 Squashable activation
1In our construction and proof, we do not need the function to be monotonic; however, in practice, most activation functions are monotonic and abstractly interpreting arbitrary functions is impractical.
functions extend the squashing functions used by Hornik et al. (1989). All of the activation functions in Fig. 2 are squashable.
Fig. 2 (top) shows activation functions that satisfy Eq. (1), 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)? It 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 t, if we can construct a new activation function t′ 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. 2 (bottom).
Proposition 3.3. Let t ∈ {ReLU, softplus, smoothReLUa,ELU}. The function t′(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.

heading: 3.2 INTERVAL ANALYSIS OF NEURAL NETWORKS
text: Given f : Rm → R and set S ⊆ Rm, we will use f(S) to denote {f(x) | x ∈ S}. We now define interval versions of the operations of a neural network, which are known as abstract transformers. This was first introduced in Cousot & Cousot (1977), which also proved the soundness of the interval domain. An m-dimensional box B is a tuple of intervals [l1, u1]× . . .× [lm, um]. All our operations are over scalars, so we define abstract transformers over 1D boxes.
Definition 3.5 (Arithmetic abstract transformers). LetB be anm-dimensional box input to the neural network. We follow the grammar in Def. 3.1 to define the abstract transformers.
c# = [c, c]
x#i = [li, ui], where li, ui are the ith lower and upper bounds of B [l1, u1] +
# [l2, u2] = [l1 + l2, u1 + u2] [c, c] ∗# [l, u] = [min(c ∗ l, c ∗ u),max(c ∗ l, c ∗ u)]
Definition 3.6 (Abstract transformer for activations). Let B = [l, u]. Then, t#(B) = [t(l), t(u)].
This transforer was introduced in (Gehr et al., 2018).

heading: 4 ABSTRACT UNIVERSAL APPROXIMATION THEOREM & ITS IMPLICATIONS
text: In this section, we state the abstract universal approximation (AUA) theorem and its implications.
Assume a fixed continuous function f : C → R, with a compact domain C ⊂ Rm, that we wish to approximate.
Definition 4.1 (δ-abstract approximation). Let δ > 0. A neural networkN δ-abstractly approximates f iff for every box B ⊆ C, we have [l + δ, u− δ] ⊆ N#(B) ⊆ [l − δ, u+ δ], where l = min f(B) and u = max f(B).
δ-abstract approximation says that the box output of abstract interpretation N#(B) is up to δ away from the tightest bounding box around the set semantics f(B). It was developed in Baader et al. (2020). Observe that the standard notions of approximation is a special case of δ-abstract approximation, when the box B is a point in C.
We now state our main theorem:
Theorem 4.2 (Abstract universal approximation). Let f : C → R be a continuous function on compact domain C ⊂ Rm. Let t be a squashable activation function. Let δ > 0. There exists a neural network N , using only activations t, that δ-abstractly approximates f .
Informally, the theorem says that we can always find a neural network whose abstract interpretation 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 t. In the appendix, we give a generalization of the AUA theorem to functions and networks with multiple outputs.
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 a robust classifier in `∞ norm. We treat f : C → R as a binary classifier, where an output < 0.5 represents one class and > 0.5 represents another.
Definition 4.3 ( -Robustness). Let x ∈ Rm, M ⊆ C and > 0. The -ball of x is R (x) = {z | ‖z− x‖∞ 6 }. We say that f is -robust on set M iff, for all x ∈ M and z ∈ R (x), we have f(x) < 0.5 iff f(z) < 0.5.
Definition 4.4 (Certifiably robust networks). A neural network N is -certifiably robust on M iff, for all x ∈M , we have N#(B) ⊆ (−∞, 0.5) or N#(B) ⊆ [0.5,∞), where B = R (x) (Note that an -ball is a box in Rm.).
From an automation perspective, the set M is typically a finite set of points, e.g., images. For every x ∈ M , the verifier abstractly interprets N on the -ball of x, deriving a lower bound and upper bound of the set of predictions N(R (x)). If the lower bound is > 0.5 or the upper bound is < 0.5, then we have proven that all images in the -ball have the same classification using N .
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 is certifiably robust. Refer to the supplementary materials for an extension to n-ary classifiers.
Theorem 4.5 (Existence of robust networks). Let f : C → R be -robust on set M ⊆ C. Assume that ∀x ∈M, z ∈ R (x). f(z) 6= 0.5.2 Let t be a squashable activation function. Then, there exists a neural network N , using activation functions t, that (1) agrees with f on M , i.e., ∀x ∈M.N(x) < 0.5 iff f(x) < 0.5, and (2) is -certifiably robust on M .

heading: 5 PROOF OF AUA THEOREM: AN OVERVIEW
text: 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 δ-abstractly approximates a function f .
Approximating indicator functions (Sec. 6). The key element, and primary novelty of our proof, is the construction of 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 approximation with a sigmoid.
It is a classical idea to use indicator functions to approximate a continuous function in a piecewise fashion—see Nielsen (2015, Ch.4) for an interactive visualization of universal approximation. However, for AUA, the input to the function is a box, and therefore we need to make sure that our indicator-function approximations provide tight abstract approximations (Def. 4.1), as will be shown in Thm. 6.2.
2This assumption eliminates the corner case where a point sits exactly on the classification boundary, 0.5.
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 = ∑ i fi. Each fi captures the behavior of f on a small interval of its range. See Fig. 4 for an example of slicing. Next, we approximate each fi using a neural network Ni. Slicing ensures that δ-abstract approximation is tight for large boxes. Because f(B) = ∑ i fi(B), when approximating fi(B) using Ni(B), we can show that for most i, fi(B) ≈ Ni(B). The smaller the range of slice fi, the tighter the abstract approximation of f using indicator functions.
Our construction and analysis are different from Baader et al. (2020) in the following ways:
1. 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 to the whole neural network.
2. The key construction of Baader et al. (2020) is to build min(x1, x2, . . . , x2m) using ReLUs. The depth of the construction depends on m, and the analysis of its interval bounds is rather complicated. Our construction uses only two layers of activations, resulting in a much simpler analysis. Because ReLU is a 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 et al. (2020).

heading: 6 ABSTRACTLY APPROXIMATING INDICATOR FUNCTIONS
text: We begin by showing the crux of our construction: how to approximate an indicator function. Recall that our goal is to δ-abstractly approximate a continuous function f : C → R. Grid of boxes. Fix > 0. Consider a standard grid of vertices over C, where any two neighboring vertices are axis-aligned and of distance ; we will call this an -grid.3 Let [a1, b1]× . . .× [am, bm] be a box G on the grid, where [ai, bi] is the range of G at dimension i. In other words, bi − ai is a multiple of . The neighborhood ν(G) of G is [a1 − , b1 + ]× . . .× [am − , bm + ]. Our goal is to construct an indicator function whose value is close to 1 within G, and close to 0 outside G’s neighborhood ν(G). The idea of using grid is similar to the nodal basis in He et al. (2018).
Indicator-function approximation intuition. Given any activation function t that satisfies Eq. (1), a key observation is that if we dilate t properly, i.e., multiply the input with a large number µ to get t(µx), 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 x > 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 1 for x ∈ (0, 1], and 0 otherwise. In what follows, we will use the above ideas to approximate the sign function and the indicator function for m-dimensional boxes.

heading: 6.1 APPROXIMATING A ONE-DIMENSIONAL INDICATOR FUNCTION
text: We will first show how to construct an indicator function for a 1D 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 t that (1) satisfies Eq. (1) and (2) has left and right limits of 0 and 1, respectively.4
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, σ, is 1, but ∀x. σ(x) 6= 1. This will lead to a loss of precision when we use t to model a sign function. However, we can carefully apply mathematical analysis to rigorously bound this imprecision.
3The vertices of the grid form a natural /2-net on C equipped with l∞ metric. 4If (1) is not satisfied, by Def. 3.2, we can construct a t′ that satisfies Eq. (1) from t. If (2) is not satisfied, we
can apply an affine transformation to the results of t to make the left and right limits 0 and 1.
Dilation to approximate sign function. We now discuss how to dilate t to get a sign-functionlike behavior. By definition of limit, we know the following lemma, which states that ∀θ > 0 by sufficiently increasing the input of t, we can get θ close to the right limit of 1, and analogously for the left limit. Figs. 5a and 5b show how sigmoid can approximate an indicator function.
Because the grid size is , we want the sign-function approximation to achieve a transition from ≈ 0 to ≈ 1 within . Let µ be the dilation factor. We would like the following (Fig. 6 illustrates the loss of precision θ incurred by our construction):
Lemma 6.1. ∀θ > 0,∃µ > 0 such that: (1) if x > 0.5 , then t(µx) ∈ (1− θ, 1]; (2) if x 6 −0.5 , then t(µx) ∈ [0, θ).
Indicator function on dimension i. Recall that the projection of a box G on dimension i is [ai, bi]. We want to build an indicator function that has value close to 1 on [ai, bi], and value close to 0 on R \ [ai − , bi + ]. 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
t̂i(x) = t (µ (x− (ai − 0.5 )))− t (µ (x− (bi + 0.5 ))) (2)
We choose the two points ai − 0.5 and bi + 0.5 , which lie in the middle of the [ai, bi] and its neighborhood, so that t̂i’s value of is close to 1 within [ai, bi], and 0 outside [ai, bi]’s neighborhood.
6.2 APPROXIMATING AN m-DIMENSIONAL INDICATOR
We saw how to construct an 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 to construct an indicator function whose value within a box G is close to 1, and outside the neighborhood ν(G) is close to 0. In the multi-dimensional case, m > 2, we do not know at which, if any, dimension j of an input is outside the neighborhood of G. The 1-dimensional indicator approximation, t̂, which we constructed earlier, can be used to tell us, for each dimension j, whether xj is within the bounds of the neighborhood of G. Therefore we can construct a logical OR approximation that applies t̂ to each dimension and takes the OR of the results. Specifically: (1) we will construct a function that applies t̂ to each dimension, and sums the results such that the answer is > 0 if x ∈ G, and < 0 if x 6∈ ν(G). (2) Then, we can use the sign-function approximation to indicate the sign of the answer.
Formally, we define the neural network NG as follows:
NG(x) = t
( µ ( m∑ i=1 Hi(xi) + 0.5 )) (3)
where Hi(x) = t̂i(x) − (1 − 2θ). Eq. (3) has a 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.
The term ∑m i=1Hi(xi) evaluates to a positive value if x ∈ G and to a negative value if x 6∈ ν(G). Observe that we need to shift the result of t̂ by (1 − 2θ) to ensure a negative answer if one of the dimensions is outside the neighborhood. Then, we use t to approximate the sign function, as we did in the 1-dimensional case, giving ≈ 1 if x ∈ G, and ≈ 0 if x 6∈ ν(G). Fig. 5c shows a plot of a two dimensional NG.
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, the following is true:
1. N#G (B) ⊆ [0, 1]. 2. If B ⊆ G, then N#G (B) ⊆ (1− θ, 1]. 3. If B ⊆ C \ ν(G), then N#G (B) ⊆ [0, θ).
Complexity of construction. To construct a single indicator function, we use 2m + 1 activation functions, with depth 2 and width 2m. If we restrict ourselves to ReLU neural network, we use 4m+ 2 neurons, with depth 4 and width 2m; in contrast, Baader et al. (2020) used 10m− 3 ReLu functions, with depth 3 + log2(m), and width 4m.

heading: 7 COMPLETE PROOF CONSTRUCTION OF AUA THEOREM
text: 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 to 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 a slicing size of δ/3 instead of δ/2 in Baader et al. (2020). We provide the detailed analysis in the appendix. In what follows, we outline on how to build the network N that satisfies the AUA theorem.
Slicing f . Let f : C → R be the continuous function we need to approximate, and δ be the approximation tolerance, as per AUA theorem statement (Thm. 4.2). Assume min f(C) = 0.5 Let u = max f(C). In other words, the range of f is [0, u].
Let τ = δ3 . We will decompose f into a sequence of function slices fi, whose values are restricted to [0, τ ]. Let K = bu/τc. The sum of the sequence of function slices is f . The sequence of functions fi : C → [0, τ ], for i ∈ {0, . . . ,K}, is:
fi(x) =  f(x)− iτ, iτ < f(x) 6 (i+ 1)τ 0, f(x) 6 iτ τ, (i+ 1)τ < f(x)
Approximating fi. We will use the indicator approximation NG (Eq. (3)) to construct a neural network Ni that approximates fi. Let G be the set of boxes whose vertices are in the grid. Because C is compact, |G| is finite. Consider 1τ fi(x); it is roughly similar to an indicator function for the set S = {x ∈ C | f(x) > (i + 1)τ}, i.e., indicating when f(x) is greater than the upper bound of the ith slice. To approximate 1τ fi(x), we will consider all boxes in G that are subsets of S, and construct an indicator function to tell us whether an input x is in those boxes. Let Gi = {G ∈ G | f(G) > (i+ 1)τ}.
Now construct Ni(x) that approximates 1τ fi(x) as Ni(x) = t ( µ (∑ G∈Gi NG(x)− 0.5 )) .
Sum all Ni. Because ∑K i=0 fi(x) = f(x), and Ni(x) approximates 1 τ fi(x), we will construct the
neural network N as N(x) = τ ∑K i=0Ni(x).
N δ-abstractly approximates f ; therefore, the AUA theorem holds.
5Otherwise, we can shift f such that min f(C) = 0.

heading: 8 CONCLUSION
text: We have shown that the AUA theorem holds for most practical neural networks, and demonstrated that in theory interval analysis can certify the robustness of neural networks. In the future, one 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.

heading: A.1 HIGHER-DIMENSIONAL FUNCTIONS
text: 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 of n scalar-valued neural networks to construct a neural network whose range is Rn. Formally, we extend the grammar as follows, where Ei are the scalar-valued sub-neural networks. Definition A.1 (Vector-valued neural network grammar). A neural networkN : Rm → Rn is defined as follows
N :− (E1, . . . , En) E :− c
| xi | E1 + E2 | c ∗ E2 | t(E1, . . . , Ek)
where c ∈ R, xi is one of the m inputs to the network, and t is an activation function. Example A.2. Consider the following neural network N : R2 → R2:
N(x) = (σ(x1 + 0.5x2), σ(0.1x1 + 0.3x2))
which we can pictorially depict as the following graph:
x1
x2
+ σ
+ σ 0.1
0.5
0.3
Generalized AUA theorem. We now generalize the AUA theorem to show that we can δ-abstractly approximate vector-valued functions.
Theorem A.3. Let f : C → Rn be a continuous function with compact domain C ⊂ Rm. Let δ > 0. Then, there exists a neural network N : Rn → Rm such that for every box B ⊆ C, and for all i ∈ [1,m],
[li + δ, ui − δ] ⊆ N#(B)i ⊆ [li − δ, ui + δ] (4) where
1. N#(B)i is the ith interval in the box N#(B), and
2. li = minSi and ui = maxSi, where S = f(B) (recall that Si is the set of ith element of every vector in S).
Proof. From the AUA theorem, we know that there exists a neural network Ni that δ-abstractly approximates fi : C → R, which is like f but only returns the ith output. We can then construct the network N = (N1, . . . , Nn). Since each Ni satisfies Eq. (4) separately, then N δ-abstractly approximates f .
A.2 ROBUSTNESS IN n-ARY CLASSIFICATION
We now extend the definition of -robustness to n-ary classifiers. We use a function f : C → Rn to denote an n-class classifier. f returns a value for each of the n classes; the class with the largest value is the result of classification. We assume there are no ties. Formally, for a given x ∈ C, we denote classification by f as class(f(x)), where
class(y) = argmax i∈{1,...,m} yi
Definition A.4 (n-ary robustness). Let M ⊂ C. We say that f is -robust on M , where > 0, iff for all x ∈M and x′ ∈ R (x), we have class(f(x)) = class(f(x′)).
We now extend the certifiably robust neural networks definition to the n-class case. Recall that R (x) = {x′ | ||x− x′|| 6 }. Definition A.5 (Certifibly robust networks). A neural network N is -certifiably robust on M iff, for all x ∈M , for all y,y′ ∈ N#(R (x)), we have class(y) = class(y′).
Existence of 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 f : C → Rn be a continuous function that is -robust on set M . Then, there exists a neural network that
1. agrees with f on M , i.e., ∀x ∈M. class(N(x)) = class(f(x)), and
2. is -provably robust on M .
Proof. First, we need to post-process the results of f as follows: For all x ∈ C,
f̂(x) = (0, . . . , |yi|, . . . , 0)
where y = f(x) and class(f(x)) = i. 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.
Let δ′ 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 δ-abstractly approximates f̂ , where δ < 0.5δ′.
STATEMENT (1): Pick any x ∈ M . Let the ith element of f̂(x) 6= 0; call it c. By construction i = class(f(x)). Let N(x) = (y1, . . . , yn). By AUA theorem, we know that 0 6 yj < 0.5δ′, for j 6= i, and yi > c− 0.5δ′. Since c > δ′, class(N(x)) = class(f(x)) = i.
STATEMENT (2): Let x ∈ M . Let S = f̂(R (x)). Let Si be the projection of all vectors in S on their ith element, where i = class(f̂(x)). We know that minSi > δ′. minSi exists because R (x) is compact, so are S and Si. By construction of f̂ and the fact that f is robust, all other elements of vectors of S are zero, i.e., Sj = {0}, for j 6= i.
Let N#(R (x)) = [lj , uj ]. By AUA theorem and its proof, for j 6= i, we have [lj , uj ] ⊂ [0, 0.5δ′). Similarly, [li, ui] ⊆ [minSi − 0.5δ′, ui] ⊆ [0.5δ′, ui]. It follows that for all y,y′ ∈ N#(R (x)), we have class(y) = class(y′) = i. This is because any value in [δ′ − 0.5δ′, ui] is larger than any value in [0, 0.5δ′).
Notice that Thm. 4.5 is a special case, so it also holds.

heading: B APPENDIX: ELIDED PROOFS

heading: B.1 PROOF OF PROPOSITION 3.3
text: It is easy to see that all the activation functions t are monotonically increasing with
lim x→−∞ t(x) = l and lim x→∞ t(x) =∞.
for some l ∈ R. Because t is increasing, t(−x) and t(1−x) are both decreasing; thus, their composition t(1− t(−x)) is increasing.
lim x→−∞ t(1− t(−x)) = t( lim x→−∞ (1− t(−x))) = l
lim x→∞ t(1− t(−x)) = t(1− lim x→∞ t(−x)) = t(1− l)
ReLU.: l = 0, and t(1− l) = ReLU(1− 0) = 1. ELU.: l = −1, and t(1− l) = ELU(2) = 2. softplus.: l = 0, and t(1− l) = softplus(1) = log(1 + e). smoothReLU.: l = 0, and t(1− l) = smoothReLUa(1) = 1− 1a log(a+1). (One can easily verify that 1a log(a+ 1) < 1 for a 6= 0).
B.2 CHOICE OF PARAMETERS θ AND
Because the our construction works for any fixed θ and , we will choose θ = min( 1K+1 , 1 4m+2 , 1 4|G| ), where τ , K and G are defined in Sec. 7; and < 0.5 be such that if ‖x− y‖∞ 6 , then |f(x) − f(y)| < τ . The latter is achievable from the Heine–Cantor Theorem (see Rudin (1986)), so f is uniformly continuous on C.
B.3 PROPERTIES OF t̂i
The following lemmas show that t̂i roughly behaves like an indicator function: its value within a box’s ith dimension [ai, bi] is ≈ 1; its value outside of the neighborhood is ≈ 0; its value globally is bounded by 1. We will analyze the values of the two terms in t̂i.
The following lemma states that if x is within the box’s ith dimension, then the first term is close to 1 and the second term is close to 0, resulting in t̂i(x) ≈ 1. Lemma B.1. If x ∈ [ai, bi], then the following is true:
1. t(µ(x+ 0.5 − ai)) ∈ (1− θ, 1].
2. t(µ(x− 0.5 − bi)) ∈ [0, θ).
Proof. STATEMENT (1): Because x > ai, x+0.5 −ai > 0.5 . From Lem. 6.1, t(µ(x+0.5 −ai)) ∈ (1− θ, 1].
STATEMENT (2): Because x 6 bi, x−0.5 −bi 6 −0.5 . From Lem. 6.1, t(µ(x−0.5 −bi)) ∈ [0, θ).
The next two lemmas state that if x is outside the neighborhood, then the two terms are similar, resulting in a t̂i(x) ≈ 0. Lemma B.2. If x 6 ai − , then the following is true:
1. t(µ(x+ 0.5 − ai)) ∈ [0, θ).
2. t(µ(x− 0.5 − bi)) ∈ [0, θ).
Proof. STATEMENT (1): Because x 6 ai − , x + 0.5 − ai 6 −0.5 . From Lem. 6.1, t(µ(x + 0.5 − ai)) ∈ [0, θ).
STATEMENT (2): Because x 6 ai − and ai < bi, x 6 bi − . Then x − 0.5 − bi 6 −0.5 . From Lem. 6.1, t(µ(x− 0.5 − bi)) ∈ [0, θ).
Lemma B.3. If x > bi + , then the following is true:
1. t(µ(x+ 0.5 − ai)) ∈ (1− θ, 1].
2. t(µ(x− 0.5 − bi)) ∈ (1− θ, 1].
Proof. STATEMENT (1): Because x > bi + and bi > ai, x > ai + . Then x+ 0.5 − ai > 0.5 . From Lem. 6.1, t(µ(x+ 0.5 − ai)) ∈ (1− θ, 1].
STATEMENT (2): Because x > bi + , x− 0.5 − bi > 0.5 . From Lem. 6.1, t(µ(x− 0.5 − bi)) ∈ (1− θ, 1].
B.3.1 ABSTRACT PRECISION OF t̂i
We are now ready to prove properties about the abstract interpretation of our 1-dimensional indicator approximation, t̂i. The following lemma states that the abstract interpretation of t̂i, t̂ # i (B), is quite precise: if the 1-dimensional input box B is outside the neighborhood of G, on G’s ith dimension, then the output box is within θ from 0; if the input box B is within the ith dimension of G, then the output box is within 2θ from 1.
Lemma B.4 (Abstract interpretation of t̂i). For a 1-dimensional box B, the following is true:
1. t̂#i (B) ⊂ (−∞, 1].
2. If B ⊆ (−∞, ai − ] or B ⊆ [bi + ,∞), then t̂#i (B) ⊆ (−θ, θ).
3. If B ⊆ [ai, bi], then t̂#i (B) ⊆ (1− 2θ, 1] .
Proof. We begin the proof by simplifying the expression t̂#i (B). Recall that t̂(x) = t(µ(x+ 0.5 − ai)) − t(µ(x − 0.5 − bi)). Let B = [a, b]. By applying abstract transformer t# (Def. 3.6) and subtracting the two terms, we get t̂#i (B) = [T1 − T4, T2 − T3], where
T1 = t(µ(a+ 0.5 − ai)) T2 = t(µ(b+ 0.5 − ai)) T3 = t(µ(a− 0.5 − bi)) T4 = t(µ(b− 0.5 − bi))
We are now ready to prove the three statements.
STATEMENT (1): By the definition of t, ∀x. t(x) ∈ [0, 1], so T1, T2, T3, T4 ∈ [0, 1]. Therefore, the upper bound of t̂#(B) is T2 − T3 6 1.

heading: STATEMENT (2):
text: Case 1: B ⊆ (−∞, ai − ]. From Lem. B.2, T1, T2, T3, T4 ∈ [0, θ), then T2 − T3 < θ, and T1 − T4 > −θ. Case 2: B ⊆ [bi + ,∞). From Lem. B.3, T1, T2, T3, T4 ∈ (1 − θ, 1], then T2 − T3 < θ, and T1 − T4 > −θ.
In either case, t̂#i (B) ⊆ (−θ, θ).
STATEMENT (3): If B ⊆ [ai, bi], a, b ∈ [ai, bi]. From Lem. B.1(1), T1, T2 ∈ (1 − θ, 1]. From Lem. B.1(2), T3, T4 ∈ [0, θ). Then T1 − T4 > 1− 2θ and T2 − T3 6 1.
Therefore, t̂#i (B) ⊆ (1− 2θ, 1].

heading: B.4 ABSTRACT PRECISION OF NG
text: We are now ready to analyze the abstract precision of NG. We first consider Hi in the following lemma. For any box B ⊆ C, let Bi be its projection on dimension i, which is an interval.
The following lemma states that if B is in the box G, then ∑ iH # i is positive; otherwise, if B is
outside the neighborhood of G, then ∑ iH # i is negative. Lemma B.5 (Abstract interpretation of Hi). For any box B ⊆ C, the following is true:
1. If B ⊆ G, then ∑m i=1H # i (Bi) ⊆ (0,∞).
2. If B ⊆ C \ ν(G), then ∑m i=1H # i (Bi) ⊆ (−∞,− ).
Proof. STATEMENT (1): If B ⊆ G, then ∀i. Bi ⊆ [ai, bi]. From Lem. B.4 (3), t̂#i (Bi) ⊆ (1−2θ, 1]; thus,
H#i (Bi) = t̂ # i (Bi) + # −(1− 2θ)# ⊆ (0, 2θ] ⊂ (0,∞)
Sum over all m dimensions, ∑m i=1H # i (Bi) ⊆ ∑m i=1(0,∞) = (0,∞).
STATEMENT (2): If B ⊆ C \ ν(G), then there is a dimension j such that either Bj ⊆ (−∞, aj − ] or Bj ⊆ [bj + ,∞). From Lem. B.4 (2), we know that t̂#(Bj) ⊆ (−θ, θ). Therefore,
H#j (Bj) = t̂ #(Bj) + # −(1− 2θ)# ⊆ (θ − 1, 3θ − 1) (5)
For the remaining m − 1 dimensions, from Lem. B.4 (1), we know that t̂#(Bi) ⊂ (−∞, 1] when i 6= j. Therefore,
H#i (Bi) = t̂ #(Bi) + # −(1− 2θ)# ⊆ (−∞, 2θ] (6)
Take the sum of all the m− 1 dimensions,∑ i∈{1,...,m}\{j}H # i (Bi) ⊆ ∑ i∈{1,...,m}\{j}(−∞, 2θ] (substitute Eq. (6))
= [m− 1,m− 1] ∗# (−∞, 2θ] (turn sum into ∗#) = (−∞, 2(m− 1)θ] (apply ∗#)
(7)
Now, take sum over all the m dimensions,∑m i=1H # i (Bi) = ∑ i∈{1,...,m}\{j}H # i (Bi) +
# H#j (Bj) (decompose sum) ⊆ (−∞, 2(m− 1)θ] +# (θ − 1, 3θ − 1) (substitute Eqs. (5) and (7)) = (−∞, (2m+ 1)θ − 1) (apply ∗#)
Because of our choice of θ, θ 6 14m+2 (see Appendix B.2). Then (2m + 1)θ 6 2m+1 4m+2 = 0.5, and therefore m∑ i=1 H#i (Bi) ⊆ (−∞,−0.5)
Also we have assumed that < 0.5 (see Appendix B.2); therefore m∑ i=1 H#i (Bi) ⊆ (−∞,− )
B.4.1 PROOF OF THM. 6.2

heading: Proof.
text: 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 0 and 1. Therefore, N#G (B) ⊆ [0, 1].
STATEMENT (2): If B ⊆ G, from Lem. B.5, we know that ∑m i=1H # i (Bi) ⊆ (0,∞). Then,
m∑ i H#i (Bi) + # (0.5 )# ⊆ (0,∞) +# (0.5 )# ⊆ (0.5 ,∞)
From Lem. 6.1, we know that if x > 0.5 , then 1− θ < t(µx) 6 1. Therefore,
N#G (B) = t #(µ# ∗# (0.5 ,∞)) ⊆ (1− θ, 1]
STATEMENT (3): If B ⊆ C \ ν(G), from Lem. B.5, we know that ∑m i=1H # i (Bi) ⊆ (−∞,− ). Then, ∑m i=1H # i (Bi) + # (0.5 )# ⊆ (−∞,− ) +# (0.5 )# ⊆ (−∞,−0.5 )
From Lem. 6.1, we know that if x 6 −0.5 , then 0 6 t(µx) < θ. Therefore,
N#G (B) = t #(µ# ∗# (−∞,−0.5 )) ⊆ [0, θ)
B.5 ABSTRACT INTERPRETATION OF Ni
Observe how for any box B ⊆ C from the abstract domain, it is overapproximated by a larger box G ⊇ B from the finitely many boxes in the -grid. Intuitively, our abstract approximation of Ni incurs an error 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 a box B ⊆ C, if B ∈ G, then B’s neighborhood GB = ν(B); otherwise, let GB be the smallest G ∈ G, by volume, such that B ⊆ G. Note that GB is uniquely defined.
The following lemma says that considering the neighborhood of B only adds up to τ of imprecision to the collecting semantics of f .
Lemma B.6 (Properties of GB). The following is true:
1. If f(B) > β, then f(GB) > β − τ .
2. If f(B) 6 β, then f(GB) 6 β + τ .
Proof. Both of the statements follow from our choice of in constructing the grid (see Appendix B.2). If ‖x− x‖∞ 6 , then |f(x)− f(y)| < τ . Consider the B and its neighborhood GB . By definition of neighborhood, ∀x ∈ GB , ∃y ∈ B, such that ‖x− y‖∞ 6 .
STATEMENT (1) Because f(B) > β, then f(y) > β, so f(x) > f(y)− τ > β− τ . Then ∀x ∈ GB , f(x) > β − τ .
STATEMENT (2) Because f(B) 6 β, then f(y) 6 β, so f(x) 6 f(y)+ τ 6 β+ τ . Then ∀x ∈ GB , f(x) 6 β + τ .
Theorem B.7 (Abstract interpretation of Ni). For any box B ⊆ C, let u = max f(B), and l = min f(B). The following is true:
1. N#i (B) ⊆ [0, 1].
2. If l > (i+ 2)τ , then ∃ui ∈ (1− θ, 1] such that [ui, ui] ⊆ N#i (B) ⊆ (1− θ, 1].
3. If u 6 (i− 1)τ , then ∃li ∈ [0, θ) such that [li, li] ⊆ N#i (B) ⊆ [0, θ).
Proof. We begin by noting that in Statement (2), [ui, ui] ⊆ N#i (B) for some ui ∈ (1 − θ, 1] is a direct corollary of N#i (B) ⊆ (1 − θ, 1]. Because if N # i (B) ⊆ (1 − θ, 1], and N # i (B) 6= ∅, then N#i (B) contains at least one point in (1 − θ, 1]. Similarly, in Statement (3), [li, li] ⊆ N # i (B) for some li ∈ [0, θ) is a direct corollary of N#i (B) ⊆ [0, θ).
In Appendix B.2, we have chosen that θ 6 14|G| , a fact we will use later in the proof.
STATEMENT (1): The outer function of Ni is t, whose range is [0, 1], by the definition of squashable function and our construction, so N#i (B) ⊆ [0, 1].
STATEMENT (2): Because f(B) > (i+ 2)τ , by Lem. B.6, f(GB) > (i+ 1)τ , so GB ∈ Gi. Thus, we can break up the sum as follows:
∑ G∈Gi NG(x) =  ∑ G∈(Gi\{GB}) NG(x) +NGB (x) From Thm. 6.2, N#GB (B) ⊆ (1− θ, 1], and N # G (B) ⊆ [0, 1] for G ∈ Gi \ {GB}. Therefore, we can conclude the following two facts:∑ G∈Gi N#G (B) ⊆ (1−θ,∞) and ∑ G∈Gi N#G (B)+ #[−0.5,−0.5] ⊆ (0.5− θ,∞) ⊂ (0.5 ,∞)
The second inequality follows from the fact that we assumed θ 6 14|G| 6 0.25 (above) and < 0.5 (see Appendix B.2). Therefore, 0.5− θ > 0.25 > 0.5 . It follows from Lem. 6.1 that
N#i (B) = t #
( µ# ∗# (∑ G∈Gi N#G (B) + # [−0.5,−0.5] )) ⊆ (1− θ, 1]
STATEMENT (3): If u 6 (i− 1)τ , we will show that ∀G ∈ Gi. B ⊂ C \ ν(G).
Pick any G ∈ Gi, then we have f(G) > (i+ 1)τ . Thus, from Lem. B.6, f(GB) > iτ . Recall that if B ∈ G, then GB = ν(B). Hence, f(ν(G)) > iτ . However, f(B) 6 u 6 (i−1)τ , so B∩ν(G) = ∅. Equivalently, B ⊂ C \ ν(G).
From Thm. 6.2, ∀G ∈ Gi. N#G (B) ⊆ [0, θ), so∑ G∈Gi N#G (B) ⊆ [0, |Gi|θ) ⊆ [0, |G|θ)
We assumed that θ 6 14|G| and < 0.5 (see Appendix B.2), so |G|θ 6 0.25, and |G|θ − 0.5 6 −0.25 6 −0.5 . Hence,∑ G∈Gi N#G (B) ⊆ [0, 0.25) and ∑ G∈Gi N#G (B)+ #[−0.5,−0.5] ⊆ [−0.5,−0.25) ⊆ (−∞,−0.5 )
It follows from Lem. 6.1 that
N#i (B) = t #
( µ# ∗# (∑ G∈Gi N#G (B) + # [−0.5,−0.5] )) ⊆ [0, θ)

heading: B.6 ABSTRACT INTERPRETATION OF N
text: 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, θ 6 1K+1 .
Lemma B.8. If η0, . . . , ηK ∈ [−θ, θ], then ∑K i=0 ηi ∈ [−1, 1].
Proof. This simply follow from the choice of θ 6 1K+1 .
Proof outline of Thm. 4.2. Our proof involves three pieces, outlined below:
(A) Because N#(B) = τ# ∗# ∑K i=0N # i (B), we need only analyze ∑K i=0N # i (B). We will
decompose the sum into five sums and analyze each separately, arriving at five results of the form: [
L̃1j , Ũ1j ] ⊆ ∑ i∈Sj N#i (B) ⊆ [ L̃2j , Ũ2j ] for j ∈ {1, . . . , 5}, where ⋃ j Sj = {0, . . . ,K} and Sj are mutually disjoint sets.
(B) Then, we sum over all five cases, getting 5∑ j=1 L̃1j , 5∑ j=1 Ũ1j  ⊆ K∑ i=0 N#i (B) ⊆  5∑ j=1 L̃2j , 5∑ j=1 Ũ2j  (C) LetLi = τ ∑5 j=1 L̃ij andUi = τ ∑5 j=1 Ũij . Then, we get the bound [L1, U1] ⊆ N#(B) ⊆
[L2, U2]. Finally, we show that [L2, U2] ⊆ [l − δ, u+ δ] and [l + δ, u− δ] ⊆ [L1, U1]. Equivalently, we will show that
l − δ 6 L2 6 L1 6 l + δ and u− δ 6 U1 6 U2 6 u+ δ
Proof assumptions. We will assume that l ∈ [pτ, (p + 1)τ) and u ∈ [qτ, (q + 1)τ), for some p 6 q 6 K. Additionally, let c, d ∈ B be such that f(c) = l and f(d) = u. Step A: Decompose sum and analyze separately. We begin by decomposing the sum into five terms.
This is the most important step of the proof. We want to show that most Ni’s in ∑K i=0N # i (B) are (almost) precise. By almost we mean that their values are ≈ 1 and ≈ 0. The motivation is then to extract as many precise terms as possible. The only tool used in the analysis is Thm. B.7.
• Consider the function slices represented by Term 1 and 5; for example, Term 1 represents abstractions N#i of function slices fi, for i ∈ [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#i (B) and the collecting semantics of fi(B) agree. For Term 1, the abstract interpretation of all N # i (B) ≈ [1, 1] and fi(B) =
[τ, τ ]. For Term 5, the abstract interpretation of all N#i (B) ≈ [0, 0] and fi(B) = [0, 0]. • Now consider function slices fi, where i ∈ [p+ 2, q − 2]. The abstraction of these function
slices is also (almost) precise. We can see f(c) = l is below the lower bound of the slices and f(d) = u is above the upper bound of the slices. Hence, fi(d) = τ and N # i ({d}) ≈ [1, 1]. Similarly, fi(c) = 0 and N # i ({c}) ≈ [0, 0]. Because c, d ∈ B, and due to continuity of f , we have fi(B) = [0, 1], and N # i (B) ≈ [0, 1].
• The remaining function slices are those in Term 2 and Term 4, and they are at the neighborhood of the boundary of [l, u]. Most precision loss of N#i (B) comes from those two terms.
This drives us to decompose the sum as follows: K∑ i=0 N#i (B) = p−2∑ i=0
N#i (B)︸ ︷︷ ︸ Term 1
+# p+1∑ i=p−1
N#i (B)︸ ︷︷ ︸ Term 2
+# q−2∑ i=p+2
N#i (B)︸ ︷︷ ︸ Term 3
+# q+1∑ i=q−1
N#i (B)︸ ︷︷ ︸ Term 4
+# K∑
i=q+2 N#i (B)︸ ︷︷ ︸ Term 5
(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 > p+ 3; the q 6 p+ 2 case will follow easily.
(i) Term 1: ∀i 6 p− 2, we have pτ > (i+2)τ . Because l = min f(B) and l ∈ [pτ, (p+1)τ), then f(B) > pτ > (i+ 2)τ .
From Thm. B.7, ∃ui ∈ (1 − θ, 1] such that [ui, ui] ⊆ N#i (B) ⊆ (1 − θ, 1]. Then∑p−2 i=0 [ui, ui] ⊆ ∑p−2 i=0 N # i (B) ⊆ ∑p−2 i=0 (1− θ, 1].
p−2∑ i=0 [ui, ui] ⊆ p−2∑ i=0 N#i (B) ⊆ (p− 1) # ∗# (1− θ, 1]
(ii) Term 5: ∀i > q + 2, we have (q + 1)τ 6 (i − 1)τ . Because u = max f(B) and u ∈ [qτ, (q + 1)τ), then f(B) < (q + 1)τ 6 (i− 1)τ . From Thm. B.7, ∃li ∈ [0, θ) such that [li, li] ⊆ N#i (B) ⊆ [0, θ). Then ∑K i=q+2[li, li] ⊆∑K
i=q+2N # i (B) ⊆ ∑K i=q+2[0, θ).
K∑ i=q+2 [li, li] ⊆ K∑ i=q+2 N#i (B) ⊆ (K − q − 1) # ∗# [0, θ)
(iii) Term 3: ∀i ∈ [p+ 2, q − 2], we have (p+ 1)τ 6 (i− 1)τ and qτ > (i+ 2)τ . f(c) = l < (p+ 1)τ 6 (i− 1)τ , and f(d) = u > qτ > (i+ 2)τ . From Thm. B.7, N#i ({c}) ⊆ [0, θ) and N # i ({d}) ⊆ (1 − θ, 1]. Because c, d ∈ B,
[θ, 1− θ] ⊆ N#i (B). Also by Thm. B.7, N#i (B) ⊆ [0, 1]. Hence, ∑q−2 i=p+2[θ, 1 − θ] ⊆ ∑q−2 i=p+2N
# i (B) ⊆∑q−2
i=p+2[0, 1].
q−2∑ i=p+2 [θ, 1− θ] ⊆ q−2∑ i=p+2 N#i (B) ⊆ (q − p− 3) # ∗# [0, 1]
(iv) Term 2: ∀i ∈ [p− 1, p+ 1], since we have assumed that q > p+ 3, then q > p+ 3 > i+ 2.
Because f(d) > qτ > (i + 2)τ , from Thm. B.7, ∃ui ∈ (1 − θ, 1] such that [ui, ui] ⊆ N#i ({d}) ⊆ (1− θ, 1]. Because d ∈ B, [ui, ui] ⊆ N#i (B). Hence, [ui, ui] ⊆ N
# i (B) ⊆ [0, 1] and∑p+1 i=p−1[ui, ui] ⊆ ∑p+1 i=p−1N # i (B) ⊆ ∑p+1 i=p−1[0, 1].
p+1∑ i=p−1 [ui, ui] ⊆ p+1∑ i=p−1 N#i (B) ⊆ 3 # ∗# [0, 1]
(v) Term 4: For ∀q − 1 6 i 6 q + 1, because q > p + 3, we have p + 1 6 q − 2 6 i − 1. Then f(c) = l < (p + 1)τ 6 (i − 1)τ . From Thm. B.7, ∃li ∈ [0, θ) such that [li, li] ⊆ N#i ({c}) ⊆ [0, θ). Because c ∈ B, [li, li] ⊆ N#i (B). Thus, [li, li] ⊆ N # i (B) ⊆ [0, 1].
q+1∑ i=q−1 [li, li] ⊆ q+1∑ i=q−1 N#i (B) ⊆ 3 # ∗# [0, 1]
Step B: Sum all five cases. We now sum up all five inequalities we derived above to derive an overall bound of the sum in the form [L′1, U ′ 1] ⊆ ∑K i=0N # i (B) ⊆ [L′2, U ′2]. For example,
L′1 = p−2∑ i=0 ui + K∑ i=q+2 li + q−2∑ i=p+2 θ + p+1∑ i=p−1 ui + q+1∑ i=q−1 li
Recall that, by Thm. B.7, ∀i ∈ {0, . . . ,K}, ui ∈ (1 − θ, 1] and li ∈ [0, θ). Let l̃i = 1 − ui, so l̃i ∈ [0, θ). We simplify L′1, L ′ 2, U ′ 1 and U ′ 2 as follows:
L′1 = ∑p−2 i=0 ui + ∑K i=q+2 li + ∑q−2 i=p+2 θ + ∑p+1 i=p−1 ui + ∑q+1 i=q−1 li
(sum of the left bound) = ∑p−2 i=0 (1− l̃i) + ∑K i=q+2 li + ∑q−2 i=p+2 θ + ∑p+1 i=p−1(1− l̃i) + ∑q+1 i=q−1 li (substitute ui with l̃i) = ( ∑p−2 i=0 + ∑p+1 i=p−1)(1) + ∑p−2 i=0 (−l̃i) + ∑K i=q+2 li + ∑q−2 i=p+2 θ + ∑p+1 i=p−1(−l̃i) + ∑q+1 i=q−1 li (Rearrange the terms) = (p+ 2) + ∑p+1 i=0 (−l̃i) + ∑K i=q−1 li + ∑q−2 i=p+2 θ
(Sum all the 1’s)
From Lem. B.8, ∑p+1 i=0 (−l̃i) + ∑q−2 i=p+2 θ + ∑K i=q−1 li ∈ [1, 1] by plugging in −l̃i, li, θ to ηi. So,
L′1 ∈ [p+ 1, p+ 3]
U ′1 = ∑p−2 i=0 ui + ∑K i=q+2 li + ∑q−2 i=p+2(1− θ) + ∑p+1 i=p−1 ui + ∑q+1 i=q−1 li (sum of right bound)
= ∑p−2 i=0 (1− l̃i) + ∑K i=q+2 li + ∑q−2 i=p+2(1− θ) + ∑p+1 i=p−1(1− l̃i) + ∑q+1 i=q−1 li (substitute ui with l̃i)
= (q − 1) + ∑p+1 i=0 (−l̃i) + ∑K i=q−1 li + ∑q−2 i=p+2(−θ) (sum all the 1’s)
From Lem. B.8, ∑p+2 i=0 (−l̃i) + ∑q−2 i=p+2(−θ) + ∑K i=q−1 li ∈ [−1, 1]. Thus,
U ′1 ∈ [q − 2, q]
L′2 = (p− 1)(1− θ) (sum of left bound) = (p− 1) + (p− 1)(−θ) (rearrange terms)
Because θ 6 1K+1 , and −K 6 p− 1 6 K, we have (p− 1)(−θ) ∈ [−1, 1]. Hence,
L′2 ∈ [p− 2, p]

heading: U ′2 = (p− 1) + (K − q − 1)θ + (q − p− 3) + 3 + 3 (sum of right bound)
text: = (p− 1 + q − p− 3 + 3 + 3) + (K − q − 1)(θ) (rearrange terms) = q + 2 + (K − q − 1)(θ) (sum all the 1’s)
Because θ 6 1K+1 , and −K 6 (K − q − 1) 6 K, we have (K − q + 1)(−θ) ∈ [−1, 1]. Then,
U ′2 ∈ [q + 1, q + 3]
Step C: Analyze the bound. It remains to show that l − δ 6 L2 6 L1 6 l + δ and u− δ 6 U1 6 U2 6 u+ δ.
Recall that we have set that δ = 3τ . Also l ∈ [pτ, (p+ 1)τ), then
l − δ < (p− 2)τ and l + δ > (p+ 3)τ
Since u ∈ [qτ, (q + 1)τ), then
u− δ < (q − 2)τ and u+ δ > (q + 3)τ
We have just analyzed L′1, L ′ 2, U ′ 1 and U ′ 2 above. Now we have:
L1 = τL ′ 1 6 (p+ 3)τ L2 = τL ′ 2 > (p− 2)τ
U1 = τU ′ 1 > (q − 2)τ U2 = τU ′2 6 (q + 3)τ
It follows from the above inequalities that
l − δ < (p− 2)τ 6 L2 6 L1 6 (p+ 3)τ 6 l + δ
and u− δ < (q − 2)τ 6 U1 6 U2 6 (q + 3)τ 6 u+ δ
This concludes the proof for the case where q > p+ 3.
Excluded case. Previously, we have shown that Terms 1, 3, and 5 are almost precise. The imprecise terms can only come from Terms 2 and 4. If q 6 p+ 2, the only analyses that will be affected are those of Terms 2 and 4. Since q 6 p+ 2, we have p+ 1 > q − 1, which means Terms 2 and 4 have potentially less sub-terms in this case. Thus imprecise terms are less than the q > p+ 3 case and we can apply the same analysis as above and derive the same bound.
We have thus shown that the neural network N that we construct δ-abstractly approximates f , and therefore the AUA theorem is true.

Review summaries:
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.  

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).

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.