MANTRA：为工具使用型 LLM 代理综合生成经 SMT 验证的合规基准

# MANTRA：为使用工具的 LLM 智能体合成经 SMT 验证的合规性基准

来源：https://arxiv.org/html/2605.06334

机构：德国凯泽斯劳滕，马普软件系统研究所

邮箱：{ashwani,ichatzi,rraha,akschmuck}@mpi-sws.org

###### 摘要

使用工具的大型语言模型（LLM）智能体正越来越多地被部署在那些依靠严格程序手册来规范其可靠行为的场景中。确保这些智能体遵守手册中的规则极具挑战性，因为这些手册通常是用自然语言写给人类阅读的，而智能体的行为则表现为工具调用的执行轨迹。现有的 LLM 智能体评估方法依赖于人工构建的基准或基于 LLM 的裁判，前者难以扩展，后者在处理复杂、长周期的手册时缺乏可靠性。为了克服这些局限性，我们提出了 MANTRA，这是一个从自然语言手册和工具模式中自动合成机器可检查的合规性基准的框架。MANTRA *独立地*生成 (i) 捕获程序依赖关系的符号世界模型，以及 (ii) 针对特定任务的一组轨迹级合规性检查，并使用 SMT 求解器验证它们的一致性。结构化的修复循环解决不一致之处，仅在最后阶段需要人工干预。重要的是，MANTRA 支持任意领域和长程序手册，并提供可调的任务复杂度概念，用于自动推导伴随合规性检查的挑战性任务。利用 MANTRA，我们以最少的人力投入，构建了包含 6 个领域、285 个任务的新基准套件，手册规模可扩展至 50 页以上。实证研究表明，与现有基准相比，MANTRA 生成的合规性检查更丰富，约束强制力更强。此外，检查的粒度可用于调试智能体的故障模式。这些结果表明，将自动化基准生成与形式化验证方法相结合，能够实现可扩展且可靠的工具使用智能体基准测试。

## 1 引言

