MENTOR: Procedural Shielding of Tool-Using LLM Agents

Ashwani Anand; Ivi Chatzi; Ritam Raha; Anne-Kathrin Schmuck

cs.CLOct 12, 2026

MENTOR: Procedural Shielding of Tool-Using LLM Agents

Authors: Ashwani Anand, Ivi Chatzi, Ritam Raha, Anne-Kathrin Schmuck

Organizations: Max Planck Institute for Software Systems, Kaiserslautern, Germany · TNO-ESI, Eindhoven, The Netherlands

Abstract

Tool-using LLM agents are increasingly used to automate workflows governed by procedural manuals, such as company rules for booking travel or procuring hardware. These manuals are written in natural language for humans and describe general requirements over such complex workflows. Ensuring compliance of LLM agents with these manuals is difficult, and state-of-the-art techniques use either LLM judges or manually written rules to forbid problematic tool-calls locally at runtime. This is insufficient because (i) only blocking tool calls keeps the agent clueless about how to make correct progress towards fulfilling its task, and (ii) can lead to overly conservative behavior of the agent, as tool calls might only be problematic in certain contexts. To overcome these challenges, we introduce MENTOR, which (i) additionally provides guidance for the agent to make procedural-compliant progress on the task, and (ii) ensures that this compliance is context-aware. We achieve these goals by building a novel history-dependent runtime shield that is obtained from the procedural manual via a multi-step autoformalization pipeline. At its core, MENTOR utilizes a game-based technique to ensure robustness against runtime uncertainty without over-resticting agents' behavior. This yields a formally assisted framework for procedural shielding of LLM agents that improves compliance well beyond existing methods. In particular, MENTOR lifts the compliance of shielded light-weight open-source LLMs above that of non-shielded proprietary models. Since a shield is synthesized once per manual and then serves every task, a MENTOR-shielded agent becomes a viable choice for repeatedly executed workflows, potentially reducing deployment costs when the offline construction cost is amortized over repeated tasks.

Figures & tables

Panel of Figure 1 — Figure 1: Running example. Our procedural shield MENTOR is generated from a procedural manual (top right) and applied to a travel-booking task (top left). MENTOR shields the interaction between an LLM agent (pink) and the environment (brown). MENTOR blocks tool calls (red), allows tool calls (green), and provides guidance towards task completion (orange).

Panel of Figure 2 — Figure 2: Overview of MENTOR . Manual and tool schema are formalized into an LTL-based template and an SMT-based solver (offline, top right), used to shield every tool call (online, left) by deterministically evaluating (bottom right) if tool calls are safe and progressing (violet, LTL), and use correct arguments (blue, SMT); unsafe and non-progressing calls receive advice (orange).

Panel of Figure 3 — Figure 3: Autoformalization.

Panel of Figure 4 — Figure 4: Game graph and template (excerpt) for the example from Fig. 1 .

