一句话：提出编程语言框架，用参数化安全证明与DSL定义自适应屏蔽，为学习控制器提供概率安全保证。
学习使能控制器在环境变化时难以保证安全，现有基于模型检测与自动推理的 shielding 方法在表达力、安全性、自适应性、精度与运行时效率之间存在硬性权衡。本文提出一个编程语言框架，允许专家静态指定面向学习使能智能体的自适应屏蔽：屏蔽规约给出一个以智能体当前知识为参数的安全模型，并可通过专用领域特定语言指定非确定性推断策略，从而在运行时以统计可靠的方式推断知识参数。借助语言设计与定理证明，该框架在提供高度建模灵活性的同时，给出严格的端到端概率安全保证。摘要未报告具体实验评估。
A major challenge to deploying cyber-physical systems with learning-enabled controllers is to ensure their safety, especially in the face of changing environments that necessitate runtime knowledge acquisition. Model-checking and automated reasoning have been successfully used for shielding, i.e., to monitor un-trusted controllers and override potentially unsafe decisions, but only at the cost of hard tradeoffs in terms of expressivity, safety, adaptivity, precision and runtime efficiency. We propose a programming-language framework that allows experts to statically specify adaptive shields for learning-enabled agents, which enforce a safe control envelope that gets more permissive as knowledge is gathered at runtime. A shield specification provides a safety model that is parametric in the current agent’s knowledge. In addition, a nondeterministic inference strategy can be specified using a dedicated domain-specific language, enforcing that such knowledge parameters are inferred at runtime in a statistically-sound way. By leveraging language design and theorem proving, our proposed framework empowers experts to design adaptive shields with an unprecedented level of modeling flexibility, while providing rigorous, end-to-end probabilistic safety guarantees.
@article{paperbot3185,
title = {Adaptive Shielding via Parametric Safety Proofs},
author = {Yao Feng and Jun Zhu and André Platzer and Jonathan Laurent},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA1},
year = {2025},
doi = {10.1145/3720450}
}