The rapid advance of deep reinforcement learning techniques enables the oversight of safety-critical systems through the utilization of Deep Neural Networks (DNNs). This underscores the pressing need to promptly establish certified safety guarantees for such DNN-controlled systems. Most of the existing verification approaches rely on qualitative approaches, predominantly employing reachability analysis. However, qualitative verification proves inadequate for DNN-controlled systems as their behaviors exhibit stochastic tendencies when operating in open and adversarial environments. In this paper, we propose a novel framework for unifying both qualitative and quantitative safety verification problems of DNN-controlled systems. This is achieved by formulating the verification tasks as the synthesis of valid neural barrier certificates (NBCs). Initially, the framework seeks to establish almost-sure safety guarantees through qualitative verification. In cases where qualitative verification fails, our quantitative verification method is invoked, yielding precise lower and upper bounds on probabilistic safety across both infinite and finite time horizons. To facilitate the synthesis of NBCs, we introduce their $k$-inductive variants. We also devise a simulation-guided approach for training NBCs, aiming to achieve tightness in computing precise certified lower and upper bounds. We prototype our approach into a tool called $\textsf{UniQQ}$ and showcase its efficacy on four classic DNN-controlled systems.

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