Neural Abstractions

TL;DR

This paper introduces a novel neural network-based abstraction method for verifying the safety of nonlinear dynamical systems, providing formal guarantees and compatibility with existing verification tools.

Contribution

It is the first to use neural networks as formal abstractions for nonlinear models, enabling safety verification via neural ODEs and hybrid automata.

Findings

Produces tight, certified overapproximations of dynamics

Guarantees safety transfer from abstract to concrete models

Effective on non-Lipschitz models, outperforming existing tools

Abstract

We present a novel method for the safety verification of nonlinear dynamical models that uses neural networks to represent abstractions of their dynamics. Neural networks have extensively been used before as approximators; in this work, we make a step further and use them for the first time as abstractions. For a given dynamical model, our method synthesises a neural network that overapproximates its dynamics by ensuring an arbitrarily tight, formally certified bound on the approximation error. For this purpose, we employ a counterexample-guided inductive synthesis procedure. We show that this produces a neural ODE with non-deterministic disturbances that constitutes a formal abstraction of the concrete model under analysis. This guarantees a fundamental property: if the abstract model is safe, i.e., free from any initialised trajectory that reaches an undesirable state, then the concrete model is also safe. By using neural ODEs with ReLU activation functions as abstractions, we cast the safety verification problem for nonlinear dynamical models into that of hybrid automata with affine dynamics, which we verify using SpaceEx. We demonstrate that our approach performs comparably to the mature tool Flow* on existing benchmark nonlinear models. We additionally demonstrate and that it is effective on models that do not exhibit local Lipschitz continuity, which are out of reach to the existing technologies.