Lookahead Shielding for Regular Safety Properties in Reinforcement Learning

Q: "Can you clarify the ambiguities I pointed out in the "Weaknesses" section, i.e. (1) Which policy is used to resolve the non-determinism when determining whether to use? (2) Can you formally states how "(given a)" is to be interpreted? Does the resolving policy always pick in or only for one step? (3) Is memoryless? (4) Can you clarify Assumption 3.8?"

A: We agree with the particular point highlighted by the reviewer here, it is not formally stated which policy/actions are used to resolve the non-determinism of the MDP. Although, I think the reviewer has correctly identified that (given $a$) means we first resolve the non-determinism of the MDP with the action $a$ sampled from $\pi_{*task*}$ and then with $\pi_{*safe*}$ thereafter, we will try to think of a way to formally state this in the revised version of our paper. Importantly, we note that this does not mean $a$ is always picked from $s$ just for the first step in resolving the non-determinism.

Technically speaking we did only formally introduce memory-less policies over the state space $\mathcal{S}$, indeed the objective that $\pi_{*safe*}$ seeks to minimize is non-Markov with respect to the the state space $\mathcal{S}$, however $\pi_{*safe*}$ operates on the product state space $\mathcal{S} \times \mathcal{Q}$ thus $\pi_{*safe*}$ is memory-less on $\mathcal{S} \times \mathcal{Q}$ and should be defined as a function $\pi_{*safe*} : \mathcal{S} \times \mathcal{Q} \to *Dist*(\mathcal{A})$, we will aim to make this more explicit. Regarding the model checking horizon $N$, this is fixed globally and does not need to be an input to $\pi_{*shield*}$.

In Assumption 3.8 the probability $\Pr(\ldots)$ is interpreted as before, by first using $a \in \mathcal{A}$ to resolve the non-determinism of the MDP and $\pi_{*safe*}$ thereafter. I think the confusion here can be resolved by implementing some of the changes mentioned above. In general, Assumption 3.8 is supposed to guarantee that there exists some optimal model checking horizon $N^*$ which we can use to identify all irrecoverable actions, $N \geq N^*$ means the actual model checking horizon $N$ that we have chosen is larger than this optimal model checking horizon, so no implication is needed here, we can try re-word this assumption to make it more clear what we mean.

Q: "The shielding policy is presented as a binary choice between the preferred maximizing action and the safe backup action. Since usually an RL agent evaluates all action, it can usually also rank all actions. Have you considered extending this to a setting where the action with the highest ranking is chosen, restricted to those actions which satisfy the condition in Eq. (1)?"

A: This is an excellent point, we have thought about this, although we haven't actually experimented with this, in theory we could rank the available actions by the task policies Q values and then iteratively check whether each action is safe or not starting from the highest ranked action and once we find a safe action we use it. For small action spaces, like grid worlds, this seems like a reasonable idea, for large action spaces, this might incur significant overhead, for example Seaquest has $|\mathcal{A}| = 18$ which might be impractical.

Q: "Can you provide an example of the theoretical bounds of Thm. 3.10 applied to some examples in your experimental setup? How far are the bounds from the actual rate of unsafe behaviour observed?"

A: For simplicity we will choose the Media streaming environment to demonstrate how our bounds hold up. In this experiment we have, $|\mathcal{S}| = 20$, $|\mathcal{A}|=2$, and we set, $\varepsilon_t = 0.001$, $N=5$, $\varepsilon'=0.02$, $\delta_t=0.01$, even using the bound provided in the appendix of [R4], which considers a known branching factor $k$ (for media streaming $k=3$), the bound appears to be unwieldy, requiring that each state-action pair be visited $O(10^7)$ times. $m \approx \frac{32 \cdot N^2}{\varepsilon'} \log (\frac{2|\mathcal{S}|^2 |\mathcal{A}^2|2^k}{(k-1)\delta_t/2})$ Nevertheless, we obtain a a safety rate of $1 - \sum^{40}\_{t=1} \varepsilon\_t = 0.96$ with probability $1 - \sum^{40}\_{t=1}\delta\_t = 0.6$. Studying Figure 6 (Appendix C) closely, we see that this safety rate is empirically achieved by QL-Shield (Exact) and we see that our approach (QL-Shield) quickly converges to the safety rate achieved by QL-Exact. Please let me know if you think I've done my calculations for this wrong or perhaps bounds such as this are always so unwieldy?

