Technical Summary: MANTRA – Synthesizing SMT-Validated Compliance Benchmarks

Problem Statement

Tool-using Large Language Model (LLM) agents are increasingly deployed in critical domains such as enterprise operations, healthcare, and travel booking, where their behavior must adhere to strict procedural manuals. A fundamental challenge in evaluating these agents is the "mismatch" between the input and the output: procedural rules are typically written as unstructured natural language for human interpretation, while agent behavior manifests as a sequence of tool calls (execution traces).

Existing evaluation methods suffer from significant limitations:

• Manual Construction: Creating benchmarks by hand is high-quality but does not scale to large, complex manuals or new domains.
• LLM-based Judges: While easier to deploy, these judges struggle to reliably enforce strict temporal constraints, preconditions, and forbidden actions over long execution traces, leading to unreliable evaluations.
• Outcome-only Evaluation: Many benchmarks only check the final state, failing to detect if an agent arrived at the correct result via a non-compliant procedural path.

There is a lack of a scalable, reproducible method to automatically generate trace-level compliance benchmarks from natural-language manuals that provide deterministic, machine-checkable grading.

Methodology: The MANTRA Framework

MANTRA (MANual-to-Test-tRAnslation) is a framework designed to automatically synthesize compliance benchmarks from natural-language procedural documents and tool schemas. It operates through a three-stage pipeline that combines LLM generation with formal verification:

1. Document Ingestion and Scenario Generation

• Dependence Graph Construction: The system ingests a procedural manual ($D$) and constructs a dependence graph ($G_D$) where nodes represent content chunks (e.g., paragraphs) and edges represent hierarchical and reference relations.
• Coverage-Driven Sampling: To control task complexity and ensure broad coverage, MANTRA samples subgraphs ($G_{DS}$) from $G_D$. Small, dense subgraphs yield simple scenarios; larger or loosely connected subgraphs induce complex scenarios involving multiple rules.
• Tool Relevance & Scenario Synthesis: For each sample, an LLM identifies relevant tools ($T_S$) and generates concrete scenarios ($\lambda$). Each scenario includes a natural-language prompt ($p_\lambda$) and a valuation of variables, including internal state variables (e.g., "request is pending") that are made explicit in the prompt to guide the agent.

2. Check Generation and World Model Creation

To evaluate compliance deterministically, MANTRA generates two independent artifacts for each scenario:

• Trace-Level Checks ($C_\lambda$): An LLM generates a set of boolean checks specifying required tool calls, forbidden calls, and temporal ordering (e.g., check_inventory must precede assign_warehouse_picker). These checks are grounded with concrete argument values.
• Symbolic World Model ($W_S$): Independently, an LLM generates a world model representing the procedural rules as a state-transition system. This model is expressed in a typed Domain Specific Language (DSL) defining state variables, tool preconditions, and postconditions. This abstraction allows for compact representation of complex procedural logic.

3. Cross-Validation via SMT Solving

The core innovation of MANTRA is the use of Satisfiability Modulo Theories (SMT) solvers (specifically Z3) to cross-validate the generated checks and the world model.

• Bounded Model Checking: Both $C_\lambda$ and $W_S$ are compiled into bounded SMT encodings ($b\Phi_h$) over a trace horizon $h$.
• Conflict Search: The system searches for two types of inconsistencies:
  1. Forward Conflict: Traces that satisfy the checks but violate the world model (indicating checks are too weak or the model is too restrictive).
  2. Backward Conflict: Traces that satisfy the world model but violate a specific check (indicating the check is too restrictive).
• Structured Repair Loop: When conflicts are found, MANTRA employs a repair loop:
  • World Model Resolution: If multiple scenarios from the same sample share a conflict, an LLM proposes a shared repair to the world model (e.g., adding a missing precondition).
  • Check Resolution: If conflicts persist, the system identifies and repairs specific checks for individual scenarios.
  • Deterministic Edits: Repairs are applied via a typed edit language to ensure well-formedness, followed by recompilation and re-validation.
• Human-in-the-Loop: If automated repairs fail after a set number of iterations, the system flags the scenario for structured human review, where a reviewer can manually resolve ambiguities.

Key Contributions

1. Automated Pipeline: A fully automated pipeline for converting natural-language manuals and tool schemas into machine-checkable benchmarks with controllable task difficulty and deterministic grading.
2. Two-Artifact Formulation: The separation of trace-level checks and symbolic world models, which are cross-validated via SMT solving. This allows for the automatic identification and repair of inconsistencies before benchmarks are accepted, minimizing human intervention.
3. Benchmark Suite: The creation of a new benchmark suite containing 285 diverse tasks across 6 domains (Operations, Sneaky Sasquatch, Cabin Safety, Retail, Airline, Telecom). These tasks scale to procedural manuals of up to ~16,000 words and 148 tools, with minimal human effort.
4. Granular Failure Analysis: The framework provides trace-level checks that enable detailed debugging of agent failure modes, distinguishing between missing calls, ordering violations, and forbidden actions.

Results and Evaluation

The authors evaluated the MANTRA framework and the resulting benchmarks using 6 different LLM agents.

• Validation Efficiency: The SMT-based cross-validation successfully validated a significant portion of generated test cases automatically. For example, in the "Operations" domain, 63 out of 66 generated cases were validated after forward and backward refinement rounds.
• Agent Performance: Evaluation revealed that current LLM agents struggle with procedural compliance. Success rates varied significantly by domain, with "Retail" and "Airline" (from $\tau$-Bench) proving particularly difficult due to complex tool usage rather than document length.
• Failure Mode Analysis: Analysis of 10,895 failed checks showed that 76% of failures were due to "Missing-Required-Call" (skipping a mandated tool) or "Missing-Anchor" (failing to execute the prerequisite for an ordering clause).
  • A dominant failure pattern was "premature writing," where agents called write-style tools before performing necessary read-style lookups.
  • The model Qwen3.6:36B demonstrated superior performance, particularly in Airline and Retail domains, by maintaining a strict "read-before-write" habit, achieving a 0% premature-write rate in these domains.
• Comparison to Existing Benchmarks: Unlike existing benchmarks that rely on manual construction or LLM judges, MANTRA provides deterministic, trace-level evaluation that scales to large, unstructured documents and new domains with minimal human effort.

Significance and Claims

The paper claims that MANTRA demonstrates the viability of combining automated benchmark generation with formally grounded validation methods to create scalable and reliable benchmarks for tool-using agents.

• Reliability: By using SMT solvers to cross-validate checks against a world model, MANTRA ensures that benchmarks are free from logical inconsistencies that might arise from LLM hallucinations, providing a higher degree of trust in the evaluation results compared to LLM-as-a-judge approaches.
• Scalability: The framework addresses the scalability bottleneck of manual benchmark creation, enabling the evaluation of agents against complex, real-world procedural manuals (up to 50+ pages) across arbitrary domains.
• Debugging Capability: The granularity of the trace-level checks allows researchers to move beyond simple pass/fail metrics to understand specific structural failures in agent reasoning, such as the tendency to skip prerequisite lookups.

The authors position MANTRA not as a standalone guarantee of safe behavior, but as a critical component for developing more trustworthy AI systems in compliance-critical settings, bridging the gap between machine learning and formal verification.