Guiding Safe Exploration with Weakest Preconditions
Authors: Greg Anderson
Swarat Chaudhuri
Isil Dillig
Venue: ICLR 2023 poster (2023)
Keywords: reinforcement learning
safe learning
safe exploration

Abstract: In reinforcement learning for safety-critical settings, it is often desirable for the agent to obey safety constraints at all points in time, including during training. We present a novel neurosymbolic approach called SPICE to solve this safe exploration problem. SPICE uses an online shielding layer based on symbolic weakest preconditions to achieve a more precise safety analysis than existing tools without unduly impacting the training process. We evaluate the approach on a suite of continuous control benchmarks and show that it can achieve comparable performance to existing safe learning techniques while incurring fewer safety violations. Additionally, we present theoretical results showing that SPICE converges to the optimal safe policy under reasonable assumptions.

Published as a conference paper at ICLR 2023
GUIDING SAFE EXPLORATION WITH WEAKEST PRECONDITIONS
Greg Anderson, Swarat Chaudhuri Isil Dillig;
Department of Computer Science
The University of Texas Austin Austin, TX, USA {ganderso, swarat, isil]fcs. utexas edu
ABSTRACT
In reinforcement learning for safety-critical settings, it often desirable for the agent to obey safety constraints at all points in time, including during training. We present a novel neurosymbolic approach called SPICE to solve this safe explo- ration problem. SPICE uses an online shielding layer based on symbolic weakest preconditions to achieve a more precise safety analysis than existing tools without unduly impacting the training process. We evaluate the approach a suite of continuous control benchmarks and show that it can achieve comparable perfor- mance existing safe learning techniques while incurring fewer safety violations. Additionally, we present theoretical results showing that SPICE converges to the optimal safe policy under reasonable assumptions.
INTRODUCTION
In many real-world applications of reinforcement learning (RI.), it crucial for the agent to hehave safely during training. Over the years, body of safe exploration techniques (Garcıa & Fernández) 2015) has emerged to address this challenge. Broadly, these methods aim to converge to high- performance policies while ensuring that every intermediate policy seen during learning satisfies a set of safety constraints. Recent work has developed neural versions of these methods (Achiam al. 2017, Dalal al. 2018 Bharadhwaj et al.) (02I)) that can handle continuous state spaces and complex policy classes.
Any method for safe exploration needs mechanism for deciding if an action can be safely ex- ecuted at given state. Some existing approaches use prior knowledge about system dynamics (Berkenkamp et al. 2017 [Anderson et al. 2020) to make such judgmentss A more broadly applica- ble class of methods make these decisions using learned predictors represented as neural networks. For example, such a predictor can be a learned advantage function over the constraints (Achiam
et al. 2017 Yang al. 2020) or a critie network (Bharadhwaj et al. 2021 Dalal et al. 2018) that predicts the safety implications of an action.
However, neural predictors of safety tions for training and also suffer from approximation errors. Both traits are problematic in safety- critical, woaldw settings. In this paper, introduce neurosymbolic approach learning safety predictors that is designed to alleviate these difficulties.
require numerous votentially-unsate environment interac-
Our approach, called SPICE filter out unsafe actions. However, the novel idea in SPICE is to use the symbolic method of weakest preconditions (Dijkstral 1976) compute, from single-time-step environment model, a predicate that decides if a given sequence of future actions is safe. Using this predicate, we symbolically compute a safety shield (Alshickh et al.) 2018) that intervenes whenever the current policy proposes an unsafe action. The environment model is repeatedly updated during the learning process using data safely collected using the shield. The computation of the weakest precondition and the shield is repeated, leading to more refined shield, on each such update.
similar to Bharadhwaj al. (222)) in that use learned model to
"cqual advising
SPICE is available

---