We thank the reviewer for their additional minor comments, they seem very helpful and we will aim to incorporate them in to a revised version of our paper.

We thank the reviewer for taking the time to read our paper and for providing such an in-depth assessment of our approach, we appreciate that they were able to see the merit of our contributions

Re Weaknesses:

Re README: apologies for this, we thought our supplementary material included READMEs, this was an oversight when submitting, the supplementary materials should now be updated to include README files.

Thanks for bringing [R3] to our attention, indeed we will aim to include this in our citation list as it seems relevant, interestingly I believe we mentioned the conservativeness of our bound given the dependence on $|S|$ which could be replaced by the maximum number of successor states if this is known, or equivalently an upper bound on the branching factor as the reviewer rightly points out. If time allows we will aim to improve the bound provided in Theorem 3.10 given the references you have provided.

Re Questions:

"I have some questions for understanding Definition 3.1:"

This is a very small technical detail we missed, thanks for bringing it to our attention. Please correct me if I am wrong, but I believe there is a slight conflation between the cost function (Definition 3.1) and the objective function $\mathbb{E}\_{\pi} [ \sum^{T}\_{t=0} \gamma^t \mathcal{C}(s\_t, q\_t) ]$ which the safe (backup) policy seeks to minimize, we claim that the cost function $\mathcal{C} : \mathcal{S} \times \mathcal{Q} \to \mathbb{R}$ is non-Markov, since the automaton state $q\_t$ at timestep $t$ could depend on some arbitrary history of past states, the cost function is Markov on the product state space $\mathcal{S} \times \mathcal{Q}$ however. On the other hand, the objective function $\mathbb{E}\_{\pi}[\sum^{T}\_{t=0}\gamma^t \mathcal{C}(s\_t, q\_t)]$ is written incorrectly. We update the $\pi\_{*safe*}$ with the following Q-learning update rule,

$\hat{Q}\_{*safe*}(s\_t, q\_t, a\_t) \stackrel{\alpha}{\longleftarrow} \gamma \max\_{a} \{ \hat{Q}\_{*safe*}(s\_{t+1}, q\_{t+1}, a) \} - \mathcal{C}((s\_t, q\_t))$

This will give us a policy that minimizes the infinite horizon discounted cost, thus the objective function should in fact be written as $\mathbb{E}\_{\pi}[\sum^{\infty}\_{t=0}\gamma^t \mathcal{C}(s\_t, q\_t)]$, we agree that the discounted finite objective function poses issues. We hope this clears up any confusion, please feel free to ask for further clarification.

Once again we thank the reviewer for their comprehensive review and for finding the time to respond to our rebuttal. We understand the reviewer still has some reservations, particularly considering the sample complexity bound. Our aim is to upload a revised version of the paper before the end of the discussion period, that implements some of the changes mentioned in our initial response. We then invite the reviewer to consider adjusting their score as they see appropriate. Thanks again.

"The product construction between the MDP and safety automata can lead to state space explosion. While the paper briefly mentions this issue, it doesn't provide a solution"

This is typically not the case. In our paper we use statistical model-checking which alleviates this issue of "state space explosion" by computing the product states on-the-fly rather than computing the full product. Also, for a fixed size MDP the size of the product is linear in the size of the safety automata.

"The need for repeated model-checking during execution could introduce significant computational overhead, especially in real-time applications"

The real time performance of 5 FPS during training may not be practical, however, we only need to repeatedly model check since the dynamics model and safe (backup) policy are non-stationary, i.e. being updated with new experience. Once training has completed and the dynamics model and safe (backup) policy are fixed, we can simply run one entire pass over each state-action pair and check if it is safe, we can then save these results in a hash-map or lookup-table and quickly look them up during deployment with minimal overhead. This is what we do for our ablation in Appendix C, and we enjoyed operation speeds of 3000 FPS.

