什么能被强制执行？面向工具使用智能体的可认证运行时安全理论

运行时防护栏（runtime guardrails）在不可逆的工具调用之前采取行动，但其保证取决于哪些策略状态是可表示的、判定器（judge）能观察到什么，以及干预是否会改变未来行为。我们区分三个问题。第一，相对于固定的预言机谓词，确定性门控恰好能强制执行其寄存器模型可识别良前缀（good prefixes）的那些非空安全策略；策略的非平凡性在带两个可递减计数器时不可判定，但对一个可分离单调片段属于PSPACE。第二，在固定的外生规律下，Neyman-Pearson给出精确的错误拦截/漏拦前沿，conformal校准给出有限样本边际证书，必要时可经由全部拦截（block-all）实现。第三，一旦拦截会改变后续提议，静态分数与未设门的轨迹未必能识别闭环前沿；一个明确规定的有限受控模型则产生一个占用程序（occupancy program）。有界表示攻击会增加鲁棒性余量，因此仅靠良性校准无法迁移。实验通过静态诊断、受控模型枚举、表示重写与成对闭环重跑来针对这些区分。