Published as a conference paper at ICLR 2023
The benefit of this approach is sample-efficienee to construct safety shield for the next & time steps, SPICE only needs enough data to learn a single-step environment model. We show this benefit using an implementation of the method in which the environment model is given by a piecewise linear function and the shield is computed through quadratic programming (QP). On a suite of chal- lenging continuous control benchmarks from prior work, SPICE has comparable performance as fully neural approaches to safe exploration and incurs far fewer safety violations on average.
In summary, this paper makes the following contributions:
We present the first neurosymbolic framework for safe exploration with learned models of safety. We present a theoretical analysis of the safety and performance of our approach. We develop an efficient, QP-based instantiation of the approach and show that it offers greater safety than end-to-end neural approaches without significant performance penalty,
2
PRELIMINARIES
Safe Exploration. We formalize safe exploration in terms of constrained Markov decision process (CMDP) with a distinguished set of unsafe states. Specifically, a CMDP is a structure = (S,A,, r, P. Po, c) where 8 is the set of states, A is the set of actions, 8 x A + R is reward function, P(x' x, u), where æ, x' E and u E A, is a probabilistic transition function, Po is initial distribution over states, and is cost signal. Following prior work (Bharadhwaj et al. (02I), we consider the case where the cost signal a boolean indicator of failure, and we further assume that the cost signal is defined by a set of unsafe states Sy- That is, c(x) = if x E Sy and c(x) = O otherwise. A policy is a stochastic function π mapping states to distribu- tions over actions. A policy, in interaction with the environment, generates trajectories (or rollouts) Zo, 2o, 21, ....... Un-1, In where To ~ Po. each u, ~ (Tx.), and each 2,+1 ~ P(x,, u.). Con- sequently, each policy induces probability distributions Sz and A, on the state and action. Given a discount factor < 1, the long-term return of a policy is R(
w (rr"r( u:]].
The goal of standard reinforcement learning is to find a policy x* = arg max, R(TT). Popu- lar reinforcement learning algorithms accomplish this goal by developing sequence of policies To. Ti...... TN such that TN R π². We refer to this sequence of polices as a learning process. Given bound 6, the goal of safe exploration is to discover a learning process .o....: TN such that
N arg max, R(T) and vi N. Pa-s,, (x SS) 6
That is, the final policy in the sequence should be optimal in terms of the long-term reward and every policy in the sequence (except for Ho) should have a bounded probability 8 of unsafe behavior. Note that this definition does not place a safety constraint on To because we assume that nothing is known about the environment a priori.
Weakest Preconditions. Our approach to the safe exploration problem is built on weakest precon- ditions DDijkstral 1976). At a high level, weakest preconditions allow us to "translate" constraints on program's output constraints on its input. As very simple example, consider the function I + +1 The weakest precondition for this function with respect to the constraint ret > 0 (where ret indicates the return value) would be x > -1. In this work, the "program" will be model of the environment dynamics, with the inputs being state-action pairs and the outputs being states.
For the purposes of this paper, we present simplified weakest precondition definition that is tailored towards our setting. Let f S x A + 2 be a nondeterministic transition function. As we will see in Section 4 ʃ represents a PAC-style bound on the environment dynamics. We define an alphabet E which consists of a set of symbolic actions wp..... .H and states - Each symbolic state and action can be thought of as a variable representing an priori unkonwn state and action. Let Φ be a first order formula over Σ. The symbolic states and actions represent a trajectory in the environment defined by f. so they are linked by the relation X++1 E f(xi, for 0 S < H. Then, for a given i, the weakest precondition of & is formula vù over Σ {x++1) such that (1) for all e E ()) we have vi = Φ(x++1 + e] and (2) for all & satisfying condition (I), v/ = th Here, the notation Φix++1 the expression e. Intuitively, the first condition ensures that, after taking one environment step from Xi under action wj. the system will always satisfy o, matter how the nondeterminism of f is resolved. The second condition ensures that á is as permissive as possible, which prevents us from ruling out states and actions that are safe in reality.
e| represents the formula ø with all instances of Xi+1 replaced by
2

---

Published as a conference paper at ICLR 2023
3 SYMBOLIC PRECONDITIONS FOR CONSTRAINED EXPLORATION
Our approach, Symbolic Precondi- tions for Constrained Exploration (SPICE), uses a learned environment model to both improve sample effi ciency and support safety analysis at training time. To do this, we build on top of model-based policy optimiza- tion (MBPO) (Janner et al., 2019). Similar to MBPO, the model in approach is used to generate syn- thetic policy rollout data which can be fed into a model-free learning al- gorithm to train policy. In contrast to MBPO, we reuse the environment model ensure the safety of the sys- tem. This dual use of the environment allows for both efficient optimization and safe exploration.
Algorithm The main learning algorithm
procedure SPICE
Initialize an empty dataset D and random policy for epoch in 1.... .V do if epoch 1 then
T +- π
else
Ts f Aa. WPSHIELD(M,, 2t, ((x) 2
Unroll real trajectores {(s;, di, s4, r:)) under ws D = DU 0e (4.r:)
M < MEARNENNMODELLE Optimize π using the simulated environment M
The main training procedure is shown in Algorithm I and simultaneously learns an environment model M and the policy т. The algorithm maintains a dataset D of observed environment tran- sitions, which is obtained by executing the current policy π in the environment. SPICE then uses this dataset to learn an environment M, which is used to optimize the current policy æ, as done in model-based RL. The key difference of our technique from standard model-based RL the use of a shielded policy Is when unrolling trajectories to construct dataset D. This is necessary for safe exploration because executing т in the real environment could result in safety violations. In contrast to prior work, the shielded policy Ts in our approach is defined by online weakest precondition computation which finds a constraint over the action space which symbolically represents all safe actions. This procedure is described in detail in Section 4
4 SHIELDING WITH POLYHEDRAL WEAKEST PRECONDITIONS
4.1 OVERVIEW OF SHIELDING APPROACH
Our high-level online intervention approach is presented Algorithm 2 Given an environ- ment model M, the current state and a proposed action uh. the WPSHIELD procedure chooses modified action uo which is as simi- lar as possible to uj while ensuring safety. We consider an action to be safe if, after executing that action in the environment, there exists a sequence of follow-up actions U1,..., u -1 which keeps the system away from the unsafe states over finite time horizon H. In more de- tail, our intervention technique works in three steps:
Algorithm Shielding a proposed action procedure WPSHIELD(M M, Tg. ug) + APPROXIMATE(M M, 2o, mn)
6H + N X E S' Sy for / from H - down to 0 do
Φi + wP( à + xo + xol (uo..... ".....,,u-I1. -
arg min
||u6 uill
Wy.... 2
return U6
Approximating the environment. Because computing the weakest precondition of a constraint with respect to a complex environment model (e.g., deep neural network) is intractable, Algorithm calls the APPROXIMATE procedure to obtain simpler first-order local Taylor approximation to the environment model centered at (Iu, u(). That is, given the environment model M, it computes matrices A and B, a vector and an error E such that f(x u) Ax + Bu + c + A where A is an unknown vector with elements in [-8,e], The error term is computed based on normal Taylor series analysis such that with high probability, M(x,, u) f(æ u) in region close to 2g and unj-
Computation of safety constraint. Given a linear approximation f of the environment, Algorithm iterates backwards in time, starting with the safety constraint Φæ at the end of the time horizon H.
Note that À anonymous function operator rather than regularization constant.
3

---

Published as a conference paper at ICLR 2023
In particular, the initial constraint Φн asserts that all (symbolic) states X1...., .. XH reached within the time horizon are inside the safe region. Then, the loop inside Algorithm 2 uses the WP procedure (described in the next two subsections) to eliminate one symbolic state at time from the formula d;- After the loop terminates, all of the state variables except for Xo have been eliminated from on. so dn is formula over Xo, wh, ..... WH--H The next line of Algorithm simply replaces the symbolic variable Xo with the current state To in order to find a constraint over only the actions.
Projection onto safe space. The final step of the shielding procedure is find sequence Mo...., - of actions such that (1) o is satisfied and (2) the distance uo u6ll is minimized. Here, the first condition enforces the safety of the shielded policy, while the second condition ensures that the shielded policy is as similar as possible to the original one. The notation uo..... = F ø indicates that á is true when the concrete values uo..... - are substituted for the symbolic val- ues wo, ... WH- in é. Thus, the arg min in Algorithm
2 is effectively projection on the set of action sequences satisfying Φ. We discuss this optimization problem in Section 4.4
4.2 WEAKEST PRECONDITIONS FOR POLYHEDRA
In this section, describe the WP procedure used in Algorithm 2 for computing the weakest pre- condition of a safety constraint & with respect to a linear environment model f. To simplify presen- tation, we assume that the safe space is given as convex polyhedron i.e., all safe states satisfy the linear constraint Px + S O. We will show how to relax this restriction in Section
Recall that our environment approximation f is a linear function with bounded error, so we have constraints over the symbolic states and actions: Xi+1 = Ax + A where A is an unknown vector with elements in [-e, In order to compute the weakest precondition of linear constraint with respect to f. we simply replace each instance of Xi+1 in ø with Ax; + Bw: + e+ A' where A the most pessimistic possibility for A. Because the safety constraints are linear and the expression for Xi+1 is also linear, this substitution results in a new linear formula which is conjunction of constraints of the form wt' v + v v''' A < y. For each element A; of A, if the coefficient of A; is positive in v, then we choose A; = s. Otherwise, we choose A = -e This substitution yields the maximum value of x" A and is therefore the most pessimistic possibility for AT
Example. We illustrate the weakest precondition computation through simple example: Consider a car driving down a (one-dimensional) road whose goal is to reach the other end of the road as quickly as possible while obeying a speed limit. The state of the car is position and velocity v. The action space consists of an acceleration a. Assume there bounded noise in the velocity updates so the dy- namics are x' = x + 0.1v and v = u + 0. + where -0.01 < E S 0.01 and the safety constraint is < 1. Suppose the current velocity is un = 0.9 and the safety horizon two. Then, starting with the safety constraint v1 < 1 A U2 < 1 and step- ping back through the environment dynamics, we getet the precondition eı < A + 0.1a, + Eι < 1. Stepping back one more time, we find the condition vo 0.1aa + E2 < 1 A to + 0.1ap + 0.1a; E1 + < 1. Picking the most pessimistic values for E1 and E2 to reach to + 0. + 0.01 < 1 A do + 0.1ag + 0.1aj + 0.02 I 1. Since Up is specified, replace to with 0.9 to simplify this
a1
4g 0.8
0.92+0.1,,0011q.11
a,
u 4-=1
Figure 1: Weakest precondition example.
constraint over the two actions dg and d1, namely 0.91 + 0.1 < 1 A 0.92 + 0.10p + 0.1a; < 1. Figure I shows this region as the shaded triangle on the left. Any pair of actions (ag, a1) which lies inside the shaded triangle is guaranteed to satisfy the safety condition for any possible values of e and É2.
4.3 EXTENSION TO MORE COMPLEX SAFETY CONSTRAINTS
In this section, we extend our weakest precondition computation technique to the setting where the safe region consists of unions of convex polyhedra. That is, the state space is represented as
set of matrices P. and set of vectors qi such that S \ Su -. {ar E S P..: + qi S 0).
4

---

Published as a conference paper at ICLR 2023
Note that, while individual polyhedra are limited in their expressive power, unions of polyhedra can approximate reasonable spaces with arbitrary precision. This is because a single polyhedron can approximate a convex set arbitrarily precisely (Bronshteyn & Ivanov 1975). unions of polyhedra can approximate unions of convex sets.
In this case, the formula Φи in Algorithm has the form Φи 1= (=1 Pix, + q S O. However, the weakest precondition a formula of this kind can be difficult to compute. Because the system may transition between two different polyhedra each time step, there is combi- natorial explosion in the size of the constraint formula, and a corresponding exponential slow- down in the weakest precondition computation. Therefore, we replace Φи with an approximation 6'n - Pix; + qi S (that is, we swap the conjunction and the disjunction). Note that ΦH and LHH are not equivalent, but O'H is a stronger formula (i.e., O'H = Φн). Thus, any states satisfying 6H also guaranteed to satisfy Φн, meaning that they will be safe. More intuitivelyy this modification asserts that, not only does the state stay within the safe region at each time step, but it stays within the same polyhedron at each step within the time horizon.
With this modified formula, we can pull the disjunction outside the weakest precondition, i.e.,
WP 1 V
N H Pxx + + S 00f -
H P.x, 9 9: 5.
i=1 WP
The conjunctive weakest precondition on the right of the form described in Section 4.2 so this computation can be done efficiently. Moreover, the number of disjuncts does not grow as we iterate through the loop in Algorithm 2 of control, allowing for the overall weakest precondition on oi to be computed quickly.
This prevents the weakest precondition formula from growing out
Intuitively, the approximation we make to the formula Φи does rule out some potentially safe action sequences. This is because it requires the system to stay within a single polyhedron over the entire horizon. However, this imprecision can be ameliorated in cases where the different polyhedra com- prising the state space overlap one another (and that overlap has non-zero volume). In that case, the overlap between the polyhedra serves as a "transition point," allowing the system to maintain safety within one polyhedron until it enters the overlap, and then switch to the other polyhedron in order to continue its trajectory. A formal development of this property, along with an argument that is satisfied in many practical cases, is laid out in Appendix B
Example. Consider an environment which represents a robot moving in 2D space. The state space four-dimensional, consisting of two position elements æ and y and two velocity elements v and v" The action space consists of two acceleration terms a= and a", giving rise to the dynamics
0.
= + 0.1
x -- 0.1aa
r = 0d + 0.
In this environment, the safe space is x 2 2V S 1, so that the upper-left part of the state space considered unsafe. Choosing a safety horizon of H
we start with the initial constraint (ri 2 2 V < 1) A (I) 2 2 y2 < 1). We transform this formula to the stronger formua (I1 2 2 x2 2 2) V (01 I $1A92 y2 S 1). By stepping backwards through the weakest precondition twice, we obtain the following formula over only the current state and future actions:
(xo + 0.1 2 xo + 0.2v + 0.01a 2) V (yo 0.1ug < 1 A yo + 0.2ug 0.01a 1).
4.4 PROJECTION ONTO THE WEAKEST PRECONDITION
After applying the ideas from Section 4.3 each piece of the safe space yields a set of linear con- straints over the action sequence Uo ..... - That is, 6 from Algorithm 2 has the form
Gi + h; S 0.
Now, we need to find the action sequence satisfying á for which the first action most closely matches the proposed action ug. In order do this, can minimize the objective function 1t00-,6l'" This function is quadratic, so we can represent this minimization problem as quadratic programming problems. That is, for each polyhedron P: qi in the safe region, solve:
minimize || uoll
subject to Σ ==
Σ Gifuy + h, S
5

---

Published as a conference paper at ICLR 2023
Such problems can be solved efficiently using existing tools. By applying the same technique inde- pendently to each piece of the safe state space, we reduce the projection problem to a relatively small number of calls to a quadratic programming solver. This reduction allows the shielding procedure to be applied fast enough to generate the amount of data needed for gradient-basee based learning.
Example: Consider again Figure Suppose the proposed action is ug 1, represented by the solid line in [igure[] Since the proposed action is outside of the safe region, the projection operation will find the point inside the safe region that minimizes the distance along the un axis only. This leads to the dashed line in Figure |
which is the action uo that is as close as possible to uy while still intersecting the safe region represented by the shaded triangle. Therefore, in this case, WPSHIELD would return 0.8 as the safe action.
5 THEORETICAL RESULTS
We will now develop theoretical results on the safety and performance of agents trained with SPICE. For brevity, proofs have been deferred to Appendix A
For the safety theorem, we will assume the model is approximately accurate with high probability and that the APPROXIMATE procedure gives a sound local approximation to the model. Formally, Prar~P(-la.a) III (ax, u) æ'1l > e) < 5M, and f = APPROXIMATE(M.. (M, Zo, un) then for all actions and all states æ reachable within H time steps, M (xx, u)) E S(x u).
Theorem Let Zn be a safe state and let ı be any policy. For S i < H, let u, WPSHIELD(M, Hi xxx))) and let Ii+1 be the result of taking action u, at state Vi. Then with probability at least (1 - d,s)', )", 2z is safe.
This theorem shows why SPICE is better able to maintain safety compared to prior work. Intuitively, constraint violations can only occur in SPICE when the environment model is incorrect. In contrast, statistical approaches to safe exploration are subject to safety violations caused by either modeling error or actions which are not safe even with respect to the environment model. Note that for safety level 5 and horizon H, modeling error can be computed as 8λ < 1 (11-(1100)) 121-6), 5)/ cxp(H -)).
The performance analysis based on treating Algorithm I as functional mirror descent in the policy space, similar to Verma et al. (219) and Anderson et al.) (2020). We assume class of neural policies F, a class of safe policies G. and a joint class H. of neurosymbolic policies. We proceed by considering the shielded policy Az. WPSHIELD( M, æ, NN (x)) to be projection of the neural policy TN into G for Bregman divergence Dy defined by a function F. We define a safety indicator Z which is one whenever WPSHIELD(M, x, ( (x)) = ạ (x)) and zero otherwise, and we let Ç = E[1 Z]. Under reasonable assumptions (see Appendix A for a full discussion), we prove a regret bound for Algorithm [
(4) Theorem 2. Let S for Siisi T be a sequence of safe policies learned by SPICE (i.e., T Ax. WPSHIELD [,, a. (x=))) and let n'g be the optimal safe policy. Additionally we assume the reward function R is Lipschitz in the policy space and let Lg be the Lipschitz constant of R, 3 and o² be the bias and variance introduced by sampling in the gradient computation, be upper bound on the bias incurred by using projection onto the weakest precondition to approximate imitation learning, Gm be an upper bound the KL divergence between the model and the true environment dynamics at all time steps, and en be an upper bound on the TV divergence between the policy used gather data and the policy being trained at all time steps. Then setting the learning rate
n V σr ( + +e). we have the expected regret bound:
R(T3) - E Σ. .-1
- ((=)))
T R(
R
B ( I + - LRC + cm +
This theorem provides a few intuitive results, based on the additive terms in the regret bound. First, < is the frequency with which we intervene in network actions and as Ç decreases, the regret bound becomes tighter. This fits our intuition that, as the shield intervenes less and less, we approach standard reinforcement learning. The two terms cm and 6 are related to how accurately the model captures the true environment dynamics. As the model becomes more accurate, the policy converges to better returns. The other terms are related to standard issues in reinforcement learning, namely the error incurred by using sampling approximate the gradient.

---

Published as a conference paper at ICLR 2023
400
200
20/0
car-racing
(b) goisy-road-22
(c) obstacle
(d) obstacle2
(e) pendulum
(1) road-2d
Figure 2: Cumulative safety violations over time.
EXPERIMENTAL EVALUATION
We now turn to practical evaluation of SPICE. Our implementation of SPICE uses PyEarth (Rudy) 2013) for model learning and CVXOPT (Anderson et al. 2022) for quadratic programming. Our
learning algorithm is based on MBPO (Janner et al. 2019 using Soft Actor-Critic (Haarnoja al.
2018a) as the underlying model-free learning algorithm. Our code adapted from Tandon (2018).
We test SPICE using the benchmarks considered in Anderson al. (2020). Further details of the
benchmarks and hyperparameters are given in Appendix
We compare against two baseline approaches: Con- strained Policy Optimization (CPO) (Achiam et al.] 2017). model-free safe learning algorithm, and a version of our approach which adopts the conserva- tive safety critic shielding framework from [harad- hwaj et al.) (222T) (CSC-MBPO). Details of the CSC-MBPO approach are given in Appendix C We additionally tested MPC-RCE (Liu et al.) (020). an- other model-based safe-learning algorithm, but we find that it is too inefficient to be run on our bench- marks. Specifically MPC-RCE was only able to fin- ish average 162 episodes within 2-day time pe- riod. Therefore, we do not include MPC-RCE in the results presented in this section.
Benchmark
CPO
CSC-MBPO
SPICE
acc
684
137
286
car-racing
2047
1047
1169
mountain-cat
2374
2389
6
noisy-road
0
0
0
noisy-road-24
286
37
31
obstacle
708
124
2
obstacle2
5592
1773
1861
pendulum
1933
2610
1211
road
0
0
0
road-2d 103
64
41
Average
9.48
3.77
1
Table 1: Safety violations during training.
Safety. First, we evaluate how well our approach ensures system safety during training. In Table [
we present the number of safety violations encountered during training for our baselines. The last row of the table shows the average increase in the number of safety violations compared to SPICE (computed as the geometric mean of the ratio of safety violations for each benchmark). This table shows that SPICE is safer than CPO every benchmark and achieves, on average, a 89% reduction in safety violations. CSC-MBPO is substantially safer than CPO, but still not safe as SPICE. We achieve 73% reduction safety violations on average compared to CSC-MBPO. To give a more detailed breakdown, Figure 2 shows how the safety violations accumulate over time for several of our benchmarks. The solid line represents the mean over all trials while the shaded envelope shows the minimum and maximum values. As be seen from these figures, CPO starts accumulate violations more quickly and continues to violate the safety property more over time than SPICE. Figures for the remaining benchmarks can be found in Appendix C
Note that there are a few benchmarks (ace, car-racing, and obstacle2) where SPICE incurs more violations than CSC-MBPO. There are potential reasons for this increase. First, SPICE relies

---

Published as a conference paper at ICLR 2023
(a) car-racing
(b) noisy-road-20
(c) obstacle
1290
000K
30000
11k0
2885
10005
stde 11000
(d) obstacle2
(c) pendulum
road-2d
Figure 3: Training curves for SPICE and CPO.
on choosing a model class through which to compute weakest preconditions (i.c., we need to fix an linear approximation,
A APPROXIMATE function in Algorithm 2). For these experiments, but this can introduce a lot of approximation error. A more complex model class allowing a more precise weakest precondition computation may help reduce safety violations. Second, SPICE uses a bounded-time analysis to determine whether safety violation can occur within the next few time steps. By contrast, CSC-MBPO uses a neural model predict the long-term safety of action. As result, actions which result in safety violations far into the future may be easier to intercept using the CSC-MBPO approach. Given that SPICE achieves much lower safety violations on average, think these trade-offs are desirable in many situations.
Performance. We also test the performance of the learned policies on each benchmark in order to under- stand what impact our safety techniques have on model learning. Figure 3 show the average return over time for SPICE and the baselines. These curves show that in most cases SPICE achieves performance close to that of CPO, and about the same as CSC-MBPO. We believe that the relatively modest performance penalty incurred by SPICE an acceptable trade-off in some safety-critical systems given the massive improvement safety. Further results are presented in Appendix C
28
Figure 4 shows the trajectories of policies learned by SPICE, CPO, and CSC-MBPO part-
Qualitative Evaluation.
Figure 4: Trajectories early in training.
way through training (after 300 episodes). In this figure, the agent controls robot moving on a 2D plane which must reach the green shaded area while avoiding the red cross-hatched area. For each algorithm, we sampled 100 trajectories and plotted the worst one. Note that, at this point during training, both CPO and CSC-MBPO behave unsafely, while the even worst trajectory sampled un- der SPICE was still safe. See Appendix C for a more complete discussion of how these trajectories evolve over time during training.
7 RELATED WORK
Existing work in safe reinforcement learning can be categorized by the kinds of guarantees it pro- vides: statistical approaches bound the probability that violation will occur, while worst-case analyses prove that a policy can never reach an unsafe state. SPICE is, strictly speaking, a statis- tical approach-wwthee predefined environment model, cannot guarantee that the agent will
8

---

Published as a conference paper at ICLR 2023
never behave unsafely. However, show experimentally. our approach is substantially safer in practice than existing safe learning approaches based on learned cost models.
Statistical Approaches. Many approaches to the safe reinforcement learning problem provide sta- tistical bounds on the system safety (Achiam et al. 2017 Liu et al., 2020, Yang et al., 2020 Ma
et al. 2021 Zhang et al. 2020; Satija al. 2020). These approaches maintain environment model and then use a variety of statistical techniques to generate a policy which is likely to be safe with respect the environment model. This leads to two potential sources of unsafe behavior: the policy may be unsafe with respect to the model, or the model may be an inaccurate representation of the environment. Compared to these approaches, we eliminate the first source of error by always generating policies that are guaranteed to be safe with respect to an environment model. We show in our experiments that this drastically reduces the number of safety violations encountered in prac- tice. Some techniques use learned model together with linearized cost model to provide bounds, similar to our approach (Dalal et al.) 2018 Li et af.) (02T). However, in these works, the system only looks ahead one time step and relies on the assumption that the cost signal cannot have too much inertia. Our work alleviates this problem by providing a way to look ahead several time steps to achieve a more precise safety analysis.
A subset of the statistical approaches are tools that maintain neural models of the cost function in order to intervene in unsafe behavior (Bharadhwaj et al. 1021 Yang et al. 2021; Yu et al. 2022) These approaches maintain a critic network which represents the long-term cost of taking a particular action in particular state. However, because of the amount of data needed to train neural networks accurately, these approaches suffer from a need to collect data in several unsafe trajectories in order build the cost model. Our symbolic approach is more data-efficient, allowing the system avoid safety violations more often in practice. This is borne out by the experiments in Section 6
Worst-Case Approaches. Several existing techniques for safe reinforcement learning provide for- mally verified guarantees with respect to worst-case environment model, either during training (Anderson et al., 22200) or convergence (Alshickh al. 2018 Bacci et al.] [02T Bastani et al., & Platzer 2019 Gillula & Tommin [0122] Zhu et al. 2019). An alternative class of approaches uses either a nominal environment model (Koller et al. 2018 Fisac et al.] 2019) or user-provided safe policy
starting point for safe learning (Chow et al. 2018 Cheng et al.) 2019). both cases, these techniques require a predefined model of the dynamics of the environ- ment. In contrast, technique does not require the user specify any model of the environment, so it can be applied to a much broader set of problems.
8 CONCLUSION
SPICE is a new approach to safe exploration that combines the advantages of gradient- sandient-based learn- ing with symbolic reasoning about safety. In contrast to prior work on formally verified ex exploration (Anderson et al.) 2020). SPICE can be used without a precise, handwritten specification of the envi- ronment behavior. The linchpin of our approach is a new policy intervention which can efficiently intercept unsafe actions and replace them with actions which are as similar as possible, but prov- ably safe. This intervention method is fast enough to support the data demands of gradient-based reinforcement learning and precise enough to allow the agent to explore effectively.
There are few limitations to SPICE. Most importantly, because the interventions are based on a linearized environment model, they are only accurate in a relatively small region near the current system state. This in turn limits the time horizons which can be considered the safety analysis, and therefore the strength of the safety properties. Our experiments show that SPICE is still able to achieve good empirical safety in this setting, but a more advanced policy intervention that can handle more complex environment models could further improve these results. Additionally, SPICE can make no safety guarantees about the initial policy used to construct the first environment model, since there is model to verify against the time that that policy is executed. This issue could be alleviated by assuming a conservative initial model which is refined over time, and there is an interesting opportunity for future work combining partial domain expertise with learned dynamics.

---

Published as a conference paper at ICLR 2023
FUNDING ACKNOWLEDGEMENT
This work was supported in part by the United States Air Force and DARPA under Contract No. PA8750-20-C-0002, by ONR under Award No. N00014-20-1-2115, and by NSF under grants CCF- 1901376 and CCF-191 1888.. Compute resources for the experiments were provided by the Texas Advanced Computing Center.
REFERENCES
Joshua Achiam, David Held, Aviv Tamar, and Pieter Abbeel. Constrained policy optimization. In Proceedings of the 34th International Conference on Machine Learning Volume 70, ICML' 17, pp. 22 JMLR. org, 2017.
Mohammed Alshiekh, Roderick Bloem, Rüdiger Ehlers, Bettina Könighofer, Scott Niekum, and Ufuk Topeu. Safe reinforcement learning via shielding. In Sheila A. Mcllraith and Kil- ian Q. Weinberger (eds.), Proceedings of the Thirty-Second AAAI Conference on Artificial In- telligence, (AAAI-18), the 30th innovative Applications of Artificial Intelligence (IAAI-18), and the 8th AAAI Symposium on Educational Advances in Artificial Intelligence (EAAI-18), New Orleans, Louisiana, USA, February 2-7, 2018, pp. 2669 2678. AAAI Press, 2018. URL https: www aaai. org/ OCS/ index. phpppppppp../pppp AAAI/
AAAIAAAAAAAAAAAAAAA AAAIIAAAIIIII 1ttppppereeeeppeeeee hatp//er/ieew/12//// 17111
Greg Anderson, Abhinav Verma, Isil Dillig, and Swarat Chaudhuri. Neurosymbolic reinforcement learning with formally verified exploration. In H. Larochelle, M. Ranzato, R. Hadsell, M.F. Balcan, and H. Lin (eds.), Advances in Neural Information Processing Systems, volume 33, pp. 6172-6183. Curran Associates, Inc., 2020. URL stttpss:/prroceddinng .eer.... www.nneuriic.mm cc/ (9tpeeedda9991111
paper/2020/File/444 F40
Martin Anderson, Joachim Dahl, and Lieven Vandenberghe. CVXOPT. https://giite
com/ http://ctxopppppp///// 2022.
Edoardo Bacci, Mirco Giacobbe, and David Parker. Verifying reinforcement learning up to infinity. In Zhi-Hua Zhou (ed.), Proceedings of the Thirtieth International Joint Conference Artificial Intelligence, IJCAI-21, pp. 2154-2160, International Joint Conferences on Artificial Intelligence Organization, 8 2021. doi: 10.2496 00.24963/jccai.2221222 URL https:://oii.ooeo http://di..rgg//...00/2
ijcai. 2021/277
Main Track.
Osbert Bastani, Yewen Pu, and Armando Solar- Verifiable reinforcement learning via policy extraction. In Advances in Neural Information Processing Systems, pp. 2494-2504, 2018.
Felix Berkenkamp, Matteo Turchetta, Angela Schoellig, and Andreas Krause. Safe model-based reinforeement learning with stability guarantees. Advances in neural information processing sys- tems, 30, 2017.
Homanga Bharadhwaj, Aviral Kumar, Nicholas Rhinehart, Sergey Levine, Florian Shkurti, and Ani- mesh Garg. Conservative safety critics for exploration. In International Conference on Learning Representations, 2021. URL httpp//e//oee.eeeeeeeeeeeeeeeeep 1o0
E. M. Bronshteyn and I.. D. Ivanov. The approximation of of convex sets by polyhedra. Sib Math J, 16(5):852 853, September- October 1975. doi: 10. 00.1000//F00067115
Richard Cheng, Gábor Orosz, Richard M. Murray, and Joel W. Burdick. End-to-end safe re- inforcement learning through barrier functions for safety-critical continuous control tasks. In Proceedings of the Phirty-Third AAAI Conference on Artificial Intelligence. AAAI'19, AAAI doi: (t..0///aai..3311.333000000 609//aai........................ v33101 w33.....311113333333.3333333333. 33013387
Press, 2019. ISBN 978-1-57733 809-1.
URL https:
//doi.org///
Yinlam Chow, Ofir Nachum, Edgar Duenez-Guzman, and Mohammad Ghavamzadeh. Iyapunov- based approach to safe reinforcement learning. In Proceedings of the 32nd International Con- ference on Neural Information Processing Systems, NeurlPS' 18, pp. 8103-81 12, Red Hook, NY, USA, 2018. Curran Associates Inc.
10

---

Published as a conference paper at ICLR 2023
Gal Dalal, Krishnamurthy Dvijotham, Matej Vecerik, Todd Hester, Cosmin Paduraru, and Yuval Tassa. Safe exploration in continuous action spaces. arXiv preprint arXiv:1801.0875) 2018.
Edsger Wybe Dijkstra. A discipline of programming, volume 613924118, prentice-hall Englewood Cliffs, 1976.
Jaime F. Fisac, Anayo Akametalu, Melanie N. Zeilinger, Shahab Kaynama, Jeremy Gillula, and Claire J. Tomlin. A general safety framework for learning- based control in uncertain robotic systems. IEEE Transactions on Automatic Control, 64(7):2737-2752, 2019, doi: 10.1 109/TAC. 2018.2876389.
Nathan Fulton and André Platzer. Verifiably safe off-model reinforcement learning. In International Conference Tools and Algorithms for the Construction and Analysis of Systems, pp. 413 413-430. Springer, 2019.
Javier Gareia and Fernando Fernández. A comprehensive survey on safe reinforcement learning. Journal of Machine Learning Research, 16(1):1437-144) 2015.
Jeremy H. Gillula and Claire J. Tomlin. Guaranteed safe online learning via reachability; tracking a ground target using quadrotor. In IEEE International Conference Robotics and Automation,
2012. doi: 10. 109/ ICRA 2012, 14-18 May, 2012, St. Paul, Minnesota, USA, pp. 2012. 22211111..2266666 6225136 ICRA.2012.6225136. httth::s://eee
org 10. www.:1119/IR......
Tuomas Haarnoja, Aurick Zhou, Pieter Abbeel, and Sergey Levine. Soft actor-critic: Off-policy maximum entropy deep reinforcement learning with stochastic actor. In Jennifer Dy and An- dreas Krause (eds.), Proceedings of the 35th International Conference on Machine Learning, volume 80 of Proceedings of Machine Learning Research, pp. 1861-1870. PMLR, 10-15 Jul ml press/ wwtpeess//e/haaaaae ja 8b. html
2018a. htttts::/pproeeeeeeeeeee
Tuomas Haarnoja, Aurick Zhou, Kristian Hartikainen, George Tucker, Sehoon Ha, Jie Tan, Vikash Kumar, Henry Zhu, Abhishek Gupta, Pieter Abbeel, and Sergey Levine. Soft actor-critic algo- rithms and applications, 2018b.
05905
Michael Janner, Justin Fu, Marvin Zhang, and Sergey Levine. When to trust your model: Model- based policy optimization. In Proceedings of the 33rd International Conference on Neural Infor- mation Processing Systems, Red Hook, NY, USA, 2019. Curran Associates Inc.
Torsten Koller, Felix Berkenkamp, Matteo Turchetta, and Andreas Krause. Learning-based model predictive control for safe exploration. In 2018 IEEE Conference on Decision and Control (CDC), pp. 6059-6066, 2018. doi: 10. 11L10//CDC.2218.86199999
Yutong Li, Nan Li, H. Eric Tseng, Anouck Girard, Dimitar Filev, and Ilya Kolmanovsky. Safe reinforcement learning using robust action governor. In Ali Jadbabaie, John Lygeros, George J. Pappas, Pablo A. Parrilo, Benjamin Recht, Claire J. Tomlin, and Melanie N. Zeilinger (eds.), Proceedings of the 3rd Conference on Learning for Dynamics and Control, volume 144 of Pro- ceedings of Machine Learning Research, pp. 1093 1 104. PMLR, 07 - 08 June 2021. URL html
https://prroeeednngg mlr wttpsnnww.........sssseesmee
Zuxin Liu, Hongyi Zhou, Baiming Chen, Sicheng Zhong, Martial Hebert, and Ding Zhao. Con- strained model-based reinforcement learning with robust cross-entropy method, 2020.
Yecheng Jason Ma, Andrew Shen, Osbert Bastani, and Dinesh Jayaraman. Conservative and adap- tive penalty for model-based safe reinforcement learteeeneeetteeennnnenaaan 2021. URL http::tss/ssii.orrrtttt abs/2112.07703
Jason Rudy. 2013.
Harsh Satija, Philip Amortila, and Joelle Pineau. Constrained markov decision processes via back- ward value functions. In Proceedings of the 37th International Conference on Machine Learning, ICML'20. JMLR. 2020.
11

---

Published as a conference paper at ICLR 2023
Richard S. Sutton, David McAllester, Satinder Singh, and Yishay Mansour. Policy gradient methods for reinforcement learning with function approximation. In Proceedings of the 12th International Conference Neural Information Processing Systems, NIPS 99, pp. 1057-1063, Cambridge, MA, USA, 1999. MIT Press.
Pranjal Tandon. PyTorch Soft Actor-Critic.
http:://ggthub..cmm/raaaaa
pytorch- soft cnctor-critio 2018.
Abhinav Verma, Hoang Lc. Yisong Yue, and Swarat Chaudhuri. imitation-prooecttee programmatic reinforcement learning. In H. Wallach, H. Larochelle, A. Beygelzimer, F. d'Alché-Buc; E. Fox, and R. Garnett (eds.). Advances in Neural Information Processing Systems, volume 32. Cur- ran Associates, Inc., 2019. URL /ttp: /ttp:/tppp.//po.eeiiinngoggggg wtw.eeeedddinnne.nii..eeee wwwrips...... wtt.e/ipss..pppppe///00000 cctppprr/ppp/ Pap.eeeffpaapprppp...
Qisong Yang. Thiago D. Simão, Simon H Tindemans, and Matthijs T. J. Spaan, Wesac: Worst- case soft actor critic for sufety-consttaiined reinforcement learning. Proceedings of the AAAI Conference on Artificial Intelligenne, 35012):00339-1664 May 2021. URL https://ojs.
Tsung-Yen Yen Yang, Justinian Rosca, Karthik Narasimhan, and Peter J Ramadge. Projection-based constrained policy optimization. arXiv preprint arXiv:2010.03152. 2020.
Dongjie Yu, Haitong Ma, Shengbo Li, and Jianyu Chen. Reachability constrained reinforcement learning. In Kamalika Chaudhuri, Stefanie Jegelka, Le Song, Csaba Szepesvari, Gang Niu, and Sivan Sabato (eds.), Proceedings of the 39th International Conference on Machine Learning, volume 162 of Proceedings of Machine Learning Research, pp. 336636225655 PMLR, 17-23 Jul 2022. URL htttttts/pppoottoo
ml mt..s...r.ssssssssss.........s.s
prw.s/ http:/vv2222/2222/2 y
Yiming Zhang, Quan Vuong, and Keith Ross. First order constrained optimization in pol- icy space. In H. Larochelle, M. Ranzato, R. Hadsell, M.F. Balcan, and H. Lin (eds.), Ad- vances in Neural Information Processing Systems, volume 33, pp. 15338-15344 Curran As-
sociates, Inc., 2020. URL UtL/htttss://ppoceedii neuriss pctppppper/222///iieeee Papeeeeeeeds5bbb-par..ppe_ pdf
He Zhu, Zikang Xiong. Stephen Magill, and Suresh Jagannathan. An inductive synthesis framework for verifiable reinforcement learning. In ACM Conference Programming Language Design and Implementation (SIGPLAN), 2019.
A PROOFS OF THEOREMS
In this section we present proofs for the theorems in Section 5 First, we will look at the safety results. We need some assumptions for this theorem:
Assumption 1. The function APPROXIMATE returns a sound, nondeterministic approximation of M in region reachable from state ag a time horizon H. That is, let Sn be the set of all states x for which there exists a sequence of actions under which the system can transition from Do to æ within H time steps. Then if f APPROXIMATE(M, xo, u.) then for all x SR and u A. M(x, u) E (xx u).
Assumption 2. The model learning procedure returns a model which is close to the actual environ- ment with high probability. That is, if M is a learned environment model then for all x, u,
Prx P( M[,, u) x'1l $] <
Definition 1. A state To is said to have realizable safety over time horizon H if there exists sequence of actions ug...., u such that, when o,....,Ip h is the trajectory unrolled starting from ao in the true environment, the formula & inside WPSHIELD(M, æ;, T(xx)) is satisfiable for all
Lemma 1. (WPSHIELD is safe under bounded error.) Let H be time horizon, æn be state with realizable safety over H. M be an environment model, and π be a policy. Choose E such that for all states and actions u. || (x. u. x'Il < where x' is sampled from the true environment transition at x and u. For S < H let u; = WPSHIELD(M (,, x;, π (xx)) and let xc+1 1 be sampled from the true environment at my and u, Then for 0 < í H, a; Su-
12

---

Published as a conference paper at ICLR 2023
Proof. Combining Assumption [ with condition 1 in the definition of weakest preconditions, conclude that for all e E (x,, u:), wP(0 f) = 01+1 H el. Stepping backward through the loop in WPSHIELD, we find that for all E ( u;-1) for 1 S S H, Φ0 on [1 H e1,..., RH H en]. Because Φи asserts the safety of the system, we have that Φp also implies that the system is safe. Then because the actions returned by WPSHIELD constrained to satisfy 6o, we also have that 2; for 0 S i S. H are safe.
Theorem 1 (WPSHIELD is probabilistically safe.) For given state 2y with realizable safety over time horizon H, a neural policy π, and an environment model M. let and 8 be the error and probability bound of the model defined in Assumption - For 0 S H, let u, WWSSHELLD M, æi, π (xx:) and let Fi+1 be the result of taking action u, at state æ; then with probability at least (1 53', 2s is safe.
Proof. By Lemma 1 if (xx u)) x''l S then n; is safe for all 0 S S H. By Assumption 2 (xx, u) x' S & with probability at least - 6. Then at each time step, with probability at most ó the assumption of Lemma[]is violated. Therefore after i time steps, the probability that Lemma] can be applied is at least (1 11-8) 8)", so a, is safe with probability at least (1 6)'
In order to establish regret bound, we will analyze Algorithm as functional mirror descent in the policy space. this view, we assume the existence of a class of safe policies, class 2 g of neural policies, and class H of mixed, neurosymbolic policies.
define a safety indicator Z which is one whenever WPSHIELD(M, x, ((x) = T T(x) and zero otherwise. We will need number of additional assumptions:
1. H. is vector space equipped with an inner product (:,-) and induced norm || v (TT,));
2. The long-term reward Li--iscchht:;
3. F is convex function H. and V is Lp-Lipschitz continuous H;
4. H. is bounded (i.e., sup(l| x'll т. x' E H} < oo);
5. [E[1 2] s Ç, i.e., the probability that the shield modifies the action is bounded above by Ç:
6. the bias introduced in the sampling process is bounded by 3, i.c.,
||E[">
y R(T) < B, where V is the estimated gradient;
7. for x E S. u E A. and policy π E H. if ( x) > 0 then 7 (
x) > 5 for some fixed
8 >>0 0;
8. the KL--divergence between the true environment dynamics and the model dynamics are is bounded by emi and
9. the TV-divergence between the policy used to gather data and the policy being trained is bounded by G-
For the following regret bound, we will need three useful lemmas from prior work. These lemmas are reproduced below for completeness.
Lemma 2. (Junner et al.) (2019), Lemma B.3) Let the expected KL-divergence between two trun- sition distributions be bounded by max, Bez=p(()) (m)) DrI(pi (æ'u .. x:) (p)(,', x)) S and max Drv (ov((Talu (u T2( ( x)) Cr. Then the difference in returns under dynamics pr with policy Ti and p2 with policy T2 is bounded by
2RT(Ex + Em) 2R
[Rp (TT) Rpp (TZ))
+ 1 = = + Em)-
71-
Lemma 3. Anderson et al. 2020 Appendix B) Let D be the diameter of H. i.e., D = sup || T'll n. n H). Then the bias incurred by approximating VuR(T) with 5 R(()) is bounded by
V
| - VH O (3 Inc)
Lemma 4. (Verma et al. (2019). Theorem 4.1 Let Let Te... Rr be sequence of safe policies returned by Algorithm (i.e. n, is the result of calling WPSHIELD on the trained policy) and let x be the optimal safe policy. Letting B and o² be bounds on the bias and variance of the gradient
13

---

Published as a conference paper at ICLR 2023
estimation and let be bound on the error incurred due to imprecision in WPSHIELD. Then
letting 1 V 1 ( + +e), we have the expected regret over T iterations:
_ R(m.) =o (oVVTttt))
R(x") E
Now using Lemma 2 we will bound the gradient bias incurred by using model rollouts rather than true-environment rollouts.
Lemma 5. For given policy n, the bias in the gradient estimate incurred by using the environment model rather than the true environment is bounded by
R(T)) R(m) = ( + 6x)
Proof. Recall from the policy gradient theorem (Sutton et al. 1999) that
VrR(T)= Ex Nov log ( x)Q (æx, u)]
where Ps is the state distribution induced by и and QT the long-term expected reward starting from state æ under action u. By Lemma 2 we have (Q" u) - Q" (xx u) I (ce + Gx) where Q" is the expected return under the learned enviromment model. Then because log r(u x) is the same regardless of whether use the environment model the true environment, have V log Tu x) V log ( x) and
R) R(T(
E
V f log
ru x=)"((; u)
E | log (u x)Q* w)]
E
V log ( [=) (x, u)
E E log (u a x) (æ, u)]
V log (
xx) (x, u)
lo x)Q2 (z. u))
r log ( x (Q* (x, u) Q (xxxxu) u
Now because assume x(u x) 8 whenever (u x) 0, the gradient of the log is bounded above by constant. Therefore,
RgR(T)= VnR(T)
O +
(i) for 1 1sisi T be sequence of Theorem (SPICE converges to optimal safe policy.) Let T
safe policies learned by SPICE (i.e., T Ax. WWS.IELDSM,,,, æ, (<)))) and let a the optimal safe policy. Let B and d² be the bias and variance in the gradient estimate which is incurred due to sampling. Then setting the learning rate 17 = v 3/2 ( + e). we have the expected regret bound:
R
E
R
( K
=0
o T + 3+ LRS cm +
T
Proof. The total bias in gradient estimates is bounded by the sum of (i) the bias incurred by sam- pling, (ii) the bias incurred by shield interference, and (iii) the bias incurred by using an environment model rather than the true environment. Part (i) is bounded by assumption, part (ii) is bounded by
Lemma 3l and part (iii) is bounded by Lemma Combining these results, we find that the total bias
in the gradient estimate is O(3 + LRς + cm + ex). Plugging this bound into Lemma 4 we reach the desired result.
14

---

Published as a conference paper at ICLR 2023
B OVERLAPPING POLYHEDRA
In Section 4.3 we claimed that in many environments, the safe region can be represented by over- lapping polyhedra. In this section, we formalize the notion of "overlapping" in our context and explain why many practical environments satisfy this property.
We say two polyhedra "overlap" if their intersection has positive volume. That is, polyhedra pi and P2 overlap if ((1 P2) > 0 where j is the Lebesgue measure.
Often in practical continuous control environments, either this property is satisfied, it is impossi- ble to verify any safe trajectories at all. This because in continuous control, the system trajectory is a path in the state space, and this path has to move between the different polyhedra defining the safe space. To see how this necessitates our overlapping property, let's 's take a look at a few possibilities for how the path can pass from one polyhedron Pi second polyhedron P2. For simplicity, we'll Ill assume the polyhedra are closed, but this argument can be extended straightforwardly to open or partially open polyhedra.
If the two polyhedra are disconnected, then the system is unable to transition between them because the system trajectory must define a path in the safe region of the state space. Since the two sets are disconnected, the path must pass through the unsafe states, and therefore cannot be safe.
Suppose the dimension of the state space is n and the intersection of the two polyhedra is an n - 1 dimensional surface (for example, if the state space is 2D then the polyhedra intersect in a line segment). In this case, we can add a new polyhedron to the set of safe polyhedra in order to provide an overlap to both P1 and p2. Specifically, let X be the set of vertices of P1 O p2- Choose a point 1 in the interior p1 and a point T2 in the interior of P2. Now define p' as the convex hull of X U [ can add p' to the set of safe polyhedra without changing the safe state space as a whole. However, p' overlaps with both p1 and P2, and therefore the modified environment has the overlapping property.
z2 Note that p' C P1 U P2, so we
Otherwise, P1 O P2 is lower-dimensional surface. Then for every point E Pi O p2 and for every e > 0 there exists an unsafe point x' such that || - x'll < c. In order for the system to transition from P1 to P2. it must pass through point which is arbitrarily close to unsafe. As a result, the system must be arbitrarily fragile - any perturbation can result in unsafe behavior. Because real-world systems are subject to noise and/or modeling error, it would be impossible to be sure the system would be safe in this case.
C FURTHER EXPERIMENTAL DATA
In this section we provide further details about our experimental setup and results.
Our experiments are taken fnom/Anderson et al. (2020), and consist of 10 environments with continu- ous state and action spaces. The mountain-car and pendulum benchmarks are continuous versions of the corresponding classical control environments. The acc benchmark represents an adaptive cruise control environment. The remaining benchmarks represent various situations arising from robotics. See Anderson al. (2000), Appendix C for a more complete description of each benchmark.
As mentioned in Section our tool is built on top of MBPO (Janner et al. 2019) using SAC (Haamoja et al. 2018a) as the underlying learning algorithm. We gather real data for 10 episodes for each model update then collect data from 70 simulated episodes before updating the en- vironment model again. We look five time steps into the future during safety analysis. Our SAC im- plementation (adapted from Tandon (2018)) uses automatic entropy tuning as proposed in Haarnoja al. (2018b). To compare with CPO we use the original implementation from Achiam et (2017). Each training process is cut off after 48 hours. We train each benchmark starting from nine distinct seeds.
Because the code for [Bharadhwaj et al. (202)) is not available, we use modified version of our code for comparison, which we label CBC- Our implementation follows Algorithm Algorithm[exceep except that WPSHIELD is replaced by alternative shielding framework. This framework learns neural safety signal using conservative Q-learning and then resamples actions from the policy until a safe action is chosen, as described in (Bharadhwaj al. (202)). We chose this implementation in order to
15

---

Published as a conference paper at ICLR 2023
-0.0
1850
1365 who
(a) acc
(b) mountain-car
(c) noisy-road
-2.0
(d) road
Figure 5: Cumulative safety violations over time.
(a) acc
(b) mountain-car
(c) noisy-road
2010 15000
(d) road
Figure 6: Training curves for SPICE and CPO.
give the fairest possible comparison between SPICE and the conservative safety critic approach, as the only differences between the two tools in our experiments is the shielding approach. The code for our tool includes our implementation of CSC-MBPO.
The safety curves for the remaining benchmarks are presented in Figure Training curves for the remaining benchmarks are presented in Figure
C.1 EXPLORING THE SAFETY HORIZON
As mentioned in Section 6 SPICE relies on choosing a good horizon over which to compute the weakest precondition. We will now explore this tradeoff in more detail. Safety curves for each benchmark under several different choices of horizon are presented Figure 7 The performance curves for each benchmark are shown in Figure 8
There are a few notable phenomena shown in these curves. As expected, in most cases using a safety horizon of one does not give particularly good safety. This is expected because the safety horizon
16

---

Published as a conference paper at ICLR 2023
1elar 11000
Wilh Wila
1000
1980
Hiar Xide
win
(b) car-racing
(c) mountain-can
0.2
2008
2000
1000
2008
1400
10:00 X0588
(d) noisy-road
(e) noisy-rooaa roadd
(f) obstacle
-2.0
00
-.
(g) obstacle2
(h) pendulum
(i) road
1200
2000
road-24
Figure 7: Safety curves for SPICE using different safety horizons
17

---

Published as a conference paper at ICLR 2023
becomes very small, it is easy for the system to end up in state where there safe actions. The obstacle benchmark shows this trend very clearly: as the safety horizon increases, the number of safety violations decreases.
On the other hand, several benchmarks (c.g,, acc, mountain-car and noisy-road- (dd show a more interesting dynamic: very large safety horizons also lead an increase in safety violations. This is little less intuitive because as we look farther into the future, we should be able to avoid more unsafe behaviors. However, in reality there is an explanation for this phenomenon. The imprecision in the environment model (both due to model learning and due to the call to APPROXIMATE accumulates for each time step we need look ahead. As result, large safety horizons lead to fairly imprecise analysis. Not only does this interfere with exploration, but it can also lead to an infeasible constraint set in the shield. (That is, @ Algorithm 2 becomes unsatisfiable.) Al Algorithm 2 is ill-defined, so SPICE relies on simplistic backup controller. This controller is not always able guarantee safety, leading an increase in safety violations as the horizon increases.
this case, the projection in
In practice, we find that safety horizon of five provides good amount of safety in most benchmarks without interfering with training. Smaller or larger values can lead to more safety violations while also reducing performance a little in some benchmarks. In general, tuning the safety horizon for each benchmark can yield better results, but for the purposes of this evaluation we have chosen to use the same horizon throughout
C.2 QUALITATIVE EVALUATION
Figure | shows trajectories sampled from each tool at various stages of training. Specifically, each 100 episodes during training, 100 trajectories were sampled. The plotted trajectories represent the worst samples from this set of 100. The environment represents robot moving in a 2D plane which must reach the green shaded region while avoiding the red crosshatched region. (Notice that while the two regions appear to move in the figure, the are actually static. The axes in each part of the figure change in order to represent the entirety of the trajectories.) From this visualization, we can see that SPICE is able to quickly find a policy which safely reaches the goal every time. By contrast, CSC-MBPO requires much more training data to find good policy and encounters more safety violations along the way. CPO is also slower to converge and more unsafe than SPICE.
18

---

Published as a conference paper at ICLR 2023
-0K
11000
Welr
(a)
car-racing
mountain-com car
1MC Wew 2008
2080
1000
2008
1400
$0.50
30-200
2002
(d) noisy-road
(e) noisy-road--
(f) obstacle
1300
g obstacle2
(h) pendulum
(i) road
12000
12000
road-2d
Figure 8: Training curves for SPICE using different safety horizons
19

---

Published as a conference paper at ICLR 2023
SPRL
CSC Mono
ppoode S03
Eprooch
ploooe S00
Esbsode 100
CP
C70
Figure 9; Trajectories at various stages of training.
20


Reviews:
[{"review_id": "d3-kXa-Agu", "reviewer": "Reviewer_euEh", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "The paper proposes a safe RL algorithm, Symbolic Preconditions for Constrained Exploration (SPICE), that uses a model-based shielding mechanism to produce safe actions. A linearization of the model and polyhedral state constraints are used to determine which actions are safe, and then the proposed action is projected onto the space of safe actions. The paper provides a regret bound for the algorithm and demonstrates that SPICE can attain fewer safety violations during training than model-free baselines.", "summary_of_the_review": "I like the proposed approach and its associated guarantees. My main issues are in the experiments, as detailed above. The state of the experiments makes it hard to recommend acceptance in the paper’s current form, in spite of other positive attributes of the paper.", "strength_and_weaknesses": "Strengths:\n* SPICE’s use of formal methods provides strong safety guarantees if the assumptions hold. This is very desirable in safety critical applications.\n* In experiments, SPICE substantially reduces the number of violations substantially compared to CPO and CSC.\n\nWeaknesses:\n* A footnote states \"We use a modified version of our approach instead of comparing to Bharadhwaj et al. (2021) directly because the code for that paper is unavailable.\" While this is reasonable, the present paper does not provide a description of your modifications. It is difficult for the reader to compare the performance of SPICE vs. “CSC” without knowing exactly what “CSC” means.\n* From Figure 3, the variance of the policy’s performance appears extremely high for both SPICE and CSC. The plots in the CSC paper look much less noisy. This raises questions about the quality of the implementation.\n* SPICE converges to a suboptimal policy (worse than CPO) in many cases.\n* The experiments do not compare to any other model-based safe RL algorithms.\n* Linearization of the model may limit what types of problems SPICE can solve effectively.", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "4: All of the claims and statements are well-supported and correct.", "technical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work.", "empirical_novelty_and_significance": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}, {"review_id": "aib0K4Qbbj", "reviewer": "Reviewer_HV3z", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "The paper proposes a method for safe reinforcement learning whereby it uses a\nlearnt environment to not only optimise policies but also to improve safe\nexploration. Concretely, this is realised by taking a linear approximation of\nthe environment, which in conjunction with the safety specification gives\nlinear constraints (called weakest preconditions in the paper) on the actions\nthat are safe to be performed.", "summary_of_the_review": "The paper builds on previous work on safe reinforcement learning  to derive a\nmethod which although makes strong, linearity assumptions on the environment is\nable to outperform the state-of-the-art in terms of the number of safety\nviolations during training.", "strength_and_weaknesses": "+ The approach reduces the number of safety violations during training when\ncompared with the state-of-the-art in the area.\n\n- Somewhat straightforward and incremental: straightforward in that it relies\n  on linear approximations of the environment and incremental in that the\n  contribution is limited to the derivation of safety predicates within a\n  previously studied framework.", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "4: All of the claims and statements are well-supported and correct.", "technical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work.", "empirical_novelty_and_significance": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}, {"review_id": "MXV1TACjo_", "reviewer": "Reviewer_aN3N", "summary": "", "questions": "", "limitations": "", "rating": 6, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "This paper deals with safe exploration in reinforcement learning in which an agent is required to ensure safety during training. The authors present a neuro-symbolic approach called SPICE. based on symbolic weakest preconditions. Empirically, they evaluate their approach on toy benchmarks, and show that it is able to achieve comparable performance to existing safe learning techniques while incurring fewer safety violations. ", "summary_of_the_review": "Though this paper presents a new, promising method for an interesting problems, there are several issues and concerns about the applicability and empirical evaluations. Hence, I recommend rejection for now.", "strength_and_weaknesses": "### Strength\n- Interesting and importance problem formulation on safe exploration.\n- Unique approach for safe exploration. As far as I know, there is no existing method using weakest precondition.\n\n### Weakness\n- Though the number and quality of baselines looks sufficient to me, benchmark problem is very easy. I think the authors should have tested their method in MuJoCo or SafetyGym benchmarks. The proposed method depends on environment approximation; hence, it is particularly important to know whether it is applicable to non-linear complicated system (I think even negative results are ok, and it is significant to know the limitations).\n- Low applicability to real problems. As the authors discuss the experimental results in the first paragraph on page 8, the proposed method works better than baselines when the environment can be approximated with linear equations. I think this is a huge limitation of the proposed method. I personally recommend the authors to connect this work with Linear MDP (https://arxiv.org/pdf/1907.05388.pdf), which would provide much richer theoretical results and good empirical results under the assumption of feature mapping functions.\n\n### Questions\n- How did the author choose weakest preconditions for each experiments? Is it possible to decrease the constraints violation while tuning the parameter of the weakest preconditions?\n\n### Other comments\n- The equation in Section 2 should be rewritten\n    - (Section 2) $\\text{Safe}(\\pi)$ is not defined.\n    - Is $P_{x∼S{_{\\pi_i}}}(x \\in S_U ) < \\delta$ really what the authors want to represent? I think the probability of an agent's trajectory being safe is $(1-\\delta)^N$ when the length of episode is $N$. I guess the authors should have represented in other equations.", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "2: Several of the paper’s claims are incorrect or not well-supported.", "technical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work.", "empirical_novelty_and_significance": "2: The contributions are only marginally significant or novel."}, "extra_text": {}}, {"review_id": "AQTBBXOc898", "reviewer": "Reviewer_PYp3", "summary": "", "questions": "", "limitations": "", "rating": 8, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "main_review": "", "summary_of_the_paper": "This paper adapts ideas from formal program analysis, i.e. weakest preconditions, to the constrained  reinforcement learning. Here an emphasis is made for (i) working in an a-priori unknown MDP and (ii) minimizing constraint violations during deployment *and* training. \n\nThe key idea is to alternate (i) shielded exploration (ii) system identification/ model learning and (iii) computing a new avoid predicate for the shield. Again, this is done by adapting a classic idea from program analysis (called weakest preconditions) where one tries to identify the largest set such of inputs (the precondition) that guarantees the property (here not violating the constraint) is satisfied.\n\nTechnically, this by linearizing the learned model and learning a (union) of precondition polyhedra. These polyhedra are then used to project the actions proposed by the learned control policy to a safe action (according the learned model).\n\nEmpirically this seems to be very effective and future extensions are proposed (using non-linear models) that would likely yield unambigously state-of-the-art performance.", "summary_of_the_review": "The paper contributes a novel algorithm for creating safety shields during the training of RL-agents. It provides a nice demonstration of the power of alternating model learning and state-of-the-art RL techniques for safe RL. In particular, the paper highlights how model learning in this setting need only deal with qualitative semantics (i.e., is it possible to reach state s) and can let the RL algorithm handle the quantitative optimizations.", "strength_and_weaknesses": "# Strengths\n\nThe technique is well motivated and a good proof of concept regarding combining model based safety analysis with model free RL. There is a clear path towards having robust theoretical guarantees (see weaknesses below) and a there is a literature of techniques on abstract interpretation that are likely to improve the representations of the preconditions.\n\n# Weaknesses\n\n1. Some of the assumptions in the theorems seems difficult to realize. In particular, because the learned safety shield biases the exploration, it seems difficult to assert that the final model will always achieve a given PAC bound. Perhaps I am missing something.\n\n2. The analysis is done using a linearization of the model. This limits the class of models for which the shield can accurately forecast safety. This is acknowledged in the paper and the proposed directions for mitigation seem reasonable.\n\n3. Missing from the related work seems to the literature on abstract interpretation that (from my outsider knowledge) offers a similar promise of learning pre-conditions for safety. Since the preconditions considered in this work are (under?) approximations for the learned model, it seems good to compare.", "limitations_and_societal_impact": "", "review_text": "", "extra_scores": {"correctness": "4: All of the claims and statements are well-supported and correct.", "technical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work.", "empirical_novelty_and_significance": "3: The contributions are significant and somewhat new. Aspects of the contributions exist in prior work."}, "extra_text": {}}]

Author rebuttal:

Decision: Accept: poster