Test Where Decisions Matter: Importance-driven Testing for Deep Reinforcement Learning

Authors: stefan  pranger
hana  chockler
martin  tappler
bettina  könighofer
Venue: NeurIPS_cc_2024_Conference
Published: 2024-05-15 15:15:17

Abstract: In many Deep Reinforcement Learning (RL) problems, decisions in a trained policy vary in significance for the expected safety and performance of the policy. Since RL policies are very complex, testing efforts should concentrate on states in which the agent's decisions have the highest impact on the expected outcome. In this paper, we propose a novel model-based method to rigorously compute a ranking of state importance across the entire state space. We then focus our testing efforts on the highest-ranked states. In this paper, we focus on testing for safety. However, the proposed methods can be easily adapted to test for performance. In each iteration, our testing framework computes optimistic and pessimistic safety estimates. These estimates provide lower and upper bounds on the expected outcomes of the policy execution across all modeled states in the state space. Our approach divides the state space into safe and unsafe regions upon convergence, providing clear insights into the policy's weaknesses. Two important properties characterize our approach. (1) Optimal Test-Case Selection: At any time in the testing process, our approach evaluates the policy in the states that are most critical for safety. (2) Guaranteed Safety: Our approach can provide formal verification guarantees over the entire state space by sampling only a fraction of the policy. Any safety properties assured by the pessimistic estimate are formally proven to hold for the policy. We provide a detailed evaluation of our framework on several examples, showing that our method discovers unsafe policy behavior with low testing effort.

Main paper: 
 introduction: 
 Deep reinforcement learning (RL) [1] is a powerful method for training policies that complete tasks in complex environments. Due to the high potential of RL in safety-critical domains, such as autonomous driving [2] , ensuring the reliability of its safety-critical properties is becoming increasingly vital. Formal verification provides provable correctness guarantees [3] . However, the most significant challenge in the formal verification of RL policies is scalability, which limits its current applicability [4] . As for conventional software, a complete safety evaluation by exhaustively testing a policy's decisions is infeasible. Hence, it is necessary to establish as much confidence as possible in a policy with a limited testing budget. We propose a novel model-based testing framework for RL policies, which tests policies in the states where their decisions matter most. We follow the insights from Chockler et al. [5] that not all decisions hold equal significance on the expected safety and performance of a policy. Decisions in certain states may have a significant impact on the overall expected outcome of the policy, while in other states, the impact may not be as severe or critical. The core of our algorithm is a ranking of the importance of states of the environment. This ranking is based on the difference that the decision in a particular state makes on the expected overall performance (e.g., accumulated reward) or safety of the policy. For lack of space, we focus on safety from here on. The proposed method can easily be adapted to evaluate the agent's performance, which we discuss in Appendix D.Figure 1 outlines our algorithm. The inputs to our algorithm are a model of the environment in the form of a Markov decision process [6] , a formal safety specification φ, and an RL agent in the form of a deterministic policy. In each iteration, our algorithm computes optimistic and pessimistic estimates, which provide lower and upper bounds for the expected probability of satisfying the safety specification over all possible policies. The algorithm terminates if the maximal difference between the estimates gets below some threshold or a maximal number of executed test cases is reached. As long as the stopping criterion is not met, the algorithm computes an importance ranking of the states. The higher the rank of a state, the more influence the decision in that state has for satisfying or violating the safety specification. Next, the most important decisions of the policy are sampled and used to fix the decisions, thus restricting the MDP. The algorithm continues with the restricted MDP to iteratively refine the estimates. Our testing framework can be modified through an optional step by clustering the highly ranked states. A fraction of test cases is then uniformly selected from the individual clusters. The intuition behind clustering is that the agent is likely to behave similarly in comparable situations. Following this intuition, we mark all states in a cluster as safe if all tested states of this cluster are verified to be safe. Otherwise, the entire cluster is marked as unsafe. This increases the scalability of our testing approach since only a fraction of each cluster needs to be tested for deriving test verdicts for all states in the cluster. However, since not all decisions in a cluster are sampled, unsafe policy behavior can be missed.Our algorithm provides the following benefits:• Optimal Test-Case Selection: At any time in the testing process, our approach evaluates the policy in the states that are most critical for safety. • Guaranteed Safety: A pessimistic estimate provides a formal verification guarantee: under the given model it is guaranteed that if the pessimistic estimate for a given state satisfies the testing criteria, then the agent's policy is formally verified from that state. • Highlighting the most important decisions is a central technique in explainable AI [7, 8] . We provide a rigorous method to compute an importance ranking. Simpler policies that only use the top-ranked decisions can help understand the policy's decision-making [5] . • The iterative nature of our approach can be used in a debugging process to construct a safety frontier: if a sampled decision in a certain state is evaluated to be unsafe, the next ranking iteration assigns higher importance to the predecessor states to be tested next. Thus, the unsafe region around a safety hazard grows until it reveals all states where the policy behaves unsafely. • Upon convergence, our approach partitions the state space into safe and unsafe regions. The identified unsafe regions offer interpretable insights into the policy's current weaknesses.Evaluation of RL policies. Off-policy evaluation (OPE) [9, 10, 11] aims to estimate the expected performance of a newly trained policy by using executions of a previously trained policy. In contrast, our approach estimates the performance of the policy under test by computing the best-possible (optimistic) estimate and the worst-possible (pessimistic) estimate in the current MDP. In contrast to OPE, our framework provides formal verification guarantees over the entire state space: any safety property assured by the pessimistic estimate is formally proven to hold. Several recent works proposed evaluation strategies to analyze RL policies [12] , by adapting software testing techniques to RL. Various approaches apply fuzz or search-based testing as a basis to find safety-critical situations in the black-box environment [13, 14, 15, 16] , in which to test the policy. Most efforts of the testing community focused on selecting test cases that falsify safety with high probability [15, 17] . These methods effectively reveal unsafe behavior, but they do not provide safety assurance from non-failing tests, as they lack proper notions of coverage. In contrast, our testing approach is model-based.Model-based testing of probabilistic systems was proposed in [18] . To the best of our knowledge, there is no model-based testing approach for RL policies with formalized criteria of completeness.That is, we are the first to propose safety estimates with formal interpretations which form the basis of our test-case generation.Model-based formal methods for model-free RL. Several recent works have proposed approaches for developing RL controllers by combining model-based formal methods and model-free RL. The appeal of this combination lies in the strengths of each approach: model-based methods offer formal safety and correctness guarantees, while model-free RL demonstrates superior scalability and yields high-performance controllers by learning from the full-order system dynamics [19, ?] . Most of the existing work in this area addresses the problem of safe exploration in RL [20, 21] . To the best of our knowledge, our work is the first to employ similar techniques for analyzing a trained policy.Importance ranking. Ranking policy decisions has been proposed for explaining and simplifying RL policies. In [5] , the ranking is based on statistical fault localization computed on a set of executions of the original policy and its small perturbations. A continuation of this work [22] uses an average treatment effect to rank policy decisions. In contrast, we provide a rigorous method to compute the importance ranking. Our estimates consider any possible behavior of the policy over the entire state space. Thus, the estimates provide strong verification guarantees. Similarly to ranking policy decisions, [23] rank the importance of individual neurons in a network to assess coverage of a given test set.Question: Do the main claims made in the abstract and introduction accurately reflect the paper's contributions and scope? Answer: [Yes] Justification: We present the first model-based testing approach that gives formal verification guarantees. We discuss the method in detail and provide a detailed evaluation in the form of several experiments. Guidelines:• The answer NA means that the abstract and introduction do not include the claims made in the paper. • The abstract and/or introduction should clearly state the claims made, including the contributions made in the paper and important assumptions and limitations. A No or NA answer to this question will not be perceived well by the reviewers. • The claims made should match theoretical and experimental results, and reflect how much the results can be expected to generalize to other settings. • It is fine to include aspirational goals as motivation as long as it is clear that these goals are not attained by the paper. 