(a) MANTRA	Operations ( $N{=}47$ )				Sneaky Sasquatch ( $N{=}43$ )				$\tau^{2}$ -retail ( $N{=}57$ )				$\tau^{2}$ -airline ( $N{=}44$ )
Guard	L3.1	Q3	Q3.6	G4	L3.1	Q3	Q3.6	G4	L3.1	Q3	Q3.6	G4	L3.1	Q3	Q3.6	G4
None	0 6 $\pm$ 4	45 $\pm$ 7	60 $\pm$ 7	51 $\pm$ 7	21 $\pm$ 6	33 $\pm$ 7	53 $\pm$ 8	23 $\pm$ 7	0 5 $\pm$ 3	11 $\pm$ 4	21 $\pm$ 5	16 $\pm$ 5	20 $\pm$ 6	36 $\pm$ 7	52 $\pm$ 8	34 $\pm$ 7
AgentSpec	13 $\pm$ 5	55 $\pm$ 7	72 $\pm$ 7	62 $\pm$ 7	14 $\pm$ 5	28 $\pm$ 7	63 $\pm$ 7	16 $\pm$ 6	0 9 $\pm$ 4	25 $\pm$ 6	26 $\pm$ 6	19 $\pm$ 5	30 $\pm$ 7	43 $\pm$ 8	50 $\pm$ 8	43 $\pm$ 8
Progent	0 4 $\pm$ 3	47 $\pm$ 7	68 $\pm$ 7	47 $\pm$ 7	21 $\pm$ 6	30 $\pm$ 7	51 $\pm$ 8	23 $\pm$ 7	0 9 $\pm$ 4	12 $\pm$ 4	25 $\pm$ 6	21 $\pm$ 5	27 $\pm$ 7	39 $\pm$ 7	45 $\pm$ 8	39 $\pm$ 7
DynaGuard	11 $\pm$ 5	21 $\pm$ 6	40 $\pm$ 7	28 $\pm$ 7	19 $\pm$ 6	30 $\pm$ 7	49 $\pm$ 8	19 $\pm$ 6	12 $\pm$ 4	23 $\pm$ 6	19 $\pm$ 5	19 $\pm$ 5	34 $\pm$ 7	34 $\pm$ 7	39 $\pm$ 7	27 $\pm$ 7
[][] Ours (prompt)	36 $\pm$ 7	72 $\pm$ 7	66 $\pm$ 7	72 $\pm$ 7	35 $\pm$ 7	63 $\pm$ 7	70 $\pm$ 7	65 $\pm$ 7	16 $\pm$ 5	33 $\pm$ 6	33 $\pm$ 6	40 $\pm$ 7	41 $\pm$ 7	64 $\pm$ 7	64 $\pm$ 7	50 $\pm$ 8

Table 1:

\mathbf{Pass\text{\textasciicircum}5}

\pm

standard error (%) over the

N

test cases of a domain. (a) Open-weights agents on MANTRA against the baselines. (b) Proprietary agents on MANTRA domains. (c) Open-weights agents on AgentOrca . None denotes no shield, and the highest value in each column is bolded.

Appendix figures & tables14 assets

Supplementary material from the paper’s appendix.

Appendix

Panel of Table 2 — Table 2: Comparison of MENTOR with existing LLM guarding approaches: supported, partially supported, not supported, – not applicable.

(a) Specification structure
$\langle\mathit{spec}\rangle$	::=	$(\{\langle\mathit{type}\rangle\},\{\langle\mathit{module}\rangle\},\{\langle\mathit{request}\rangle\},\{\langle\mathit{observation}\rangle\})$
$\langle\mathit{type}\rangle$	::=	$(S,\kappa)$
$\langle\mathit{module}\rangle$	::=	$(S,\{\langle\mathit{proposition}\rangle\},\{\langle\mathit{requirement}\rangle\},\{\langle\mathit{constraint}\rangle\})$
$\langle\mathit{proposition}\rangle$	::=	$(p(v),t,e)$
$\langle\mathit{requirement}\rangle$	::=	$(\mathsf{kind},\varphi,m)$
$\langle\mathit{constraint}\rangle$	::=	$(p(v),e,m)$

Appendix

Figure 6: Abstract structure and syntax of the specification language. Braces denote finite collections. In (a),

S

is an entity type and

\kappa

its entity-identification rules;

\mathsf{kind}

classifies a temporal requirement as a safety requirement or an obligation, and

m

is its source sentence. A request declaration gives a pseudo tool name

Q

, a typed argument schema

\Sigma

, defaults

d

, and extraction instructions

I

. An observation declaration identifies the free-text and label fields of an outcome and its label vocabulary

\Lambda

. In (c),

c

is a constant,

\pi

a field path, and

b_{v}

the event introducing the entity. The function meanings are given in Table 3 . Auxiliary string, list, and conversion helpers are omitted from the core expression grammar.

Expression	Meaning
$\operatorname{last}(p(v))$	The latest earlier event satisfying $p(v)$ ; if none exists, its fields are undefined ( $\mathsf{null}$ ).
$\operatorname{exists}(p(v))$ , $\operatorname{count}(p(v))$	Whether an earlier event satisfies $p(v)$ , and the number of such events, respectively.
$\operatorname{hist}(p(v),\pi)$	The non-null values at path $\pi$ from earlier events satisfying $p(v)$ , in chronological order.
$\operatorname{present}(e)$	Whether $e$ is neither null, an empty string, nor an empty list.
$\operatorname{len}(e)$	The length of a string or list; zero for an unsuitable value.
$\operatorname{contains}(e_{1},e_{2})$	For a list $e_{1}$ , whether it contains an element equal to $e_{2}$ ; for a string, a case-insensitive substring test.

