REVIEW 4 major objections 6 minor 32 references
Verification-Guided Falsification for Safe RL via Explainable Abstraction and Risk-Aware Exploration
T0 review · 4 major / 6 minor · reviewed 2026-08-07 · deepseek-v4-flash
Pith's one-line read The paper argues that formal verification of an RL policy's safety should be paired with risk-guided falsification, and claims an (ε_r, δ)-PAC bound on the chance of missing an unsafe trajectory.
desk verdict The integrated pipeline is real and the empirical work is mostly credible, but the PAC theorem in §4.3 does not follow from the stated assumptions and should be removed or reframed. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
The load-bearing object is the CAPS graph, $G_\pi = (V, E)$, an interpretable finite abstraction of the policy whose nodes are clusters of states from the offline dataset and whose edges are policy transitions annotated with empirical probabilities and safety costs. The framework augments each node with a learned risk critic $\hat{Q}_{\text{risk}}$ approximating expected cumulative safety cost, uses ensemble contrastive encoders to score epistemic uncertainty of state-action pairs, and ranks seed states by risk to focus falsification rollouts. A gradient-based mutation (Eq. 5) pushes the search along the direction of high TD-error into poorly represented regions. The PAC theorem connects these pieces through three assumptions: abstraction soundness, risk-estimator accuracy, and uncertainty-estimator coverage; Eq. (7) is the formal target of the paper.
What would settle it
Take a small fully enumerable MDP, such as a one-dimensional corridor with a narrow unsafe interval, train a policy, and build the CAPS graph from a dataset that deliberately excludes trajectories through part of the unsafe interval. Enumerate all reachable states of the true MDP and compare with the set represented by the CAPS graph plus high-risk flags: if some reachable unsafe state is neither in the graph nor flagged high-risk, then Assumption 1 is violated and Eq. (7) can be shown to fail by observing the missed trajectory.
Extended reading notes
Core claim
The paper's central claim is that verification and falsification should be treated as one pipeline rather than alternatives. If the CAPS abstraction graph $G_\pi$ over-approximates the true reachable space, if the learned risk critic is within $\epsilon_r$ of the true expected cumulative safety cost, and if the ensemble uncertainty estimator flags out-of-distribution state-action pairs with failure probability at most $\delta$, then the framework is $(\epsilon_r, \delta)$-PAC: the probability that an unsafe trajectory exists and escapes both the model checker and the falsification phase is at most $\delta$, as stated in Eq. (7). A violation found by the model checker is a certified counterexample—the policy is unsafe with certainty—while an absence of violations is treated as a reason to search, not a certificate of safety. Empirically, the paper claims the combined method finds more violations than both a purely uncertainty-based and a purely risk-based searcher in the tested domains, with greater novelty in the safety-critical dosing task.
Load-bearing premise
The guarantee rests on Assumption 1: the abstract graph, built from a finite offline dataset, is assumed to over-approximate the true reachable space, so every unsafe trajectory either shows up in the graph or starts in a state the risk critic flags as high-risk; the paper provides no construction, algorithm, or proof that this must hold, and if the finite data misses a critical transition while the risk critic also misrates it, the PAC bound loses its force.
Editorial extensions
If this is right
- Model checking alone is not enough: an empty result from the checker does not certify safety, and the paper's pipeline treats it as a cue to begin falsification.
- Counterexamples returned by the model checker are interpretable traces through abstract states, so the same output used for verification also supports debugging.
- If the PAC claim is correct, a practitioner can bound the probability of missing a safety violation, which is what a deployment-time safety argument needs beyond raw violation counts.
- The runtime shield can reduce violations without retraining, but the paper's RQ5 results show shielding can make the policy appear safe to the model checker even when falsification still finds failures—so shielding does not replace falsification.
- Abstraction fidelity matters for verification: the paper reports that a clustering baseline preserves the policy's action in fewer states and consequently misses nearly all violations.
Reading between the lines
- I infer that the PAC guarantee is best read as a conditional statement about an idealized abstraction; in practice the hard part is establishing Assumption 1 from finite data, and until that is done the real contribution is a guided search heuristic with strong empirical behavior.
- I infer that the same abstraction-plus-falsification loop could be applied to other temporal specifications beyond reach-avoid, such as bounded liveness or energy constraints, since the model checker only needs a finite graph and PCTL properties.
- I infer there is a circularity risk worth testing: if the risk critic is wrong in a region the dataset does not cover, the mutation procedure may never be sent there, so varying the risk critic's error directly and measuring how often violations are missed would stress the guarantee.
- The evaluation suggests a division of labor: model checking provides certain-but-limited counterexamples, while risk-guided search provides broad-but-heuristic coverage; a deployment checklist would probably use both, with the bound interpreted only under conditions that are themselves verified.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. The paper proposes a hybrid safety-assurance framework for reinforcement learning policies, combining CAPS-based explainable abstraction, Storm probabilistic model checking, risk- and uncertainty-guided falsification, and a runtime safety shield. The central claim is that this framework provides an (epsilon_r, delta)-PAC guarantee on the completeness of safety-violation detection, formalized in Eq. (7). The paper also presents empirical evaluations on Navigation2, Maze, and a simulated insulin-dosing task, comparing falsification effectiveness, diversity, novelty, and efficiency against uncertainty-based and DRLFuzz baselines.
Significance. If the theoretical guarantee were valid, the framework would be a valuable integration of interpretability, formal verification, and targeted falsification, with practical relevance for safety-critical RL. The empirical study is extensive: it includes multiple domains, a realistic medical task, baselines, ablations (mutation depth, KMeans vs. CAPS, shielding), and metrics covering effectiveness, efficiency, diversity, and novelty. The interpretable counterexamples returned by Storm and the modular shielding without retraining are useful contributions. However, the PAC guarantee is a central advertised contribution, and it is not established by the paper; this substantially weakens the significance of the work as presented.
major comments (4)
- [§4.3, Assumption 1] Assumption 1 states that the CAPS graph G_pi over-approximates the true reachable space, so any unsafe trajectory either appears in G_pi or begins in an abstract state flagged as high-risk. However, §3 and §4.1 construct G_pi from a fixed finite offline dataset D using CAPS, and the paper itself concedes in §3 that limited samples may omit critical transitions. No explicit abstraction relation, simulation relation, or proof of over-approximation is provided, and the construction as described cannot introduce states or transitions not present in D. Thus Assumption 1 is not justified and is at odds with the finite-data construction; the PAC guarantee in Eq. (7) rests on an unverified premise.
- [§4.3, proof of Eq. (7)] Even if Assumption 1 were granted, the proof of the second case does not follow from the stated assumptions. Assumption 2 only bounds the estimation error as |Q_hat_risk - Q_risk| <= epsilon_r; it does not imply that an unsafe trajectory contains a state-action pair with Q_hat_risk > alpha. If all true Q_risk values along the trajectory are at or below alpha, Algorithm 1 (lines 19-21) will never flag the trajectory as violated, regardless of the risk critic's accuracy. A threshold-separation condition (for example, unsafe implies there exists a state-action pair with Q_risk(s,a) > alpha + epsilon_r) is required but is neither stated nor used in the proof.
- [§4.3, Assumption 3 and Algorithm 1] Assumption 3 says the ensemble assigns high uncertainty to out-of-distribution pairs with failure probability at most delta, but this does not guarantee that such pairs are actually selected as seeds or visited during the bounded falsification phase. Algorithm 1 operates with a finite seed budget N, a depth limit L, and an uncertainty threshold delta; high uncertainty alone does not force a rollout to be executed or a violation to be flagged. Consequently, Eq. (7)'s probability bound is essentially a restatement of Assumption 3 rather than a derived completeness guarantee. The proof sketch's phrase 'prompting their inclusion in the falsification phase' has no corresponding mechanism in Algorithm 1 that ensures inclusion within the budget.
- [§4.3, Theorem statement] The claimed PAC guarantee is circular: the delta in Eq. (7) is exactly the failure probability already assumed in Assumption 3. The theorem does not provide a new bound derived from the method's construction; it repackages the uncertainty-estimator assumption as a formal guarantee. This is a load-bearing issue because the abstract and Section 1 advertise a 'PAC-style guarantee on the completeness of safety violation detection' as a core contribution.
minor comments (6)
- [References] Reference [11] contains the typo 'Philaldelpia' for 'Philadelphia', and reference [9] has 'V olk' with a stray space.
- [Eq. (5)] Equation (5) uses Q(st, at) and Qtarget(st+1) without defining the Q-function; the reader is left to infer it is the task value function, which should be stated explicitly and distinguished from the risk critic Q_risk.
- [Algorithm 1] The pseudocode structure is confusing: lines 10-18 introduce an inner depth loop inside the while loop that already iterates over steps, and the variable 'l' is not clearly related to the maximum depth L. The mutation procedure and termination conditions should be clarified.
- [Eq. (8)] The safety threshold in Eq. (8) is denoted epsilon, which clashes with the risk-estimation error epsilon_r used in Section 4.3; using distinct symbols (e.g., epsilon_shield) would improve readability.
- [Section 5.1] The hardware description '1 physical core per CPU' is unclear; presumably the authors mean one socket or one core per CPU, and this should be stated precisely.
- [Figures 4-6] The abbreviations 'Dep.10' and 'Dep.20' in the figures and captions are not defined in the main text; they should be introduced when the depth ablation is described.
Circularity Check
The PAC guarantee in §4.3 is a restatement of Assumptions 1 and 3: the δ in Eq. (7) is copied from Assumption 3, and the proof invokes Assumption 1 verbatim as its main step, while Assumption 1 is exactly the unsupported coverage property the framework needs.
-
self definitional
[Section 4.3, Assumption 1 and Theorem (PAC Safety Violation Guarantee), Eq. (7)]
"Assumption 1 (Abstraction Soundness): The CAPS graph Gπ over-approximates the true reachable space. Any unsafe trajectory τ in the concrete environment either (i) appears in Gπ, or (ii) begins in an abstract state flagged as high-risk. ... Theorem ... Under assumptions (1)–(3), the probability of failing to detect any safety violation (if one exists) is at most δ. Formally ... P (∃ τ ∼ πtask : τ violates safety and τ /∈ Vfound) ≤ δ."
Eq. (7) is the probabilistic wrapper of Assumption 1 plus Assumption 3. Assumption 1 already asserts, without probability, that every unsafe trajectory is represented in Gπ or begins in a high-risk abstract state, and the proof sketch says Storm detects case (i) "by the soundness of the abstraction (Assumption 1)". The δ on the right of Eq. (7) is exactly the failure probability δ from Assumption 3, not a derived concentration bound. The only way CAPS could satisfy Assumption 1 is if the graph were a true over-approximation, but CAPS is built from the finite offline dataset D; Section 3 concedes that "limited samples in D may omit critical transitions, yielding incomplete or misleading abstractions".
-
other
[Section 4.2, Algorithm 1 lines 19–21; Section 4.3, Proof Sketch]
"risk ← Q̂risk(currentState, a) (Eq.1) ... if risk > α then violated = True ... During exploration, if τ leads to a safety violation, the risk critic Q̂risk, which is ϵr-accurate by Assumption 2, will identify at least one risky state-action pair along τ, leading to its detection."
The falsification detector flags a trajectory as a violation only if some state-action has Q̂risk > α. The proof requires the bridge "τ violates safety ⇒ some (s,a) in τ has Q̂risk(s,a) > α", but Assumptions 1–3 do not provide it: Assumption 2 only bounds |Q̂risk − Qrisk| ≤ ϵr, and the temporal safety property φ is never tied to the threshold α. If all true Qrisk values along an unsafe τ are at most α, the loop at lines 19–21 will never set violated = True even with an exact risk critic, so Eq. (7) is false. Conversely, if "unsafe" is definitionally identified with Qrisk > α, the guarantee is about the risk critic's own threshold, not about the state-space safety property φ. The theorem therefore silently imports an unstated threshold-separation condition.
full rationale
The paper's empirical falsification results against DRLFuzz and uncertainty-based search are externally benchmarked and are not circular, and the self-citations to CAPS [24] and the adversarial safety policy [26] are used as implementation tools rather than as the load-bearing proof of the PAC claim. However, the central formal result is not established as a derivation. Assumption 1 asserts exactly the completeness property that the framework needs: every unsafe trajectory is either present in the CAPS graph or seeded through a high-risk abstract state. Section 3 states the opposite concern, that finite data can omit critical transitions, and no abstraction-relation proof is given to reconcile the two. The proof of Eq. (7) then uses Assumption 1 directly for the Storm case and Assumption 3's δ for the falsification case, so the theorem reduces to its assumptions. In addition, the falsification detection criterion in Algorithm 1 is threshold-based on Q̂risk, and the proof needs an unstated guarantee that any safety-violating trajectory contains a state-action above the threshold α; Assumptions 1–3 do not imply this. Accordingly, the claimed (ϵr, δ)-PAC guarantee is forced by definition rather than derived from the presented construction, giving a circularity score of 8.
Assumptions & free parameters
free parameters (7)
- Risk threshold alpha =
not specified in main text
- Uncertainty threshold delta =
not specified
- Number of seed states N =
not specified
- Max trajectory depth L =
not specified
- Risk critic Q_phi,risk =
neural network weights fit to offline transitions
- Ensemble size K =
5
- Mutation step size alpha =
not specified
assumptions (5)
- domain assumption CAPS abstraction over-approximates the true reachable space (Assumption 1).
- domain assumption Risk critic error is uniformly bounded by epsilon_r for all (s,a) (Assumption 2).
- domain assumption Ensemble uncertainty flags all out-of-distribution pairs with failure probability at most delta (Assumption 3).
- standard math Storm model checking is correct for finite MDPs.
- domain assumption The CMDP with safety cost functions accurately models the real environment's safety constraints.
Cite this review
Pith. "Pith review of Verification-Guided Falsification for Safe RL via Explainable Abstraction and Risk-Aware Exploration." pith.science (2026). https://pith.science/paper/3OSCP2NA
@misc{pith2026250603469,
author = {Pith},
title = {Pith review of: Verification-Guided Falsification for Safe RL via Explainable Abstraction and Risk-Aware Exploration},
year = {2026},
howpublished = {\url{https://pith.science/paper/3OSCP2NA}},
note = {Machine review of arXiv:2506.03469}
}
read the original 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.
Reference graph
Works this paper leans on
-
[1]
M. Alshiekh, R. Bloem, R. Ehlers, B. Könighofer, S. Niekum, and U. Topcu. Safe reinforcement learning via shielding. Proceedings of the AAAI Conference on Artificial Intelligence, 32(1), 2018
work page 2018
-
[2]
P. Bachman, A. Sordoni, and A. Trischler. Learning algorithms for active learning. In International Conference on Machine Learning (ICML), pages 301–310, 2017
work page 2017
-
[3]
Baier and J.-P
C. Baier and J.-P. Katoen. Principles of model checking . MIT press, 2008
2008
-
[4]
O. Bastani. Safe reinforcement learning with formal guarantees. Pro- ceedings of the AAAI Conference on Artificial Intelligence , 35(17): 15102–15110, 2021
work page 2021
-
[5]
O. Biza and R. Platt. Online abstraction with mdp homomorphisms for deep learning. In Proceedings of the 18th International Confer- ence on Autonomous Agents and MultiAgent Systems , AAMAS ’19, page 1125–1133, Richland, SC, 2019. International Foundation for Au- tonomous Agents and Multiagent Systems. ISBN 9781450363099
work page 2019
- [6]
-
[7]
D. A. Cohn, Z. Ghahramani, and M. I. Jordan. Active learning with statistical models. Journal of Artificial Intelligence Research , 4:129– 145, 1996
work page 1996
- [8]
Show all 32 references
-
[9]
Dehnert, S
C. Dehnert, S. Junges, J.-P. Katoen, and M. V olk. A storm is coming: A modern probabilistic model checker. In International Conference on Computer Aided Verification (CAV), pages 592–600. Springer, 2017
2017
-
[10]
J. V . Deshmukh, X. Jin, J. Kapinski, K. Ueda, and M. Butts. Stochas- tic search techniques for reachability analysis of markov decision pro- cesses. In Tools and Algorithms for the Construction and Analysis of Systems, pages 211–229. Springer, 2015
2015
-
[11]
Dukkipati, R
A. Dukkipati, R. S. Ayyagari, B. Dasgupta, P. Dutta, and P. R. Onteru. Active reinforcement learning strategies for offline policy improvement. In Proceedings of the 39th AAAI Conference on Artificial Intelligence (AAAI-25), Philaldelpia, USA, 2025. AAAI Press. To appear
2025
-
[12]
P. Geibel. Reinforcement learning for mdps with constraints. European Conference on Machine Learning, pages 646–653, 2006
2006
-
[13]
Haarnoja, A
T. Haarnoja, A. Zhou, P. Abbeel, and S. Levine. Soft actor-critic: Off- policy maximum entropy deep reinforcement learning with a stochastic actor. In International conference on machine learning , pages 1861–
-
[14]
E. M. Hahn, A. Hartmanns, C. Hensel, M. Klauck, J. Kretinsky, D. Parker, T. Quatmann, E. Ruijters, and M. Steinmetz. Storm: A mod- ern probabilistic model checker. In International Conference on Com- puter Aided Verification, pages 592–600. Springer, 2019
2019
-
[15]
Karakovskiy and J
S. Karakovskiy and J. Togelius. The mario ai benchmark and compe- titions. IEEE Transactions on Computational Intelligence and AI in Games, 4(1):55–67, 2012
2012
-
[16]
Karunakaran and S
P. Karunakaran and S. A. Seshia. Counterexample-guided reinforce- ment learning with model-based exploration. In Advances in Neural Information Processing Systems (NeurIPS), 2020
2020
-
[17]
D. Kim, S. Moon, D. E. Hostallero, W. J. Kang, T. Lee, K. Son, and Y . Yi. Safe reinforcement learning: A survey. arXiv preprint arXiv:2005.00903, 2020
2005
-
[18]
Kwiatkowska, G
M. Kwiatkowska, G. Norman, and D. Parker. Prism 4.0: Verification of probabilistic real-time systems. In International Conference on Com- puter Aided Verification (CAV), pages 585–591. Springer, 2011
2011
-
[19]
Levine, A
S. Levine, A. Kumar, G. Tucker, and J. Fu. Offline reinforcement learn- ing: Tutorial, review, and perspectives on open problems.arXiv preprint arXiv:2005.01643, 2020
2005 arXiv
-
[20]
L. Li, T. J. Walsh, and M. L. Littman. Towards a unified theory of state abstraction for mdps. In International Symposium on Artificial Intelligence and Mathematics, 2006
2006
-
[21]
B. Liu, Y . Xia, and P. S. Yu. Clustering via decision tree construction. 2004
2004
-
[22]
Liu and N
J. Liu and N. Ozay. Abstraction, discretization, and robustness in tem- poral logic control of dynamical systems. InProceedings of the 17th In- ternational Conference on Hybrid Systems: Computation and Control , HSCC ’14, page 293–302, New York, NY , USA, 2014. Association for...
2014
-
[23]
V . J. Manes, H. Han, C. Han, S. K. Cha, M. Egele, E. J. Schwartz, and M. Woo. The art, science, and engineering of fuzzing: A survey. In IEEE Transactions on Software Engineering, volume 47, pages 2312–
-
[24]
McCalmon, T
J. McCalmon, T. Le, S. Alqahtani, and D. Lee. Caps: Comprehensible abstract policy summaries for explaining reinforcement learning agents. In Proceedings of the 21st International Conference on Autonomous Agents and Multiagent Systems, AAMAS ’22, page 889–897, Richland, SC, 20...
2022
-
[25]
Mihatsch and R
O. Mihatsch and R. Neuneier. Risk-sensitive reinforcement learning. Machine Learning, 49(2-3):267–290, 2002
2002
-
[26]
M. A. Rahman, T. Liu, and S. Alqahtani. Adversarial behavior exclusion for safe reinforcement learning. In E. Elkind, editor, Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI-23, pages 483–491. International Joint Conferences on...
2023 doi
-
[27]
Ruggeri, A
F. Ruggeri, A. Russo, R. Inam, and K. H. Johansson. Explainable rein- forcement learning via temporal policy decomposition. arXiv preprint arXiv:2501.03902, 2025
2025 arXiv
-
[28]
B. Settles. From theories to queries: Active learning in practice. In I. Guyon, G. Cawley, G. Dror, V . Lemaire, and A. Statnikov, editors, Active Learning and Experimental Design workshop In conjunction with AISTATS 2010 , volume 16 of Proceedings of Machine Learning Research...
2010
-
[29]
Tappler, A
M. Tappler, A. Pferscher, B. K. Aichernig, and B. Könighofer. Learn- ing and repair of deep reinforcement learning policies from fuzz-testing data. In Proceedings of the IEEE/ACM 46th International Conference on Software Engineering, ICSE ’24, New York, NY , USA, 2024. Asso- c...
2024
-
[30]
Thananjeyan, A
B. Thananjeyan, A. Balakrishna, S. Nair, M. Luo, K. Srinivasan, M. Hwang, J. E. Gonzalez, J. Ibarz, C. Finn, and K. Goldberg. Recov- ery rl: Safe reinforcement learning with learned recovery zones. IEEE Robotics and Automation Letters, 6(3):4915–4922, 2021
2021
-
[31]
X. Wan, T. Li, W. Lin, Y . Cai, and Z. Zheng. Coverage-guided fuzzing for deep reinforcement learning systems. Journal of Systems and Soft- ware, 210:111963, 2024. ISSN 0164-1212. doi: https://doi.org/10.1016/ j.jss.2024.111963. URL https://www.sciencedirect.com/science/articl...
2024
-
[32]
T.-W. Wang, X. Huang, B. Li, S. Jha, S. Jha, and J. Chen. To- wards verification of neural-network control systems. arXiv preprint arXiv:2003.06139, 2020
2003 arXiv
Reviewed August 7, 2026 · model on record in the stance chip above.
Discussion (0). Sign in to comment.