background: 
 Markov Decision Process. A Markov decision process (MDP) [24] M = (S, A, P, µ) is a tuple with a finite state set S, a finite set A = {a 1 . . . , a n } of actions, a probabilistic transition function P : S × A × S → [0, 1], and a probability distribution of initial states µ : S → [0, 1]. An execution (or path) is a finite or infinite sequence ρ = s 0 , a 0 , s 1 , a 1 . . . with P(s i , a i , s i+1 ) > 0 and µ(s 0 ) > 0.A (memoryless deterministic) policy π : S → A is a function mapping states to actions. Π denotes the set of all memoryless deterministic policies. Applying π to an MDP M induces a Markov chain (MC) M π . An execution in M π is a sequence ρ = s 0 , s 1 , s 2 , . . . with P(s i , π(s i ), s i+1 ) > 0. P π s denotes the unique probability measure of M π over infinite executions starting in s.Probabilistic Model Checking. Probabilistic model checking [3] computes the probabilities of satisfying a temporal-logic formula φ over a finite or infinite horizon. We define the properties below with a bound n. For the unbounded horizon, n = ∞. For a given MDP M, a policy π, and a property φ in Computation Tree Logic (CTL) [3] , model checking computes the following probabilities:• P M π ,φ : S × N → [0, 1]is the expected probability to satisfy φ state s ∈ S within n steps in M π .• P max M,φ (s, n) = max π∈Π P M π ,φ (s, n) is the maximal expected probability over all policies in Π from a state s within n steps.• P min M,φ (s, n) = min π∈Π P M π ,φ (s, n) is the minimal expected probability over all policies in Π from a state s within n steps.For the remainder of this paper, let φ be a formula in the safety fragment of CTL. Using φ and a user-defined safety threshold δ φ , we define safety objectives as follows:Algorithm 1 Importance-driven model-based testing (IMT) Input: MDP M, policy π, safety objective ⟨φ, δ φ ⟩ Parameters: # samples m, safety threshold δ φ , minimal difference ε φ Output: failure states S f ⊆ S, safe states S s ⊆ S, estimates e opt : S → R and e pes : S → R1: M (0) ← M; S u ← S; S f ← ∅; S s ← ∅; i ← 0 2: loop 3:e opt , e pes ← computeEstimates(M (i) ) 4: S s ← S s ∪ {s ∈ S u | e pes (s) ≥ δ φ } 5: S f ← S f ∪ {s ∈ S u | e opt (s) < δ φ } 6: S u ← S u \ {s ∈ S u | e opt (s) < δ φ ∨ e pes (s) ≥ δ φ } 7: if [max s (e opt (s) -e pes (s)) < ε φ ] then 8:S rank ←[computeRanking(M (i) , m)] 11: {(s 1 , a 1 ) . . . (s m , a m )} ← samplePolicy(π, S rank ) 12: M (i+1) ← restrictMDP(M (i) , {(s 1 , a 1 ) . . . (s m , a m )}) 13:i ← i + 1 14: end loop 15: return S f , S s , e opt , e pes Definition 2.1 (Safety objective). Given an MDP M = (S, A, P, µ), a safety property φ, and a threshold δ φ ∈ [0, 1]. A safety objective is a tuple ⟨φ, δ φ ⟩. A policy π satisfies ⟨φ, δ φ ⟩ from a given state s ∈ S within n steps ifP M π ,φ (s, n) ≥ δ φ .Reinforcement Learning. An RL [1] agent learns a task via interactions with an unknown environment modeled by an MDP M with an associated reward function R : S → R. In each state s ∈ S, the agent chooses an action a ∈ A, the environment then moves to a state s ′ with probability P(s, a, s ′ ). The return ret ρ of an execution ρ is the discounted cumulative reward defined by ret ρ = Σ ∞ t=0 γ t R(s t ), using the discount factor γ ∈ [0, 1]. The objective of the agent is to learn a deterministic memoryless optimal policy π ⋆ that maximizes the expectation of the return.Question: Does the paper discuss the limitations of the work performed by the authors?Answer: [Yes]Justification: The method currently assumes that the policies under test are determinisitic, as stated in the introduction. We will extend IMT to test stochastic policies in future work.Guidelines:• The answer NA means that the paper has no limitation while the answer No means that the paper has limitations, but those are not discussed in the paper. • The authors are encouraged to create a separate "Limitations" section in their paper.• The paper should point out any strong assumptions and how robust the results are to violations of these assumptions (e.g., independence assumptions, noiseless settings, model well-specification, asymptotic approximations only holding locally). The authors should reflect on how these assumptions might be violated in practice and what the implications would be. • The authors should reflect on the scope of the claims made, e.g., if the approach was only tested on a few datasets or with a few runs. In general, empirical results often depend on implicit assumptions, which should be articulated. • The authors should reflect on the factors that influence the performance of the approach.For example, a facial recognition algorithm may perform poorly when image resolution is low or images are taken in low lighting. Or a speech-to-text system might not be used reliably to provide closed captions for online lectures because it fails to handle technical jargon. • The authors should discuss the computational efficiency of the proposed algorithms and how they scale with dataset size. • If applicable, the authors should discuss possible limitations of their approach to address problems of privacy and fairness. • While the authors might fear that complete honesty about limitations might be used by reviewers as grounds for rejection, a worse outcome might be that reviewers discover limitations that aren't acknowledged in the paper. The authors should use their best judgment and recognize that individual actions in favor of transparency play an important role in developing norms that preserve the integrity of the community. Reviewers will be specifically instructed to not penalize honesty concerning limitations. 