We thank the reviewer for taking the time to read our paper paper and ask some very thoughtful questions.

For our response we will first aim to clear up the reviewers questions and we think this should resolve some the perceived limitations of our approach.

Re Questions:

• The union bound for episodic safety seems very conservative. Have you explored tighter bounds or alternative approaches? For instance, could martingale-based techniques provide tighter guarantees?

We agree that the union bound does seem overly conservative in practice, as in general we may often not be in a safety-critical state. Although, we note that these results are in line with prior work [1] that also use union bounds for probabilistic safety guarantees. Regrettably we have not explored alternative approaches for tighter bounds, although martingale-based techniques do sounds like a very useful suggestion. In particular, we could use Azuma-Hoeffding to try and bound the expected discounted cost objective of the full shielded policy, this could then offer tighter bounds on the probability of satisfaction of the safety properties, if time permits we will try and see if such an analysis is possible and include it in the revised version of our paper.

[1] "Safe Reinforcement Learning via Statistical Model Predictive Shielding." by Bastani, Osbert, Shuo Li, and Anton Xu.

• How can we verify Assumption 3.8 (existence of finite N* for identifying irrecoverable actions) in practice? Could you provide a method or heuristic for estimating N*?

The choice of $N^*$ is crucial for our safety guarantees, knowing something about the environment can help to choose $N^*$ appropriately, in general we would want $N^*$ to be the longest path from any given state to the probabilistic safe set of the backup policy, in a self-driving car example $N^*$ could be the longest time it takes the car to decelerate to a stationary position, as a heuristic, slightly more than the shortest path in the DFA from the initial state to the accepting state is a good choice that we used in our experiments. For more details we point the reviewer to [2] where, to the best of our knowledge, this assumption appeared for the first time (there is a probabilistic interpretation in the appendix of [2]).

[2] "Safe reinforcement learning by imagining the near future" by Thomas, Garrett and Luo, Yuping and Ma, Tengyu

• For large DFAs representing complex safety properties, the product state space becomes intractable. Have you explored hierarchical or compositional approaches to manage this complexity?

In general, we deemed the synthesis of DFA from complex safety properties beyond the scope for this paper. We assume a DFA is already provided which corresponds to some regular safety property. We note that, for a fixed MDP, the size of the product state space only grows linearly in the size of the DFA. Although, indeed for large DFA and MDP this can get out of hand. Our model checking approach which is based on statistical model checking, mostly alleviates this issue by computing the product states on-the-fly, meaning the (possibly) costly full product does not need to be computed. The only restriction really is if we can fit the DFA in memory, which is usually the case for properties of interest.

• The backup policy seems crucial for performance. Could you elaborate on alternative designs for the backup policy beyond the current cost-based approach?

One could generally use any well-tuned RL algorithm for learning the backup policy online using the cost function. Other works [2] consider LQR to construct a backup policy before hand, although this is not relevant for discrete state spaces, in our ablations in Appendix C, we use value iteration to pre-compute the backup policy. Sound value iteration is used by STORM model checker, interval-bound value iteration can also be used to compute safe policies, although these approaches are only possible when we have access to the precise dynamics of the MDP ahead of time, we make no such assumptions in our paper.

• Could you provide more details about the real-time performance requirements? What is the typical computation time for model-checking in your deep RL experiments?

Model checking is relatively fast, we use JAX and JIT compilation to implement statistical model checking which can generate thousands of samples per second. On good hardware we were able to achieve at least 5 FPS (interactions with the environment) for the most complex safety property (15x15 grid world property (3)) and much quicker for the simpler properties. In the deep RL experiments, model checking during learning resulted in a slow down of x2 -- from 400 down to 200 FPS. We acknowledge that 5 FPS for real-time performance may not necessary be brilliant, however once the dynamics model and safe (backup) policy are fixed we can do much better (discussed in the next comment).

If the reviewer has no more questions or comments at this time, we will deem, for the most part, the issues raised by the reviewer as resolved, and we will touch upon some of our response in the revised version of our paper, that will be uploaded before the end of the discussion period. In any case we encourage the reviewer to adjust their score as they see appropriate.

