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

Summary

MANTRA automatically synthesises machine-checkable compliance benchmarks from a natural-language procedural manual plus a tool schema, with no ground-truth trajectories and no LLM judge. It builds a dependence graph over the manual, samples a subgraph (the sample size is the difficulty knob), and has an LLM emit a scenario — a prompt plus a concrete valuation of the relevant DB variables. It then generates two independent artifacts from the same document region: a set of deterministic trace-level checks over tool calls, and a symbolic world model expressed as a typed DSL state-transition system. Both are compiled to bounded SMT encodings and cross-validated with Z3 in two directions — find a trace satisfying the checks but violating the world model (checks too weak), and a trace satisfying the world model but violating exactly one check (checks too strong) — feeding a structured repair loop, with human review only as a fallback via a conflict-inspection web UI. The prototype (GPT-5.4, Z3, trace bound h=16, ≤5 refinement rounds, 4 scenarios per sample) produced 285 validated tasks across 6 domains from 703 generated candidates, over manuals of 1,158–16,644 words and tool schemas of 13–148 tools, three domains lifted straight from τ-bench. Evaluating 6 models × 5 runs, none reaches high procedural compliance; of 10,895 failed checks, 76% are Missing-Required-Call or Missing-Anchor, largely because weaker models write before they read.

Key points

• Difficulty is controlled structurally, not by prompt: the dependence graph captures hierarchy and reference relations in the manual, and the sampled subgraph decides how many interacting rules a scenario must satisfy (one paragraph = easy, two linked paragraphs = harder). A coverage_islands sampling strategy spreads scenarios over the manual. This is a principled, tunable complexity axis derived from the source document rather than from author intuition.
• The check language is a small grammar over traces: atomic call(t,a) and no_call(t,a) with partial argument maps (only the arguments explicitly named must match), plus disjunction and temporal operators after, before, follows, precedes. Arguments are grounded in the scenario’s variable valuation, not symbolic. Mean checks per case ranges 2.75–6.19 by domain.
• The core trick is redundancy plus a solver: two artifacts generated independently from the same text, compared formally. The authors explicitly do not treat the world model as ground truth — the validation signal is disagreement, and they report finding no case where the LLM hallucinated the same error into both, which would have produced a false-positive validation.
• They argue directly against both existing verification approaches: end-state checks “cannot determine whether the agent followed the correct procedure”, and LLM judges are “sensitive to the variability of LLM judgments”. Trace-level deterministic checks are their answer to grading a task with many valid orderings.
• Yield and cost of the automation: 703 candidate cases → 285 validated, ~41%; validated counts climb across refinement rounds R1–R5 without saturating; unresolved conflicts are left for human review (which the authors did not do), and they did inspect every auto-validated case, removing a few broken by engineering artifacts such as an argument pinning an exact string (a check that allowed only “Cookies” where any high-glucose food should qualify).
• The failure taxonomy comes free from the check granularity: each failed check names which required call or ordering anchor was missing, so “76% of failures are missing required calls” is a measured fact rather than a judged one. The derived behavioural finding — premature writing, i.e. calling a write tool before any read tool — cleanly separates strong from weak models, and Qwen3.6:36B never writes prematurely on tau2-airline/retail and leads there.
• Counterintuitive result worth carrying: the τ-bench domains are the hardest despite having the shortest manuals and fewest tools — tool complexity, not policy volume, drove difficulty.
• Limitations the authors name: no formal certification against the original document (only cross-validation between two generated artifacts); a fixed trace bound h=16 means inconsistencies beyond that horizon go undetected; the tool schema and database must be supplied as input, not generated; only tool-call traces are gradable, so anything that is not a tool call is invisible; six English-language manuals.

Relevance

• ITSMBench — the most direct answer in this batch to the project’s verifier question. V2’s current verifiers are binary end-state pytest checks, and the project’s own open question is “end-state only misses policy-violating paths; what trajectory checks are needed and what do they cost?” MANTRA answers both: the checks are a tiny temporal grammar over tool calls, and the cost is a dependence graph, an LLM pass, a DSL world model, and bounded Z3 — all automatable, and it runs on manuals up to 16,644 words with 148 tools, which is the scale of an ITSM runbook and V1’s ~309 mocked operations. It is also the one paper here that generates tasks and verifiers together from a policy document, which is exactly the “task assets” layer we say logs do not provide. What it does not cover: it never touches event logs, so it says nothing about whether the resulting task distribution matches real work — its coverage guarantee is over the manual, not over what people actually do. It also assumes the tool schema and database already exist, needs no user simulator (single-shot prompt, no conversation), and has no multi-agent story.
• WorldSmith — the strongest evidence yet that verifier authoring can be automated without trusting an LLM judge, by generating two independent representations and letting a solver find their disagreements. That is a general recipe: any artifact an LLM can express twice in different formalisms can be cross-validated. The measured yield (703 → 285, ~41%, with refinement still climbing at round 5) and the residual human role (inspect auto-validated cases, adjudicate leftover conflicts through a UI) put concrete numbers on the automation/human split. Compare with Curation-Bench’s execution-research gap: here the LLM is not searching a policy space, it is transcribing a document into two formalisms, which is the kind of task the Curation-Bench evidence says agents do reliably.
• Benchmark Research — a benchmark-design contribution on three counts: difficulty as a sampled subgraph of a document dependence graph; trace-level compliance checks as a middle path between end-state diffs and LLM judges; and a failure taxonomy that falls out of check granularity instead of being annotated after the fact.
• Environment Generation — home concept since 2026-09-10

Questions it raises for ITSMBench:

• MANTRA’s tasks are validated against a manual. BPI logs are behaviour, not policy — and real ITSM practice routinely diverges from the runbook. If a MANTRA-style pipeline ran on an ITSM policy document, would its checks mark the actual observed log behaviour non-compliant, and is that a bug in the benchmark or the most interesting finding available?
• Could the world model be generated from the event log instead of from a second LLM pass over the document — a process model discovered by PM4Py or AgentSimulator — turning the cross-validation into “does the policy agree with what people really did”? That would make the log a formal validator rather than only a realism yardstick.
• Their checks are grounded per scenario, and the whole pipeline assumes a fixed tool schema. V2 has ~309 operations across five mocked vendor APIs and a frozen clock. What is the actual cost of running this on that schema, and does h=16 cover ITSM tasks whose human trajectories run 20–40 steps?

Notes

(Our take: to add after reading; drafted 2026-09-09, not yet discussed)