为智能体框架提供不依赖对齐的安全保证，确保其行为在边界内。
Containment Verification: AI Safety Guarantees Independent of Alignment
- 将安全验证置于智能体框架本身，通过类型化动作边界约束行为。
- 证明了对可实现边界的普遍安全保证，并在Dafny中形式化验证。
- 适用于需强安全保障的自主系统，尤其适合对模型不可信的场景。
智能体框架是人工智能代理在世界中行动的软件层。现有安全方法干预模型，因此依赖于无法验证的模型行为属性。本文提出「容器验证」，将安全保证定位在智能体框架内部。在混沌预言机语义下，AI被建模为框架类型化动作空间上的无约束预言机，而验证的容器层必须对所有可能输出的动作值强制执行边界策略。对于可由模型边界事件、动作参数和状态表达的边界可实现属性，我们通过前向仿真精化证明了普遍性保障，并在Dafny中机械化实现。我们以一个极简的智能体大模型框架PocketFlow为例，使用智能体合成流水线生成规范、操作模型和精化证明，且在信息屏障下避免同义循环规范。据我们所知，这是首个对智能体框架的演绎式形式化验证。该保障独立于对齐，因其量化的是框架的类型化动作边界，而非模型行为。
原文摘要 · Abstract (English)
Agentic frameworks are the software layer through which AI agents act in the world. Existing safety methods intervene on the model and therefore remain conditional on unverifiable properties of learned behavior. We introduce containment verification, which locates safety guarantees in the agentic framework itself. Under havoc oracle semantics, the AI is modeled as an unconstrained oracle over the framework's typed action space, and the verified containment layer must enforce the boundary policy for every typed action value the AI can emit. For boundary-enforceable properties, expressed over modeled boundary events, action arguments, and state, we prove a universal guarantee by forward-simulation refinement and mechanize it in Dafny. We instantiate the paradigm by verifying PocketFlow, a minimalist agentic LLM framework, and use an agentic synthesis pipeline to generate the specification, operational model, and refinement proof under an information barrier against tautological specifications. To our knowledge, this is the first deductive formal verification of an agentic framework. The guarantee is independent of alignment because it quantifies over the framework's typed action boundary rather than over model behavior.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。