Floating-Point Neural Networks Are Provably Robust Universal Approximators

TL;DR

This paper proves that floating-point neural networks can universally approximate functions with robustness guarantees, extending the theoretical understanding of their expressiveness beyond real-valued models.

Contribution

It establishes the first interval universal approximation theorem for floating-point neural networks, demonstrating their perfect ability to approximate rounded functions and their robustness.

Findings

Floating-point neural networks can exactly capture the direct image map of any rounded function.

The theorem implies the existence of provably robust floating-point neural networks.

It shows the computational completeness of floating-point straight-line programs.

Abstract

The classical universal approximation (UA) theorem for neural networks establishes mild conditions under which a feedforward neural network can approximate a continuous function $f$ with arbitrary accuracy. A recent result shows that neural networks also enjoy a more general interval universal approximation (IUA) theorem, in the sense that the abstract interpretation semantics of the network using the interval domain can approximate the direct image map of $f$ (i.e., the result of applying $f$ to a set of inputs) with arbitrary accuracy. These theorems, however, rest on the unrealistic assumption that the neural network computes over infinitely precise real numbers, whereas their software implementations in practice compute over finite-precision floating-point numbers. An open question is whether the IUA theorem still holds in the floating-point setting. This paper introduces the first IUA theorem for floating-point neural networks that proves their remarkable ability to perfectly capture the direct image map of any rounded target function $f$, showing no limits exist on their expressiveness. Our IUA theorem in the floating-point setting exhibits material differences from the real-valued setting, which reflects the fundamental distinctions between these two computational models. This theorem also implies surprising corollaries, which include (i) the existence of provably robust floating-point neural networks; and (ii) the computational completeness of the class of straight-line programs that use only floating-point additions and multiplications for the class of all floating-point programs that halt.