Abstract
With growing concerns about the safety and robustness of neural networks, anumber of researchers have successfully applied abstract interpretation withnumerical domains to verify properties of neural networks. Why do numericaldomains work for neural-network verification? We present a theoretical resultthat demonstrates the power of numerical domains, namely, the simple intervaldomain, for analysis of neural networks. Our main theorem, which we call theabstract universal approximation (AUA) theorem, generalizes the recent resultby Baader et al. [2020] for ReLU networks to a rich class of neural networks.The classical universal approximation theorem says that, given function $f$,for any desired precision, there is a neural network that can approximate $f$.The AUA theorem states that for any function $f$, there exists a neural networkwhose abstract interpretation is an arbitrarily close approximation of thecollecting semantics of $f$. Further, the network may be constructed using anywell-behaved activation function---sigmoid, tanh, parametric ReLU, ELU, andmore---making our result quite general. The implication of the AUA theorem is that there exist provably correctneural networks: Suppose, for instance, that there is an ideal robust imageclassifier represented as function $f$. The AUA theorem tells us that thereexists a neural network that approximates $f$ and for which we canautomatically construct proofs of robustness using the interval abstractdomain. Our work sheds light on the existence of provably correct neuralnetworks, using arbitrary activation functions, and establishes intriguingconnections between well-known theoretical properties of neural networks andabstract interpretation using numerical domains.