💬 NLP

MANTRA: Synthesizing SMT-Validated Compliance Benchmarks for Tool-Using LLM Agents

本文介绍了 MANTRA，这是一个框架，它通过从自然语言程序手册中生成符号化世界模型和经 SMT 验证的轨迹级检查，自动合成并形式化验证可扩展的、可机器检查的工具使用大语言模型代理合规性基准。

原作者： Ashwani Anand, Ivi Chatzi, Ritam Raha, Anne-Kathrin Schmuck

发布于 2026-05-08

📖 1 分钟阅读☕ 轻松阅读

原作者： Ashwani Anand, Ivi Chatzi, Ritam Raha, Anne-Kathrin Schmuck

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象一下，你拥有一个非常聪明、乐于助人的机器人助手（AI 智能体），它能使用工具为你做事，比如预订航班、订购硬件或管理患者记录。然而，这个机器人工作在一个严格的办公环境中，必须遵循一本用通俗英语写成的、长达 50 页的规则手册。

问题在于：这本手册是写给人类看的，但机器人使用的是“工具调用”（数字命令）。检查机器人是否遵守了规则，就像试图仅通过查看学生的草稿纸来批改作文，却不知道他们是否真正遵循了老师的指示。

解决方案：MANTRA
本文的作者创建了一个名为 MANTRA（Manual-to-Test-Translation，手册到测试翻译）的系统。你可以将 MANTRA 想象成一位自动化、极度严格的质检员，它为这些机器人助手构建“试驾”测试。

以下是其工作原理，使用一个简单的类比：

1. 食谱与厨师

规则手册（手册）： 想象一份复杂的舒芙蕾食谱，上面写着：“如果鸡蛋新鲜，就将其搅打；如果不新鲜，就购买更多。在 20 分钟之前切勿打开烤箱门。”
机器人（智能体）： 这就是试图制作舒芙蕾的厨师。
问题： 你如何知道厨师是否遵循了食谱？他们是否先检查了鸡蛋？他们是否过早地窥视了烤箱？

2. 构建测试（“世界模型”）

与其仅仅让人类阅读食谱然后观察厨师（这既缓慢又容易出错），MANTRA 采取了一种巧妙的方法。它利用食谱和厨师拥有的工具列表（搅拌器、烤箱、计时器），自动构建一个厨房的数字模拟。

世界模型： 这是规则的数字孪生。它知道：“如果鸡蛋不新鲜，搅拌器工具还不能使用。”
检查项： MANTRA 还会生成一份具体检查事项的列表，例如：“厨师是否在搅打前检查了鸡蛋？”

3. “数学侦探”（SMT 求解器）

这是神奇的部分。由于食谱和检查项都是由 AI 编写的（AI 有时会犯错或产生幻觉），MANTRA 不会盲目信任它们。它使用一个数学逻辑引擎（称为 SMT 求解器）来充当“数学侦探”。

交叉验证： 侦探会问：“是否存在某种方式，让厨师遵循了‘检查项’列表，却违反了‘世界模型’的规则？”
修复循环： 如果侦探发现了一个漏洞（例如，检查项说“搅打鸡蛋”，但世界模型说“必须先确保鸡蛋新鲜”），它会自动修复测试。它会不断重复此过程，直到测试在数学上完美无缺。
人工备份： 只有当数学侦探陷入困境时，人类才会介入以修复最终细节。

4. 结果：完美的考试

最终产物是一个基准测试套件。这是一套包含 285 道不同“考题”的集合，涵盖 6 个不同领域（如航空预订、医院安全和硬件订购）。

确定性评分： 与其他需要人类或另一个 AI 猜测机器人是否表现良好的测试不同，MANTRA 的测试就像标准化答题卡扫描。机器人要么遵循了所需的精确工具调用序列，要么没有。这里没有猜测。
发现故障： 当作者在 6 个不同的 AI 模型上测试这些考试时，他们发现大多数机器人失败是因为跳过了“阅读”步骤。例如，它们会在“检查”商品是否有库存之前就尝试“写入”订单。MANTRA 的详细测试捕捉到了这些具体错误，清晰地展示了机器人究竟在哪里失败了。

