New paper! What if you could guarantee (using a mix of formal verification and PDE theory) that a neural network would *always* give you the correct answer, even when making inferences arbitrarily far away from the training data? Introducing BEACONS. arXiv link below. (1/15)

Back in the 90s, excellent work was done by Mhaskar, Pinkus and others on *quantitative* versions of the fêted Universal Approximation Theorems for neural networks: how accurately can a shallow neural network with N hidden neurons approximate a d-dimensional function? (3/15)

But these worst-case error bounds all depend crucially on the smoothness of the function being approximated (i.e. worst-case error scales like N^(-n/d), where n is the number of continuous derivatives the function has). Which presents a major problem for extrapolation. (4/15)

How can we ever know anything about the smoothness of a function, outside of the subdomain on which we've trained? This is the essential reason why one cannot bound errors on neural network approximations of functions far from the convex hull of the training data. (5/15)

But with BEACONS - Bounded-Error, Algebraically-COmposable Neural Solvers - we exploit the fact that the function we're learning is not arbitrary, but rather is the solution to a PDE (or system of PDEs). So we can apply techniques like the method of characteristics... (6/15)

...or elliptic regularity theorems to predict *a priori* how many continuous derivatives must exist, anywhere in space or time, even arbitrarily far from the training domain, by exploiting the analytical structure of the PDEs themselves. Hence, the "Bounded-Error" part. (7/15)

But such rigorous bounds are only provable for shallow neural networks (with a single hidden layer). What if we want to construct a deeper, more expressive architecture? That's where the "Algebraically-Composable" part comes in. Using ideas from applied category theory... (8/15)

...we show how it is possible to construct deeper BEACONS architectures as compositions of shallower ones, in such a way that the error bounds remain tightly controlled. Specifically, we "factorize" our complicated PDE solution into a composition of simpler functions... (9/15)

...in such a way that the large bounds on the errors for discontinuous parts of the solution are arbitrarily suppressed by small bounds on the errors for smooth, slowly-varying parts of the solution, effectively generalizing the theory of nonlinear flux limiters. (10/15)

Just specify the equations you want to solve, plus the neural network hyperparameters to solve them with, and our framework automatically generates highly optimized C code for training and validating a BEACONS architecture for those equations, and inferring new solutions. (12/15)

Simultaneously, it generates formal proofs of correctness for the underlying classical solver, as well as for the bootstrapped neural network-based solver, with rigorous extrapolatory bounds on the worst case L^infinity errors for both smooth and non-smooth solutions. (13/15)

These proofs are represented as symbolic Racket code, and hence are fully executable (and therefore machine-checkable). For a variety of both linear and non-linear equations systems, we find that BEACONS architectures dramatically outperform traditional neural networks. (14/15)

The goal is to raise the overall level of mathematical rigor underlying scientific ML, placing neural network-based methods on an equal footing with classical numerical methods, and guaranteeing properties like conservation, convergence, stability, and correctness. (15/15)