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

针对工具使用大语言模型智能体在严格程序手册下的合规性挑战，本文提出 MANTRA 框架。该框架能从自然语言手册和工具模式中自动合成机器可检查的合规性基准，通过生成符号世界模型与轨迹级检查，并利用 SMT 求解器验证一致性。实验构建了涵盖 6 个领域、285 个任务的新基准套件，支持长篇幅手册且无需大量人工干预。结果表明，该方法生成的检查更具约束力，能有效调试智能体失败模式，实现了可扩展且可靠的工具使用智能体评估。