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.

翻译：我们提出一种新颖的非线性动力学模型安全性验证方法，该方法利用神经网络表示其动力学的抽象表示。神经网络此前已被广泛用作近似器；在本工作中，我们更进一步，首次将其作为抽象表示使用。对于给定的动力学模型，我们的方法综合生成一个神经网络，通过确保逼近误差具有任意紧致的形式化认证界限，对模型的动力学进行过逼近。为此，我们采用反例引导的归纳综合程序。我们证明，该方法生成的带有非确定性扰动的神经ODE（常微分方程）构成了待分析具体模型的形式化抽象。这保证了一个基本性质：若抽象模型是安全的（即所有从初始状态出发的轨迹均不会到达不良状态），则具体模型也是安全的。通过使用带ReLU激活函数的神经ODE作为抽象表示，我们将非线性动力学模型的安全验证问题转化为仿射动力学的混合自动机验证问题，并利用SpaceEx工具进行验证。我们证明，该方法在现有基准非线性模型上可与成熟工具Flow*相媲美。此外，我们还证明其对于不存在局部Lipschitz连续性的模型（现有技术无法处理此类问题）同样有效。