用大模型自动把人工指令转为可验证的代码策略，提升高风险场景安全
Autoformalization of Agent Instructions into Policy-as-Code
- 通过大模型生成-评判循环，将自然语言指令转为形式化策略
- 在MedAgentBench上覆盖更完整的政策描述，优于手工编码方案
- 适合需要强安全保障的医疗、金融等高风险智能体应用
高风险领域中的智能体安全依赖形式化策略执行，但现有方法或依赖无形式保证的概率防护（微调分类器、提示引导），或依赖难以扩展的手写符号式执行。本文提出一种自动形式化流程，利用基于大模型的生成-评判循环，将智能体提示、MCP工具描述和自然语言政策文档转换为使用Cedar策略语言的形式化可验证策略。在MedAgentBench基准测试中，自动形式化的策略覆盖了远超先前手写符号执行的工作的原始自然语言规范内容。
原文摘要 · Abstract (English)
Agent safety in high-stakes domains requires formal policy enforcement, but most existing approaches either rely on probabilistic guardrails (fine-tuned classifiers, prompt-based steering) that offer no formal guarantees, or on hand-coded symbolic enforcement that does not scale to the breadth of real policy specifications. We present an autoformalization pipeline that translates agent prompts, MCP tool descriptions, and natural language policy documents into formally verified policies using an LLM-based generator-critic loop. The resulting policies are written in the Cedar Policy Language. On the MedAgentBench benchmark, our autoformalized policies cover substantially more of the source natural-language specification than the hand-coded symbolic enforcement in prior work.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。