# Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems

arXiv: https://arxiv.org/abs/2404.01769 · HTML: https://mlsanity.com/paper/2404.01769/

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- Placed in Safe and constrained RL, one of 15 directions in Deep reinforcement learning methods.
- Builds on 29 of its 71 references that are in the map.
- First posted on arXiv 2 Apr 2024.

## Placed in

- Deep reinforcement learning methods / [Safe and constrained RL](https://mlsanity.com/deeprl/safe-and-constrained-rl/)

## Builds on (most cited first, 29 of 29)

- [Continuous control with deep reinforcement learning](https://mlsanity.com/paper/1509.02971/) (2015)
- [Playing Atari with Deep Reinforcement Learning](https://mlsanity.com/paper/1312.5602/) (2013)
- [Safe Model-based Reinforcement Learning with Stability Guarantees](https://mlsanity.com/paper/1705.08551/) (2017)
- [Robust Deep Reinforcement Learning against Adversarial Perturbations on State Observations](https://mlsanity.com/paper/2003.08938/) (2020)
- [Safe Control with Learned Certificates: A Survey of Neural Lyapunov, Barrier, and Contraction methods](https://mlsanity.com/paper/2202.11762/) (2022)
- [Robust Reinforcement Learning on State Observations with Learned Optimal Adversary](https://mlsanity.com/paper/2101.08452/) (2021)
- [Reachability Analysis of Deep Neural Networks with Provable Guarantees](https://mlsanity.com/paper/1805.02242/) (2018)
- [The Probabilistic Model Checker Storm](https://mlsanity.com/paper/2002.07080/) (2020)
- [POLAR: A Polynomial Arithmetic Framework for Verifying Neural-Network Controlled Systems](https://mlsanity.com/paper/2106.13867/) (2021)
- [Towards Scalable Verification of Deep Reinforcement Learning](https://mlsanity.com/paper/2105.11931/) (2021)
- [Stability Verification in Stochastic Control Systems via Neural Network Supermartingales](https://mlsanity.com/paper/2112.09495/) (2021)
- [Learning Control Policies for Stochastic Systems with Reach-avoid Guarantees](https://mlsanity.com/paper/2210.05308/) (2022)
- [Safety Certification for Stochastic Systems via Neural Barrier Functions](https://mlsanity.com/paper/2206.01463/) (2022)
- [Probabilistic Guarantees for Safe Deep Reinforcement Learning](https://mlsanity.com/paper/2005.07073/) (2020)
- [Probabilistic Model Checking and Autonomy](https://mlsanity.com/paper/2111.10630/) (2021)
- [Reactive and Safe Road User Simulations using Neural Barrier Certificates](https://mlsanity.com/paper/2109.06689/) (2021)
- [Algorithmic Analysis of Qualitative and Quantitative Termination Problems for Affine Probabilistic Programs](https://mlsanity.com/paper/1510.08517/) (2015)
- [Verified Probabilistic Policies for Deep Reinforcement Learning](https://mlsanity.com/paper/2201.03698/) (2022)
- [Inner-Approximating Reachable Sets for Polynomial Systems with Time-Varying Uncertainties](https://mlsanity.com/paper/1811.01086/) (2018)
- [Reach-Avoid Analysis for Polynomial Stochastic Differential Equations](https://mlsanity.com/paper/2208.10752/) (2022)
- [Safety Verification and Refutation by k-invariants and k-induction (extended version)](https://mlsanity.com/paper/1506.05671/) (2015)
- [Categorical Liveness Checking by Corecursive Algebras](https://mlsanity.com/paper/1704.04872/) (2017)
- [Ranking and Repulsing Supermartingales for Reachability in Probabilistic Programs](https://mlsanity.com/paper/1805.10749/) (2018)
- [Lower Bounds for Possibly Divergent Probabilistic Programs](https://mlsanity.com/paper/2302.06082/) (2023)
- [Unbounded-Time Safety Verification of Stochastic Differential Dynamics](https://mlsanity.com/paper/2006.01858/) (2020)
- [Model Checking Temporal Properties of Recursive Probabilistic Programs](https://mlsanity.com/paper/2111.03501/) (2021)
- [Data-driven Safety Verification of Stochastic Systems via Barrier Certificates](https://mlsanity.com/paper/2112.12709/) (2021)
- [Safety Barrier Certificates for Stochastic Hybrid Systems](https://mlsanity.com/paper/2208.03478/) (2022)
- [A New Framework for Bounding Reachability Probabilities of Continuous-time Stochastic Systems](https://mlsanity.com/paper/2312.15843/) (2023)

## Built on by (most cited first, 6 of 6)

- [Neural Model Checking](https://mlsanity.com/paper/2410.23790/) (2024)
- [Neural Control and Certificate Repair via Runtime Monitoring](https://mlsanity.com/paper/2412.12996/) (2024)
- [Neural Proofs for Sound Verification and Control of Complex Systems](https://mlsanity.com/paper/2512.18389/) (2025)
- [Value Functions as Supermartingale Certificates](https://mlsanity.com/paper/2605.31524/) (2026)
- [Supermartingale Certificates for Parametric MDPs](https://mlsanity.com/paper/2609.12715/) (2026)
- [Large Language Models in the Loop: A Stability- and Network-Aware Survey in Networked Control, Cyber-Physical, and Multi-Agent Systems](https://mlsanity.com/paper/2609.16599/) (2026)

## Abstract (arXiv)

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 textsfUniQQ and showcase its efficacy on four classic DNN-controlled systems.