importance-driven testing for rl: 
 In this section, we will describe our framework for importance-driven model-based testing, which we abbreviate with IMT. An overview of our algorithm is depicted in Fig. 1 . Its central elements are the computation of the estimates and the importance ranking that guides the selection of the test cases. In Sec. 3.1 we discuss IMT in detail, and in Sec.3.2 we discuss its extension with clustering.Alg. 1 gives the pseudo-code of our approach for importance-driven safety testing. Our algorithm evaluates a policy π with respect to a safety objective ⟨φ, δ φ ⟩ over a horizon of n steps (for the unbounded horizon, n = ∞). The algorithm takes as input an MDP M = (S, A, P, µ), a policy under test π : S → A, and a safety objective ⟨φ, δ φ ⟩. It returns as result a classification of states into safe and failure states (S s and S f , respectively), and the optimistic and pessimistic estimates for all states in the state space (e opt : S → [0, 1] and e pes : S → [0, 1], respectively), which are derived as the expected maximal and minimal probability of satisfying the safety objective ⟨φ, δ φ ⟩.Safety estimates. In Line 3, IMT computes the safety estimates for the current (restricted) MDP M (i) . The optimistic estimate e opt (s, n) is the maximal expected probability of satisfying φ for an execution in M (i) from a given state s within a n steps quantified over all policies. Similarly, the pessimistic estimate e pes (s, n) is the minimal expected probability of satisfying φ.This yields the following definition: Definition 3.1 (Safety estimates). For a given MDP M = (S, A, P, µ), a given safety property φ, and a given number of n steps, the optimistic and pessimistic safety estimate e opt , e pes : S×N → [0, 1] are defined as follows:∀s ∈ S : e opt (s, n) = P max M,φ (s, n), and ∀s ∈ S : e pes (s, n) = P min M,φ (s, n). For a state action pair (s, a) and a bound n, the maximal expected probability of satisfying φ from a state s after executing a is ∀s ∈ S, ∀a ∈ A : e opt (s, a, n) = s ′ ∈S (P(s, a, s ′ ) • e opt (s ′ , n -1)).Based on the estimates, the algorithm classifies undetermined states from S u as verified safe and adds them to S s or classifies them as unsafe and adds to the set of failure states S f (Lines 4 and 5). A state s ∈ S satisfies the safety objective ⟨φ, δ φ ⟩ if e pes (s, n) ≥ δ φ . Note that the pessimistic safety estimate is achieved in an execution that chooses the most unsafe actions in each non-restricted state. Thus, if for a given state e pes (s, n) ≥ δ φ , then P M π ,φ (s, n) ≥ δ φ holds. This highlights the strength of our algorithm: by assuming the worst policy behavior in unrestricted states, we provide verification results without sampling the policy in every state. A state s ∈ S is unsafe if e opt (s, n) ≤ δ φ . The optimistic safety probability is achieved in an execution that chooses the safest action in each non-restricted state. Thus, if e opt (s, n) ≤ δ φ , the policy π cannot pick actions that would yield higher probabilities of satisfying φ from s.Stopping criteria. In Line 7, the stopping criterion is defined via a user-defined threshold ε φ for the minimal difference between the estimates. IMT stops if the difference between the optimistic and the pessimistic safety estimate is below the threshold ε φ for all states, i.e., max s [e opt (s, n)-e pes (s, n)] < ε φ . For small values of e pes , further restricting the MDP would only marginally change the testing results. Otherwise, IMT continues with sampling the policy and restricting the MDP, as the optimistic and pessimistic estimates are sufficiently different. As an alternative stopping criterion, a user could also define a total testing budget.Importance ranking. In each iteration, IMT computes an importance ranking over all states in the current MDP M (i) (Line 10). In the following steps, the m most important decisions of the policy are sampled and used to restrict M (i) , which results in refined estimates. The rank of a state s reflects the maximal difference that a decision can have on satisfying the safety objective. Definition 3.2. (Importance ranking for safety.) Given an MDP M = (S, A, P, µ), a safety property φ, and a bound n, the importance ranking rank : S × N → R is given as the maximal difference between the optimistic estimates with respect to the available actions:∀s ∈ S : rank(s, n) = max a,a ′ ∈A (e opt (s, a, n) -e opt (s, a ′ , n)).For the importance ranking, we consider the impact of decisions on the optimistic estimates. That is, a state s is important if, for some actions a and a ′ , it holds that the expected maximal safety probability that can still be achieved after executing a from s is considerably larger than the probability that can be obtained after executing a ′ from s. The importance ranking returns the set of states S rank of the m highest ranked states of M (i) .Sampling the policy. In Line 11, IMT samples the decisions of the policy in the highest ranked states s ∈ S rank of M (i) . This results in the set Γ = {(s 1 , a 1 ), . . . , (s m , a m )} with a i = π(s i ).Restricting the MDP. In Line 12, our algorithm restricts M (i) according to the sampled policy's decisions, i.e., actions not chosen by π in the sampled states are removed from M (i) . Given the current MDP M (i) = (S, A, P (i) , µ) and the sampled state-action pairs Γ, the restricted MDP M (i+1) = (S, A, P (i+1) , µ) has the following probabilistic transition function:∀s, s ′ ∈ S ∀a ∈ A : P (i+1) (s, a, s ′ ) = P (i) (s, a, s ′ ) s / ∈ S rank or (s, a) ∈ Γ 0else. In every iteration of the algorithm, more actions in the MDP model become fixed to the actions chosen by π, leading to more accurate safety estimates for π, i.e., e pes (s, n) monotonically increases and e opt (s, n) monotonically decreases, for all s ∈ S.Theorem 1. The algorithm IMT as described in Alg. 1 terminates.Proof Sketch. For a fully restricted MDP, for any s ∈ S, for any n, it holds that e opt (s, n) = e pes (s, n). This holds because a fully restricted MDP is a Markov chain that describes the policy completely. Hence the estimates are the same.Input: M, π, ⟨φ, δ φ ⟩ Parameters: importance threshold δ i , testing fraction κ, testing horizon n, δ φ , ε φ Output: S f ⊆ S, S s ⊆ S, e opt : S → R, e pes : S → R 1: // Line 1 -8 are as in Alg. 19: S rank ←[computeRanking(M (i) )] 10: C ←[clusterStates(S rank , δ i )] 11: {(c 1 , v 1 ) . . . (c |C| , v |C| )} ← executeTests(π, C, κ) 12: M (i+1) ← restrictMDP(M (i) , {(c 1 , v 1 ) . . . (c |C| , v |C| )})13: // Line 12 -14 are as in Alg. 1In this section, we extend IMT by introducing clustering in Alg. 1. Fig. 1 shows the high-level view of IMT including clustering. For problems with very large state spaces, sampling the agents in all highly-ranked states becomes too expensive. To tackle this scalability issue, we propose to cluster similar states and test only a fixed fraction of the states in each cluster. By doing so, we balance the trade-off between accuracy and scalability: The fewer states from a cluster are tested, the higher the scalability of our testing approach. However, the likelihood that some unsafe behavior of the agent remains undetected increases. Clustering offers the additional advantage that similar states are grouped. Under the assumption that the agent implements a policy that selects the same action in similar situations, IMT most likely detects unsafe behavior by sampling a large enough fraction of each cluster. Alg. 2 states the changes in the pseudo-code for IMT with clustering.Clustering. In Line 10, after computing the importance ranking, IMT performs clustering on all states with an importance ranking value greater than some bound δ i = rank(s.n). States are clustered according to their state information and their importance value, i.e., we compute a clustering assignment cl : S × [δ i , 1] → N. This gives a partitioning of S rank into sets of states sharing the same cluster label. Note that any off-the-shelf clustering algorithm can be used to compute the clusters of states. 1Executing tests. In Line 11, the behavior of the policy in the clustered states is evaluated. From each cluster, a fixed percentage κ of states is randomly selected to be tested. To test a state s, the agent is executed from s for a certain number of steps. If the safety objective is violated during the execution, s is marked as unsafe and added to S f . Based on the testing results of the individual states we assign verdicts v j to the clusters proposing a conservative evaluation of safety. Each cluster c j with a tested state s ∈ S f is assigned a failing verdict v j = FAIL. Consequently, all states s ∈ c j are marked unsafe and added to S f . Conversely, if a cluster c j does not contain a single tested state from S f , it is assigned a safe verdict v j = SAFE, and its states are added to S s .Restricting the MDP. In Line 12, IMT restricts M (i) in all states that belong to a cluster c j by turning the states into sink states. Additionally, if a cluster c j has the verdict v j = FAIL, all states are considered a safety violation.The effects of clustering. Since IMT with clustering only tests a fraction κ of each individual cluster, the size and quality of the computed clusters affect the testing process. Clusters that are too large can lead to unnecessary testing efforts, as safe behavior might be deemed unsafe due to conservative evaluation. Additionally, if a cluster contains states that are not sufficiently similar, IMT with clustering may fail to detect unsafe behavior in the policy.Complexity Analysis. We discuss the computational complexity of a single iteration of IMT. The safety estimates are computed via value iteration in O(poly(size(M)) • n), with n being the bound for the objective [3] . The computation of the ranking only requires sorting of the computed estimates and thus requires O(|S| log |S|) time. The subsequent restriction of M is linear in the number of actions present in M, i.e. O(|S| • |A|). Lastly, the complexity of sampling the policy is dependent on the network architecture and the costs for clustering the state space depend on the chosen algorithm. Question: For each theoretical result, does the paper provide the full set of assumptions and a complete (and correct) proof?Answer: [NA] Justification: -Guidelines:• The answer NA means that the paper does not include theoretical results.• All the theorems, formulas, and proofs in the paper should be numbered and crossreferenced. • All assumptions should be clearly stated or referenced in the statement of any theorems.• The proofs can either appear in the main paper or the supplemental material, but if they appear in the supplemental material, the authors are encouraged to provide a short proof sketch to provide intuition. • Inversely, any informal proof provided in the core of the paper should be complemented by formal proofs provided in appendix or supplemental material. • Theorems and Lemmas that the proof relies upon should be properly referenced. 
