Certified Neural Approximations of Nonlinear Dynamics

TL;DR

This paper introduces a novel verification method for neural network approximations of nonlinear dynamical systems, providing formal error bounds to ensure safe application in critical systems, and demonstrating scalability and versatility on various benchmarks.

Contribution

The paper presents a new adaptive, parallelizable verification approach that offers formal error bounds for neural approximations of dynamical systems, enabling their safe use in critical applications.

Findings

Outperforms state-of-the-art verification methods

Successfully addresses neural network compression scenarios

Effectively applies to Koopman operator-based trajectory prediction

Abstract

Neural networks hold great potential to act as approximate models of nonlinear dynamical systems, with the resulting neural approximations enabling verification and control of such systems. However, in safety-critical contexts, the use of neural approximations requires formal bounds on their closeness to the underlying system. To address this fundamental challenge, we propose a novel, adaptive, and parallelizable verification method based on certified first-order models. Our approach provides formal error bounds on the neural approximations of dynamical systems, allowing them to be safely employed as surrogates by interpreting the error bound as bounded disturbances acting on the approximated dynamics. We demonstrate the effectiveness and scalability of our method on a range of established benchmarks from the literature, showing that it significantly outperforms the state-of-the-art. Furthermore, we show that our framework can successfully address additional scenarios previously intractable for existing methods - neural network compression and an autoencoder-based deep learning architecture for learning Koopman operators for the purpose of trajectory prediction.