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

使用工具的 大语言模型 (LLM) 代理越来越多地部署在其可靠行为受严格程序手册控制的环境中。确保此类代理遵守这些手册中的规则具有挑战性，因为它们通常是用自然语言为人类编写的，而代理行为表现为工具调用的执行跟踪。现有的 LLM 代理评估依赖于手动构建的基准或基于 LLM 的判断，这些判断要么无法扩展，要么缺乏复杂的长期手册的可靠性。为了克服这些限制，我们提出了 MANTRA，这是一个从自然语言手册和工具模式自动合成机器可检查的合规性基准的框架。 MANTRA 独立生成 (i) 捕获程序依赖性的符号世界模型，以及 (ii) 针对给定任务的一组跟踪级别合规性检查，并使用 SMT 求解验证其一致性。结构化修复循环可以解决不一致问题，仅需要人工干预作为后备措施。 %这产生了经过正式验证的基准。重要的是，MANTRA 支持任意领域和冗长的程序手册，并提供任务复杂性的可调概念，用于自动导出伴随合规性检查的挑战性任务。使用 MANTRA，我们构建了一个新的基准套件，其中包含 6 个领域的 285 项任务，以最少的人力扩展到 50 多页手册。根据经验，我们表明与现有基准相比，合规性检查更丰富，约束执行更严格。此外，检查的粒度可用于调试代理的故障模式。这些结果表明，将自动基准生成与正式验证方法相结合，可以对使用工具的代理进行可扩展且可靠的基准测试。