Training neural networks to be certifiably robust is critical to ensure their safety against adversarial attacks. However, it is currently very difficult to train a neural network that is both accurate and certifiably robust. In this work we take a step towards addressing this challenge. We prove that for every continuous function $f$, there exists a network $n$ such that:
 (i) $n$ approximates $f$ arbitrarily close, and (ii) simple interval bound propagation of a region $B$ through $n$ yields a result that is arbitrarily close to the optimal output of $f$ on $B$. Our result can be seen as a Universal Approximation Theorem for interval-certified ReLU networks. To the best of our knowledge, this is the first work to prove the existence of accurate, interval-certified networks. Much recent work has shown that neural networks can be fooled into misclassifying adversarial examples (Szegedy et al., 2014) , inputs which are imperceptibly different from those that the neural network classifies correctly. Initial work on defending against adversarial examples revolved around training networks to be empirically robust, usually by including adversarial examples found with various attacks into the training dataset (Gu and Rigazio, 2015; Papernot et al., 2016; Zheng et al., 2016; Athalye et al., 2018; Eykholt et al., 2018; Moosavi-Dezfooli et al., 2017; Xiao et al., 2018) . However, while empirical robustness can be practically useful, it does not provide safety guarantees. As a result, much recent research has focused on verifying that a network is certifiably robust, typically by employing methods based on mixed integer linear programming (Tjeng et al., 2019) , SMT solvers (Katz et al., 2017) , semidefinite programming (Raghunathan et al., 2018a) , duality (Wong and Kolter, 2018; Dvijotham et al., 2018b) , and linear relaxations (Gehr et al., 2018; Weng et al., 2018; Wang et al., 2018b; Zhang et al., 2018; Singh et al., 2018; Salman et al., 2019) . Because the certification rates were far from satisfactory, specific training methods were recently developed which produce networks that are certifiably robust: Mirman et al. (2018) ; Raghunathan et al. (2018b) ; Wang et al. (2018a) ; Wong and Kolter (2018) ; Wong et al. (2018) ; Gowal et al. (2018) train the network with standard optimization applied to an over-approximation of the network behavior on a given input region (the region is created around the concrete input point). These techniques aim to discover specific weights which facilitate verification. There is a tradeoff between the degree of the over-approximation used and the speed of training and certification. Recently, (Cohen et al., 2019b) proposed a statistical approach to certification, which unlike the non-probabilistic methods discussed above, creates a probabilistic classifier that comes with probabilistic guarantees. So far, some of the best non-probabilistic results achieved on the popular MNIST (Lecun et al., 1998) and CIFAR10 (Krizhevsky, 2009 ) datasets have been obtained with the simple Interval relaxation (Gowal et al., 2018; Mirman et al., 2019) , which scales well at both training and verification time. Despite this progress, there are still substantial gaps between known standard accuracy, experimental robustness, and certified robustness. For example, for CIFAR10, the best reported certified robustness is 32.04% with an accuracy of 49.49% when using a fairly modest l ∞ region with radius 8/255 (Gowal et al., 2018) . The state-of-the-art non-robust accuracy for this dataset is > 95% with experimental robustness > 50%. Given the size of this gap, a key question then is: can certified training ever succeed or is there a fundamental limit? In this paper we take a step in answering this question by proving a result parallel to the Universal Approximation Theorem (Cybenko, 1989; Hornik et al., 1989) . We prove that for any continuous function f defined on a compact domain Γ ⊆ R m and for any desired level of accuracy δ, there exists a ReLU neural network n which can certifiably approximate f up to δ using interval bound propagation. As an interval is a fairly imprecise relaxation, our result directly applies to more precise convex relaxations (e.g., Zhang et al. (2018); Singh et al. (2019) ). Theorem 1.1 (Universal Interval-Certified Approximation, Figure 1 ). Let Γ ⊂ R m be a compact set and let f : Γ → R be a continuous function. For all δ > 0, there exists a ReLU network n such that for all boxes [a, b] in Γ defined by points a, b ∈ Γ where a k ≤ b k for all k, the propagation of the box [a, b] using interval analysis through the network n, denoted n ([a, b]), approximates the set We recover the classical universal approximation theorem (|f (x) − n(x)| ≤ δ for all x ∈ Γ) by considering boxes [a, b] describing points (x = a = b). Note that here the lower bound is not [l, u] as the network n is an approximation of f . Because interval analysis propagates boxes, the theorem naturally handles l ∞ norm bound perturbations to the input. Other l p norms can be handled by covering the l p ball with boxes. The theorem can be extended easily to functions f : Γ → R k by applying the theorem component wise. Practical meaning of theorem The practical meaning of this theorem is as follows: if we train a neural network n on a given training data set (e.g., CIFAR10) and we are satisfied with the properties of n (e.g., high accuracy), then because n is a continuous function, the theorem tells us that there exists a network n which is as accurate as n and as certifiable with interval analysis as n is with a complete verifier. This means that if we fail to find such an n, then either n did not possess the required capacity or the optimizer was unsuccessful. Focus on the existence of a network We note that we do not provide a method for training a certified ReLU network -even though our method is constructive, we aim to answer an existential question and thus we focus on proving that a given network exists. Interesting future work items would be to study the requirements on the size of this network and the inherent hardness of finding it with standard optimization methods. Universal approximation is insufficient We now discuss why classical universal approximation is insufficient for establishing our result. While classical universal approximation theorems state that neural networks can approximate a large class of functions f , unlike our result, they do not state that robustness of the approximation n of f is actually certified with a scalable proof method (e.g., interval bound propagation). If one uses a non scalable complete verifier instead, then the standard Universal approximation theorem is sufficient. To demonstrate this point, consider the function f : R → R (Figure 2b ) mapping all x ≤ 0 to 1, all x ≥ 1 to 0 and all 0 < x < 1 to 1 − x and two ReLU networks n 1 (Figure 2a ) and n 2 (Figure 2c ) perfectly approximating f , that is n 1 (x) = f (x) = n 2 (x) for all x. For δ = 1 4 , the interval certification that n 1 maps all However, interval certification succeeds for n 2 , because n 2 ([0, 1]) = [0, 1] . To the best of our knowledge, this is the first work to prove the existence of accurate, interval-certified networks. We proved that for all real valued continuous functions f on compact sets, there exists a ReLU network n approximating f arbitrarily well with the interval abstraction. This means that for arbitrary input sets, analysis using the interval relaxation yields an over-approximation arbitrarily close to the smallest interval containing all possible outputs. Our theorem affirmatively answers the open question, whether the Universal Approximation Theorem generalizes to Interval analysis. Our results address the question of whether the interval abstraction is expressive enough to analyse networks approximating interesting functions f . This is of practical importance because interval analysis is the most scalable non-trivial analysis.
We prove that for a large class of functions f there exists an interval certified robust network approximating f up to arbitrary precision.
{"src": "scitldr-AIC_train", "paper_id": "B1gX8kBtPr"}