Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems
Dapeng Zhi, Peixin Wang, Si Liu, Luke Ong, Min Zhang
TL;DR
This paper addresses the challenge of providing safety guarantees for DNN-controlled systems under environmental uncertainty by unifying qualitative and quantitative verification through Neural Barrier Certificates (NBCs). It develops a framework that converts safety verification tasks into NBC synthesis, enabling almost-sure safety proofs and probabilistic safety bounds over both infinite and finite horizons; it introduces $k$-inductive BCs to ease synthesis and a simulation-guided training approach to tighten bounds. The authors formalize a broad set of results, including conditions for NBCs to certify qualitative safety and to compute linear and exponential bounds on safety probabilities, with proofs and supplementary materials. They implement the UniQQ toolkit and validate it on four classic DNN-controlled systems, showing that NBC-based verification can deliver reliable safety certificates and that $k$-induction and simulation guidance substantially reduce overhead and improve bound tightness. The work offers a scalable, multipurpose safety verification paradigm for DNN controllers, with potential impact on certifiable safety in real-world autonomous and robotic systems.
Abstract
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.