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

• URL: http://arxiv.org/abs/2506.03469v1
• Date: Wed, 04 Jun 2025 00:54:01 GMT
• Title: Verification-Guided Falsification for Safe RL via Explainable Abstraction and Risk-Aware Exploration
• Authors: Tuan Le, Risal Shefin, Debashis Gupta, Thai Le, Sarra Alqahtani,
• Abstract summary: We propose a hybrid framework that integrates explainability, model checking, and risk-guided falsification to achieve both rigor and coverage.<n>Our approach begins by constructing a human-interpretable abstraction of the RL policy using Comprehensible Abstract Policy Summarization (CAPS)<n>If no violation is detected, we cannot conclude satisfaction due to potential limitation in the abstraction and coverage of the offline dataset.
• Score: 8.246285288584625
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: 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.

Related papers

• COIN: Uncertainty-Guarding Selective Question Answering for Foundation Models with Provable Risk Guarantees [51.5976496056012]
  COIN is an uncertainty-guarding selection framework that calibrates statistically valid thresholds to filter a single generated answer per question.<n>COIN estimates the empirical error rate on a calibration set and applies confidence interval methods to establish a high-probability upper bound on the true error rate.<n>We demonstrate COIN's robustness in risk control, strong test-time power in retaining admissible answers, and predictive efficiency under limited calibration data.
  arXiv  Detail & Related papers  (2025-06-25T07:04:49Z)
• Advancing Neural Network Verification through Hierarchical Safety Abstract Interpretation [52.626086874715284]
  We introduce a novel problem formulation called Abstract DNN-Verification, which verifies a hierarchical structure of unsafe outputs.<n>By leveraging abstract interpretation and reasoning about output reachable sets, our approach enables assessing multiple safety levels during the formal verification process.<n>Our contributions include a theoretical exploration of the relationship between our novel abstract safety formulation and existing approaches.
  arXiv  Detail & Related papers  (2025-05-08T13:29:46Z)
• Learning Verifiable Control Policies Using Relaxed Verification [49.81690518952909]
  This work proposes to perform verification throughout training to aim for policies whose properties can be evaluated throughout runtime.<n>The approach is to use differentiable reachability analysis and incorporate new components into the loss function.
  arXiv  Detail & Related papers  (2025-04-23T16:54:35Z)
• Probabilistic Counterexample Guidance for Safer Reinforcement Learning (Extended Version) [1.279257604152629]
  Safe exploration aims at addressing the limitations of Reinforcement Learning (RL) in safety-critical scenarios. Several methods exist to incorporate external knowledge or to use sensor data to limit the exploration of unsafe states. In this paper, we target the problem of safe exploration by guiding the training with counterexamples of the safety requirement.
  arXiv  Detail & Related papers  (2023-07-10T22:28:33Z)
• SaFormer: A Conditional Sequence Modeling Approach to Offline Safe Reinforcement Learning [64.33956692265419]
  offline safe RL is of great practical relevance for deploying agents in real-world applications. We present a novel offline safe RL approach referred to as SaFormer.
  arXiv  Detail & Related papers  (2023-01-28T13:57:01Z)
• Information-Theoretic Safe Exploration with Gaussian Processes [89.31922008981735]
  We consider a sequential decision making task where we are not allowed to evaluate parameters that violate an unknown (safety) constraint. Most current methods rely on a discretization of the domain and cannot be directly extended to the continuous case. We propose an information-theoretic safe exploration criterion that directly exploits the GP posterior to identify the most informative safe parameters to evaluate.
  arXiv  Detail & Related papers  (2022-12-09T15:23:58Z)
• Recursively Feasible Probabilistic Safe Online Learning with Control Barrier Functions [60.26921219698514]
  We introduce a model-uncertainty-aware reformulation of CBF-based safety-critical controllers. We then present the pointwise feasibility conditions of the resulting safety controller. We use these conditions to devise an event-triggered online data collection strategy.
  arXiv  Detail & Related papers  (2022-08-23T05:02:09Z)
• Safe Exploration Incurs Nearly No Additional Sample Complexity for Reward-free RL [43.672794342894946]
  Reward-free reinforcement learning (RF-RL) relies on random action-taking to explore the unknown environment without any reward feedback information. It remains unclear how such safe exploration requirement would affect the corresponding sample complexity in order to achieve the desired optimality of the obtained policy in planning. We propose a unified Safe reWard-frEe ExploraTion (SWEET) framework, and develop algorithms coined Tabular-SWEET and Low-rank-SWEET, respectively.
  arXiv  Detail & Related papers  (2022-06-28T15:00:45Z)
• Learn Zero-Constraint-Violation Policy in Model-Free Constrained Reinforcement Learning [7.138691584246846]
  We propose the safe set actor-critic (SSAC) algorithm, which confines the policy update using safety-oriented energy functions. The safety index is designed to increase rapidly for potentially dangerous actions. We claim that we can learn the energy function in a model-free manner similar to learning a value function.
  arXiv  Detail & Related papers  (2021-11-25T07:24:30Z)
• Risk Minimization from Adaptively Collected Data: Guarantees for Supervised and Policy Learning [57.88785630755165]
  Empirical risk minimization (ERM) is the workhorse of machine learning, but its model-agnostic guarantees can fail when we use adaptively collected data. We study a generic importance sampling weighted ERM algorithm for using adaptively collected data to minimize the average of a loss function over a hypothesis class. For policy learning, we provide rate-optimal regret guarantees that close an open gap in the existing literature whenever exploration decays to zero.
  arXiv  Detail & Related papers  (2021-06-03T09:50:13Z)
• An Abstraction-based Method to Verify Multi-Agent Deep Reinforcement-Learning Behaviours [8.95294551927446]
  Multi-agent reinforcement learning (RL) often struggles to ensure the safe behaviours of the learning agents. We present a methodology that combines formal verification with (deep) RL algorithms to guarantee the satisfaction of formally-specified safety constraints.
  arXiv  Detail & Related papers  (2021-02-02T11:12:30Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.