核心问题：把自然语言政策编译成能通过静态检查的确定性规则，究竟保证了规则可执行，还是保证了原始授权语义被保留？
论文卡片
- 原题： NOMOS: Compiling Written Policies into Statically Verified Tool-Call Gates for LLM Agents
- 作者与机构： Min-Young Yu、Tony Kim、Jang Won Choi；Corners Co., Ltd.
- 日期与版本： 2026-10-08，arXiv v1，28 页；cs.CR、cs.AI、cs.LG。作者注明已投稿 IEEE Access，不代表已经录用。
- 定位： 政策编译、静态分析与可验证 Agent 工作流的交叉研究；实验对象是客服与工具使用 Agent，并非芯片或 GPU 性能优化。
- 阅读入口： arXiv · HTML 全文（v1） · PDF（v1） · alphaXiv
简短导读：不让模型逐次决定是否合规
NOMOS 将政策离线编译为规则数据，运行时由确定性门控决定工具调用能否执行。四个阶段是 Parse、Extract、Resolve、Materialize；只有 Extract 调用 LLM。模型从人工定义的谓词词表中选择条件并绑定工具，Resolve 检查参数是否匹配、前置条件是否可能满足，以及规则是否把解除自身限制的工具也封锁了。
一个直观例子是认证死锁：“先认证才能操作”若绑定所有工具，连完成认证的查询也无法调用。删除这些错误绑定有明确价值；它修复的是规则结构，不是重新理解整份政策。
证据与它没有证明的事
作者在 τ²-bench 上用独立手写规则检查已执行的写调用，航空为 50 个任务各跑 5 次，零售为 114 个任务各跑 4 次。航空领域违规率从 234/353（66.3%）降至 3/116（2.6%）；零售从 188/611（30.8%）降至 40/582（6.9%）。这些数字只覆盖检查器编码的条款，且门控拒绝的调用不进入分母，不能直接解释为整份政策的合规率。
航空任务的一次成功率从 39.2% 升到 47.6%，但该差异的置信区间包含零；重复成功指标 pass^k 在 k=2–4 时显著改善。这里 pass^k 指多次均成功的可靠性，不是多次尝试至少成功一次。
更能显出权衡的是 AgentDojo banking。以下为同一主要 Agent 模型 gemma-4-26B-A4B 下的报告值；ASR 衡量是否达到 benchmark 指定的攻击目标。
| 方法 | ASR，越低越好 | 无攻击任务成功率 |
|---|---|---|
| 无防御 | 46.5% | 79.2% |
| Progent 自动策略 | 5.6% | 62.5% |
| NOMOS | 0.0% | 70.8% |
各条件包含 288 个攻击样本对和 48 次无攻击运行。Progent 在自己的框架中以相同任务、模型和重复预算重跑，并非只替换一个组件的严格消融。NOMOS 的 banking 政策由作者编写，且依据无攻击运行修订过，因此无攻击成功率不是完全留出的测试结果。
零 ASR 也不是零非授权行为。 在 288 个受防御的 banking 攻击样本对中，仍有 8 个被注入诱导向历史收款人转账；它们没有达到评分器指定的攻击目标。另一端，Slack 的无攻击成功率从 90.5% 降到 14.3%：只允许用户点名目标的规则，也阻断了需要从文档中发现目标的正常任务。
最值得细读的反例
旅行场景的原条款要求日历事件符合用户请求，编译后的谓词却只检查用户是否请求过某种写操作。用户要求发邮件，门控便放行了注入诱导的日历创建。这个绑定结构合法，语义却弱于条款；反方向的过度限制也存在。
因此，标题中的“statically verified”不能读成政策语义等价证明。检查依赖人工词表和表格；单条规则不自阻塞也不保证多条规则之间没有循环死锁。行为预检用历史轨迹筛查异常拒绝，但不是完整性证书。编译器、谓词实现和抽取提示词未公开，也限制了独立核验。
重点读哪里
读 §3.1–3.4，分清词表、结构检查与行为预检；读 §4、§5.1–5.3，看指标分母、检查器覆盖和授权解释如何影响数字；再读 §5.8、§5.11、附录 C 的残余行为与弱绑定，最后看 §6 和 Reproducibility。
思想启发
以下是导读者的推论，不是论文新增的实证结论。
这里有三个不应合并的判断：规则是否有意义地运行、是否忠实表达条款、条款是否足以保护用户意图。确定性执行只使既定判断稳定，并不会自动把第一层提升为后两层。
论文的价值也不必被表述为“解决了安全”。它让某些失败有了明确名字：自阻塞、参数错绑、语义弱化、过度拒绝、评分器漏记。能够区分失败发生在哪一层，本身就是比一个总成功率更清楚的研究结果。
三个思考问题
1. 当词表里没有恰好对应政策的谓词时，编译器应该如何理解“成功”？
选择较弱谓词会漏放，选择较强谓词会误拒；拒绝编译则保留了未知。哪一种结果才诚实表达了系统的知识边界？
展开思考线索
“找到了一个可执行绑定”是表示层面的成功，不必然是翻译成功。若无法判断源条款与目标谓词的蕴含关系，静默选择会把解释不确定性藏进确定性执行中。允许输出“无法表达”，可能降低自动化覆盖，却让保证范围更可辨认；其价值取决于系统是否同时报告了未覆盖条款。
2. 一个评分器认可的零攻击成功率，应该排除哪些行为才有充分意义？
没有把钱转给指定攻击者，却执行了用户未请求的其他转账，这应算防御成功、部分失败，还是暴露了攻击目标本身过窄？
展开思考线索
固定目标使评测可重复，但用户关心的损害集合可能更大。目标是否达成、恶意工具调用是否执行、最终状态是否偏离授权，是三种不同观察。它们不必被压成一个数字；否则防御可能只是把攻击引向评分器没有命名的位置。
3. 若正常任务与攻击具有相同的可观察结构，门控还能兼顾两者吗？
当两者都要求操作“从读到的材料中发现、而非用户亲口点名的目标”，仅靠来源类别还能作出正确区分吗？
展开思考线索
在现有特征上完全相同的两类行为，确定性判定无法仅凭这些特征分开。继续收紧规则会同时拒绝两者，放宽则同时接纳；缺少的可能不是更精巧的判断，而是任务级授权、对象关系或可信来源等额外信息。引入这些信息又会产生新的信任前提，因此安全与可用性的矛盾没有被消除，只是被重新定位。