Appendix

Table 3: Functions in the core expression language. History operations use earlier recorded events with the entity parameter

v

bound. A field path

\pi

selects information from an event’s tool arguments or outcome.

Domain	Model	None	AgentSpec	Progent	DynaGuard	Ours	Ours
						(prompt)	(token)
	Llama 3.1	0.26 $\pm$ 0.05	0.34 $\pm$ 0.06	0.27 $\pm$ 0.05	0.20 $\pm$ 0.05	0.61 $\pm$ 0.06	0.58 $\pm$ 0.06
	Qwen3	0.62 $\pm$ 0.06	0.71 $\pm$ 0.06	0.66 $\pm$ 0.06	0.34 $\pm$ 0.06	0.80 $\pm$ 0.05	0.70 $\pm$ 0.06
	Qwen3.6	0.72 $\pm$ 0.06	0.84 $\pm$ 0.05	0.75 $\pm$ 0.06	0.51 $\pm$ 0.07	0.79 $\pm$ 0.05	0.74 $\pm$ 0.06
	Gemma 4	0.63 $\pm$ 0.07	0.69 $\pm$ 0.06	0.65 $\pm$ 0.06	0.39 $\pm$ 0.07	0.84 $\pm$ 0.05	0.73 $\pm$ 0.06
	GPT-5.4 mini	0.72 $\pm$ 0.06	–	–	–	0.82 $\pm$ 0.05	–

Appendix

Table 4: Pass@

\mathbf{1}

on the four MANTRA domains for open-weight (white) and proprietary (gray) agents.

Domain	Model	None	AgentSpec	Progent	DynaGuard	Ours	Ours
						(prompt)	(token)
	Llama 3.1	0.43 $\pm$ 0.07	0.60 $\pm$ 0.07	0.47 $\pm$ 0.07	0.32 $\pm$ 0.07	0.77 $\pm$ 0.06	0.81 $\pm$ 0.06
	Qwen3	0.72 $\pm$ 0.07	0.81 $\pm$ 0.06	0.79 $\pm$ 0.06	0.47 $\pm$ 0.07	0.85 $\pm$ 0.05	0.77 $\pm$ 0.06
	Qwen3.6	0.79 $\pm$ 0.06	0.89 $\pm$ 0.05	0.81 $\pm$ 0.06	0.64 $\pm$ 0.07	0.85 $\pm$ 0.05	0.85 $\pm$ 0.05
	Gemma 4	0.70 $\pm$ 0.07	0.74 $\pm$ 0.06	0.79 $\pm$ 0.06	0.49 $\pm$ 0.07	0.87 $\pm$ 0.05	0.83 $\pm$ 0.06
	GPT-5.4 mini	0.81 $\pm$ 0.06	–	–	–	0.85 $\pm$ 0.05	–

Appendix

Table 5: Pass@

\mathbf{5}

on the four MANTRA domains for open-weight (white) and proprietary (gray) agents.

		TSR
Domain	Model	None	Ours	Ours
			(prompt)	(token)
Patient intake ( $N=35$ )	Llama 3.1	0.03 $\pm$ 0.05	0.29 $\pm$ 0.28	0.38 $\pm$ 0.20
	Qwen3	0.29 $\pm$ 0.11	0.61 $\pm$ 0.04	0.46 $\pm$ 0.07
	Qwen3.6	0.90 $\pm$ 0.07	1.00 $\pm$ 0.00	1.00 $\pm$ 0.00
	Gemma 4	1.00 $\pm$ 0.00	1.00 $\pm$ 0.00	1.00 $\pm$ 0.00

Appendix

Table 6: Task Success Rate (TSR), SOP-Bench’s flawed benchmark score, of open-weights agents on two domains.

