Pith. sign in

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 →

arxiv 2506.03469 v1 pith:3OSCP2NA submitted 2025-06-04 cs.AI cs.LG

classification cs.AIcs.LG
keywords safereinforcementlearningformalverificationprobabilisticmodelcheckingpolicyabstractionfalsificationPACguaranteerisk-awareexplorationsafetyshielding
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper proposes that the safety of a trained reinforcement-learning policy can be assured by combining three things that are usually kept separate: an interpretable abstraction of the policy, formal probabilistic model checking, and risk-guided search for counterexamples. The authors build the abstraction as a finite graph (CAPS) from offline trajectories, verify a temporal safety property on that graph with a probabilistic model checker, and, when the checker finds no violation, use estimates of risk and epistemic uncertainty to steer extra rollouts toward regions the data underrepresents. They claim this hybrid detects more, and more novel, safety violations than uncertainty-only or risk-only search, and that the whole procedure carries an (ε_r, δ)-PAC guarantee: the probability of overlooking an unsafe trajectory is at most δ. The appeal of the claim is practical: formal guarantees and interpretable counterexamples are obtained without requiring the full Markov decision process or retraining the policy.

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.

Watch

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

Editorial extensions of the paper, not claims the author makes directly.

  • 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.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 6 minor

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)
  1. [§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.
  2. [§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.
  3. [§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. [§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)
  1. [References] Reference [11] contains the typo 'Philaldelpia' for 'Philadelphia', and reference [9] has 'V olk' with a stray space.
  2. [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.
  3. [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.
  4. [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.
  5. [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.
  6. [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

2 steps flagged · score 8.0 of 10

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.

  1. 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".

  2. 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 7 free parameters · 5 assumptions · 0 invented entities

The central theoretical guarantee rests on three assumptions (abstraction soundness, risk-estimator accuracy, uncertainty coverage), none of which are verified or derived. The first is contradicted by finite-data construction; the third is the theorem's conclusion. The empirical results depend on hand-chosen thresholds and a risk critic fit to offline data.

free parameters (7)
  • Risk threshold alpha = not specified in main text
    Algorithm 1 flags a state as a violation when Q_risk(currentState, a) > alpha; the value is chosen by hand and directly determines reported violation counts.
  • Uncertainty threshold delta = not specified
    Used in Algorithm 1 to decide if a state is well-represented; controls mutation trigger and affects search trajectories.
  • Number of seed states N = not specified
    Algorithm 1 parameter limiting falsification budget; affects how many high-risk states are explored.
  • Max trajectory depth L = not specified
    Algorithm 1 rollout depth limit; important for delayed-failure domains like Dosing.
  • Risk critic Q_phi,risk = neural network weights fit to offline transitions
    Trained by minimizing Eq. (2); used both to label unsafe nodes in CAPS and to detect violations during falsification. Its accuracy is assumed, not demonstrated.
  • Ensemble size K = 5
    Algorithm 1 line 1 sets numModels=5; uncertainty estimate depends on this choice.
  • Mutation step size alpha = not specified
    Equation (5) uses alpha as a gradient ascent step; the same symbol is used for the risk threshold, and no value is given.
assumptions (5)
  • domain assumption CAPS abstraction over-approximates the true reachable space (Assumption 1).
    Needed for the PAC theorem; contradicted by construction from a finite offline dataset, as Section 3 acknowledges coverage limitations.
  • domain assumption Risk critic error is uniformly bounded by epsilon_r for all (s,a) (Assumption 2).
    Needed for the theorem; no training procedure, regularization, or formal verification establishes this uniform bound.
  • domain assumption Ensemble uncertainty flags all out-of-distribution pairs with failure probability at most delta (Assumption 3).
    This assumption is essentially the theorem's conclusion; no calibration proof or empirical validation is provided.
  • standard math Storm model checking is correct for finite MDPs.
    Standard correctness of probabilistic model checking algorithms; reasonable background assumption.
  • domain assumption The CMDP with safety cost functions accurately models the real environment's safety constraints.
    The framework verifies against this model, not the physical system; the paper does not validate the model against real-world data.

how reviews work

0 comments
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.

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

32 extracted references · 25 canonical work pages

  1. [1]

    Alshiekh, R

    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

  2. [2]

    Bachman, A

    P. Bachman, A. Sordoni, and A. Trischler. Learning algorithms for active learning. In International Conference on Machine Learning (ICML), pages 301–310, 2017

  3. [3]

    Baier and J.-P

    C. Baier and J.-P. Katoen. Principles of model checking . MIT press, 2008

  4. [4]

    O. Bastani. Safe reinforcement learning with formal guarantees. Pro- ceedings of the AAAI Conference on Artificial Intelligence , 35(17): 15102–15110, 2021

  5. [5]

    Biza and R

    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

  6. [6]

    Cheng, J

    Z. Cheng, J. Yu, and X. Xing. A survey on explainable deep reinforce- ment learning. arXiv preprint arXiv:2502.06869, 2025

  7. [7]

    D. A. Cohn, Z. Ghahramani, and M. I. Jordan. Active learning with statistical models. Journal of Artificial Intelligence Research , 4:129– 145, 1996

  8. [8]

    Corsi, E

    D. Corsi, E. Marchesini, and A. Farinelli. Formal verification of neural networks for safety-critical tasks in deep reinforcement learning. Pro- ceedings of the Thirty-Seventh Conference on Uncertainty in Artificial Intelligence, 2021

Show all 32 references
  1. [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

  2. [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

  3. [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

  4. [12]

    P. Geibel. Reinforcement learning for mdps with constraints. European Conference on Machine Learning, pages 646–653, 2006

  5. [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–

  6. [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

  7. [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

  8. [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

  9. [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

  10. [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

  11. [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

  12. [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

  13. [21]

    B. Liu, Y . Xia, and P. S. Yu. Clustering via decision tree construction. 2004

  14. [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...

  15. [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–

  16. [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...

  17. [25]

    Mihatsch and R

    O. Mihatsch and R. Neuneier. Risk-sensitive reinforcement learning. Machine Learning, 49(2-3):267–290, 2002

  18. [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...

  19. [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

  20. [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...

  21. [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...

  22. [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

  23. [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...

  24. [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

Pith tools

Reviewed August 7, 2026 · model on record in the stance chip above.