• How do different choices of reward shaping or learning for the safe policy based affect performance?

One could consider using potential based reward-shaping for further improving the speed of convergence of the safe (backup) policy. We found that counter factual experience alleviated all issues we had with slow convergence for the safety properties that we considered in our experiments.

• How complicated do the safety properties need to be for the approach to start breaking down?

The only main restrictions on the complexity of the safety properties is whether the DFA can fit in memory, and how quickly counterfactual experiences can be run over the DFA. There is no restriction really for model checking as we leverage statistical model checking which computes the product states on-the-fly meaning we don't have to compute the full product Markov chain. For more complicated safety properties we might also want to increase the model checking horizon $N$ which will incur additional computation time although the dependence on $N$ is linear.

• Have you tried comparing your approach to previous approaches to temporal-logic constrained policy optimization e.g. [1] and [2], rather than just CMDP-based approaches?

We thank the reviewer for bringing these works to out attention, as both works seek to solves problems similar (but not identical) to our problem. With regards to [1], [1] makes non-trivial assumptions, such as access to a generative model of the true dynamics $P$ from which they can sample transitions $s \sim P(s, a)$ for any state-action pair. This assumption immediately breaks the standard RL setting where we have to sequentially interact with the environment from a given initial state. Thus, setting up a fair comparison between our approach and [1] becomes unrealistic.

The only assumptions made by [2] appear to be knowing the optimal discount $\gamma$ for the LTL-objective and choosing the Lagrange multiplier $\lambda > \lambda^*$ greater than the optimal $\lambda^*$. In this instance we could attempt to make a fair comparison, however [2] firstly lacks an open source implementation, and secondly we would need to take care to translate the DFA and its satisfaction condition to a corresponding Buchi automata, highlighting these technical details in the main paper might confuse readers and obfuscate our technical contributions.

Some further discussion about [2], the objective function in [2] becomes $\pi^* = \arg\max_{\pi} [R_{\pi} + \lambda V_{\pi}]$ , the baseline (QL-cost) essentially optimizes this objective (without reward shaping, but with CFE) for a fixed $\lambda$ (in most of our experiments we choose $\lambda = 10.0$), in principle one could adaptively update $\lambda$ using the estimates of $R_{*max*}$ and $R_{*min*}$ during training, I think this is almost exactly what ROSARL is [3].

[3] "ROSARL: Reward-Only Safe Reinforcement Learning" by Geraud Nangue Tasse, Tamlin Love, Mark Nemecek, Steven James, Benjamin Rosman

Before the end of the discussion period we will try clear up any further questions you have, and we will aim to update the paper with additional ablations, although, owing to space constraints, these will likely have to be put in the appendix.

We thank the reviewer for providing a thorough assessment. We will take the time necessary to iron out any typographical errors and issues with phrasing etc.

Re Weaknesses:

We appreciate that the reviewer finds some merit in our contributions and recognizes that separately learning a safe (backup) policy is a unique property of our approach. In response to "However, the guarantees made here also rely on the quality of the learned dynamics model and safe policy - in practice, we'll rarely know for sure that these learned components are 'good enough'", we point the reviewer to the theoretical contributions in our paper (Theorem 3.10) which give a precise bound on when we know that our learned dynamics model is good enough for accurate model checking. In particular, after each state-action pair has been visited at least $\mathcal{O}\left(\frac{N^2|\mathcal{S}|^2}{{\varepsilon'}^2} \log\left( \frac{|\mathcal{A}||\mathcal{S}|^2}{\delta'}\right)\right)$ times, then dynamics model is 'good enough' for our purposes, we can easily monitor the number of visits during training. Verifying if the backup policy is 'good enough' is trickier, however given an $\epsilon$-accurate MDP one could run value iteration to compute an $\epsilon$-optimal backup policy, with respect to the expected discounted cost objective. We encourage the reviewer to read Appendix C, where we ablate our approach, by providing the model checker with a perfect model of the MDP and a perfect backup policy (computed with value iteration before training). In this instance we can provide safety guarantees in line with Theorem 3.10 from the beginning of training, empirically we see that our approach here (QL-Shield) quickly matches the performance of (QL-Exact) demonstrating that the dynamics model and backup policy have successfully been learnt.

