统一深度神经网络控制系统的定性与定量安全验证

深度强化学习技术的快速发展使得通过深度神经网络（DNN）来监控安全关键系统成为可能。这凸显了为此类DNN控制系统迅速建立认证安全保证的迫切需求。现有验证方法大多依赖定性方法，主要采用可达性分析。然而，定性验证对于DNN控制系统并不充分，因为它们在开放和对抗性环境中运行时表现出随机性。本文提出了一种新颖的框架，统一了DNN控制系统的定性和定量安全验证问题。这是通过将验证任务表述为有效神经屏障证书（NBC）的合成来实现的。首先，该框架旨在通过定性验证建立几乎确定的安全保证。在定性验证失败的情况下，调用我们的定量验证方法，在无限和有限时间范围内给出概率安全性的精确下界和上界。为了促进NBC的合成，我们引入了它们的$k$-归纳变体。我们还设计了一种模拟引导的方法来训练NBC，旨在实现计算精确认证上下界的紧致性。我们将我们的方法原型化为一个名为$\textsf{UniQQ}$的工具，并在四个经典的DNN控制系统上展示了其有效性。