Domain	Model	Claude Opus 5	Claude Sonnet	gpt-5.5	gpt-5.6-luna	Qwen3.8
Operations ( $N=47$ )	Llama 3.1	0.38 $\pm$ 0.06	0.09 $\pm$ 0.04	0.47 $\pm$ 0.07	0.13 $\pm$ 0.05	0.11 $\pm$ 0.05
	Qwen3	0.64 $\pm$ 0.07	0.34 $\pm$ 0.07	0.68 $\pm$ 0.07	0.23 $\pm$ 0.06	0.34 $\pm$ 0.07
	Gemma 4	0.75 $\pm$ 0.06	0.68 $\pm$ 0.07	0.79 $\pm$ 0.06	0.36 $\pm$ 0.07	0.55 $\pm$ 0.07
$\tau^{2}$ -retail ( $N=57$ )	Llama 3.1	0.28 $\pm$ 0.05	0.25 $\pm$ 0.06	0.09 $\pm$ 0.04	0.16 $\pm$ 0.05	0.14 $\pm$ 0.05
	Qwen3	0.39 $\pm$ 0.06	0.46 $\pm$ 0.07	0.39 $\pm$ 0.07	0.28 $\pm$ 0.06	0.42 $\pm$ 0.07
	Gemma 4	0.33 $\pm$ 0.06	0.32 $\pm$ 0.06	0.35 $\pm$ 0.06	0.30 $\pm$ 0.06	0.35 $\pm$ 0.06

Appendix

Table 7:

\mathbf{Pass\text{\textasciicircum}3}

of the prompt shield on two MANTRA domains and three agents, with the specification written by different models.

Domain	Model	None	AgentSpec (LLM-gen)	AgentSpec (our loop)	Ours
Operations ( $N=43$ )	Llama 3.1	0.00 $\pm$ 0.00	0.05 $\pm$ 0.03	0.00 $\pm$ 0.00	0.26 $\pm$ 0.07
	Qwen3	0.28 $\pm$ 0.07	0.26 $\pm$ 0.07	0.19 $\pm$ 0.06	0.58 $\pm$ 0.08
	Qwen3.6	0.60 $\pm$ 0.08	0.77 $\pm$ 0.07	0.77 $\pm$ 0.07	0.70 $\pm$ 0.07
	Gemma 4	0.56 $\pm$ 0.08	0.63 $\pm$ 0.07	0.56 $\pm$ 0.08	0.70 $\pm$ 0.07
Sneaky Sasquatch ( $N=39$ )	Llama 3.1	0.08 $\pm$ 0.04	0.03 $\pm$ 0.03	0.00 $\pm$ 0.00	0.15 $\pm$ 0.06
	Qwen3	0.44 $\pm$ 0.08	0.23 $\pm$ 0.07	0.41 $\pm$ 0.08	0.69 $\pm$ 0.07

Appendix

Table 8:

\mathbf{Pass\text{\textasciicircum}5}

\pm

standard error over the

N

held-out cases of a domain, for the prompt shield with AgentSpec rules written by AgentSpec ’s LLM rule generator (LLM-gen) and by our autoformalization loop (our loop), next to the unshielded agent (None) and our specification (Ours).

	$\mathbf{Pass\text{\textasciicircum}3}$
	Sneaky Sasquatch		$\tau^{2}$ -retail
Labeler	Qwen3	Gemma 4	Qwen3	Gemma 4
gpt-4.1-mini	0.70 $\pm$ 0.07	0.62 $\pm$ 0.07	0.39 $\pm$ 0.06	0.33 $\pm$ 0.06
Qwen3-4B	0.68 $\pm$ 0.07	0.60 $\pm$ 0.07	0.44 $\pm$ 0.06	0.28 $\pm$ 0.05
Gemma 4	0.07 $\pm$ 0.04	0.07 $\pm$ 0.04	0.42 $\pm$ 0.07	0.28 $\pm$ 0.06
gpt-oss	0.02 $\pm$ 0.02	0.07 $\pm$ 0.04	0.35 $\pm$ 0.06	0.26 $\pm$ 0.06

Appendix

Table 9: Labeler ablation:

\mathbf{Pass\text{\textasciicircum}3}

of the prompt shield on two MANTRA domains and two agents.

		Prompt shield	Prompt shield	Token shield
		(gpt-4.1-mini)	(gpt-4.1)	(gpt-4.1)