Re smaller point:

For the tabular RL setting, Q-learning has consistently proved to be the most fruitful approach. We agree with the reviewer that in the deep RL setting, Q-learning based approaches have limitations, for our deep RL experiments we do not use Q-learning and leverage DreamerV3 for both policy optimization and dynamics learning. For CMDPs and safe RL more generally model-based approaches have been shown to dramatically outperform model-free approaches based on PPO/TRPO, which is why we opted for DreamerV3, see [1,2].

[1] "Constrained policy optimization via bayesian world models" by As, Yarden and Usmanova, Ilnura and Curi, Sebastian and Krause, Andreas

[2] "Safe DreamerV3: Safe Reinforcement Learning with World Models" by Huang, Weidong and Ji, Jiaming and Zhang, Borong and Xia, Chunhe and Yang, Yaodong

Re Additional Comments:

We felt it necessary to include the technical comparison to CMDP-based approaches given that we compare these approaches in our experiments. From a technical stand point it is clear that CMDP-based approaches struggle to satisfy absolute or high probability constraints, as is further evidenced by our experimental results. However, we felt that this was a fair comparison given that, like our approach, CMDP-based approaches also assume no prior knowledge of the transition dynamics of the MDP, no safe backup policy or any other restrictive assumptions.

With regards to line 84 we do not quite see how this is a technical mistake, we defined $*Dist*(\mathcal{S})$ as the set of distributions over $S$, writing $\mathcal{P}: \mathcal{S} \times \mathcal{A} \to *Dist*(\mathcal{S})$ is standard notation that means that the function $\mathcal{P}$ maps from the set of state action pairs to distributions over states, which is the desired interpretation.

We beleive that most of the issues and reservations raised by the reviewer have been adressed, if the reviewer has no further comments we will deem these issues resolved and aim to add the additional ablations suggested by the reviewer to the revised version of our paper, before the end of the discussion period. In any case we encourage the reviewer to adjust their score as they see appropriate.

We gently encourage the reviewer to bring to our attention any remaining issues they have in light of the revised paper. If they find any of their issues resolved, for the most part, we encourage them to reconsider their score.