总结

MANTRA 是一个框架，它将杂乱无章、由人类编写的规则手册转化为干净、经过数学验证的 AI 智能体测试。它利用“生成、交叉验证和修复”的循环，确保测试的公平性和准确性，使我们能够可靠地判断 AI 智能体是否真正遵守了规则，还是仅仅在凭感觉行事。

核心要点： 正如你不会在没有经过严格、数学验证的碰撞测试的情况下信任自动驾驶汽车一样，如果没有像 MANTRA 这样的系统来验证其是否遵循手册，你也不应信任使用工具的 AI。

技术摘要：MANTRA – 合成经 SMT 验证的合规性基准

问题陈述

工具使用型大语言模型（LLM）智能体正越来越多地部署于企业运营、医疗保健和旅行预订等关键领域，其行为必须严格遵守程序手册。评估这些智能体的一个根本性挑战在于输入与输出之间的“不匹配”：程序规则通常以非结构化的自然语言编写以供人类解读，而智能体的行为则表现为一系列工具调用（执行轨迹）。

现有评估方法存在显著局限性：

人工构建：手工构建基准质量高，但无法扩展到大型复杂手册或新领域。
基于 LLM 的评判者：虽然部署更容易，但这些评判者在长执行轨迹上难以可靠地执行严格的时间约束、前置条件和禁止动作，导致评估结果不可靠。
仅结果评估：许多基准仅检查最终状态，未能检测智能体是否通过不合规的程序路径得出了正确结果。

目前缺乏一种可扩展、可复现的方法，能够从自然语言手册自动生成轨迹级合规性基准，并提供确定性、机器可检查的评分。

方法论：MANTRA 框架

MANTRA（Manual-to-Test-Translation，手册到测试翻译）是一个旨在从自然语言程序文档和工具模式自动合成合规性基准的框架。它通过结合 LLM 生成与形式化验证的三阶段流水线运行：

1. 文档摄入与场景生成

依赖图构建：系统摄入程序手册（ $D$ ）并构建依赖图（ $G_D$ ），其中节点代表内容块（如段落），边代表层级和引用关系。
覆盖驱动采样：为了控制任务复杂度并确保广泛覆盖，MANTRA 从 $G_D$ 中采样子图（ $G_{DS}$ ）。小型、密集的子图产生简单场景；较大或连接松散的子图则引发涉及多条规则的复杂场景。
工具相关性与场景合成：对于每个样本，LLM 识别相关工具（ $T_S$ ）并生成具体场景（ $\lambda$ ）。每个场景包含一个自然语言提示（ $p_\lambda$ ）和变量赋值，其中包括内部状态变量（例如“请求待处理”），这些变量在提示中被显式化以引导智能体。

2. 检查生成与世界模型创建

为了确定性评估合规性，MANTRA 为每个场景生成两个独立工件：

轨迹级检查（ $C_\lambda$ ）：LLM 生成一组布尔检查，指定所需的工具调用、禁止的调用以及时间顺序（例如，check_inventory 必须在 assign_warehouse_picker 之前执行）。这些检查基于具体的参数值进行实例化。
符号世界模型（ $W_S$ ）：独立地，LLM 生成一个世界模型，将程序规则表示为状态转换系统。该模型用一种类型化的领域特定语言（DSL）表达，定义了状态变量、工具前置条件和后置条件。这种抽象允许紧凑地表示复杂的程序逻辑。

3. 通过 SMT 求解进行交叉验证

MANTRA 的核心创新在于使用可满足性模理论（SMT）求解器（具体为 Z3）对生成的检查和世界模型进行交叉验证。

