Agent 指令向策略即代码的自动形式化：构建高可靠性 AI 代理的安全护栏

背景

在高风险领域（如医疗、金融、自动驾驶等）部署 AI Agent（智能体）时，安全性是首要考量。然而，当前保障 Agent 安全的主流方法存在明显的局限性，主要体现在两个极端：

1. 概率性护栏（Probabilistic Guardrails）：大多数现有方案依赖于微调的分类器或基于提示词（Prompt）的引导技术。这些方法本质上是概率性的，它们无法提供形式化的安全保证（Formal Guarantees）。这意味着，即使模型经过精心调优，仍有可能在边缘情况下违反安全策略，且这种违反往往难以预测和量化。
2. 手工编码的符号执行（Hand-coded Symbolic Enforcement）：另一种极端是完全依赖人工编写的符号逻辑来强制执行策略。虽然这种方法提供了严格的形式化保证，但其扩展性极差。现实世界中的政策规范（Policy Specifications）往往复杂且广泛，人工编码难以覆盖所有细节，导致维护成本高昂且容易遗漏。

因此，业界亟需一种能够结合两者优势的方法：既具备形式化验证的严格安全性，又能自动处理广泛且复杂的自然语言政策规范。

核心内容

本文提出了一种自动形式化流水线（Autoformalization Pipeline），旨在解决上述矛盾。该流水线利用大语言模型（LLM）作为核心引擎，将非结构化的 Agent 指令、工具描述以及自然语言政策文档，自动转换为经过形式化验证的策略代码。

工作流程：生成器-批评家循环（Generator-Critic Loop）

该流水线采用了一种基于 LLM 的“生成器-批评家”迭代机制：

1. 输入整合：系统接收多种输入源，包括 Agent 的 Prompt 指令、MCP（Model Context Protocol）工具描述以及详细的自然语言政策文档。
2. 生成阶段：LLM 作为生成器，尝试将这些自然语言描述翻译为形式化的策略语言。
3. 批评与验证阶段：LLM 同时扮演批评家角色，对生成的代码进行自我审查和逻辑验证，确保其符合原始政策意图且语法正确。
4. 输出结果：最终生成的策略代码采用 Cedar Policy Language 编写。Cedar 是一种由 AWS 主导开发的形式化策略语言，旨在提供强大且可验证的策略执行能力。

性能评估：MedAgentBench 基准测试

为了验证该方法的有效性，研究团队在 MedAgentBench 基准上进行了测试。这是一个专注于医疗领域 Agent 安全的评估平台。

• 对比对象：将自动形式化生成的策略与之前工作中手工编写的符号执行策略进行对比。
• 核心指标：策略对源自然语言规范的覆盖率（Coverage）。
• 结果：自动形式化生成的策略在覆盖源自然语言规范的范围上，显著优于手工编码的符号执行方案。这表明该方法能够更完整、更准确地捕捉复杂政策中的细微差别，而无需人工逐行编写逻辑。

关键要点

• 解决安全与扩展性的矛盾：该方法填补了“无形式化保证的概率护栏”与“高维护成本的手工符号执行”之间的空白，实现了可扩展的形式化安全。
• 多源输入融合：流水线不仅处理自然语言政策，还能整合 Agent 的 Prompt 和 MCP 工具描述，实现了从指令到策略的全链路形式化。
• 基于 LLM 的生成-验证闭环：利用 LLM 的生成能力进行代码转换，同时利用其推理能力进行自我批评和验证，形成了自动化的形式化过程。
• 采用 Cedar 策略语言：输出结果采用 Cedar Policy Language，这是一种经过设计用于形式化验证的策略语言，确保了策略的可执行性和可证明性。
• 实证优势：在 MedAgentBench 基准测试中，自动生成的策略在覆盖自然语言规范方面显著优于传统手工编码方法，证明了其在处理复杂、广泛政策规范时的优越性。

意义与影响

这项研究对 AI Agent 的安全部署具有深远意义：

1. 提升高风险领域 AI 的可信度：通过提供形式化保证，该方法使得 AI Agent 在医疗、金融等对错误零容忍的领域中更具可信度。企业可以确信，Agent 的行为严格遵循预设的安全边界，而非仅仅依赖概率性的“最好情况”。
2. 降低合规与维护成本：自动形式化流水线使得将复杂的法律、医疗或行业合规政策转化为机器可执行代码成为可能。这大大减少了人工编写和维护策略代码的需求，加速了政策落地过程。
3. 推动策略即代码（Policy-as-Code）的普及：通过将自然语言直接转化为 Cedar 等正式策略语言，该方法降低了策略管理的门槛，使得非程序员也能通过自然语言定义复杂的安全规则，并由系统自动确保其正确执行。
4. 为未来 Agent 架构奠定基础：随着 Agent 在更多关键任务中的应用，这种自动化的、形式化的安全机制将成为标准基础设施的一部分，确保 Agent 在享受自主决策能力的同时，不牺牲安全性和可控性。