# MANTRA: Synthesizing SMT-Validated Compliance Benchmarks for Tool-Using LLM Agents

arXiv: https://arxiv.org/abs/2605.06334 · HTML: https://mlsanity.com/paper/2605.06334/

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Placed in Tool learning and function calling, one of 16 directions in LLM agents and tool use.
- Builds on 14 of its 48 references that are in the map.
- First posted on arXiv 7 May 2026.

## Placed in

- LLM agents and tool use / [Tool learning and function calling](https://mlsanity.com/agents/tool-learning-and-function-calling/)

## Builds on (most cited first, 14 of 14)

- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Retrieval-Augmented Generation for Large Language Models: A Survey](https://mlsanity.com/paper/2312.10997/) (2023)
- [From Local to Global: A Graph RAG Approach to Query-Focused Summarization](https://mlsanity.com/paper/2404.16130/) (2024)
- [τ2-Bench: Evaluating Conversational Agents in a Dual-Control Environment](https://mlsanity.com/paper/2506.07982/) (2025)
- [ScienceBoard: Evaluating Multimodal Autonomous Agents in Realistic Scientific Workflows](https://mlsanity.com/paper/2505.19897/) (2025)
- [TravelAgent: An AI Assistant for Personalized Travel Planning](https://mlsanity.com/paper/2409.08069/) (2024)
- [IntellAgent: A Multi-Agent Framework for Evaluating Conversational AI Systems](https://mlsanity.com/paper/2501.11067/) (2025)
- [SOP-Bench: Complex Industrial SOPs for Evaluating LLM Agents](https://mlsanity.com/paper/2506.08119/) (2025)
- [The Fusion of Large Language Models and Formal Methods for Trustworthy AI Agents: A Roadmap](https://mlsanity.com/paper/2412.06512/) (2024)
- [Agent-Diff: Benchmarking LLM Agents on Enterprise API Tasks via Code Execution with State-Diff-Based Evaluation](https://mlsanity.com/paper/2602.11224/) (2026)
- [VERGE: Formal Refinement and Guidance Engine for Verifiable LLM Reasoning](https://mlsanity.com/paper/2601.20055/) (2026)
- [VeriCoT: Neuro-symbolic Chain-of-Thought Validation via Logical Consistency Checks](https://mlsanity.com/paper/2511.04662/) (2025)
- [A Neurosymbolic Approach to Natural Language Formalization and Verification](https://mlsanity.com/paper/2511.09008/) (2025)
- [Governing AI Agents](https://mlsanity.com/paper/2501.07913/) (2025)

## Built on by (most cited first, 4 of 4)

- [When Retrieval Metrics Mislead: Measuring Policy Signal in Long-Horizon Tool-Use Agents](https://mlsanity.com/paper/2606.23937/) (2026)
- [AeroCopilotBench: A Two-Tier Benchmark for Evaluating LLM Agents as Aviation Copilots in an Interactive Virtual Cockpit Environment](https://mlsanity.com/paper/2608.16349/) (2026)
- [Policy Loopholes in Agent Evaluation: When Policy Ambiguity Masquerades as Agent Error](https://mlsanity.com/paper/2609.14400/) (2026)
- [MENTOR: Procedural Shielding of Tool-Using LLM Agents](https://mlsanity.com/paper/2610.17039/) (2026)

## Abstract (arXiv)

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.