MANTRA：为工具使用 LLM 智能体合成 SMT 验证的合规性基准
计算与语言
2026-05-08 v1 机器学习
计算机科学中的逻辑
摘要
工具使用大语言模型 (LLM) 智能体越来越多地部署在其可靠行为受严格程序手册约束的环境中。确保此类智能体遵守这些手册中的规则极具挑战性，因为这些手册通常以自然语言为人类编写，而智能体行为表现为工具调用的执行轨迹。现有的 LLM 智能体评估依赖人工构建的基准或基于 LLM 的评判器，这些方法对于复杂、长周期的手册要么无法扩展，要么缺乏可靠性。为克服这些限制，我们提出了 MANTRA，一个从自然语言手册和工具模式自动合成机器可检查合规性基准的框架。MANTRA 独立生成 捕捉程序依赖关系的符号世界模型，以及 给定任务的一组轨迹级合规性检查，并使用 SMT 求解验证其一致性。结构化修复循环解决不一致性，仅在万不得已时需要人工干预。重要的是，MANTRA 支持任意领域和长程序手册，并提供可调的任务复杂度概念，用于自动生成伴随合规性检查的挑战性任务。使用 MANTRA，我们构建了一个包含跨 6 个领域 285 个任务的新基准套件，可扩展至 50 多页的手册且只需极少的人力。实验表明，与现有基准相比，合规性检查更丰富且具有更强的约束执行能力。此外，检查的粒度可用于调试智能体的失败模式。这些结果表明，将自动化基准生成与形式化验证方法相结合，能够实现对工具使用智能体的可扩展且可靠的基准测试。
引用
@article{arxiv.2605.06334,
title = {MANTRA: Synthesizing SMT-Validated Compliance Benchmarks for Tool-Using LLM Agents},
author = {Ashwani Anand and Ivi Chatzi and Ritam Raha and Anne-Kathrin Schmuck},
journal= {arXiv preprint arXiv:2605.06334},
year = {2026}
}