近年来，使用工具的大型语言模型（LLM）智能体的能力有了显著提高。现代智能体可以自主规划、调用外部工具，并在企业运营[44](https://arxiv.org/html/2605.06334#bib.bib42), [27](https://arxiv.org/html/2605.06334#bib.bib41)、科学发现[38](https://arxiv.org/html/2605.06334#bib.bib44), [33](https://arxiv.org/html/2605.06334#bib.bib45)、旅行预订[6](https://arxiv.org/html/2605.06334#bib.bib40)以及医疗保健[13](https://arxiv.org/html/2605.06334#bib.bib43), [25](https://arxiv.org/html/2605.06334#bib.bib46)等各种领域执行复杂的多步骤工作流。然而，它们的实际效用不仅取决于其成功完成任务的能力，还取决于它们是否遵守管理它们的法规和程序[18](https://arxiv.org/html/2605.06334#bib.bib48), [48](https://arxiv.org/html/2605.06334#bib.bib47)。例如，在购买公司硬件时，员工必须遵守详细的政策，规定在哪些条件下应内部 sourcing 物品 versus 订购，以及在购买前必须完成哪些审批步骤。此类政策通常以自然语言手册的形式编写，供人类解读，而智能体的行为则观察为工具调用的执行轨迹。这种不匹配使得为评估工具使用智能体的程序合规性设计基准变得内在困难，因为它需要将非正式指令转换为对执行轨迹的可机器检查的约束。

现有基准通过人工约束构建、基于 LLM 的裁判或两者的结合来解决这个问题[32](https://arxiv.org/html/2605.06334#bib.bib3), [43](https://arxiv.org/html/2605.06334#bib.bib13), [2](https://arxiv.org/html/2605.06334#bib.bib14), [20](https://arxiv.org/html/2605.06334#bib.bib51), [22](https://arxiv.org/html/2605.06334#bib.bib50), [26](https://arxiv.org/html/2605.06334#bib.bib4), [31](https://arxiv.org/html/2605.06334#bib.bib49), [39](https://arxiv.org/html/2605.06334#bib.bib7), [30](https://arxiv.org/html/2605.06334#bib.bib8)（见表 1[1](https://arxiv.org/html/2605.06334#S1.T1)）。人工构建可以产生高质量的评估，但跨领域和长手册扩展的成本高昂。基于 LLM 的裁判更易于部署，但它们难以可靠地处理长轨迹中的严格时间约束、前置条件和禁止操作。因此，当前方法没有提供一种可扩展且可重现的方法来从自然语言手册构建轨迹级合规性基准。

我们提出 MANTRA（MANual-to-Test-tRAnslation，手册到测试转换）来填补这一空白，这是一个从自然语言程序文档和工具模式中自动生成合规性基准的框架。与所有现有方法不同，MANTRA 展现了*极高*的自动化水平，并产生了高质量的轨迹级合规性检查，从而允许确定性地评估智能体。因此，MANTRA 可扩展到大型非结构化程序文档，并且可以以最少的人力投入轻松扩展到新的领域。

##### 贡献。具体而言，我们做出了以下贡献：

(i) 我们开发了一个自动化流水线，将给定的自然语言程序手册和工具模式转换为机器可检查的合规性基准，具有可控的任务难度和确定性的轨迹级评分。

(ii) 我们引入了一种双产物公式，分别生成符号世界模型和合规性检查，并通过可满足性模理论（SMT）[8](https://arxiv.org/html/2605.06334#bib.bib2), [3](https://arxiv.org/html/2605.06334#bib.bib1)求解器自动交叉验证。这使得在基准项被接受之前能够自动识别和修复不一致之处。支持人工审核，但仅作为后备方案需要。

(iii) 为了展示 MANTRA 作为基准生成器的能力，我们创建了包含 285 个多样基准的套件，跨越 6 个领域。我们通过实证表明，轨迹级检查的粒度可用于调试智能体的故障模式。代码可用地址为 [https://anonymous.4open.science/r/mantra-for-compliance/](https://anonymous.4open.science/r/mantra-for-compliance/)，基准数据可用地址为 [https://huggingface.co/datasets/mantra-anon/MANTRA](https://huggingface.co/datasets/mantra-anon/MANTRA)。

表 1：MANTRA 与代表性工具使用和智能体合规性基准的比较，包括支持的（✓）、部分/间接支持的（△）和不支持的（✗）功能。

注释：*自动化生成*如果任务自动生成但需要大量人工验证或手工构建环境，则部分满足（△）。*大文档大小*如果使用长结构化指令而非非结构化程序手册，则仅部分支持（△）。*扩展到新领域*如果需要特定领域的手工努力，则仅部分满足（△）。*轨迹评估*当检查执行轨迹的程序属性（例如，必需或禁止的调用、约束顺序等）而不仅仅是最终答案或数据库状态时，支持（✓），如果轨迹级属性由 LLM 裁判评估，则部分支持（△）。*确定性评估*如果每个测试的评分完全可重现而不调用 LLM 裁判，则支持（✓），如果评估仅部分依赖 LLM 裁判，则部分支持（△）。

##### 相关工作。

我们的工作建立在关于基准测试工具使用智能体、自动化基准生成以及使用形式化方法验证 LLM 输出的日益增长的文献基础之上。工具使用智能体的研究一直是近期研究的重点[24](https://arxiv.org/html/2605.06334#bib.bib21)，提出了大量基准，涵盖网络导航[42](https://arxiv.org/html/2605.06334#bib.bib26), [47](https://arxiv.org/html/2605.06334#bib.bib27)、科学[36](https://arxiv.org/html/2605.06334#bib.bib18)以及一般工具和 API 使用[21](https://arxiv.org/html/2605.06334#bib.bib36), [23](https://arxiv.org/html/2605.06334#bib.bib17), [17](https://arxiv.org/html/2605.06334#bib.bib20), [29](https://arxiv.org/html/2605.06334#bib.bib25), [30](https://arxiv.org/html/2605.06334#bib.bib8)等各种领域。然而，如表 1[1](https://arxiv.org/html/2605.06334#S1.T1)所示，基准在处理非结构化和开放式任务方面的能力仍然有限（详见附录 [0.A](https://arxiv.org/html/2605.06334#Pt0.A1)）。即使是最相似的基准 SOP-Bench[26](https://arxiv.org/html/2605.06334#bib.bib4)，在基准生成、验证和扩展到新领域方面也需要大量人力，这极大地限制了其相对于 MANTRA 的可扩展性。

自动化基准生成最近在不同背景下得到了探索[40](https://arxiv.org/html/2605.06334#bib.bib12)，特别是用于编码任务[37](https://arxiv.org/html/2605.06334#bib.bib33), [46](https://arxiv.org/html/2605.06334#bib.bib32), [16](https://arxiv.org/html/2605.06334#bib.bib34), [19](https://arxiv.org/html/2605.06334#bib.bib35)。然而，这些基准依赖于对结构化任务的基于准确性的评估，并非设计用来测试智能体的工具使用能力，也不涉及检查工具轨迹与为人类使用设计的复杂自然语言手册的合规性。MANTRA 将这些技术带到了工具使用 LLM 智能体日益部署的非结构化领域。

尽管形式化方法在软件系统的规范和验证方面有着悠久的历史[1](https://arxiv.org/html/2605.06334#bib.bib37)，但其在 LLM 背景下的应用仍然探索不足[45](https://arxiv.org/html/2605.06334#bib.bib23)。一条新兴的研究线研究了使用符号求解器来改善 LLM 生成的代码[5](https://arxiv.org/html/2605.06334#bib.bib28)、逻辑推理[28](https://arxiv.org/html/2605.06334#bib.bib39), [41](https://arxiv.org/html/2605.06334#bib.bib38), [11](https://arxiv.org/html/2605.06334#bib.bib31)和规划[15](https://arxiv.org/html/2605.06334#bib.bib24)，以及检测幻觉声明[34](https://arxiv.org/html/2605.06334#bib.bib29)。最近，有人提出了将自然语言政策和 LLM 输出翻译为符号规范以进行响应接地[4](https://arxiv.org/html/2605.06334#bib.bib30)，其重点在于验证静态自然语言输出。相比之下，MANTRA 不仅验证最终输出，还构建轨迹级合规性检查以评估工具调用序列。

**硬件采购程序手册**

*标准履行 (A)。* 在履行硬件请求时，智能体必须首先 *检查库存*。如果所请求的物品有库存，智能体必须 *分配仓库拣货员*。它*不得*为有库存的物品 *创建采购订单*。...

*集成实验室采购 (B)。* 对于需要采购的 *集成实验室请求*，智能体必须首先在 *创建采购订单* 之前 *检查遗留门户*，并且必须为 incoming 硬件 *设置交付选项*。

**工具模式**

```
check_inventory
assign_warehouse_picker
create_purchase_order
check_legacy_portal
set_delivery_options
...
```

**案例 1** 使用段落 (A)

*场景。* “请为 Lake Union Studio 的 Maya Torres 获取 1 台 Dell UltraSharp U2723QE 显示器。报价物品价格为 $1,850，属于刷新请求 HW-2841。此请求仍处于待处理状态，尚未创建采购订单。”

```
CALL check_inventory(item_name="Dell UltraSharp U2723QE")
CALL assign_warehouse_picker(item_id="HWM2741", quantity=1)
check_inventory PRECEDES assign_warehouse_picker
NO-CALL create_purchase_order
```

**案例 2** 使用段落 (A), (B)

*场景。* “我需要为位于 4100 Blake Street, Denver, CO 80216 的丹佛集成实验室获取 1 个 Cisco Catalyst 9300 交换机。报价物品价格为 $1,995，如果必须购买，供应商报价显示交货时间为 9 天。将其归入待处理请求 LAB-9315。”

```
CALL check_inventory(item_name="Cisco Catalyst 9300")
CALL check_legacy_portal(item_id="HWC9305")
check_inventory PRECEDES check_legacy_portal
CALL create_purchase_order(item_id="HWC9305", quantity=1)
create_purchase_order FOLLOWS check_legacy_portal
CALL set_delivery_options(item_id="HWC9305")
```

图 1：运行示例。从硬件采购手册和工具模式中，MANTRA 合成带有具体场景和轨迹级检查的基准项。案例 1 由段落 (A) 生成，而案例 2 结合了段落 (A) 和 (B)。

## 2 概述

在详细介绍 MANTRA 之前，我们使用图 1[1](https://arxiv.org/html/2605.06334#S1.F1) 中的运行示例来说明其操作——如图 2[2](https://arxiv.org/html/2605.06334#S3.F2) 所示。该示例基于硬件采购程序手册 $\mathcal{D}$，图 1[1](https://arxiv.org/html/2605.06334#S1.F1) 左侧显示了其中两个代表性段落。此外，MANTRA 接收一个全局工具模式 $\mathcal{T}$，描述工具使用智能体可用于与隐藏数据库 $DB$（变量为 $\mathrm{Var}_{\texttt{DB}}$）交互的工具。

给定这些输入，MANTRA 构建一个经过验证的测试用例基准套件 $\mathcal{B}=\{b_i\}_{i\in[n]}, n\in\mathbb{N}$，图 1[1](https://arxiv.org/html/2605.06334#S1.F1) 右侧显示了其中两个。每个测试用例 $b_i$ 围绕一个场景 $\lambda_i$ 展开，该场景在图 2[2](https://arxiv.org/html/2605.06334#S3.F2) 的步骤 1 中从 $\mathcal{D}$ 生成。为此，MANTRA 首先构建一个依赖图 $\mathcal{G}_{\mathcal{D}}$，以捕获 $\mathcal{D}$ 中的层次结构和引用关系，然后采样一个子图 $\mathcal{G}_{\mathcal{D}_\mathrm{S}}$，对应于 $\mathcal{D}$ 的区域 $\mathcal{D}_\mathrm{S}$ 以及相关工具的子集 $\mathcal{T}_\mathrm{S}$。然后，LLM 将 $(\mathcal{D}_\mathrm{S}, \mathcal{T}_\mathrm{S})$ 映射到一个具体场景 $\lambda$，包括提示 $p_\lambda$ 和相关变量的估值。这一步的关键设计选择是采样子图控制场景复杂度：在图 1[1](https://arxiv.org/html/2605.06334#S1.F1) 中，案例 1 仅使用段落 (A)，而案例 2 结合段落 (A) 和 (B)。

当提示 $p_\lambda$ 随后与 $\mathcal{D}$ 一起提供给智能体时，它产生一个执行轨迹 $\tau=[(t_0, a_0), \dots, (t_{l-1}, a_{l-1})]$，其中每个 $t_i \in \mathcal{T}$ 是一个工具调用，每个 $a_i$ 实例化其参数。MANTRA 的步骤 2 为每个场景 $\lambda$ 生成一组轨迹级检查 $\mathcal{C}_\lambda$，规定此类轨迹是否符合采样的文档区域。这些检查为智能体轨迹提供了确定性评估程序。由于检查由 LLM 生成，MANTRA 不假设它们正确。相反，步骤 3 为相同的 $\mathcal{D}_\mathrm{S}$ 独立生成世界模型 $\mathcal{W}_\mathrm{S}$，并使用基于 SMT 的交叉验证来比较 $\mathcal{C}_\lambda$ 和 $\mathcal{W}_\mathrm{S}$ 所允许的有界轨迹。具体而言，MANTRA 搜索满足检查但违反世界模型的有界轨迹，这表明检查约束不足或世界模型过度约束，以及搜索满足世界模型但仅违反单个检查的有界轨迹，这可能...