Source-linked AI summary
Safe Reinforcement Learning via Shielding
Mohammed Alshiekh, Roderick Bloem, Ruediger Ehlers, Bettina Könighofer, Scott Niekum, Ufuk Topcu
TL;DR
Reinforcement learning can optimize reward without guaranteeing safety during learning or execution. The paper synthesizes reactive shields from temporal-logic specifications and environment abstractions, using preemptive or post-posed intervention. Across several reinforcement-learning scenarios, shielded agents were at least as good as unshielded agents and usually learned better, while requiring an approximate unsafe-action model.
Problem
Reinforcement learning lacks guaranteed safety or correctness during learning and execution, despite its ability to optimize reward.
Method
The paper synthesizes reactive shields from temporal-logic safety specifications and environment abstractions to restrict or correct unsafe learner actions.
Results
Across several reinforcement-learning scenarios, shielded agents performed at least as well as unshielded agents and usually improved learning performance.
Takeaways & Limitations
Shielding separates safety enforcement from learning and can preserve safe operation while remaining compatible with different learning algorithms.
Takeaways & Limitations
The approach requires an approximate model indicating when actions are unsafe, because state-dependent action safety cannot otherwise be determined.
Abstract
from arXiv · showhide
Reinforcement learning algorithms discover policies that maximize reward, but do not necessarily guarantee safety during learning or execution phases. We introduce a new approach to learn optimal policies while enforcing properties expressed in temporal logic. To this end, given the temporal logic specification that is to be obeyed by the learning system, we propose to synthesize a reactive system called a shield. The shield is introduced in the traditional learning process in two alternative ways, depending on the location at which the shield is implemented. In the first one, the shield acts each time the learning agent is about to make a decision and provides a list of safe actions. In the second way, the shield is introduced after the learning agent. The shield monitors the actions from the learner and corrects them only if the chosen action causes a violation of the specification. We discuss which requirements a shield must meet to preserve the convergence guarantees of the learner. Finally, we demonstrate the versatility of our approach on several challenging reinforcement learning scenarios.
1 Introduction
The paper addresses the gap between reinforcement learning’s optimization capabilities and limited safety guarantees by enforcing temporal-logic specifications during learning and execution. It introduces shielding, with preemptive and post-posed placements, to restrict or correct unsafe actions while preserving learning flexibility.
- Motivation: Reinforcement learning optimizes long-term reward, but safety during learning and controller execution has received less attention.The concern is especially relevant for learning-based controllers operating in physical systems near humans.
- Motivation: The framework uses temporal logic, focusing algorithmically on its safety fragment, to specify correctness requirements.This provides an unambiguous specification language for safety and broader correctness properties.
- Approach: A shield is computed from the safety specification and an abstraction of environment dynamics to enforce safety with minimum interference.It forbids actions only when they could endanger safe system behavior.
- Approach: Preemptive shielding supplies the learner with safe actions before each decision, whereas post-posed shielding corrects a selected action only when it is unsafe.Preemptive shielding restricts choices while allowing any safe policy; post-posed shielding intervenes after the learner acts.
- Implications: Shielding separates safety and correctness from learning convergence and optimality, while remaining largely agnostic to the learning algorithm.The framework also accommodates function approximation and requires relatively mild assumptions about the learner’s input-output structure.
2 Related Work
Prior work treats safety in reinforcement learning and formal methods largely as separate concerns. This paper connects them by adapting reactive shielding to the learning setting, combining formal safety enforcement with reinforcement learning.
- Safety in Reinforcement Learning: Safe reinforcement learning has been studied through notions such as avoiding undesirable states and incorporating external teacher advice.The paper’s temporal-logic safety fragment is more general than the invariance notion discussed in earlier work.
- Safety in Formal Methods: Formal-methods approaches derive correct-by-construction controllers from abstractions of environment dynamics, but faithful abstractions can be difficult and computationally burdensome.Reinforcement learning partly addresses the control problem but typically lacks correctness guarantees.
- Connection: The paper adopts the idea of synthesizing a runtime shield and develops a realization tailored to reinforcement learning.The shield connects temporal-logic-constrained control with the learning setting.
3 Preliminaries
The preliminaries define the formal objects used to combine temporal-logic safety with reinforcement learning: reactive systems, specifications, safety games, and Markov decision processes. These definitions establish how traces, safe states, actions, transitions, and rewards are represented.
- MDPs and Reinforcement Learning: An MDP models finite states, actions, probabilistic transitions, and rewards, while reinforcement learning seeks a policy maximizing expected discounted return.The discount factor γ controls the influence of future rewards.
- Reactive Systems: Reactive systems map input traces to output traces through finite-state transitions and output functions.Their combined input-output behavior forms traces over the product alphabet.
- Specifications: Specifications define allowed trace languages, and a system realizes a specification when all of its traces are allowed.Linear temporal logic expresses such specifications using Boolean and temporal operators.
- Safety Specifications: A safety specification requires every violating trace to have a bad prefix after which all continuations remain violating.Safety automata characterize satisfaction by runs that visit only safe states.
- Safety Games: A safety game alternates environment inputs and system outputs, with the system winning when only safe states are visited.A shield implements a winning strategy through its reactive-system transition and output functions.
4 Safety Specifications, Abstractions, and Game Solving
The paper combines temporal-logic safety specifications with conservative environment abstractions and safety-game solving. This yields reactive controllers that can enforce safety while reinforcement learning optimizes application-specific performance.
- Goal: The paper aims to combine formal correctness guarantees from reactive synthesis with reinforcement learning’s optimality under an unknown performance criterion.This combination targets controllers that are both specification-compliant and reward-optimizing.
- Safety Specifications: Safe reinforcement learning learns an optimal policy while satisfying a temporal-logic safety specification during learning and execution.The safety specification is represented as a deterministic safety word automaton whose visited states must remain safe.
- Game Solving: Reactive synthesis solves a safety game formed from the specification and an environment abstraction, planning ahead to avoid states from which future violation is unavoidable.This can require intervention before an abnormal condition is directly detectable.
- Abstractions: The environment abstraction need not be complete, but it must conservatively represent possible MDP behavior for reasoning about unavoidable specification violations.The abstraction may have finitely many states even when the underlying MDP is larger or infinite.
- Example: In the hot-water-tank example, the specification constrains water levels and requires minimum valve-open and valve-closed durations.The abstraction uses valve actions and coarse filling-level labels to summarize the tank’s behavior.
- Example: The synthesized tank shield opens inflow when the level is too low and prevents opening above 93 because the valve must remain open for three seconds.It targets a minimum level of 4 while preventing overflow under the modeled inflow range.
5 Framework for Shielded Reinforcement Learning
The framework inserts a correct-by-construction shield into reinforcement learning to enforce safety while minimizing interference. It supports preemptive action restriction and post-posed action correction, with both approaches preserving safe operation during learning and execution.
- Framework: The shield modifies the learning loop to enforce a safety specification while allowing the learner to retain as much freedom as possible.It removes or overrides actions only when they could endanger safe system behavior.
- Preemptive Shielding: In preemptive shielding, the shield supplies the learner with the safe actions available at each time step.The environment executes the learner’s selected action after unsafe actions have been removed from the available set.
- Preemptive Shielding: Preemptive shielding can transform the original MDP into a product MDP whose state-dependent action sets exclude unsafe actions.The transformed transition function retains only distributions associated with the remaining actions.
- Post-Posed Shielding: In post-posed shielding, the shield monitors the learner’s selected action and replaces it with a safe action only when necessary.The learner can receive the executed action and reward, while the shield handles safety correction.
- Post-Posed Shielding: Post-posed shielding can protect even a fixed policy during execution, without requiring the learning algorithm to observe the shield.However, unsafe actions may remain in the learned policy, so the shield is needed during both learning and execution.
- Post-Posed Shielding: A post-posed shield can use the learner’s ranking of allowed actions to select the highest-ranked safe action and support multiple policy updates when necessary.If all ranked actions are unsafe, the shield selects a safe action outside the ranking and the learner can update using the resulting information.
6 A Shield Synthesis Algorithm for Reinforcement Learning
The paper synthesizes reactive shields from temporal-logic safety specifications and environment abstractions, enforcing correctness while minimizing interference with reinforcement learning. The construction uses safety-game solving to disable only actions that may permit specification violations.
- Shield synthesis: A shield is synthesized from a safety specification and an MDP abstraction, then inserted before or after the learning agent.Both placements enforce runtime correctness and minimum interference.
- Properties: The construction guarantees correctness and minimal interference, with correctness allowing specification errors only after the abstraction itself has proved incorrect.The shield also maintains at least one available action and deactivates an action only when a consistent MDP could otherwise violate the specification.
- Shield synthesis: The shared construction translates the specification and abstraction into a safety game whose state space is their product.The environment chooses observations, while the system chooses actions.
- Shield synthesis: The shield is obtained from the winning region and permits actions guaranteed to remain in that region for every next observation.Actions that may lead to an error state are disabled according to the abstraction.
- Shield variants: Preemptive shields provide safe action lists, whereas post-posed shields output a single corrected action and can use ranked learner actions.The shield follows the highest-ranked allowed action and deviates only when all ranked actions are unsafe.
7 Convergence
Shielded learning can be analyzed as learning on a product MDP combining the shield and environment. Standard convergence results therefore carry over under a fixed action-selection condition for post-posed shielding.
- Convergence: The product MDP represents the shield and original MDP together, so algorithms converging on standard MDPs also converge with shielding.This applies to both preemptive and post-posed shields.
- Convergence: For post-posed shielding, corrected actions must follow a fixed probability distribution whenever the learner selects no safe action.The distribution may depend on the MDP state, shield, and selected ranking, but must remain constant over time.
- Convergence: The convergence argument assumes that the learner can observe the shield state and condition its actions on that state.For certain state-label safety specifications, the shield can sometimes be reduced to a single state plus special states, relaxing this observation requirement.
8 Experiments
Across grid worlds, driving, Seaquest, and a water-tank task, shielding prevented specified unsafe behavior while preserving or accelerating learning. The experiments also show that shielding settings affect whether the learned policy is optimal.
- Experimental scope: The experiments covered robot navigation, autonomous driving, Atari Seaquest, and water-tank control under temporal-logic safety specifications.The robot tasks required ordered region visits while avoiding walls, an opponent, or prolonged bomb occupancy.
- Grid world example: In grid worlds, only unshielded versions experienced negative rewards, while shielded versions were safe and generally learned faster.For the 15x9 task, only the |rankt| = 3 shield without penalty found the optimal path.
- Self-driving car example: In the self-driving car task, the shielded learner without punishment learned more rapidly and never crashed, unlike unshielded learning.Unshielded accumulated reward increased but crashes still occurred at the end of simulation.
- Seaquest example: In Seaquest, shielding did not change performance, while the two specified safety properties were not violated.The shield operated on the black-box learner’s actions and used simulator-derived inputs.
- Water tank example: In the water-tank task, both shielded and unshielded Q-learning and SARSA reached an optimal policy, but shielding shortened the time to reach it.The comparison used shielded and unshielded implementations across both learning algorithms.
9 Conclusion
The paper develops shielded reinforcement learning that enforces temporal-logic safety independently of the learner’s internal details. Across several scenarios, shielded agents performed at least as well as unshielded agents, while requiring an approximate model of unsafe actions.
- Shielding enforces reinforcement-learning safety constraints expressed as temporal logic by intercepting decisions that could violate the specification.The method focuses on shielding the underlying learner’s decisions and includes automated shield synthesis.
- A shield depends on monitored input-output behavior, an environment abstraction, and correctness specifications rather than the learning algorithm’s intricate internal details.
- Across several reinforcement-learning scenarios, shielded agents performed at least as well as unshielded agents, with improved learning performance in most cases.
- The main limitation is the need for an approximate model identifying when actions are unsafe, especially when allowed actions depend on the environment state.The authors argue this model is unavoidable in state-dependent settings.