有界模型检查： $C_\lambda$ 和 $W_S$ 均被编译为在轨迹视界 $h$ 上的有界 SMT 编码（ $b\Phi_h$ ）。
冲突搜索：系统搜索两类不一致性：
1. 前向冲突：满足检查但违反世界模型的轨迹（表明检查过弱或模型过于严格）。
2. 后向冲突：满足世界模型但违反特定检查的轨迹（表明检查过于严格）。
结构化修复循环：当发现冲突时，MANTRA 采用修复循环：
- 世界模型解析：如果来自同一样本的多个场景共享冲突，LLM 会提出对世界模型的共享修复（例如，添加缺失的前置条件）。
- 检查解析：如果冲突持续存在，系统会识别并修复特定场景的特定检查。
- 确定性编辑：修复通过类型化编辑语言应用以确保形式正确性，随后进行重新编译和重新验证。
人在回路：如果自动化修复在设定迭代次数后失败，系统会将该场景标记为结构化人工审查，审查者可手动解决歧义。

主要贡献

自动化流水线：一个完全自动化的流水线，可将自然语言手册和工具模式转换为具有可控任务难度和确定性评分的机器可检查基准。
双工件公式：轨迹级检查与符号世界模型的分离，并通过 SMT 求解进行交叉验证。这使得在基准被接受之前能够自动识别和修复不一致性，最大限度地减少人工干预。
基准套件：创建了一个新的基准套件，包含6 个领域（运营、Sneaky Sasquatch、客舱安全、零售、航空、电信）中的 285 个多样化任务。这些任务可扩展至长达约 16,000 字的手册和 148 种工具，仅需极少量人工努力。
细粒度故障分析：该框架提供轨迹级检查，使智能体故障模式的详细调试成为可能，区分缺失调用、顺序违规和禁止动作。

结果与评估

作者使用 6 种不同的 LLM 智能体评估了 MANTRA 框架及其生成的基准。

验证效率：基于 SMT 的交叉验证成功自动验证了大部分生成的测试用例。例如，在“运营”领域，经过前向和后向细化轮次后，66 个生成案例中有 63 个通过了验证。
智能体性能：评估显示，当前的 LLM 智能体在程序合规性方面存在困难。成功率因领域而异，其中“零售”和“航空”（来自 $\tau$ -Bench）被证明特别困难，这是由于复杂的工具使用而非文档长度所致。
故障模式分析：对 10,895 个失败检查的分析显示，76% 的失败是由于“缺失必需调用”（跳过强制工具）或“缺失锚点”（未能执行排序条款的前置条件）造成的。
- 一种主导的失败模式是“过早写入”，即智能体在执行必要的读取式查找之前调用了写入式工具。
- Qwen3.6:36B 模型表现出卓越的性能，特别是在航空和零售领域，通过保持严格的“先读后写”习惯，在这些领域实现了 0% 的过早写入率。
与现有基准的比较：与依赖人工构建或 LLM 评判者的现有基准不同，MANTRA 提供确定性、轨迹级评估，能够以极少量人工努力扩展到大型非结构化文档和新领域。

意义与主张

该论文主张，MANTRA 证明了将自动化基准生成与形式化基础验证方法相结合，为工具使用型智能体创建可扩展且可靠的基准是可行的。

可靠性：通过使用 SMT 求解器将检查与世界模型交叉验证，MANTRA 确保基准免受 LLM 幻觉可能引发的逻辑不一致性影响，与“LLM 即评判者”的方法相比，提供了更高程度的评估结果可信度。
可扩展性：该框架解决了人工基准创建的可扩展性瓶颈，使智能体能够在任意领域针对复杂、现实世界的程序手册（长达 50 多页）进行评估。
调试能力：轨迹级检查的细粒度使研究人员能够超越简单的通过/失败指标，深入了解智能体推理中的具体结构性故障，例如倾向于跳过前置条件查找的倾向。

作者将 MANTRA 定位为并非安全行为的独立保证，而是开发合规关键环境中更可信 AI 系统的关键组成部分，弥合了机器学习与形式化验证之间的鸿沟。