Domain	Model	$\mathbf{Pass\text{\textasciicircum}k}$ 5	$\mathbf{Pass\text{\textasciicircum}k}$ 5	$\mathbf{Pass\text{\textasciicircum}k}$ 5
Operations	Llama 3.1	0.28 $\pm$ 0.07	0.21 $\pm$ 0.06	0.38 $\pm$ 0.07
	Qwen3	0.62 $\pm$ 0.07	0.64 $\pm$ 0.07	0.55 $\pm$ 0.07
	Qwen3.6	0.72 $\pm$ 0.07	0.70 $\pm$ 0.07	0.66 $\pm$ 0.07
	Gemma 4	0.72 $\pm$ 0.07	0.77 $\pm$ 0.06	0.57 $\pm$ 0.07

Appendix

Table 10: Labeler ablation:

\mathbf{Pass\text{\textasciicircum}5}

on all MANTRA with the GPT-4.1 mini and the GPT-4.1 labeler.

		$\mathbf{Pass\text{\textasciicircum}5}$
Domain	Model	None	Ours (gpt-4.1)	Ours (Qwen3-4B FT)
Operations ( $N=47$ )	Llama 3.1	0.00 $\pm$ 0.00	0.21 $\pm$ 0.06	0.30 $\pm$ 0.07
	Qwen3	0.28 $\pm$ 0.07	0.64 $\pm$ 0.07	0.60 $\pm$ 0.07
	Qwen3.6	0.62 $\pm$ 0.07	0.72 $\pm$ 0.07	0.72 $\pm$ 0.07
	Gemma 4	0.55 $\pm$ 0.07	0.77 $\pm$ 0.06	0.70 $\pm$ 0.07
Sneaky Sasquatch ( $N=43$ )	Llama 3.1	0.07 $\pm$ 0.04	0.09 $\pm$ 0.04	0.14 $\pm$ 0.05

Appendix

Table 11:

\mathbf{Pass\text{\textasciicircum}5}

\pm

standard error over the

N

test cases of a domain, on the MANTRA synthetic domains (top) and the MANTRA

\tau^{2}

domains (bottom), without a shield (None) and with our prompt shield, with gpt-4.1 or the fine-tuned Qwen3-4B as the labeler.

Domain	Model	None	AgentSpec	Progent	DynaGuard	Ours (prompt)	Ours (token)
Operations ( $N=47$ )	Llama 3.1	0.59 $\pm$ 0.03	0.57 $\pm$ 0.02	30.70 $\pm$ 0.46	3.01 $\pm$ 0.07	0.73 $\pm$ 0.04	2.26 $\pm$ 0.05
	Qwen3	10.00 $\pm$ 0.67	9.95 $\pm$ 0.13	44.31 $\pm$ 1.29	13.28 $\pm$ 0.20	9.58 $\pm$ 0.55	10.52 $\pm$ 0.18
	Qwen3.6	18.96 $\pm$ 0.82	25.72 $\pm$ 2.31	54.21 $\pm$ 1.85	65.25 $\pm$ 5.64	29.12 $\pm$ 2.98	23.87 $\pm$ 2.90
	Gemma 4	0.64 $\pm$ 0.01	0.64 $\pm$ 0.01	34.47 $\pm$ 0.92	2.63 $\pm$ 0.06	0.75 $\pm$ 0.03	0.99 $\pm$ 0.03
Sneaky Sasquatch ( $N=43$ )	Llama 3.1	0.39 $\pm$ 0.01	0.40 $\pm$ 0.01	21.25 $\pm$ 0.98	2.34 $\pm$ 0.14	0.45 $\pm$ 0.00	1.66 $\pm$ 0.04
	Qwen3	7.52 $\pm$ 0.69	8.89 $\pm$ 0.28	28.77 $\pm$ 1.08	10.68 $\pm$ 0.79	6.72 $\pm$ 0.22	10.57 $\pm$ 1.47

Appendix

Table 12: Seconds per proposed tool call (including blocked), mean

\pm

standard deviation.

