部分观测下与生成器无关的运行时保障
Generator-Independent Runtime Assurance under Partial Observation
- State Key Laboratory of Robotics and Intelligent Systems, Shenyang Institute of Automation, Chinese Academy of Sciences（机器人学与智能系统国家重点实验室，中国科学院沈阳自动化研究所）
- University of Chinese Academy of Sciences（中国科学院大学）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
本文提出同时集合健全性作为生成器无关的运行时保障的充要条件，并给出部分观测下的信息论下界，通过顺序风险账本实现可实施的契约安全保证。
AI中文摘要：
基于提案的控制器——学习策略、语言模型规划器以及其他黑盒生成器——日益被部署在运行时验证门之后。我们研究闭环安全保证何时与生成器解耦。普遍的逐候选认证模式不可组合：在重试或最佳k选择下，逐候选的误接纳水平α可能膨胀至1-(1-α)^k。我们的主要定理表明，同时集合健全性——认证一组不包含不可行动作的可接纳提案——是生成器无关的接纳健全性的充分必要条件，即所有生成器执行不可行动作的最坏情况概率等于集合失败概率；结合设计时证书和无旁路规则，它足以实现契约安全，其违规界限Γ+∑_t ε_t+η在任意甚至对抗性替换生成器下保持不变。第二个定理限制了部分观测下每个接纳机制：对于固定的探测和接纳策略，如果两个信息律在总变差距离δ内的状态假设需要不同的安全决策，则α+β+δ≥1。顺序风险账本使保证可通过时间一致置信管实现，并表明确定性接纳计算将所有统计风险集中在状态估计中。Simplex式运行时保障和控制障碍函数滤波被恢复为退化情况。
英文摘要：
Proposal-based controllers---learned policies, language-model planners, and other black-box \emph{generators}---are increasingly deployed behind runtime verification gates. We ask when the closed-loop safety guarantee decouples from the generator. The prevailing per-candidate certification pattern does not compose: under retry or best-of-$k$ selection a per-candidate false-admission level $α$ can inflate to $1-(1-α)^{k}$. Our main theorem shows that \emph{simultaneous setwise soundness}---certifying a set of admissible proposals containing no nonviable action---is necessary and sufficient for generator-independent \emph{admission soundness}, the worst case over all generators of executing a nonviable proposal equalling the probability of setwise failure; together with a design-time certificate and a no-bypass rule it is sufficient for \emph{contract safety}, with violation bound $Γ+\sum_t\varepsilon_t+η$ invariant under arbitrary, even adversarial, replacement of the generator. A second theorem bounds every admission mechanism under partial observation: for a fixed probing and admission policy, if two state hypotheses whose information laws lie within total-variation distance $δ$ require different safe decisions, then $\abar+β+δ\ge1$. A sequential risk ledger makes the guarantee implementable with time-uniform confidence tubes, and shows that deterministic admission computations concentrate all statistical risk in state estimation. Simplex-style runtime assurance and control-barrier-function filtering are recovered as degenerate cases.
