Synthesizing Efficient and Permissive Programmatic Runtime Shields for Neural Policies

• URL: http://arxiv.org/abs/2410.05641v1
• Date: Tue, 8 Oct 2024 02:44:55 GMT
• Title: Synthesizing Efficient and Permissive Programmatic Runtime Shields for Neural Policies
• Authors: Jieke Shi, Junda He, Zhou Yang, Đorđe Žikelić, David Lo,
• Abstract summary: We propose a novel framework that synthesizes lightweight and permissive programmatic runtime shields for neural policies. Aegis achieves this by formulating the seeking of a runtime shield as a sketch-based program synthesis problem. Compared to the current state-of-the-art, Aegis's shields exhibit a 2.1$times$ reduction in time overhead and a 4.4$times$ reduction in memory usage.
• Score: 7.831197018945118
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: With the increasing use of neural policies in control systems, ensuring their safety and reliability has become a critical software engineering task. One prevalent approach to ensuring the safety of neural policies is to deploy programmatic runtime shields alongside them to correct their unsafe commands. However, the programmatic runtime shields synthesized by existing methods are either computationally expensive or insufficiently permissive, resulting in high overhead and unnecessary interventions on the system. To address these challenges, we propose Aegis, a novel framework that synthesizes lightweight and permissive programmatic runtime shields for neural policies. Aegis achieves this by formulating the seeking of a runtime shield as a sketch-based program synthesis problem and proposing a novel method that leverages counterexample-guided inductive synthesis and Bayesian optimization to solve it. To evaluate Aegis and its synthesized shields, we use four representative control systems and compare Aegis with the current state-of-the-art. Our results show that the programmatic runtime shields synthesized by Aegis can correct all unsafe commands from neural policies, ensuring that the systems do not violate any desired safety properties at all times. Compared to the current state-of-the-art, Aegis's shields exhibit a 2.1$\times$ reduction in time overhead and a 4.4$\times$ reduction in memory usage, suggesting that they are much more lightweight. Moreover, Aegis's shields incur an average of 1.6$\times$ fewer interventions than other shields, showing better permissiveness.

Related papers

• Compositional Shielding and Reinforcement Learning for Multi-Agent Systems [1.124958340749622]
  Deep reinforcement learning has emerged as a powerful tool for obtaining high-performance policies. One promising paradigm to guarantee safety is a shield, which shields a policy from making unsafe actions. In this work, we propose a novel approach for multi-agent shielding.
  arXiv  Detail & Related papers  (2024-10-14T12:52:48Z)
• Shield Synthesis for LTL Modulo Theories [2.034732821736745]
  We develop a novel approach for generating shields conforming to complex safety specifications. To the best of our knowledge, this is the first approach for synthesizing shields for such expressivity.
  arXiv  Detail & Related papers  (2024-06-06T15:40:29Z)
• Approximate Model-Based Shielding for Safe Reinforcement Learning [83.55437924143615]
  We propose a principled look-ahead shielding algorithm for verifying the performance of learned RL policies. Our algorithm differs from other shielding approaches in that it does not require prior knowledge of the safety-relevant dynamics of the system. We demonstrate superior performance to other safety-aware approaches on a set of Atari games with state-dependent safety-labels.
  arXiv  Detail & Related papers  (2023-07-27T15:19:45Z)
• Safety Shielding under Delayed Observation [59.86192283565134]
  Shields are correct-by-construction enforcers that guarantee safe execution. Shields should pick the safe corrective actions in such a way that future interferences are most likely minimized. We present the first integration of shields in a realistic driving simulator.
  arXiv  Detail & Related papers  (2023-07-05T10:06:10Z)
• Approximate Shielding of Atari Agents for Safe Exploration [83.55437924143615]
  We propose a principled algorithm for safe exploration based on the concept of shielding. We present preliminary results that show our approximate shielding algorithm effectively reduces the rate of safety violations.
  arXiv  Detail & Related papers  (2023-04-21T16:19:54Z)
• Model-based Dynamic Shielding for Safe and Efficient Multi-Agent Reinforcement Learning [7.103977648997475]
  Multi-Agent Reinforcement Learning (MARL) discovers policies that maximize reward but do not have safety guarantees during the learning and deployment phases. Model-based Dynamic Shielding (MBDS) to support MARL algorithm design.
  arXiv  Detail & Related papers  (2023-04-13T06:08:10Z)
• Online Shielding for Reinforcement Learning [59.86192283565134]
  We propose an approach for online safety shielding of RL agents. During runtime, the shield analyses the safety of each available action. Based on this probability and a given threshold, the shield decides whether to block an action from the agent.
  arXiv  Detail & Related papers  (2022-12-04T16:00:29Z)
• Sample-Efficient Safety Assurances using Conformal Prediction [57.92013073974406]
  Early warning systems can provide alerts when an unsafe situation is imminent. To reliably improve safety, these warning systems should have a provable false negative rate. We present a framework that combines a statistical inference technique known as conformal prediction with a simulator of robot/environment dynamics.
  arXiv  Detail & Related papers  (2021-09-28T23:00:30Z)
• It's Time to Play Safe: Shield Synthesis for Timed Systems [53.796331564067835]
  We show how to synthesize timed shields from timed safety properties given as timed automata. A timed shield enforces the safety of a running system while interfering with the system as little as possible.
  arXiv  Detail & Related papers  (2020-06-30T11:21:42Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.