Domain	Model	None	AgentSpec	Progent	DynaGuard	Ours (prompt)	Ours (token)
Operations ( $N=47$ )	Llama 3.1	4.8 $\pm$ 0.1	7.4 $\pm$ 0.3	5.0 $\pm$ 0.2	18.1 $\pm$ 1.1	8.7 $\pm$ 0.5	11.0 $\pm$ 0.3
	Qwen3	4.3 $\pm$ 0.1	4.9 $\pm$ 0.2	4.4 $\pm$ 0.1	13.3 $\pm$ 0.9	5.3 $\pm$ 0.1	8.3 $\pm$ 0.9
	Qwen3.6	5.0 $\pm$ 0.1	5.3 $\pm$ 0.2	5.1 $\pm$ 0.3	9.0 $\pm$ 0.8	6.3 $\pm$ 0.3	10.9 $\pm$ 0.4
	Gemma 4	5.2 $\pm$ 0.1	5.2 $\pm$ 0.0	5.1 $\pm$ 0.1	5.3 $\pm$ 0.2	6.1 $\pm$ 0.6	10.5 $\pm$ 1.0
Sneaky Sasquatch ( $N=43$ )	Llama 3.1	8.6 $\pm$ 1.5	11.8 $\pm$ 1.1	8.7 $\pm$ 1.1	10.8 $\pm$ 1.1	9.0 $\pm$ 0.3	8.8 $\pm$ 0.6
	Qwen3	4.2 $\pm$ 0.2	5.6 $\pm$ 0.3	4.5 $\pm$ 0.2	6.1 $\pm$ 0.6	5.6 $\pm$ 0.1	6.5 $\pm$ 0.3

Appendix

Table 13: Number of tool calls the agent proposed per testcase (including blocked) mean

\pm

standard deviation.

		GPT-4.1 mini		GPT-4.1
Domain	cases	cents/case	USD/domain	cents/case	USD/domain
Operations	47	0.06	0.029	0.30	0.143
Sneaky Sasquatch	43	0.07	0.030	0.35	0.150
$\tau^{2}$ -retail	57	0.25	0.141	1.24	0.705
$\tau^{2}$ -airline	44	0.20	0.086	0.97	0.429

Appendix

Table 14: Cost of the labeler per domain, in US cents per testcase and in USD per one run over the full domain, at prices of GPT-4.1 mini (0.40/1.60 USD per 1M input/output tokens) and GPT-4.1 (2.00/8.00).

LLM Guardrails

Large language model guardrails detect or constrain harmful outputs, prompt attacks, and unsafe agent actions before they cause harm.

See all 194 papers

MANTRA: Synthesizing SMT-Validated Compliance Benchmarks for Tool-Using LLM Agents
May 7, 2026Ashwani Anand, Ivi Chatzi, Ritam Raha +1Computer-Use Agent Benchmarks AI Agent Reliability
Max Planck Institute for Software Systems, Kaiserslautern, Germany
AgentLTL: A Trace-Verification Framework for Measuring, Enforcing, and Training Procedural Compliance in Tool-Using LLM Agents
Jul 1, 2026Laïla Elkoussy, Julien PerezLLM Agent Evaluation Formal Verification
LRE, EPITA · LRE · Bpifrance
Compile, Then Page: Executable SOP Programs and a Capability-Gated Runtime for Procedural LLM Agents
Jul 13, 2026Chenglin Yu, Li Yin, Ying Yu +4Instruction Following Runtime Enforcement for AI Agents
Department of Industrial and Systems Engineering, The Hong Kong Polytechnic University · Department of Data and Systems Engineering, The University of Hong Kong · College of Economics and Management, Zhejiang Normal University +3

May 7, 2026J/K move · Enter open · S save

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

Ashwani Anand, Ivi Chatzi, Ritam Raha, Anne-Kathrin Schmuck

Max Planck Institute for Software Systems, Kaiserslautern, Germany

Computer-Use Agent Benchmarks AI Agent Reliability LLM Agent Verification AI Agent Benchmarks Synthetic Benchmark Generation Tool-Using Agents+1

Open paper AskPDF 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.

Abstract

LLM Guardrails

Explore similar work

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

AgentLTL: A Trace-Verification Framework for Measuring, Enforcing, and Training Procedural Compliance in Tool-Using LLM Agents

Compile, Then Page: Executable SOP Programs and a Capability-Gated Runtime for Procedural LLM Agents