To verify safety and robustness of neural networks, researchers have successfully applied \emph{abstract interpretation}, primarily using the interval abstract domain. In this paper, we study the theoretical \emph{power and limits} of the interval domain for neural-network verification.

First, we introduce the \emph{interval universal approximation} (IUA) theorem. IUA shows that neural networks not only can approximate any continuous function $f$ (universal approximation) as we have known for decades, \emph{but} we can find a neural network, using any well-behaved activation function, whose interval bounds are an arbitrarily close approximation of the set semantics of $f$ (the result of applying $f$ to a set of inputs). We call this notion of approximation \emph{interval approximation}. Our theorem generalizes the recent result of Baader et al. [2020] from ReLUs to a rich class of activation functions that we call \emph{squashable functions}. Additionally, the IUA theorem implies that we can always construct provably robust neural networks under $\ell_\infty$-norm using almost any practical activation function.

Second, we study the computational complexity of constructing neural networks that are amenable to precise interval analysis. This is a crucial question, as our constructive proof of IUA is exponential in the size of the approximation domain. We boil this question down to the problem of approximating the range of a neural network with squashable activation functions. We show that the range approximation problem (RA) is a $\Delta_2$-intermediate problem, which is strictly harder than $\mathsf{NP}$-complete problems, assuming $\mathsf{coNP}\not\subset \mathsf{NP}$. As a result, \emph{IUA is an inherently hard problem}: No matter what abstract domain or computational tools we consider to achieve interval approximation, there is no efficient construction of such a universal approximator. This implies that it is hard to construct a provably robust network, even if we have a robust network to start with.

#### Thu 20 JanDisplayed time zone: Eastern Time (US & Canada) change

 10:20 - 12:00 Foundation and Verification of Machine-Learning SystemsPOPL at Salon I Chair(s): Gilbert Louis Bernstein University of California at Berkeley 10:2025mResearch paper A Dual Number Abstraction for Static Analysis of Clarke JacobiansInPersonPOPLJacob Laurel University of Illinois at Urbana-Champaign, Rem Yang University of Illinois at Urbana-Champaign, Gagandeep Singh University of Illinois at Urbana-Champaign; VMware, Sasa Misailovic University of Illinois at Urbana-Champaign DOI Media Attached 10:4525mResearch paper Provably Correct, Asymptotically Efficient, Higher-Order Reverse-Mode Automatic DifferentiationRemotePOPLFaustyna Krawiec University of Cambridge, Simon Peyton Jones Microsoft Research, Neel Krishnaswami University of Cambridge, Tom Ellis Microsoft Research, Richard A. Eisenberg Tweag, Andrew Fitzgibbon Graphcore DOI Media Attached 11:1025mResearch paper Interval Universal Approximation for Neural NetworksInPersonPOPLZi Wang University of Wisconsin-Madison, Aws Albarghouthi University of Wisconsin-Madison, Gautam Prakriya Chinese University of Hong Kong, Somesh Jha University of Wisconsin DOI Media Attached 11:3525mResearch paper PRIMA: General and Precise Neural Network Certification via Scalable Convex Hull ApproximationsInPersonPOPLMark Niklas Müller ETH Zurich, Gleb Makarchuk ETH Zurich, Gagandeep Singh University of Illinois at Urbana-Champaign; VMware, Markus Püschel ETH Zurich, Martin Vechev ETH Zurich DOI Media Attached