该论文聚焦于一个现实痛点：自然语言描述访问控制需求易于人读，却难以直接落地为机器可执行的策略代码，而让大模型一次性生成策略往往在编译、语义与安全边界上频繁出错。作者提出并实现了一套基于 LLM 的模块化端到端管线，把自然语言访问控制策略（NLACP）逐级转化为 Open Policy Agent（OPA）可执行的 Rego 代码。管线并非依赖单次提示直接出码，而是拆分为多个可验证阶段：策略语句检测、主体/动作/资源等组件抽取、针对目标 schema 的校验、代码 lint、编译，以及自动化测试的生成与执行。这种结构化分解加 schema 感知校验的设计，目标是在部署可靠性与安全正确性上弥合人读需求与策略即代码（PaC）之间的鸿沟。评估数据为 372 条 ACRE 完整且主体、动作、资源标注均非空的访问控制语句，对照基线是直接单提示 LLM 生成。结果显示，系统端到端策略正确率为 50.3%，基线仅 15.3%，提升约 3.3 倍；注意其正确性判定极为严格，必须同时通过编译、lint、正向测试与负向测试，因而衡量的是真正可部署的正确性。在安全关键模式上优势更明显：deny 策略的正确拒绝语义达 87.5%（基线 37.5%），带所有权限定的策略 100%（基线 40%），带状态限定的策略 100%（基线 55.6%）。作者据此认为，结构化分解与 schema 感知校验对提升 LLM 生成授权策略的可靠性起关键作用。

本文提出一种自动形式化（autoformalization）流水线，旨在将智能体指令转化为“策略即代码”（Policy-as-Code），以在高风险领域中实现正式的策略执行。现有方法主要分为两类：一是基于概率性护栏（如微调分类器、提示引导），这类方法无法提供形式化保证；二是手工编写的符号化策略执行，但难以扩展到真实业务策略的广泛定义。该流水线利用基于LLM的生成器-评论家循环（generator-critic loop），将智能体提示、MCP工具描述以及自然语言策略文档自动翻译为使用Cedar策略语言编写的正式验证策略。在MedAgentBench基准上，自动形式化策略对源自然语言规范的覆盖范围显著超过先前工作中手工编写的符号化执行。该方法的核心贡献在于：通过自动形式化弥合了自然语言策略与形式化验证之间的鸿沟，使得非专家也能为智能体行为定义可验证的约束，而无需手工编码或形式化方法专业知识。实验证明，该流水线生成的策略在覆盖率和正确性上均优于手工基线，为智能体安全提供了一种可扩展、可验证的解决方案。