神经抽象在效率与精度之间的权衡

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