提出可验证的运行时安全机制，解决工具型智能体的安全保障难题。
What Can Be Enforced? A Theory of Certified Runtime Safety for Tool-Using Agents
- 用确定性门控识别可保证的安全策略，受限于状态表示能力。
- 在固定外部规则下，通过统计方法实现误拦与漏检的精确边界控制。
- 引入闭环控制模型，突破静态评分局限，适用于高风险决策场景。
运行时防护机制在不可逆工具调用前生效，但其安全性依赖于策略状态的可表征性、判断器的观测范围以及干预是否影响未来行为。本文区分三个核心问题：第一，相对于固定的预言机谓词，确定性门控仅能保证其寄存器模型可识别的非空安全策略；策略非平凡性在双递减计数器模型下不可判定，但在可分单调片段中属于PSPACE；第二，在固定外生法则下，Neyman-Pearson给出精确的误拦/漏检前沿，共形校准提供有限样本边际证书，可能通过全阻断实现；第三，一旦阻断影响后续提议，静态评分与未受控轨迹无法识别闭环前沿，需采用指定的有限可控模型生成占据程序。有限表示攻击引入鲁棒性裕度，因此单纯良性校准无法迁移。实验通过静态诊断、可控模型枚举、表示重写及配对闭环重跑来验证这些区分。
原文摘要 · Abstract (English)
Runtime guardrails act before irreversible tool calls, but their guarantees depend on what policy state is representable, what a judge observes, and whether intervention changes future behavior. We separate three questions. First, relative to fixed oracle predicates, a deterministic gate enforces exactly the nonempty safety policies whose good prefixes its register model recognizes; policy nontriviality is undecidable with two decrementable counters but in PSPACE for a separable monotone fragment. Second, under a fixed exogenous law, Neyman-Pearson gives the exact false-block/miss frontier and conformal calibration gives a finite-sample marginal certificate, possibly via block-all. Third, once blocking changes future proposals, static scores and ungated trajectories need not identify the closed-loop frontier; a specified finite controlled model instead yields an occupancy program. Bounded representation attacks add a robustness margin, so benign calibration alone does not transfer. Experiments target these distinctions through static diagnostics, controlled-model enumeration, representation rewrites, and paired closed-loop reruns.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。