Adaptive Shielding via Parametric Safety Proofs

Explore a conference presentation that introduces a novel programming-language framework for creating adaptive shields in cyber-physical systems with learning-enabled controllers. Learn how this approach addresses the critical challenge of ensuring safety in dynamic environments where systems must acquire knowledge at runtime while maintaining rigorous safety guarantees. Discover how the proposed framework enables experts to statically specify adaptive shields that enforce a safe control envelope, which becomes more permissive as the agent gathers knowledge during operation. Understand the key innovation of parametric safety models that adapt based on the current agent's knowledge state, moving beyond the traditional hard tradeoffs between expressivity, safety, adaptivity, precision, and runtime efficiency that plague existing model-checking and automated reasoning approaches. Examine the technical foundations including the use of differential dynamic logic for hybrid systems modeling, statistical inference methods for knowledge parameter estimation, and a dedicated domain-specific language for specifying nondeterministic inference strategies. See how the framework leverages language design principles and theorem proving to provide end-to-end probabilistic safety guarantees while offering unprecedented modeling flexibility. Gain insights into the practical applications for safe reinforcement learning in cyber-physical systems, where traditional shielding approaches fall short in adapting to changing environmental conditions. Learn about the statistical soundness guarantees that ensure knowledge parameters are inferred correctly at runtime, enabling systems to safely expand their operational envelope as they learn. The presentation covers the theoretical underpinnings, implementation details, and evaluation results that demonstrate the framework's ability to balance safety and adaptivity in learning-enabled control systems, making it particularly relevant for researchers and practitioners working on safe AI deployment in critical applications.