Both [1] and [2] are closely related to "Safe reinforcement learning via probabilistic shields." by Jansen, Nils and K{"o}nighofer, Bettina and Junges, Sebastian and Serban, Alexandru C and Bloem, Roderick

We will comment on the differences between our approach and this body of work more generally. [1,2] are closely related to our approach in that verification or shielding of the agents actions is done online in real time, rather than exhaustively over the state space before training. [1,2,3] also consider a $k$-step lookahead horizon for model checking in the same way that we do, however there are several key differences between our approach and [1,2,3] which we highlight here. Firstly, [1,2,3] assume access to the precise transition dynamics of the MDP or at the very least a safety-relevant fragment of the MDP which must only be computed from the true MDP using prior knowledge, I quote them here: "In this paper, we consider the setting where the safety-relevant fragment of the MDP together with a temporal logic safety specification is given" [2]. We make no such assumption -- learning the dynamics of the MDP from scratch. [1,2,3] also do not provide any global safety guarantees in line with ours, I quote: "In contrast, a sequence of bad choices may violate $\varphi$ with high probability" [3], loosely speaking this is because verifying the safety of an action for $k$-steps does not guarantee that [1,2,3] don't go down a suboptimal path that violates the safety-requirement $\varphi$ with high-probability, unless we make additional assumptions. We address this issue by making the suitable assumptions on the model checking horizon (see Assumption 3.8 (line 330) in our paper). Furthermore, [1,2,3] also rely on planning in the reachable sub-MDP to compute safe actions, we do not need to plan rather the safe actions are learned and encoded in the safe (backup) policy, side-stepping the need for planning -- making our approach more practical in online scenarios.

[1] "Online Shielding for Stochastic Systems" by Bettina Könighofer, Julian Rudolf, Alexander Palmisano, Martin Tappler, and Roderick Bloem.

[2] "Online Shielding for Reinforcement Learning" by Bettina Könighofer, Julian Rudolf, Alexander Palmisano, Martin Tappler, and Roderick Bloem.

[3] "Safe reinforcement learning via probabilistic shields." by Jansen, Nils and K{"o}nighofer, Bettina and Junges, Sebastian and Serban, Alexandru C and Bloem, Roderick

We now comment on the differences with [4]. [4] is specifically concerned with continuous state action spaces which are typically more tricky. However, in [4] the authors assume access to the transition dynamics, I quote "we focus on planning, where the dynamics are known", the authors also assume access to a backup policy which is computed with LQR and verified before training. No such assumption is made here. The environments considered in [4] also have equilibrium points in which the agent can remain in indefinitely given some control $u^*$, for discrete state spaces this corresponds to having safe end-components where the agent can remain in indefinitely, safe end-components do not always exist and are not trivial to compute.

[4] "Safe Reinforcement Learning with Nonlinear Dynamics via Model Predictive Shielding" by Osbert Bastani.

Summing up, we appreciate the reviewer for bringing these works to our attention. We will aim to include a similar (more concise) discussion in the revised version of our paper.

In general [1,2,3,4] make non-trivial and often restrictive assumptions which we do not make, this makes it hard to setup a fair comparison between our approach and these works, rather we opt for a comparison with CMDP-based approaches that also make no assumptions about the MDP or backup policy.

For the time being we invite the reviewer to ask any more questions they may have.

We thank for the reviewer for taking the time to read our paper and we appreciate their assessment.

"The framework seems to rely on a lookahead mechanism that verifies the probability of reaching an unsafe state after an action is selected rather than ensuring safety beforehand."

This is not strictly correct, the lookahead mechanism verifies the probability of reaching an unsafe state given the action proposed by the task (reward) policy, the verification is done in the approximate model of the environment, not the real one. Thus the action proposed by the task policy, if unsafe, is not actually used in the environment, preventing the selection of unsafe actions before they are actually performed.

When we lack a precise model of the MDP or a safety-relevant abstraction of the MDP, as it is the case in many real-world application, synthesis cannot be done beforehand and the safety of the system cannot be absolutely guaranteed. Still, we show how useful the construction of an approximate transition model can be provided.

We would like to take this opportunity to re-iterate the contributions of our paper. Firstly, we assume minimal prior knowledge, this includes, no access to a model of the MDP or a safety-relevant abstraction of the MDP, and no access to a hand-crafted backup policy. Both the approximate dynamics model of the MDP and the backup policy are learned online, meaning indeed, we cannot immediately provide safety assurances, however, in the tabular setting we can provide probabilistic safety assurances given that each state action pair is visited at least $\mathcal{O}\left(\frac{N^2|\mathcal{S}|^2}{{\varepsilon'}^2} \log\left( \frac{|\mathcal{A}||\mathcal{S}|^2}{\delta'}\right)\right)$ times. We discuss in the paper that this bound is quite conservative but in practice we can do much better.

While we understand that this is not required, we also encourage the reviewer to read Appendix C, where we ablate our approach, by providing the model checker with a perfect model of the MDP and a perfect backup policy (computed with value iteration before training). In this instance we can immediately provide safety assurances before training, we also demonstrate that our approach (QL-Shield) quickly matches the performance of this ablation (QL-Exact) demonstrating that the dynamics model and backup policy have successfully been learnt.

If the reviewer has no further comments we will deem the issues raised by the reviewer as resolved and aim to implement the changes mentioned above to the revised version of our paper before the end of the discussion period. In any case we encourage the reviewer to adjust their score as they see appropriate.

We have now uploaded a revised version of the paper. Beyond some minor changes to notation, we have also extended the related work section to include the papers brought to our attention by the reviewer, and we have added additional experiments to the appendix. We kindly invite the reviewer to read the new material that they find interesting, and we invite them to ask any further questions they may have or adjust their score as they see appropriate.

We gently encourage the reviewer to bring to our attention any remaining issues they have in light of the revised paper and invite them to ask further questions which hopefully we can adress with the time left. If they find any of their issues resolved, for the most part, we encourage them to reconsider their score.