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$激活函数的神经网络获得，由此生成的神经常微分方程模型具有分段仿射动力学，并可等价解释为线性混合自动机。在本工作中，我们观察到抽象的效用取决于其用途：某些场景可能需要易于分析的粗粒度抽象，而其他场景则可能需要更复杂的精细化抽象。因此，我们考虑替代形状的神经抽象，即分段常数或非线性非多项式（具体而言，通过sigmoidal激活获得）。我们采用形式化归纳合成程序来生成具有这些语义的动力学模型的神经抽象。通过实验，我们展示了这些不同神经抽象模板在精度与合成时间，以及安全验证所需时间（通过可达性计算完成）方面的权衡。我们改进了现有合成技术以实现更高维模型的抽象，并额外讨论了复杂神经常微分方程的抽象以提高这些模型可达性分析的效率。