Neural abstractions have been recently introduced as formal approximations of complex, nonlinear dynamical models. They comprise a neural ODE and a certified upper bound on the error between the abstract neural network and the concrete dynamical model. So far neural abstractions have exclusively been obtained as neural networks consisting entirely of $ReLU$ activation functions, resulting in neural ODE models that have piecewise affine dynamics, and which can be equivalently interpreted as linear hybrid automata. In this work, we observe that the utility of an abstraction depends on its use: some scenarios might require coarse abstractions that are easier to analyse, whereas others might require more complex, refined abstractions. We therefore consider neural abstractions of alternative shapes, namely either piecewise constant or nonlinear non-polynomial (specifically, obtained via sigmoidal activations). We employ formal inductive synthesis procedures to generate neural abstractions that result in dynamical models with these semantics. Empirically, we demonstrate the trade-off that these different neural abstraction templates have vis-a-vis their precision and synthesis time, as well as the time required for their safety verification (done via reachability computation). We improve existing synthesis techniques to enable abstraction of higher-dimensional models, and additionally discuss the abstraction of complex neural ODEs to improve the efficiency of reachability analysis for these models.

翻译：神经抽象方法最近被引入作为复杂非线性动力学模型的形式化近似。该方法包含一个神经常微分方程，以及关于抽象神经网络与具体动力学模型之间误差的认证上界。迄今为止，神经抽象方法完全通过仅由ReLU激活函数构成的神经网络实现，从而产生具有分段仿射动力学的神经常微分方程模型，这些模型可等价解释为线性混合自动机。在本工作中，我们观察到抽象的有效性取决于其用途：某些场景可能需要易于分析的粗粒度抽象，而另一些场景则可能需要更复杂、更精细的抽象。因此，我们研究了替代形式的神经抽象，即分段常数型或非线性非多项式型（具体通过sigmoid激活函数获得）。我们采用形式化归纳合成程序来生成具有这些语义的动力学模型的神经抽象。通过实验，我们展示了这些不同神经抽象模板在精度、合成时间以及安全验证所需时间（通过可达性计算实现）之间的权衡关系。我们改进了现有合成技术，使其能够实现更高维度模型的抽象，并进一步讨论了复杂神经常微分方程的抽象方法，以提高这些模型的可达性分析效率。