MANTRA: Synthesizing SMT-Validated Compliance Benchmarks for Tool-Using LLM Agents
作者: Ashwani Anand, Ivi Chatzi, Ritam Raha, Anne-Kathrin Schmuck
分类: cs.CL, cs.LG, cs.LO
发布日期: 2026-05-07
💡 一句话要点
MANTRA：合成SMT验证的合规性基准，用于工具型LLM Agent
🎯 匹配领域: 支柱二：RL算法与架构 (RL & Architecture) 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 工具型LLM Agent 合规性基准 SMT验证 形式化验证 自动基准生成
📋 核心要点
- 现有工具型LLM Agent的评估依赖人工构建基准或LLM评判，存在可扩展性差或对复杂任务缺乏可靠性的问题。
- MANTRA框架通过自动合成机器可检查的合规性基准，并使用SMT求解器验证其一致性，解决了现有方法的局限性。
- MANTRA构建了一个包含285个任务的新基准测试套件，并验证了其合规性检查的丰富性和约束执行的强度，可用于调试Agent的失败模式。
📝 摘要（中文）
工具型大型语言模型（LLM）Agent越来越多地部署在需要严格程序手册来规范其可靠行为的场景中。确保这些Agent遵守手册中的规则极具挑战性，因为手册通常以自然语言为人类编写，而Agent的行为表现为工具调用的执行轨迹。现有的LLM Agent评估依赖于手动构建的基准或基于LLM的评判，这些方法要么无法扩展，要么对于复杂、长期的手册缺乏可靠性。为了克服这些限制，我们提出了MANTRA，一个从自然语言手册和工具模式自动合成机器可检查的合规性基准的框架。MANTRA独立生成（i）捕获程序依赖关系的符号世界模型，以及（ii）给定任务的一组轨迹级合规性检查，并使用SMT求解验证它们的一致性。一个结构化的修复循环解决不一致问题，仅在作为后备方案时才需要人工干预。这产生了经过正式验证的基准。重要的是，MANTRA支持任意领域和长程序手册，并提供可调的任务复杂性概念，用于自动推导具有挑战性的任务以及合规性检查。使用MANTRA，我们构建了一个新的基准测试套件，包含跨越6个领域的285个任务，可扩展到50多页的手册，且只需极少的人工干预。经验表明，与现有基准相比，合规性检查更丰富，约束执行更强。此外，检查的粒度可用于调试Agent的失败模式。这些结果表明，将自动基准生成与形式化验证方法相结合，能够实现工具型Agent的可扩展和可靠的基准测试。
🔬 方法详解
问题定义：现有工具型LLM Agent的评估方法，如人工构建基准或LLM评判，在面对复杂、长流程的任务时，存在可扩展性不足和可靠性低的问题。人工构建成本高昂，且难以覆盖所有可能的场景。LLM评判则可能受到偏见和不一致性的影响，难以保证评估的客观性。
核心思路：MANTRA的核心思路是自动化生成合规性基准，并利用形式化方法（SMT求解）验证其正确性。通过符号世界模型捕获程序依赖关系，并生成轨迹级别的合规性检查，从而实现对Agent行为的精确评估。这种方法避免了人工构建的局限性，并提供了更可靠的评估结果。
技术框架：MANTRA框架包含以下主要模块：1) 符号世界模型生成器：从自然语言手册和工具模式中提取信息，构建符号世界模型，捕获程序依赖关系。2) 合规性检查生成器：基于符号世界模型，生成轨迹级别的合规性检查，用于验证Agent的行为是否符合规则。3) SMT验证器：使用SMT求解器验证符号世界模型和合规性检查的一致性。4) 修复循环：如果发现不一致，则通过结构化的修复循环进行修正，必要时需要人工干预。
关键创新：MANTRA的关键创新在于将自然语言手册转化为机器可验证的合规性基准，并利用SMT求解器进行形式化验证。这种方法实现了基准的自动生成和验证，大大提高了评估的效率和可靠性。此外，MANTRA还支持任意领域和长程序手册，并提供了可调的任务复杂性概念，使得可以生成具有挑战性的任务。
关键设计：MANTRA的关键设计包括：1) 使用符号逻辑表示程序依赖关系，使得可以使用SMT求解器进行验证。2) 设计了结构化的修复循环，用于解决符号世界模型和合规性检查中的不一致性。3) 提供了可调的任务复杂性概念，允许用户控制生成的任务的难度。具体参数设置和损失函数等细节未在摘要中详细说明，属于未知信息。
🖼️ 关键图片
📊 实验亮点
MANTRA构建了一个包含285个任务的新基准测试套件，覆盖6个领域，手册页数超过50页。实验结果表明，MANTRA生成的合规性检查比现有基准更丰富，约束执行更强。此外，检查的粒度可用于调试Agent的失败模式，帮助开发者更好地理解和改进Agent的行为。
🎯 应用场景
MANTRA可应用于各种需要工具型LLM Agent遵循严格程序手册的领域，例如：自动化客服、流程自动化、机器人控制等。该研究的实际价值在于提供了一种可扩展和可靠的Agent评估方法，有助于提高Agent的合规性和可靠性，从而降低风险和提高效率。未来，该方法可以进一步扩展到更复杂的领域，并与其他形式化验证技术相结合。
📄 摘要（原文）
Tool-using large language model (LLM) agents are increasingly deployed in settings where their reliable behavior is governed by strict procedural manuals. Ensuring that such agents comply with the rules from these manuals is challenging, as they are typically written for humans in natural language while agent behavior manifests as an execution trace of tool calls. Existing evaluations of LLM agents rely on manually constructed benchmarks or LLM-based judges, which either do not scale or lack reliability for complex, long-horizon manuals. To overcome these limitations, we present MANTRA, a framework for automatically synthesizing machine-checkable compliance benchmarks from natural-language manuals and tool schemas. MANTRA independently generates (i) a symbolic world model capturing procedural dependencies, and (ii) a set of trace-level compliance checks for a given task, and validates their consistency using SMT solving. A structured repair loop resolves inconsistencies, requiring human intervention only as a fallback. %This yields benchmarks that are formally validated. Importantly, MANTRA supports arbitrary domains and long procedural manuals, and provides a tunable notion of task complexity which is utilized to automatically derive challenging tasks accompanying compliance checks. Using MANTRA, we build a new benchmark suite with 285 tasks across 6 domains scaling to 50+ page manuals with minimal human effort. Empirically, we show that the compliance checks are richer with stronger constraint enforcement compared to existing benchmarks. Additionally, the granularity of the checks can be used for debugging the agents' failure modes. These results demonstrate that combining automated benchmark generation with formally grounded validation methods enables scalable and reliable benchmarking of tool-using agents.