REVIEW 4 major objections 6 minor 21 references
Assuring the Safety of Reinforcement Learning Components: AMLAS-RL
T0 review · 4 major / 6 minor · reviewed 2026-08-06 · deepseek-v4-flash
Pith's one-line read The paper adapts the AMLAS assurance process into AMLAS-RL, a six-stage iterative method for building safety arguments for reinforcement-learning components.
desk verdict The AMLAS-RL framework is a credible, genuinely useful extension of AMLAS, but the wheeled-vehicle case study's model-checking evidence is self-contradictory and needs major revision before the demonstration can be trusted. 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 mechanism is AMLAS-RL's six-stage argument-generation cycle: RL Assurance Safety Scoping, RL Safety Requirements Assurance, Data Management, Model Learning, Model Verification, and Model Deployment. Each stage produces an argument pattern, that is, a reusable template connecting a claim to the evidence that supports it, and the pattern is instantiated with the artefacts collected at that stage. The RL-specific changes carry the argument: Stage 3 replaces dataset construction with training, internal-test, and verification plans; Stage 4 logs the reward function and model choices; Stage 5 adds targeted unsafe-scenario tests and a DTMC abstraction of the state space with PCTL properties for goal success, collision, and unsafe-zone time; Stage 6 logs erroneous behavioural sequences. The DTMC abstraction is a concrete verification device, abstracting the vehicle's state as $(m_t,e_t,d_{o,t},d_{u,t})$ and using model checking to estimate the safety requirement probabilities.
What would settle it
Deploy the trained policy on a physical wheeled vehicle with the same sensor configuration in an environment matching the simulator layout, and measure the three safety metrics over repeated runs. If the observed goal-success rate with $E>0$ falls below 0.6, the time in unsafe zones exceeds 20 timesteps, or the collision probability exceeds 0.1, the simulator-transfer premise on which the Stage 3 data justification rests is empirically false, and the AMLAS-RL safety argument built on those results does not transfer.
Extended reading notes
Core claim
The paper's central claim is that assurance for RL components is not a post-training certification task but a lifecycle activity, and AMLAS-RL specifies how to run that activity. Each of the six stages, safety scoping, safety-requirement assurance, data management, model learning, model verification, and deployment, produces an argument pattern instantiated with the evidence gathered at that stage. The adaptation's substance is in where RL differs from supervised learning: the data stage outputs a training plan, an internal test plan, and an independent verification plan rather than a static dataset; the model-learning stage records the reward function and training choices in a development log so that reward hacking can be traced; the verification stage augments reward-based evaluation with targeted unsafe scenarios and DTMC/PCTL model checking; and the deployment stage tracks sequences of behaviour in an erroneous-behaviour log. The case study applies the process to a delivery vehicle that must reach a goal within an energy budget, avoid an obstacle, and limit time in unsafe zones. Internal tests and baseline verification pass, but targeted near-obstacle verification fails two safety requirements, which the paper treats not as refutation but as the iterative loop doing its job: the process tells the team to revisit an earlier stage and re-plan training and verification.
Load-bearing premise
The case study's safety evidence assumes the simulator perfectly reproduces the real vehicle, its sensors, and the operating environment, so that results obtained in simulation transfer unchanged to deployment.
Editorial extensions
If this is right
- Safety requirements for an RL component can be fixed before training and traced through data, training, testing, and deployment, giving each safety claim a documented chain of evidence.
- Reward functions become first-class assurance artefacts, so reward hacking is detectable by verifiers and by later deployment monitoring.
- Independent verification with deliberately unsafe starting conditions can expose requirement violations that average internal-test metrics hide.
- The iterative loop converts a failed verification into a trigger for re-planning, so unsatisfied requirements are caught before deployment rather than after.
- The same six-stage story applies to other RL-enabled cyber-physical systems, not just wheeled vehicles, because the stages do not depend on the specific platform.
Reading between the lines
- The paper leaves implicit that simulator fidelity should be treated as a data-requirement property with quantitative evidence; making that explicit would let AMLAS-RL incorporate domain-randomization or sim-to-real gap studies as assurance evidence.
- A natural testable extension is to vary which verification scenarios are kept hidden from the development team, quantifying how much assurance the independent verification plan actually adds.
- The DTMC abstraction used at Stage 5 could be reused at deployment as a runtime safety monitor or to constrain exploration during training, connecting AMLAS-RL to post-shielding approaches.
- The safety thresholds used in the case study, such as a 0.6 success probability and 0.1 collision probability, are taken as given; a fuller extension would derive them from hazard analysis and risk acceptance criteria.
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
Summary. This paper proposes AMLAS-RL, a six-stage adaptation of the AMLAS assurance methodology for reinforcement-learning components, and demonstrates it on a simulated differential-drive vehicle navigating to a goal while avoiding collisions and unsafe zones. The stages are safety scoping, safety requirements assurance, data management (training/internal test/verification plans), model learning, model verification, and model deployment. The case study trains a DDPG policy in Safety-Gymnasium, performs internal and independent verification, and uses a PCTL model check on a DTMC abstraction. The paper claims that the framework supports auditable safety arguments across the RL lifecycle rather than at the trained-model level only.
Significance. If the framework and case study were sound, this would be a useful contribution: it gives practitioners a concrete process for generating assurance arguments for RL components, with explicit artefacts and iterative loops, and it attempts to connect RL-specific concerns (reward design, state-action uncertainty, verification planning) to structured safety cases. The use of a separate verification plan and a formal model-checking step is a strength. However, the current demonstration does not support the central claim because the reported verification evidence is internally inconsistent: the PCTL properties in Eq. (3) are the reverse of the corresponding safety requirements, and the model-checking numbers in Table III cannot be the output of those properties. The paper also does not yet validate the DTMC abstraction or qualify the strong simulator-fidelity assumption. The framework itself is plausible, but the paper needs a corrected and more carefully supported case study before the demonstration claim can be accepted.
major comments (4)
- [Section IV-C, Eq. (3)] Equation (3) inverts the PCTL properties with respect to the stated safety requirements. From Eq. (2), m=2 denotes collision and m=3 denotes reaching the goal. Eq. (3) sets C1: P[m=2]>=0.6 and C2: P[m=3]<=0.1, which would require a collision probability of at least 60% and a goal probability of at most 10%. This is the opposite of SR1 (goal with probability at least 0.6) and SR3 (collision with probability at most 0.1). The model-checking results in Table III (goal 60.4%, collision 5.8%) cannot be the output of the properties as written. The parenthetical claim that 'C1 evaluates SR1 (as m=2 can only occur while e>0)' is also incorrect for the stated definitions. Please correct the property labels and verify that the reported results correspond to the intended properties.
- [Section IV-E, verification narrative] The narrative in Section IV-E is internally inconsistent about the verification outcome. The text states that Table III results are 'in agreement of the vehicle's compliance with the safety requirements' and then immediately reports that targeted testing shows the vehicle is 'unable to satisfy SR1 and SR2.' Since Table III includes the targeted results (57.6% goal, 23.48 timesteps in unsafe zone), the sentence cannot be read as a consistent summary. Please separate the compliance evaluation from the targeted edge-case failures and explain how the Stage 5 evidence, including the model-checking results, supports the decision to revisit Stage 3.
- [Section IV-C and Section IV-E, DTMC abstraction] The DTMC abstraction used for model checking is not validated as assurance evidence. In Section IV-C, the state s_t=(m_t,e_t,d_o,t,d_u,t) is described as an abstraction, but the discretisation of the continuous distances and energy is not specified, and in Section IV-E the transition probabilities are extracted from 5000 rollouts of the same policy under verification. The paper should provide evidence that the abstraction preserves the properties of interest (for example, by comparing model-checking probabilities with independent rollouts and quantifying uncertainty), or should present the model-checking results as exploratory insight rather than as verification evidence.
- [Section IV-D, Eq. (4)] The reward function in Eq. (4) has a sign error. The text says 'a penalising cost value is applied' and defines c_t=-0.1 for unsafe zones and c_t=-10 for collisions, but the equation is R_t=r_t-c_t, so these negative values add +0.1 and +10 to the reward instead of penalising. Please correct the sign convention or the equation and state which form was actually used in training.
minor comments (6)
- [Section IV-C, simulator assumption] The claim that Safety-Gymnasium 'perfectly captures' the operating domain is unqualified and stronger than typical sim-to-real assumptions. Since the case study is the demonstration of the framework, please state this as an explicit assumption in the safety case and clarify that the demonstration is for the simulated operating domain only.
- [Section IV-C, Eq. (3), R0] The reward property R0 is not defined; specify the reward structure and the precise PCTL formula so that it can be checked against SR2.
- [Section III, SR3] The wording 'will not collide with the obstacle on any mission with probability of 0.1' is ambiguous; it should read 'with probability at most 0.1'.
- [Table I] The text refers to blue highlighting for AMLAS-RL changes, but the table is reproduced without color; use a symbol or boldface to mark the changes.
- [Table III] The column header 'Percentage of collision with vase' should say 'obstacle'.
- [Section IV-B, Stage 2] SR1 is described as 'a safety violation,' but it is a mission-success requirement rather than a safety violation; please rephrase.
Circularity Check
Model-checking evidence is partly self-confirming because the DTMC is fitted from the verified policy's own rollouts; the methodology itself is not circular.
-
fitted input called prediction
[Section IV-C (Stage 3, 'Constructing training, testing, and verifying plans for the vehicle example') and Section IV-E (Stage 5, 'Verification of RL-controlled vehicle example'), Eqs. (1)-(3)]
"The transition probabilities will be extracted from running 5000 trials. ... The verification team also conducts 5000 trials to gather data for calculating transition probabilities for the DTMC detailed in stage 3. Table III presents the test and model checking results, which are in agreement of the vehicle's compliance with the safety requirements."
The DTMC's transition probabilities are estimated from rollouts of the very policy under verification. Model checking this DTMC therefore computes the empirical frequencies of that policy's behaviour, re-expressed as reachability probabilities: the reported model-checking values (60.4% goal, 5.8% collision) are built into the fitted model by construction and add no independent evidence for compliance. The 500/250-trial held-out tests are separate, but the formal model-checking pass, offered as verification evidence, is self-confirming.
full rationale
The central contribution is an adaptation of the authors' AMLAS framework to RL; citing [7] is expected and not itself circular because AMLAS-RL is presented as guidance, not as a theorem whose proof is imported by citation. The main circular step is narrower: the Stage 5 DTMC is fitted from 5000 rollouts of the exact policy being verified, making the model-checking probabilities a re-description of that policy's behaviour rather than an independent verification. The case study does, however, also use 500 random and 250 targeted held-out trials, so the demonstration does not rest entirely on the fitted model. Separately, and non-circularly, the paper contains a serious internal inconsistency: Eq. (3) states C1: P[m=2]>=0.6 and C2: P[m=3]<=0.1, while Eq. (2) defines m=2 as obstacle collision and m=3 as reaching the goal, which is the reverse of SR1/SR3; Stage 5 also says results are 'in agreement of the vehicle's compliance' and then reports that targeted testing shows SR1 and SR2 are not satisfied. These are correctness risks, not circularity. The assumption that Safety-Gymnasium 'perfectly captures' the real operating domain is strong but is an unverified premise rather than a circular reduction. Overall, one fitted verification component is partially circular, but the principal claim--a methodological framework--has independent content, so the circularity score is moderate.
Assumptions & free parameters
free parameters (4)
- Reward penalty coefficients =
-0.1 (unsafe zone), -10 (obstacle)
- Unsafe-zone and obstacle thresholds (hat u, hat o) =
0.2 and 0.1
- Discount factor beta =
unspecified
- Trial counts for training and verification =
500 training episodes, 1000 internal trials, 5000 transition-extraction trials, 500 general and 250 targeted…
assumptions (4)
- domain assumption The safety requirements allocated to the RL component at Stage 1 are assumed correct.
- ad hoc to paper SafetyGymnasium perfectly captures the operating domain.
- ad hoc to paper The DTMC abstraction with state s_t=(m_t,e_t,d_o,t,d_u,t) faithfully represents the policy for PCTL verification.
- standard math The MDP framework correctly models the RL problem.
Cite this review
Pith. "Pith review of Assuring the Safety of Reinforcement Learning Components: AMLAS-RL." pith.science (2026). https://pith.science/paper/K5U5KIPU
@misc{pith2026250708848,
author = {Pith},
title = {Pith review of: Assuring the Safety of Reinforcement Learning Components: AMLAS-RL},
year = {2026},
howpublished = {\url{https://pith.science/paper/K5U5KIPU}},
note = {Machine review of arXiv:2507.08848}
}
read the original abstract
The rapid advancement of machine learning (ML) has led to its increasing integration into cyber-physical systems (CPS) across diverse domains. While CPS offer powerful capabilities, incorporating ML components introduces significant safety and assurance challenges. Among ML techniques, reinforcement learning (RL) is particularly suited for CPS due to its capacity to handle complex, dynamic environments where explicit models of interaction between system and environment are unavailable or difficult to construct. However, in safety-critical applications, this learning process must not only be effective but demonstrably safe. Safe-RL methods aim to address this by incorporating safety constraints during learning, yet they fall short in providing systematic assurance across the RL lifecycle. The AMLAS methodology offers structured guidance for assuring the safety of supervised learning components, but it does not directly apply to the unique challenges posed by RL. In this paper, we adapt AMLAS to provide a framework for generating assurance arguments for an RL-enabled system through an iterative process; AMLAS-RL. We demonstrate AMLAS-RL using a running example of a wheeled vehicle tasked with reaching a target goal without collision.
Figures
Reference graph
Works this paper leans on
-
[20]
M. Sivakumar, A. B. Belle, J. Shan, O. Odu, and M. Yuan, “Design of the safety case of the reinforcement learning-enabled component of a quanser autonomous vehicle,” in REW, pp. 57–67, 2024
work page 2024
-
[1]
R. S. Sutton and A. G. Barto, Reinforcement learning - an introduction . Adaptive computation and machine learning, MIT Press, 1998
work page 1998
-
[2]
S. Xiong, D. Liu, Y . Chen, Y . Zhang, and X. Cai, “A deep reinforcement learning approach based energy management strategy for home energy system considering the time-of-use price and real-time control of energy storage system,” Energy Reports, vol. 11, pp. 3501–3508, 2024
work page 2024
-
[3]
Deep reinforcement learning for autonomous driving: A survey,
B. R. Kiran, I. Sobh, V . Talpaert, P. Mannion, A. A. A. Sallab, S. Yo- gamani, and P. P ´erez, “Deep reinforcement learning for autonomous driving: A survey,” 2021
work page 2021
-
[4]
Deep reinforcement learning: An overview,
Y . Li, “Deep reinforcement learning: An overview,” 2018
work page 2018
-
[5]
Challenges of real-world reinforcement learn- ing: definitions, benchmarks and analysis,
G. Dulac-Arnold, N. Levine, D. J. Mankowitz, J. Li, C. Paduraru, S. Gowal, and T. Hester, “Challenges of real-world reinforcement learn- ing: definitions, benchmarks and analysis,” Machine Learning, vol. 110, no. 9, p. 2419–2468, 2021
work page 2021
-
[6]
Explainable reinforcement learning: A survey,
E. Puiutta and E. M. S. P. Veith, “Explainable reinforcement learning: A survey,” ArXiv, vol. abs/2005.06247, 2020
arXiv 2005
-
[7]
Guidance on the assurance of machine learning in autonomous systems (amlas),
R. Hawkins, C. Paterson, C. Picardi, Y . Jia, R. Calinescu, and I. Habli, “Guidance on the assurance of machine learning in autonomous systems (amlas),” arXiv preprint arXiv:2102.01564 , 2021
arXiv 2021
Show all 21 references
-
[8]
Uther, Markov Decision Processes , pp
W. Uther, Markov Decision Processes , pp. 642–646. Springer, 2010
2010
-
[9]
A review of safe reinforcement learning: Methods, theories, and applica- tions,
S. Gu, L. Yang, Y . Du, G. Chen, F. Walter, J. Wang, and A. Knoll, “A review of safe reinforcement learning: Methods, theories, and applica- tions,” IEEE Transactions on Pattern Analysis and Machine Intelligence, vol. 46, no. 12, pp. 11216–11235, 2024
2024
-
[10]
Safe reinforcement learning for autonomous vehicles through parallel constrained policy optimization,
L. Wen, J. Duan, S. E. Li, S. Xu, and H. Peng, “Safe reinforcement learning for autonomous vehicles through parallel constrained policy optimization,” in ITSC, pp. 1–7, 2020
2020
-
[11]
Reinforcement learning in healthcare: A survey,
C. Yu, J. Liu, S. Nemati, and G. Yin, “Reinforcement learning in healthcare: A survey,” ACM CSUR, vol. 55, no. 1, pp. 1–36, 2021
2021
-
[12]
Safe learning in robotics: From learning-based control to safe reinforcement learning,
L. Brunke, M. Greeff, A. W. Hall, Z. Yuan, S. Zhou, J. Panerati, and A. P. Schoellig, “Safe learning in robotics: From learning-based control to safe reinforcement learning,” Annual Review of Control, Robotics, and Autonomous Systems , vol. 5, no. 1, pp. 411–444, 2022
2022
-
[13]
An analysis of iso 26262: Using machine learning safely in automotive software,
R. Salay, R. Queiroz, and K. Czarnecki, “An analysis of iso 26262: Using machine learning safely in automotive software,” arXiv preprint arXiv:1709.02435, 2017
2017 arXiv
-
[14]
Making the case for safety of machine learning in highly automated driving,
S. Burton, L. Gauerhof, and C. Heinzemann, “Making the case for safety of machine learning in highly automated driving,” inSAFECOMP, pp. 5–16, 2017
2017
-
[15]
Can you trust your agent? the effect of out-of-distribution detection on the safety of reinforcement learning systems,
T. Haider, K. Roscher, B. Herd, F. Schmoeller Roza, and S. Burton, “Can you trust your agent? the effect of out-of-distribution detection on the safety of reinforcement learning systems,” in Proceedings of the 39th ACM/SIGAPP Symposium on Applied Computing , pp. 1569–1578, 2024
2024
-
[16]
Safety-driven design of machine learning for sepsis treatment,
Y . Jia, T. Lawton, J. Burden, J. McDermid, and I. Habli, “Safety-driven design of machine learning for sepsis treatment,” Journal of Biomedical Informatics, vol. 117, p. 103762, 2021
2021
-
[17]
Assuring the machine learning lifecycle: Desiderata, methods, and challenges,
R. Ashmore, R. Calinescu, and C. Paterson, “Assuring the machine learning lifecycle: Desiderata, methods, and challenges,” ACM CSUR , vol. 54, no. 5, pp. 1–39, 2021
2021
-
[18]
Defining and characterizing reward gaming,
J. Skalse, N. Howe, D. Krasheninnikov, and D. Krueger, “Defining and characterizing reward gaming,” Advances in Neural Information Processing Systems, vol. 35, pp. 9460–9471, 2022
2022
-
[19]
What is acceptably safe for reinforcement learning?,
J. Bragg and I. Habli, “What is acceptably safe for reinforcement learning?,” in SAFECOMP, pp. 418–430, 2018
2018
-
[21]
Reliable safety decision-making for autonomous vehicles: a safety assurance reinforce- ment learning,
Y . Niu, Y . Wang, M. Xiao, W. Zhu, and T. W. and, “Reliable safety decision-making for autonomous vehicles: a safety assurance reinforce- ment learning,” Transportmetrica B, vol. 13, no. 1, p. 2439997, 2025
2025
Reviewed August 6, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.