experimental evaluation: 
 All details of the experimental setup can be found in Appendix A. We provide the implementation and tested policies as supplementary material. We compare IMT with our model-based approach without importance ranking (MT) and model-free random testing (RT) as a baseline. Thus, in MT, our algorithm restricts the MDP by the sampled agent's decisions and computes e opt and e pes to provide evaluation results on the entire state space but samples the policy randomly. For RT, the policy is executed from random states for a certain number of steps. Any violation of the evaluation objective is reported. We report the runtimes averaged over 10 runs for each experiment in seconds, unless indicated otherwise, as total time(± STDev) / total time for computing the estimates(± STDev) / total time for querying the policy (± STDev).We performed our first experiment in the Farama Minigrid environment [26] . A description of the environment and the RL training parameters are given in Appendix B. The Gridworld is depicted in Fig. 2a . The agent has to reach the green goal without touching the lava. The lava is surrounded by slippery tiles, stepping on which carries a predefined probability of slipping into lava. The size of the state space is |S| = 7 × 7 × 4 = 196, with 49 cells multiplied by 4 for the different orientations of the agent. The safety objective φ requires the agent to not enter the lava with a probability δ φ ≥ 1.0.RL training parameters. We trained policies π 1 and π 2 by utilizing a DQN. We used a sparse reward function with a reward of 1 for reaching the green goal and -1 for falling into the lava. We trained π 1 using a fixed initial state and π 2 using initial states uniformly sampled from S.IMT/MT parameters. We used a horizon of n = ∞, a minimal difference of ε φ = 0.05, a number of samples per iteration of m = 10. For IMT, no states with a ranking value close to 0 were sampled.Visualizing IMT. Fig. 2b visualizes the iterations of our IMT algorithm when evaluating π 1 . Per iteration, the picture on the top visualizes the highest-ranked states, with the intensity of the color capturing the ranking. Note that a state represents the (x, y)-coordinates of the grid and the orientation of the agent and is thus visualized as a triangle. Per iteration, IMT samples π 1 in the highest-ranked states (blue triangles) and computes the estimates. The pictures on the bottom show the updated sets of verified states after computing the estimates: S s is visualized in green, S f in red, and S u in blue. Brighter colors represent states in which the decisions of π 1 were sampled. IMT terminates after 5 iterations when evaluating π 1 . Note that the evaluation iteratively reveals the area in which π 1 violates safety. Fig. 2c visualizes the evaluation of the policy π 2 . IMT terminates after a single iteration and positively verifies π 2 in all states in which the safety objective can be fulfilled.Evaluation results. Thus, IMT provides complete verification results of π 1 over the entire state space with only 33 policy samples. In contrast, on average, MT verifies the entire state space after sampling the agent's decisions almost on the entire state space. Fig. 3b plots the values for the optimistic (green) and pessimistic (red) safety estimates for IMT (solid lines) and MT (dashed lines), averaged over all states, which show that the averaged estimates of IMT tighten faster than for MT. Finally, we report the findings of RT in Fig. 3c when executing a test case for 10 steps. The results show the clear advantage of exploiting our testing approach. By utilizing testing with model checking, we obtain verification results on the entire state space in contrast to RT which is only able to report a small number of states from which φ is violated.Runtimes. The costs for computing the estimates per iteration are in the range of milliseconds. The total runtime to verify π 1 was 12.29(±0. For the second set of experiments, we test policies computed for drone navigation by Badings et al. [27] . We refer to this work for details regarding the policy and environment, which is illustrated in. Fig. 4a . The task of the drone is to navigate to the goal location (green box). The safety objective φ states that the drone must not collide with a building (grey boxes) and must stay within the boundaries with a probability δ φ ≥ 0.95. The state space |S| comprises 25.517 states. The wind in the simulation affects the drone, which is modeled stochastically and controlled through the parameter η.IMT parameters. We used m = 500 samples per iteration, n, and ε φ , as above.Evaluation results. Our testing approach IMT/MT was able to verify control policies computed under five difference noise settings of η ∈ {0.1, 0.25, 0.5, 0.75, 1.0} over the entire state space. Fig. 4c gives the number of verified unsafe states per policy. All policies with η < 0.75 are verified safe in all states from which it is possible to behave safely (light red bars indicate states from which safety violations cannot be avoided). Even though the policies have been specially designed to be safe, IMT was able to find safety violations for policies with η ≥ 0.75. The policies showed unsafe behavior in 15 or 775 additional states, respectively, for which safe behavior would have been possible (dark bars). Fig. 4b shows the verification results for IMT and MT for η = 0.1. The test results for the policies with η ≥ 0.25 can be found in Appendix C. As before, adding importance-ranking for sampling the policy decreases the number of required samples to verify the policy. We performed RT We have evaluated IMT with clustering, IMTc for short, by testing a learned policy for Atari Skiing [28] . In Skiing, the player controls the tilt of the skies to reach the goal as fast as possible.The safety objective φ is to avoid collisions with trees and poles with a probability of δ φ ≥ 1.0. IMT parameters. We used a time horizon of n = 200, a minimal difference of ϵ φ = 0.05, and a fraction κ = 0.2 of tested states per cluster. The clusters have been computed using k-means for states with δ i > 0.8 with a k to create average cluster sizes of ζ ∈ {25, 50, 100, 150}.Visualizing IMT. Fig. 5 visualizes the initial clustering of the highest-ranked states and the iterations of IMTc with an average cluster size of ζ = 25. We show the results for states in which tilt = 4, i.e. the skier is aligned with the slope, and v = 4. The visualization for different values of tilt and v can be found in Appendix E. We depict states from which the policy has been tested with lighter colors. Darker colors depict implied results.The results show that the agent robustly learned to avoid collisions (it avoids any collision as long as it is not placed too close to an obstacle).Evaluation results. We evaluated IMTc using different values for ζ and compared it with IMT, i.e. ζ = 1, and RT. Fig. 6a plots the total number of failure states S f and safe states S s for the whole state space over the number of executed test cases for different values of ζ. The green curves (left to right) plot the results for S s using the cluster sizes {25, 50, 100, 150, 1}, the red curves for S f accordingly. For comparison, we executed RT 10 times and plot the average number of failing (orange dashed) and safe test cases (teal dashed), where the shaded areas show the minimal and maximal values. The results show that IMTc terminates faster with smaller cluster sizes. Larger cluster sizes overapproximate unsafe regions more heavily. Thus, more testing effort is needed around the unsafe regions in the subsequent iterations. However, all instances of IMTc reduce the testing budget required compared to IMT, which was to be expected since only 20% of the states of each cluster were tested. These facts are also underlined by Figures 6b and 6c , which show the number of safe and failed tests, and the implied verdicts for cluster states in the final iteration, respectively. Fig. 6b shows that clustering heavily increases the scalability of our approach since it lowers the needed testing budget by up to a factor of 5 for ζ = 25.Runtimes. The runtimes for evaluating the policy, excluding the time needed to render the testing results, for ζ ∈ {25, 50, 100, 150} are 86 minutes (±8.3) / 40 (±4.5) / 8.5 (±2.3). Evaluating the policy for ζ = 1 took 127 minutes / 59 (±7.3) / 35.9 (±4.4).Question: Does the paper fully disclose all the information needed to reproduce the main experimental results of the paper to the extent that it affects the main claims and/or conclusions of the paper (regardless of whether the code and data are provided or not)?Answer: [Yes] Justification: We provide a docker image containing all the necessary data and code to reproduce the experiments. The README containing instructions on how to reproduce the results is available via https://figshare.com/s/b8dfb68930da2593749c and the docker image can be downloaded from: https://figshare.com/s/011d813f0b4ad260db5e. Guidelines:• The answer NA means that the paper does not include experiments.• If the paper includes experiments, a No answer to this question will not be perceived well by the reviewers: Making the paper reproducible is important, regardless of whether the code and data are provided or not. • If the contribution is a dataset and/or model, the authors should describe the steps taken to make their results reproducible or verifiable. • Depending on the contribution, reproducibility can be accomplished in various ways.For example, if the contribution is a novel architecture, describing the architecture fully might suffice, or if the contribution is a specific model and empirical evaluation, it may be necessary to either make it possible for others to replicate the model with the same dataset, or provide access to the model. In general. releasing code and data is often one good way to accomplish this, but reproducibility can also be provided via detailed instructions for how to replicate the results, access to a hosted model (e.g., in the case of a large language model), releasing of a model checkpoint, or other means that are appropriate to the research performed. • While NeurIPS does not require releasing code, the conference does require all submissions to provide some reasonable avenue for reproducibility, which may depend on the nature of the contribution. , with an open-source dataset or instructions for how to construct the dataset). (d) We recognize that reproducibility may be tricky in some cases, in which case authors are welcome to describe the particular way they provide for reproducibility.In the case of closed-source models, it may be that access to the model is limited in some way (e.g., to registered users), but it should be possible for other researchers to have some path to reproducing or verifying the results. • If the authors answer No, they should explain the special circumstances that require a deviation from the Code of Ethics. • The authors should make sure to preserve anonymity (e.g., if there is a special consideration due to laws or regulations in their jurisdiction). 10. Broader Impacts Question: Does the paper discuss both potential positive societal impacts and negative societal impacts of the work performed? Answer: [NA] Justification: -Guidelines:• The answer NA means that there is no societal impact of the work performed.• If the authors answer NA or No, they should explain why their work has no societal impact or why the paper does not address societal impact. • Examples of negative societal impacts include potential malicious or unintended uses (e.g., disinformation, generating fake profiles, surveillance), fairness considerations (e.g., deployment of technologies that could make decisions that unfairly impact specific groups), privacy considerations, and security considerations. • The conference expects that many papers will be foundational research and not tied to particular applications, let alone deployments. However, if there is a direct path to any negative applications, the authors should point it out. For example, it is legitimate to point out that an improvement in the quality of generative models could be used to generate deepfakes for disinformation. On the other hand, it is not needed to point out that a generic algorithm for optimizing neural networks could enable people to train models that generate Deepfakes faster. • The authors should consider possible harms that could arise when the technology is being used as intended and functioning correctly, harms that could arise when the technology is being used as intended but gives incorrect results, and harms following from (intentional or unintentional) misuse of the technology.• The answer NA means that the paper does not release new assets.• Researchers should communicate the details of the dataset/code/model as part of their submissions via structured templates. This includes details about training, license, limitations, etc. • The paper should discuss whether and how consent was obtained from people whose asset is used. • We recognize that the procedures for this may vary significantly between institutions and locations, and we expect authors to adhere to the NeurIPS Code of Ethics and the guidelines for their institution. • For initial submissions, do not include any information that would break anonymity (if applicable), such as the institution conducting the review. 
conclusion & future work: 
 We presented importance-driven testing for RL agents. The process iteratively (1) ranks the states based on the influence of the agent's decisions on the expected overall safety, (2) samples the DRL policy under test from the ranking, and (3) restricts the model of the environment. By utilizing probabilistic model checking, our algorithm provides upper and lower bounds on the expected outcomes of the policy execution across all modeled states in the state space. These estimates provide formal guarantees about the violation or compliance of the policy to formal properties. We presented an extension of the basic algorithm by introducing clustering to increase scalability. In future work, we will adapt IMT to allow the testing of stochastic policies by adapting the restriction of the MDP and the verification procedure. We will Furthermore, we will introduce several abstraction techniques to further increase the scalability of our approach. Finally, we will use recently proposed approaches to both learn discrete models of domains that are continuous in both their state and action spaces to increase the applicability of IMT and learn the MDP online during the training phase of the policy.Bettina Könighofer and Stefan Pranger were supported by the State Government of Styria, Austria -Department Zukunftsfonds Steiermark, Martin Tappler was partially supported by the WWTF project ICT22-023, and Hana Chockler was supported in part by the UKRI Trustworthy Autonomous Systems Hub (EP/V00784X/1), the UKRI Strategic Priorities Fund to the UKRI Research Node on Trustworthy Autonomous Systems Governance and Regulation (EP/V026607/1), and CHAI -EPSRC Hub for Causality in Healthcare AI with Real Data (EP/Y028856/1). We thank both Antonia Hafner and Martin Plank for their proof-of-concept implementations of the experimental evaluation.  
 
 Appendix: In this section we discuss the necessary background and definitions needed to adapt IMT for testing for performance.Model checking of performance objectives. Model checking can be used to compute the expected accumulated reward for all states and actions in M. In particular, for a given MDP M, a policy π, and a reward function R : S → R, it computes the following values:• E M π ,R : S × N → R gives the expected accumulated reward in M π from a state s within n steps.• E max M,R (s, n) = max π∈Π E M π ,R (s, n)gives the maximal expected accumulated reward over all policies in Π from a state s within n steps.• E min M,R (s, n) = min π∈Π E M π ,R (s, n)gives the minimal expected accumulated reward over all policies in Π from a state s within n steps.A performance objective ⟨R, δ R ⟩ is defined over the reward function R and a threshold δ R ∈ R that defines the lowest-acceptable expected accumulated reward over n steps. E M π ,R (s, n) ≥ δ R .IMT can be easily adapted to evaluate a policy π for performance objectives. To tailor Alg. 1 for performance testing, we provide as inputs a performance objective ⟨R, δ R ⟩, and a minimal difference in performance ε R between optimistic and pessimistic estimates. These inputs replace the corresponding safety-related parameters φ, δ φ , and ε φ . The performance estimates (Line 3) are defined by: Definition D.2 (Performance estimates). For a given MDP M = (S, A, P, µ), a reward function R : S → R, and a given number of n steps, the optimistic and pessimistic performance estimate e opt,R , e pes,R : S × N → R are defined as follows:∀s ∈ S : e opt,R (s, n) = E max M,R (s, n), and ∀s ∈ S : e pes,R (s, n) = E min M,R (s, n).For the optimistic performance estimate, the computation assumes that the policy π selects the action that maximizes the expected reward in each unrestricted state. Conversely, for the pessimistic estimate, the assumption is that the least optimal actions concerning the reward are chosen. A state s ∈ S satisfies the performance objective ⟨R, δ R ⟩ if e pes,R (s, n) ≥ δ R (Line 4). A state s ∈ S violates the performance objective if e opt,R (s, n) ≤ δ R (Line 5).For the stopping criterion, the difference between performance estimates is compared to ε R (Line 7).We modeled a part of Barcelona in a Minigrid environment as illustrated in Fig. 8a . The size of the state space is |S| = 426. The agent's task is to navigate to Sagrada Família (within 100 steps), while respecting the traffic rules, i.e., not driving against the one-ways. We trained and evaluated two policies π 3 and π 4 .RL training parameters. π 3 and π 4 were trained utilizing a DQN. The agent is given the reward of 1 for reaching the goal and additionally -0.01 per step. Both policies have been trained using initial states uniformly sampled from |S|.IMT/MT parameters. We used the same parameters as for the experiment in Section 4.1, but used m = 15.Visualizing IMT. Fig. 8b visualizes the sets of verified states for π 3 in selected iterations of Alg. 1. We visualize S s , S f , and S u in the same way as in our first experiment. Brighter colors again represent states where π 3 was sampled. IMT iteratively samples the agent's decisions at crossings ranked on the difference the decisions of the individual roads have on the total length of the path to Sagrada Família. Figures 10 and 11 visualize S s , S f , and S u for π 4 . IMT needs 9 iterations to fully verify that π 4 behaves optimally in any of the modelled states.Evaluation results. Fig. 9a plots the number of verified states and Fig. 9b plots the estimates when evaluating π 3 . As above, we compare IMT and the average results for MT over 10 runs. Even though π 3 performed well on large parts of the state space, IMT and MT identified wrong decisions at several crossings that do not allow the agent to reach the goal in time. For RT we executed π 3 with a budget of 2000 policy queries and a maximum number of 100 time steps. Fig. 9c plots the average number of identified violations. While IMT and MT only have to sample the agent's decisions at the crossings to verify the entire state space, RT on average only found 13.25 (±2.75) states from which a test case failed. Fig. 12a plots the number of verified states and 12b plots the estimates when evaluating π 4 .Runtimes. The runtime to verify π 3 was 36.79 sec (±2.0) with MT and 24.70 sec (±2.2) with IMT.Both approaches MT and IMT needed a similar total runtime of about 9.84sec. (±0.2) to verify π 4 . For vision-based state spaces, deep clustering approaches could be used[25]. 


Decision: The paper introduces a novel technique for safe RL leveraging differentiable NN verification tools. The algorithm uses the $\alpha,\beta$-crown verification method. 

The reviewers agreed that the approach is novel, and the authors addressed their main concerns during the rebuttal phase. The main concern was the assumption of having an environment model at hand. Nonetheless, it seems to be the first successful application of Model-Based Testing in RL; there are numerous applications where the world model is accessible.

I therefore accept the paper for the NeurIPS conference.
 
In the final version of the paper, please include the discussion on the neural network-controlled systems, the missing related work, and the additional benchmarks and clarifications provided in the response to the reviewers.

Reviews: review: paper_summary: paper_summary: The paper proposes an algorithm (IMT) to test a deterministic policy in finite MDPs where a model of the MDP is available. The primary contributions of the paper are algorithmic and empirical. IMT works by iteratively partitioning the state space into safe, unsafe or undetermined. Using the MDP model, IMT is able to construct optimistic and pessimistic bounds on the property being tested (e.g., safety). These estimates are used to identify the states with the largest gap in their optimistic estimates between any pair of actions. IMT prioritizes testing these states next, which has the effect of tightening the bounds and taking the largest possible step towards convergence and halting. The final result includes a partitioning of the state space into safe and unsafe states, which is valuable feedback for improving the policy (offline). The paper also includes a clustering-based variant to scale the algorithm to larger MDPs. Experiments on 3 domains demonstrate the utility of IMT against a random baseline and a variant which does not rank the states.
strength_weakness: strength_weakness: - The paper does not provide sufficient detail on important algorithmic implementation details. Examples include the prerequisites for the algorithm (simulators, CTL), implementation of `computeEstimates`, $e_opt(s, a, n)$, clustering similarity/distance function, etc.

- The assumption of a correct model of the MDP is a somewhat large one in many domains. A discussion of the effort needed to obtain such a model would improve the paper and make its applicability to new domains clearer. Additionally, exploring the use of noisy simulators with varying levels of noise in the dynamics would be really interesting to see. As the paper mentions in Line 331, being able to leverage models of the environment learned from data is likely to increase the applicability. However, these are likely to include noisy dynamics so an experimental evaluation of the impact of noisy dynamics in the current experimental setup would have strengthened the paper.

- A comparison to stronger baselines would make it easier to assess the empirical contributions of the paper. Currently, the only comparison is to random testing. Comparing safety-violation detection rates against black-box policy testers (e.g., MDPFuzz, STARLA) using the same budget would have helped place this paper in the larger body of work on DRL testing as well as understand the applicability of these techniques in domains with different characteristics (size, model availability or learnability, etc.).
questions: questions: - What is the exact implementation of `computeEstimates`? How does it scale with the size of the input (restricted) MDP? Similarly, how exactly is $e_opt(s, a, n)$ estimated?

- What steps are involved in adding a new domain from scratch? How easy or hard is it to create the simulator, specify the CTL objective, etc.?

- Is it feasible to quantify or conduct investigations into how AMT might handle noise in the transition function in the current experimental setup?

- What is the precise definition of a robust policy in Line 195?

- What is the computational cost of the clustering approach used here? Should it be reflected in the complexity analysis in Lines 214 - 219?

- How does the quality of the resulting clusters affect performance? Does Alg 2 degrade gracefully as cluster quality decreases?

- Is it necessary to use a different mechanism (sink states) to restrict the MDP when clustering? How does terminating the trajectory at the sink state affect the e_opt, e_pes estimates, if at all? Does the approach still work if the restriction mechanism from Alg 1 is used?

- Does it make sense to compare safety-violation detection rates against other baselines (MDPFuzz, STARLA)?

- Does it make sense to consider continuous state and / or action MDPs using this framework? If yes, what modifications might be needed to make it work on cMDPs?
limitations: limitations: Yes
paper_summary: paper_summary: This work looks into the RL testing problem. RL policies are complex and hard to understand in terms of safety and performance. This work aims to test the policies via states in which the agent’s decisions have the highest impact on the expected outcome. This paper proposes a model-based method to compute a ranking of state importance and focus the testing on the highest-ranked states. The evaluation covers multiple benchmarks and shows that this approach can find unsafe policies.
strength_weakness: strength_weakness: 1. The guarantee about the correctness of the ranking does not seem to be clarified. Do you iterate over all the actions in the action set? What if the action space is large and continuous?
2. The testing is based on probabilistic model checking instead of worst-case checking. It would be good to bring out this in the abstract and introduction explicitly.
questions: questions: 1. How is the ranking computed? Do you cover continuous space?
2. What’s the scalability of this approach? Are there any cases where testing fails?
limitations: limitations: The limitations are not discussed in the main test.
paper_summary: paper_summary: This paper presents a framework called importance-driven model based testing for RL models.  ​ It uses a model-based approach to compute estimates of safety based on the MDP explored so far using the policy and ranks the importance of states based on the impact of decisions on safety.  Then it samples the policy on these state to further restrict the MDP. ​ The framework provides formal verification guarantees and partitions the state space into safe and unsafe regions. ​ The authors also propose a version to cluster similar states to further reduce the number of samples but at the cost of a relaxed guarantees. Experimental evaluations on different environments of various sizes demonstrate its effectiveness in reducing number of samples needed compared to random sampling both with and without the model. ​
strength_weakness: strength_weakness: Some of the weaknesses of this paper are:
- The approach relies on very strict assumptions on having a model for the environment with fixed set of states and actions, which could be very restricting for real world RL tasks. 

- The introduction and abstract could better motivate and establish the problem. Currently, they only explain the algorithm without much context. For example, it is not clear how the safety estimates are computed until sections 2 and 3 or why computing them iteratively is easier than sampling the action on every state.
questions: questions: - How can number of policy queries in Fig 3c be greater than the number of states in the environment? 

- For runtimes, it will also be useful to break it down into model checking and policy sampling times for both IMT and MT approaches. 

- Please add legends to Figure 3
limitations: limitations: The authors briefly talk about limitation about the requirements of the current approach, but they could definitely expand a bit more on these limitations early on the paper.
paper_summary: paper_summary: This paper proposed a novel model-based importance-driven framework for testing trained DRL policies. By focusing on testing the cases with higher importance ranks, the proposed framework improves the testing scalability. The evaluation of several case studies demonstrates that the proposed framework can more efficiently discover unsafe policy behavior with low testing effort.
strength_weakness: strength_weakness: 1. The definition of the safety formula $\phi$  and the formula for calculating $\mathbb{P}\_{\mathcal{M}^\pi, \phi}$ should be stated clearly.
2. The current framework depends on several human-defined thresholds, for instance, $\delta_{\phi}$, $\epsilon_{\phi}$ $\delta_{i}$. How those parameters are determined and sensitive to the final testing result should be discussed more clearly.
3. The current framework is shown to be applicable in a discrete state and action space. It would be nice to see the discussion on the potentials and limitations applied to the continuous state and action space.
questions: questions: 1. The importance ranking is based on the maximal difference between the optimistic estimates concerning the available actions, which considers the impact of decisions on the optimistic estimates. Why not use the pessimistic estimate, as it is more concerned about safety violations?
limitations: limitations: No
paper_summary: paper_summary: This paper proposes a model-based method for testing the safety properties of Deep Reinforcement Learning (DRL). The method computes a ranking of state importance across the entire state space, dividing the state space into safe and unsafe regions. The approach provides optimal test-case selection and guaranteed safety by providing formal verification guarantees over the entire state space. The method is evaluated on several examples, showing it discovers unsafe policy behavior with low testing effort.
strength_weakness: strength_weakness: - Some technical details should be explained more clearly.
- The authors doesn't compare IMT with the SOTA DRL testing method, like [15] mentioned by the authors in the paper.
questions: questions: In general, the idea of ranking the importance of the state and leveraging it as the testing guidance is very interesting. I believe this work would have a certain impact on the further development of DRL testing. 

There are a few technical points unclear.

1. Page 2, Line 60. It would be good if the authors gave a more concrete concept of the formal guarantee provided by IMT, like probabilistic certification.

2. Page 5, Line 175. What do you mean by "significantly larger"? Do you perform statistical testing here?

Moreover, some related work is missing:

- Gerasimou, Simos, Hasan Ferit Eniser, Alper Sen, and Alper Cakan. "Importance-driven deep learning system testing." In Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering, pp. 702-713. 2020.
- Song, Jiayang, Xuan Xie, and Lei Ma. "$\mathtt {SIEGE} $: A Semantics-Guided Safety Enhancement Framework for AI-enabled Cyber-Physical Systems." IEEE Transactions on Software Engineering (2023).
- Shi, Ying, Beibei Yin, and Zheng Zheng. "Multi-granularity coverage criteria for deep reinforcement learning systems." Journal of Systems and Software 212 (2024): 112016.
limitations: limitations: Yes, the authors address it in the guideline.

Comments: title: Re. author response
comment: Thank you for the rebuttal! It address my concerns and I think it should be accepted.
I thank the authors for their detailed response to the reviewers. After reading the response, other reviews and comments, I've increased my score to "Weak Accept". While I don't think there's anything technically wrong with the paper, there are a number of major assumptions being made, which might reduce the applicability of the proposed approach. The performance of the proposed method is not explored on abstract or learned models of the environment, which is the most likely scenario. Including these experiments would significantly strengthen the paper, in my opinion. In the absence of these, it becomes challenging to evaluate the paper for impact and overall utility.