# Verification-Guided Falsification for Safe RL via Explainable Abstraction and Risk-Aware Exploration

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Safe and constrained RL, one of 15 directions in Deep reinforcement learning methods.
- Builds on 12 of its 30 references that are in the map.
- First posted on arXiv 4 Jun 2025.

## Placed in

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

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

- [Soft Actor-Critic: Off-Policy Maximum Entropy Deep Reinforcement Learning with a Stochastic Actor](https://mlsanity.com/paper/1801.01290/) (2018)
- [Offline Reinforcement Learning: Tutorial, Review, and Perspectives on Open Problems](https://mlsanity.com/paper/2005.01643/) (2020)
- [Safe Reinforcement Learning via Shielding](https://mlsanity.com/paper/1708.08611/) (2017)
- [Recovery RL: Safe Reinforcement Learning with Learned Recovery Zones](https://mlsanity.com/paper/2010.15920/) (2020)
- [Risk-sensitive Reinforcement Learning](https://mlsanity.com/paper/1311.2097/) (2013)
- [The Art, Science, and Engineering of Fuzzing: A Survey](https://mlsanity.com/paper/1812.00140/) (2018)
- [A storm is Coming: A Modern Probabilistic Model Checker](https://mlsanity.com/paper/1702.04311/) (2017)
- [Learning Algorithms for Active Learning](https://mlsanity.com/paper/1708.00088/) (2017)
- [Online Abstraction with MDP Homomorphisms for Deep Learning](https://mlsanity.com/paper/1811.12929/) (2018)
- [A Survey on Explainable Deep Reinforcement Learning](https://mlsanity.com/paper/2502.06869/) (2025)
- [Explainable Reinforcement Learning via Temporal Policy Decomposition](https://mlsanity.com/paper/2501.03902/) (2025)
- [Active Reinforcement Learning Strategies for Offline Policy Improvement](https://mlsanity.com/paper/2412.13106/) (2024)

## Abstract (arXiv)

Ensuring the safety of reinforcement learning (RL) policies in high-stakes environments requires not only formal verification but also interpretability and targeted falsification. While model checking provides formal guarantees, its effectiveness is limited by abstraction quality and the completeness of the underlying trajectory dataset. We propose a hybrid framework that integrates (1) explainability, (2) model checking, and (3) risk-guided falsification to achieve both rigor and coverage. Our approach begins by constructing a human-interpretable abstraction of the RL policy using Comprehensible Abstract Policy Summarization (CAPS). This abstract graph, derived from offline trajectories, is both verifier-friendly, semantically meaningful, and can be used as input to Storm probabilistic model checker to verify satisfaction of temporal safety specifications. If the model checker identifies a violation, it will return an interpretable counterexample trace by which the policy fails the safety requirement. However, if no violation is detected, we cannot conclude satisfaction due to potential limitation in the abstraction and coverage of the offline dataset. In such cases, we estimate associated risk during model checking to guide a falsification strategy that prioritizes searching in high-risk states and regions underrepresented in the trajectory dataset. We further provide PAC-style guarantees on the likelihood of uncovering undetected violations. Finally, we incorporate a lightweight safety shield that switches to a fallback policy at runtime when such a risk exceeds a threshold, facilitating failure mitigation without retraining.