1 Introduction↩︎

Tool-augmented LLM agents are increasingly used in enterprise and safety-critical settings, yet evaluation still focuses on final-answer accuracy, often with LLM judges. Two traces can produce the same answer while differing in retrieval, branching, or tool grounding. Answer correctness collapses these differences into a single outcome.
In many settings, the procedure is part of correctness. A clinical triage agent that skips a required contraindication check is not correct, even if its recommendation is. 1 illustrates this common shortcut: the agent answers from parametric memory instead of tool outputs. This fails silently when memory and environment diverge.
We introduce AgentLTL, a language derived from First-Order Linear Temporal Logic (FO-LTL) for expressing procedural, semantic, and grounding constraints over execution traces. Comparing a trace against these constraints yields a deterministic, judge-free compliance score. The same constraints support two uses. When the LTL fragment permits, they gate tool calls before execution, detecting and blocking violating calls. The score also serves as a reinforcement learning reward. A shared constraint language avoids drift between evaluation, deployment, and training.

1.0.0.1 Contributions.

(i) We introduce AgentLTL and its compliance score. (ii) We build a benchmark of 12 workflow templates and evaluate 7 language models under three harnesses that intervene on the trace at different strengths, localizing failures in ordering, branching, iteration, and argument grounding. (iii) We show that the same score is an effective reward: finetuning a target model improves both compliance and answer correctness on held-out templates, including unseen tool-name aliases. (iv) We show that grounding constraints can detect parametric-memory hallucination by distinguishing supported answers from unsupported recall. AgentLTL, the benchmark, training corpus, and scripts are available here.

2 Related Work↩︎

2.0.0.1 Tool-augmented LLM agents.

The tool-using paradigm began with ReAct [1] and expanded through finetuning [2], [3], larger tool inventories [4], [5], and reliability benchmarks such as \(\tau\)-bench [6] and AgentBoard [7]. BFCL [8] evaluates function calling against gold abstract syntax trees, while \(\tau^2\)-bench [9] studies dual-control settings where agents and users jointly modify shared state. OSWorld [10] studies long-horizon failures, and [11] separate process and outcome rewards for computer-use agents. A common finding is the compositionality gap [12]: agents succeed on atomic calls but fail when calls must be composed. Existing evaluations stop at per-call correctness or rely on LLM judges. AgentLTL instead scores the temporal structure of the trace with a deterministic metric.

2.0.0.2 Runtime enforcement and pre-execution guardrails.

Recent systems intercept tool calls before execution. AgentSpec [13] applies per-step DSL rules, AEGIS [14] adds runtime auditing, [15] compile policies into SMT-LIB checks, and PCAS [16] models multi-agent state with Datalog queries. [17] introduces Reinforced Agent, a dual agent architecture with a reviewer to vet tool calls. These systems focus on enforcement and provide limited temporal reasoning over multi-step traces. The agent-reviewer approach also introduces nondeterministic reviewer errors. AgentLTL uses a single specification language for both offline evaluation and online enforcement, with deterministic checks over ordered and parameterized traces.

2.0.0.3 Formal methods and temporal logic for LLM verification.

LTL [18] is the standard temporal formalism, with first-order extensions for entity quantification [19], [20]. [21] translate constraints into LTL to prune unsafe robot plans, [22] verify LLM plans against LTL, and VLTL-Bench [23] surveys the persistent grounding problem in NL-to-LTL translation. Runtime verification over data words [24] also reasons about parametric events. With AgentLTL, we avoid the NL translation step by authoring constraints directly over typed tool signatures, with grounding provided by the recorded call and its response.

2.0.0.4 Process conformance checking.

Process conformance checking has been extensively studied in process mining [25], where event logs are validated against prescriptive workflow models. DECLARE [26] introduced a declarative framework based on \(\text{LTL}_f\) constraints over finite traces, which directly motivates AgentLTL’s specification language. More recently, [27] emphasize online and streaming-based enforcement in contrast to purely retrospective auditing. AgentLTL builds on this line of work by adapting conformance checking to tool-augmented LLM agents, modeling tool invocations as typed events grounded in explicit entities and execution context.

2.0.0.5 Characterization of agent failures.

A separate line of work has sought to characterize how agents fail in practice. MAST [28] applies grounded theory to 1600+ multi-agent traces and identifies 14 failure modes, scaled with an LLM-as-a-Judge pipeline. TravelPlanner [29] reports complementary patterns in single-agent planning, including argument errors, dead loops, and uncorrected early hallucinations, evaluated through keyword-driven rules. Both depend on a judge to reach a verdict. AgentLTL scores the trace directly against a typed FO-LTL specification, removing the judge and localizing failures to specific procedural layers.

2.0.0.6 Hallucination detection and entity grounding.

Agentic hallucination is often entity-level. Models emit plausible identifiers from parametric memory instead of tool outputs [30], and a single incorrect entity can corrupt downstream calls [31]. Post-hoc factuality systems such as Factool [32] verify outputs after generation, while existing enforcement systems do not treat grounding as a core property. With AgentLTL, we express grounding directly as a trace constraint that requires every entity in the final answer to appear in prior tool outputs.

3 The AgentLTL Framework↩︎

3.1 Preliminaries↩︎

We model a tool-using agent as a ReAct type of system [1]: \[\mathcal{A} = \langle \mathcal{M}, \mathcal{T}, \mathcal{E}, \mathcal{H}\rangle,\] where \(\mathcal{M}\) is a language model, \(\mathcal{T}\) a tool set, \(\mathcal{E}\) an execution environment, and \(\mathcal{H}\) the context window. At step \(i\), the model produces a thought \(\theta_i\) and proposes a tool invocation with name \(n_i \in \mathcal{T}\) and arguments \(a_i\). The environment executes the invocation and returns a result \(r_i\), which is appended to the context \(\mathcal{H}\). We record the step as the tuple \[c_i = (n_i,\, a_i,\, r_i,\, i).\] AgentLTL operates on the resulting execution trace \(\tau= \langle c_0,\ldots,c_{n-1}\rangle\). It also uses a metrics record \(\mu\) that stores aggregate statistics over the trace, such as token and tool call counts.

3.2 Formula Language↩︎

AgentLTL specifies properties over execution traces using a fragment of FO-LTL. The language is used to express procedural rules such as “a search must be cited before the final answer” or “every opened file must eventually be closed.” Full syntax and semantics appear in Appendix 10.
Formulas are evaluated against a trace \(\tau\). A formula \(\varphi\) can contain variables ranging over values observed in the trace, such as tool arguments, retrieved entities, or file names. Under a specific trace and a variable assignment, \(\varphi\) evaluates to a boolean. A formula without free variables is a constraint, denoted by \(\kappa\), and is either satisfied or violated by \(\tau\). The language has three components.

3.2.0.1 Atomic propositions.

Atomic propositions describe observable properties of tool calls, including occurrence, ordering, argument matching, return-value checks, and aggregate statistics. For example, \(\mathsf{CalledWith}(\texttt{search}, \{q : \text{``foo''}\})\) holds when a call to search was issued with argument \(q = \text{``foo''}\). The language also supports open predicates, user-defined Boolean functions for domain-specific checks. For example, a user could define \(\mathsf{IsEven}(x)\) to check whether a given integer is even and use it within formulas.

3.2.0.2 Temporal operators.

AgentLTL includes standard LTL operators over finite traces. These operators express temporal relations such as precedence or eventuality. For example, \[\mathsf{G}(\texttt{search} \rightarrow \mathsf{F}\,\texttt{cite})\] states that every search call must eventually be followed by a cite call.

3.2.0.3 Data quantifiers.

Quantifiers range over finite domains extracted from \(\tau\) or \(\mu\), such as tool inputs, generated files, or retrieved entities. To evaluate a formula containing a quantifier, we use eager instantiation: given a domain extractor \(D(\tau)=\{e_1,\ldots,e_n\}\), the formula \(\forall x \in D.\,\varphi(x)\) is evaluated by substituting each entity into \(\varphi\) and checking the resulting formulas independently. Quantifiers may nest and rebind, allowing constraints such as “every file read is eventually written back.”

3.3 Compliance Scoring↩︎

A procedure \(P\) is a weighted set of constraints \(G_P = \{(\kappa_i, w_i)\}\), where each \(\kappa_i\) is an AgentLTL constraint and \(w_i > 0\) denotes its importance. A pair \((\kappa_i, w_i)\) is violated when \(\tau\) does not satisfy \(\kappa_i\).

3.3.0.1 Constraint design.

The weights \(w_i\) are not chosen by the formalism and strongly affects the expressiveness of the score. Indeed, uniform weighting can make the metric brittle: a single arithmetic or reasoning error can invalidate all dependent checks, collapsing the score even when most behavioral constraints are still satisfied. To prevent this, we organize constraints into six layers (L1–L6) of abstraction, each capturing a different failure mode. This separation isolates routing, ordering, and computation errors so they contribute independently to the score.

3.4 Using The Compliance Score↩︎

We introduce to usage of our compliance score. First, harnessing: the same procedure can score a trace offline or block tool calls online. Second, finetuning: because the score is continuous, it serves as a training reward. A harness is a runtime enforcement layer around an agent that monitors behavior and can intercept or regulate tool calls before execution [13], [14]. Existing harnesses use hand-written rules tied to a specific runtime. Ours is built directly from an AgentLTL procedure.

3.4.0.1 Harness implementation.

Given a trace and a procedure, the score measures how closely the agent followed the procedure. Offline mode evaluates a completed trace. The full constraint set \(G_P\) is checked against \(\tau\), and the framework reports both the overall score and per-constraint results. This supports benchmarking and post-hoc analysis. Online mode evaluates a prefix trace \(\tau^{\le i} = \langle c_0, \ldots, c_i \rangle\) before each tool execution. A proposed call is appended to the prefix and checked against the enforceable subset of \(G_P\). The call executes only if no enforceable constraint is definitively violated.
Some constraints cannot be decided from prefixes. For example, a constraint that requires an event to eventually occur cannot be refuted until execution ends. Such constraints are deferred to offline evaluation. Each enforceable constraint has a severity level that determines the response, from logging to corrective feedback or blocking execution.

3.4.0.2 Training reward implementation.

Because \(C(\tau, G_P) \in [0,1]\) is continuous, we can use it directly as a reward. The decomposition over constraints provides dense credit assignment: traces receive partial reward even when only some constraints are satisfied. Layered weighting further separates structural and computational failures, so traces with different error profiles receive different rewards rather than collapsing to the same score.

4 Experimental Settings↩︎

We first describe how our data is generated, then evaluate model compliance under AgentLTL enforcement, finetune on the compliance signal, and finally apply the framework to repository-QA.

4.1 Data Generation and Constraint Design↩︎

4.1.0.1 Dataset.

A template is a named procedural pattern that fixes a procedure and a tool set. We use twelve templates grouped into five structural types. Each template has a production mode for benchmarking and a simplified mode for training. The two modes share the same procedural pattern but differ in prompt length, parameter ranges, and tool-set size. An instance is one (template, difficulty, seed) tuple, which deterministically yields a prompt, a gold trace, an expected answer, and a constraint set. Difficulty (D1–D5) scales one structural parameter of the template, such as loop bound or list length.

4.1.0.2 Generation.

For each instance, a Python function executes the procedure on deterministic arithmetic tools and emits the gold trace and expected answer. Tools have generic names such as tool_a and tool_b but execute fixed integer operations. Every correct answer is derivable from the trace, so failures reflect procedure compliance rather than arithmetic knowledge. The procedures mirror common agent patterns such as paginated fetching, per-record validation, and graph traversal.

4.1.0.3 Constraints.

From each gold trace we instantiate the six constraint layers described in Section 3.3, yielding one constraint set \(G_P\) per task. Structural layers (L3, L4, L5) carry roughly 73% of total weight; L6 is downweighted to prevent a single early arithmetic error from cascading into a near-zero score. 2 shows the constraints generated for one such trace.

4.2 Harnessing Agents↩︎

We evaluate twelve templates at five difficulty levels, with gold traces ranging from 2 to 50 required tool calls, and report compliance per layer, producing a per-trace profile that separates routing errors from argument errors and skipped branches.

4.2.0.1 Settings.

We compare three settings that share the same constraints. Baseline runs the agent to completion and scores offline. Block-and-warn uses online enforcement: a violating call is blocked with a warning, but the same call reissued with the same arguments is allowed through. Soft-block also uses online enforcement, escalates after three violations of the same constraint, and terminates the run. The three settings isolate, respectively, unaided compliance, responsiveness to redirection, and behavior under deployed guardrails.

4.2.0.2 Setup.

We evaluate \(7\) zero-shot models of varying parameter sizes (Gemma-4-26B-A4B, Gemma-4-31B, Qwen3-Next-80B-A3B-Instruct, DeepSeek-V4-Flash, Qwen3.5-397B-A17B, DeepSeek-V4-Pro, Kimi-K2.6) via AgentLTL’s smolagents [33] integration. We run six trials per (model, template, difficulty, seed) across seeds \(s \in \{42, 123\}\), giving \(360\) runs per model per setting, with a budget of \(10d + 10\) tool calls at difficulty \(d\). Answer correctness is exact integer match; compliance is \(C(\tau, G_P)\).

4.3 Compliance-Supervised Finetuning↩︎

4.3.0.1 Training corpus.

We build 300 examples from 15 simplified templates, each using 3–7 tool calls from a pool of four tools and covering sequential, branching, fan-out, and multi-stage patterns. We instantiate each template with multiple tool permutations and augment instances by optionally prepending or appending one extra tool call. This is to discourage memorization of fixed call sequences. Two benchmark templates, loop_termination and branch_selection, are excluded from training and used only for unseen-pattern evaluation.

4.3.0.2 Reward.

We train with Group Relative Policy Optimization (GRPO) using trl [34] under a weighted reward [0.5,0.25,0.25] combining three terms: the main term is \(C(\tau, G_P)\); answer correctness, where correctly formatted but incorrect answers receive \(0.1\) to preserve gradient signal; and a trace-distance term \(R_{\text{dist}}(\tau, \tau^{*}) = \exp(-d(\tau, \tau^{*}))\) based on weighted Levenshtein distance to the gold trace (same tool with different arguments costs \(0.5\), a different tool costs \(1.0\), and insertions and deletions cost \(1.0\)).

4.3.0.3 Training setup.

We finetune Qwen3-4B-Instruct [35] with LoRA (\(r{=}8\), \(\alpha{=}16\)) on q_proj and v_proj for \(1\) epoch, using a round-robin-no-repeat curriculum, fp32 precision, \(N{=}16\) rollouts per prompt, and \(\beta{=}10^{-3}\).

4.3.0.4 Evaluation splits.

We evaluate on four held-out validation splits and the full production benchmark. Unaugmented (83 instances) re-instantiates the 15 training templates with new parameter values. Augmented (100 instances) adds the optional prefix/suffix calls from training. Unseen-pattern (39 instances) uses the two excluded benchmark templates with the training tool set. Diverse-tool (39 instances) keeps trained patterns but swaps in unseen tool names. The production benchmark (360 instances) is partitioned into three transfer groups: direct-simplification (shared high-level flow with a training simplification), motif-overlap (recombined motifs in new configurations), and no-coverage (no structural counterpart in training).

4.4 Trace-Grounding Analysis↩︎

4.4.0.1 Grounding predicate.

For a trace \(\tau\) with final answer \(a\), let \(\mathrm{ent}(\cdot)\) be an open predicate returning the referential tokens (identifiers, file paths, numeric literals) in its argument, and let \(\mathrm{out}(\tau)\) denote the entities observed in tool outputs. We implement \(\mathrm{ent}(\cdot)\) via regex matching and \(\mathrm{out}(\cdot)\) by parsing tool outputs into an abstract syntax tree. The grounding predicate \[\kappa_{\mathrm{ground}} \;\equiv\; \forall e \in \mathrm{ent}(a),\; e \in \mathrm{out}(\tau)\] holds when every entity mentioned in \(a\) was observed in some tool output. Correctness is scored separately from grounding. An answer is correct if it contains all ground-truth entities defined for the question (function signatures, file paths, identifiers).

4.4.0.2 Setup.

We evaluate on 160 (repo, questions) pairs on 16 Python repositories of varying size and popularity. For each repository, we generate 10 questions using Claude Opus 4.7 asking for the location of a public function or a class definition. We test , , and with filesystem tools (list_directory,read_file). We compare a default prompt against a strict-grounding prompt that instructs the model to answer only from retrieved evidence or refuse. Across two seeds per configuration, we collect 1,917 valid traces.

4.4.0.3 Evaluation.

To validate \(\kappa_{\mathrm{ground}}\) as a hallucination signal, we compare it against a trace-aware LLM judge (DeepSeek-V4-Pro) applied post-hoc. The judge receives the question, the full tool trace, and the answer, and is asked whether every factual claim in the answer is supported by the trace. It makes five independent calls per trace and returns a mean boolean decision. The judge does not drive the primary evaluation; it exists to test whether \(\kappa_{\mathrm{ground}}\) verdicts correlate with LLM judgment.

5 Results↩︎

5.1 Harnessing Agents↩︎

5.1.0.1 Enforcement effects.

Table 1 shows block-and-warn improves compliance for five of seven models, with the largest gains on the weakest models. It raises accuracy by \(+0.019\)on average. Two strong models regress slightly under block-and-warn. Soft-block is the worst setting for four of seven models, since forced termination prevents recovery from violations. The two settings affect trace length in opposite ways: block-and-warn pushes models past early stopping points and lengthens traces, while soft-block shortens them through forced termination. Enforcement events concentrate on argument extraction and global sequence (L2: \(61,111\) and L3:\(62,811\)). Branch and count violations are sparse but high-impact. Insistence on blocked calls is rare.

5.1.0.2 Baseline evaluation and compliance profiles.

4 reports per-layer pass-rates. L3 (global sequence) is the weakest layer for every model. L4 (pair-order) tracks L3 closely, so the same trace failures violate both global and pairwise ordering. L4 accounts for 55-77% of weighted loss across models. Branch routing, argument extraction, and call-count pass at much higher rates, so failures concentrate in ordering rather than tool selection or argument formatting. The compliance-correctness gap varies by model. DeepSeek-V4-Pro produces correct answers from non-compliant traces; Qwen3-Next-80B shows the inverse, with high compliance but low accuracy. Composite templates show the lowest L3 pass-rates and the lowest correctness.

5.2 Compliance-Supervised Finetuning↩︎

5.2.0.1 Training details.

Over the \(4{,}800\) GRPO generations, training-time evaluation rewards improve jointly: AgentLTL compliance from \(0.511\) to \(0.770\), answer correctness from \(0.296\) to \(0.728\), and gold-trace distance reward from \(0.301\) to \(0.782\).

5.2.0.2 Held-out validation.

Table 2 compares the finetuned and base models. Answer correctness more than triples across all four splits with parallel compliance gains. The unseen-pattern and diverse-tool splits yield matched accuracy gains of 38.5 percentage points, consistent with the reward inducing structural rather than surface skill. Trace lengths on the held-out splits are similar before and after finetuning, so the accuracy gains come from better-ordered execution rather than longer execution.

5.2.0.3 Benchmark transfer.

The full benchmark gains 43.8 and 21.3 percentage points in accuracy and compliance under finetuning. Trace lengths reveal the mechanism. The base model issues many tool calls but converts few of them into compliant or correct execution. The finetuned model uses far fewer calls and reaches much higher accuracy and compliance. Gains are consistent across all three transfer groups. The no-coverage gain is evidence for transferable procedural skill rather than memorization, since these templates share no structural counterpart in training. The one remaining failure is , where deeply nested control flow is not recovered by training.

4pt

3pt

3pt

8pt

5.3 Trace-Grounding Analysis↩︎

5.3.0.1 Correctness, grounding, and prompt effects.

Table 3 shows how correctness and grounding combine. Two patterns stand out. First, the larger models (Qwen3.5-397B, Gemma-4-31B) give mostly correct but ungrounded answers, while grounds more of its answers but gets them wrong. Second, the strict prompt raises grounding for all models, but the extra grounded traces are mostly refusals, not correct answers: IG grows more than CG for Qwen3.5-397B and Gemma-4-31B. Splitting by repository popularity makes this clearer. On low-popularity repositories, CG rises from 0.7% to 4.0% under the strict prompt; on high-popularity ones, only from 1.2% to 1.7%. Correctness under the default prompt drops from 52.0% to 24.0% as popularity falls, and the most common category shifts from CU to IU. CG stays at or below 4.0% in every bucket. This fits the idea that the models recall less as repositories appear less often in pretraining. More detailed results in Appendix 17.

5.3.0.2 Comparison with an LLM judge.

\(\kappa_{ground}\) and the trace-aware judge agree on 77.6% of traces, but Cohen’s \(\kappa\) = 0.09 reflects class imbalance. The judge assigns grounded verdicts to 6.4% of answers versus 20.9% for \(\kappa_{ground}\). The judge therefore treats \(\kappa_{ground}\) as a necessary but not sufficient condition for grounding.

6 Discussion↩︎

6.0.0.1 Compliance and correctness diverge.

The two metrics correlate overall. More specifically, is high compliance with low correctness; the large models invert this with correct-but-ungrounded traces. Final-answer accuracy hides both patterns. Previous qualitative evaluations such as MAST document this divergence but cannot quantify it without a judge.

6.0.0.2 Enforcement settings act as diagnostics.

Block-and-warn and soft-block share the same constraints but differ in whether retries are free. Their gap measures how much non-compliance is locally recoverable. Gains under block-and-warn but not soft-block indicate corrigible mistakes rather than absent capability, a pattern concentrated in weaker models. Stronger models converge across settings as first-attempt violations become rare. Soft-block also acts as a deployment proxy: a large drop under it means the model’s baseline score depended on recovering from its own mistakes later in the trace.

6.0.0.3 Sequence failures share one mechanism.

The hardest composite templates map to common agent workloads: and to batch RAG, to routing, and to long-horizon planning. TravelPlanner reports similar failures in single-agent planning. Many L3/L4 violations and correct-but-ungrounded traces appear to stem from the same behavior: when faithful execution becomes costly, models shortcut to parametric memory. This appears either as batching sequential calls into parallel steps or skipping retrieval entirely. The repository-popularity gradient supports this interpretation.

6.0.0.4 Compliance and accuracy rise together.

The no-coverage accuracy gain is the strongest evidence for transferable procedural skill rather than memorization. The full-benchmark compliance gain also resolves a measurement artifact: under step-boundary ordering, the base model’s long traces violate sequence and pair-order constraints repeatedly as it cycles through tools without progressing. The finetuned model traverses the procedure in order. On the held-out splits, where base trace lengths are already close to gold, compliance and accuracy rise together without a length change.

7 Conclusion↩︎

In this paper, we introduced AgentLTL, a framework that treats procedural compliance as an explicit evaluation axis for tool-using LLM agents. Our unified FO-LTL specification language supports evaluation, runtime enforcement, and finetuning within the same formal framework. AgentLTL improves both accuracy and compliance on the proposed benchmark after finetuning. These gains also transfer to the no-coverage split, where templates are unseen during training, suggesting that the reward captures reusable procedural structure rather than template memorization. Our benchmark reveals failure modes that are not reflected by final-answer accuracy alone, including correct-but-ungrounded traces, premature termination, and unproductive loops. Most violations are concentrated in tool ordering and pairwise sequencing constraints. The harness also helps weaker models recover from early-stopping failures without reducing correctness. Overall, these results provide a quantitative view of procedural failures in tool-using agents and suggest that formal specifications can support more reliable agent behavior.

8 Limitations↩︎

Several limitations qualify our findings and point to future work.

8.0.0.1 Vacuous grounding.

The trace-grounding predicate \(\kappa_{\mathrm{ground}}\) is satisfied trivially by refusals, since the universal quantifier holds when the answer contains no entities to verify. Most of the strict-prompt grounding gains for the larger models in our repository-QA experiment are refusals rather than supported answers.

8.0.0.2 Confounded popularity.

The popularity stratification in the grounding study confounds pretraining exposure with repository size and complexity. We cannot separate the two with this design. A cleaner causal claim would require controlled splits matching size across popularity levels, or held-out private repositories with no pretraining footprint.

8.0.0.3 Synthetic tool environment.

The benchmark uses synthetic arithmetic tools to keep ground truth deterministic and decouple procedural compliance from world knowledge. The procedural patterns are drawn from common agent workflows, and the failure modes we isolate match those reported qualitatively in prior work on real-world agents. Whether they transfer quantitatively to noisier real-world environments, with stochastic tool outputs, partial failures, and ambiguous arguments, remains an open question.

8.0.0.4 Model finetuning.

Our finetuning experiments use a single base model (), because of computational limitations, with LoRA adapters. The transfer results on unseen patterns and unseen tools are suggestive of structural learning, but have not been replicated across scales or model families. It is unclear whether the compliance reward remains effective at larger scales where parametric recall is stronger and the shortcut behavior we target is harder to dislodge.

8.0.0.5 Constraints authoring cost.

AgentLTL shifts the cost of evaluation from labeling answers to writing FO-LTL constraints. For benchmarks generated from gold traces this cost is amortized, but in deployment the constraints must be authored by domain experts. We do not address the human factors of constraints authoring, the failure modes of mis-specified procedures, or how errors in constraints propagate into compliance scores and training signals.

8.0.0.6 Constraint coverage and expressiveness.

Our six-layer constraint schema covers the structural failure modes we designed for, but it does not exhaust the space of procedural errors. Constraints on timing, resource consumption, privacy, and inter-agent coordination are outside the current schema. FO-LTL also cannot express hyperproperties, such as non-interference between parallel tool calls, which may matter in multi-agent settings.

8.0.0.7 Enforcement side effects.

The block-and-warn and soft-block results show that enforcement is not uniformly beneficial. Soft-block is the worst setting for most models, since forced termination prevents recovery from violations that block-and-warn would only flag. Block-and-warn helps most models on both compliance and accuracy, but perturbs two of the strongest models that were already near their compliance ceiling. We do not yet have a principled account of when enforcement helps versus hurts, and the right enforcement policy likely depends on model capability and task structure in ways we have not characterized. A deeper issue is that in critical or irreversible workflows, simply stopping execution on a violation may itself cause harm. Blocking a tool call that has already triggered a side effect, or terminating a trace mid-procedure in a multi-step transaction, can leave the system in an inconsistent state. The appropriate response to a violation, whether to block, warn, roll back, or escalate to a human, is use-case dependent and requires richer enforcement semantics than the two settings we evaluate here.

8.0.0.8 Benchmark difficulty.

The template remains at 0.0% correctness after finetuning. Deeply nested control flow is not recovered by training on simpler motifs, and the compliance reward provides no gradient signal when the model cannot produce even a partial trace. More structured curricula, or decomposed constraints that reward partial progress on subprocedures, may be needed for these cases.

8.0.0.9 Single-turn constraints.

Our framework evaluates each trace against a fixed specification written before execution. In practice, procedures may need to adapt mid-execution in response to tool outputs, for example skipping a branch because a preceding call returned an empty result. Dynamic or reactive constraints, where the constraint set is updated as the trace unfolds, are a natural extension that we leave to future work.

9 Ethical Considerations↩︎

9.0.0.1 Use of AI assistance.

We used AI assistants during the preparation of this work. Their use falls within the ACL Policy on AI Writing Assistance. Specifically, we used AI tools for (i) language polishing and paraphrasing of author-written content (category a) and (ii) literature search support, where we verified citation accuracy and relevance for all cited works (category c). No AI system contributed research ideas, framing, or analysis that would warrant acknowledgement as a collaborator. The authors take full responsibility for the correctness of all text, methods, results, and code.

9.0.0.2 Intended use and dual-use considerations.

AgentLTL is designed to evaluate and improve procedural compliance in tool-using LLM agents, with particular relevance to safety-critical settings such as clinical triage, enterprise workflows, and retrieval-grounded question answering. The framework is descriptive: a constraint captures what a procedure requires, but does not validate that the procedure itself is appropriate. A mis-specified or harmful procedure that an agent complies with perfectly is not made safe by a high compliance score. Deployment in any sensitive setting requires domain experts to author and review constraints, and the compliance score should be one signal among several rather than a sufficient certification.

9.0.0.3 Dataset and benchmark.

The benchmark uses synthetic arithmetic tools with no personal, copyrighted, or otherwise sensitive content. The 16 Python repositories in the trace-grounding study are publicly available open-source projects; we use them only for evaluation and do not redistribute their content. The generated questions reference public function and class definitions in those repositories.

9.0.0.4 Compute and environmental cost.

Training Qwen3-4B-Instruct with GRPO required approximately 317 GPU-hours on a single NVIDIA DGX Spark, run continuously from April 29 to May 12, 2026. Evaluation of seven zero-shot models across \(360\) runs per setting and three harness configurations represents an additional compute cost, performed via API access to hosted models. We report all settings and hyperparameters in 4.3 to enable reproduction without redundant recomputation.

9.0.0.5 Reproducibility.

We release the AgentLTL framework, the benchmark with all twelve templates and difficulty levels, the training corpus, the finetuned model adapters, and the evaluation scripts. All experiments use fixed seeds documented in the codebase.

9.0.0.6 Risks of procedural enforcement.

Our harnessing settings can block tool calls before execution. In real deployments, blocking a tool call that has already triggered a side effect, or terminating a trace mid-procedure, can leave a system in an inconsistent state. We discuss this further in 8; in this paper we evaluate enforcement only in synthetic environments where rollback is not required.

10 Appendix A — The AgentLTL Framework (Formal Details)↩︎

This appendix provides the complete formal specification of the AgentLTL framework, complementing 3. It formalizes the trace model, specification language, constraint evaluation, and online enforcement. Throughout, we use \(\tau\) for traces (resolving to \(\tau\) in display) to match the notation of 3. All positions are 0-indexed.

10.1 Trace and Execution Model↩︎

10.1.1 Trace↩︎

A trace is a finite sequence \[\tau= \langle c_0, \dots, c_{n-1} \rangle,\] where each call is the 4-tuple \[c_i = (n_i,\, a_i,\, r_i,\, i),\] with \(n_i \in \mathcal{T}\) the tool name, \(a_i : \text{Key} \to \text{Value}\) the argument mapping, \(r_i \in \text{Value}\) the (possibly structured) result, and \(i\) the position. We write \(c_i.\mathsf{name}, c_i.\mathsf{args}, c_i.\mathsf{result}, c_i.\mathsf{position}\) for the four projections. The position induces a total order: \(i < j \iff c_i \text{ precedes } c_j\). When a trace \(\tau\) satisfies a formula \(\varphi\), we \(\tau\models \varphi\), and \(\tau\not\models \varphi\) when it does not.

10.1.2 Tool Call Schema↩︎

Each call is derived from a JSON record of the form:

{
  "tool_name": "...",
  "arguments": {...},
  "tool_result": "..."
}

and normalized into the tuple above. Arguments are structured mappings; results may be structured or unstructured and are treated opaquely except through the comparator \(\mathsf{match}\) (defined below).

10.1.3 Metrics Record↩︎

A metrics record accompanies the trace: \[\begin{align} \mu = (&\mathsf{tool\_calls},\; \mathsf{num\_steps}, \\ &\mathsf{num\_tool\_calls},\; \mathsf{token\_counts},\; \dots). \end{align}\]

Only \(\mathsf{tool\_calls}\) is required for formal semantics; other fields are auxiliary. See Listing [lst:metrics-example] for a representative instance.

10.1.3.1 Evaluation on recorded traces.

Evaluation is performed on the recorded trace; the framework does not require re-execution. The trace \(\tau\) and metrics \(\mu\) are fixed and fully observable during evaluation, so the semantics below are deterministic regardless of any nondeterminism in the underlying agent or tools.

10.1.4 Auxiliary Functions↩︎

The following helpers are used throughout the predicate definitions. All are 0-indexed. We write \(\bot\) for an undefined value; predicates that depend on a \(\bot\) operand evaluate to false.

• \(\mathsf{first}(t) = \min\{i : c_i.\mathsf{name} = t\}\), or \(\bot\) if \(t\) never occurs.

• \(\mathsf{nth}(t, k) =\) position of the \((k{+}1)\)-th occurrence of \(t\) (0-based: \(\mathsf{nth}(t,0) = \mathsf{first}(t)\)), or \(\bot\) if fewer than \(k{+}1\) occurrences exist.

• \(\mathsf{first\_after}(t, i) = \min\{j \ge i : c_j.\mathsf{name} = t\}\), or \(\bot\) if no such \(j\).

• \(\mathsf{match}(c.\mathsf{result}, r)\): a user-pluggable comparator over results; the default is structural equality.

10.2 FO-LTL Specification Language↩︎

10.2.1 Syntax↩︎

\[\begin{align} \varphi ::= {} & \top \mid \bot \mid p \mid \neg \varphi \mid \varphi \land \varphi \mid \varphi \lor \varphi \\ & \mid \mathsf{X}\varphi \mid \mathsf{F}\varphi \mid \mathsf{G}\varphi \\ & \mid \varphi\,\mathsf{U}\,\varphi \mid \varphi\,\mathsf{W}\,\varphi \mid \varphi\,\mathsf{R}\,\varphi \\ & \mid \forall x \in D.\;\varphi \mid \exists x \in D.\;\varphi \end{align}\]

10.2.2 Atomic Predicates↩︎

Atomic predicates fall into five categories: occurrence (\(\mathsf{Called}\)), ordering (\(\mathsf{Before}, \mathsf{After}, \mathsf{InOrder}\)), argument checks (\(\mathsf{CalledWith}\)), result checks (\(\mathsf{CalledWithResult}\)), and counts (\(\mathsf{CalledN}\)). All predicates are evaluated globally over \(\tau\).

For argument predicates, we write \(\mathbf{a} \sqsubseteq c_i.\mathsf{args}\) to mean that every key–value pair in \(\mathbf{a}\) is present in \(c_i.\mathsf{args}\) (i.e., \(\mathbf{a}\) is a sub-mapping of \(c_i.\mathsf{args}\)).

• \(\mathsf{Called}(t)\): \(\exists i.\; c_i.\mathsf{name} = t\)

• \(\mathsf{CalledN}(t,n,\odot)\): \(|\{i : c_i.\mathsf{name} = t\}| \odot n\), \(\odot \in \{=,\ge,\le,>,<\}\)

• \(\mathsf{Before}(t_1,t_2)\): \(\mathsf{first}(t_1) < \mathsf{first}(t_2)\) (false if either side is \(\bot\)).

• \(\mathsf{After}(t_1,t_2)\): \(\mathsf{first}(t_1) > \mathsf{first}(t_2)\) (false if either side is \(\bot\)).

• \(\mathsf{AllBefore}(\mathbf{T},g)\): \(\forall t \in \mathbf{T}.\; \mathsf{first}(t) < \mathsf{first}(g)\).

• \(\mathsf{InstanceBefore}(t_1,n,t_2,m)\): \(\mathsf{nth}(t_1,n) < \mathsf{nth}(t_2,m)\) (false if either is \(\bot\)).

• \(\mathsf{InOrder}(\mathbf{T})\): for \(\mathbf{T} = \langle t_1,\ldots,t_k\rangle\), there exist indices \(i_1 < i_2 < \cdots < i_k\) with \(c_{i_j}.\mathsf{name} = t_j\) for all \(j\).

• \(\mathsf{WithinSteps}(t_1,t_2,k)\): \(\mathsf{first\_after}(t_2,\mathsf{first}(t_1)) - \mathsf{first}(t_1) \le k\).

• \(\mathsf{CalledWith}(t,\mathbf{a})\): \(\exists i.\; c_i.\mathsf{name} = t \;\wedge\; \mathbf{a} \sqsubseteq c_i.\mathsf{args}\)

• \(\mathsf{CalledWithResult}(t,r,\mathbf{a})\): \(\exists i.\; c_i.\mathsf{name} = t \;\wedge\; \mathbf{a} \sqsubseteq c_i.\mathsf{args} \;\wedge\; \mathsf{match}(c_i.\mathsf{result}, r)\)

• \(\mathsf{BranchCalled}(t^+,t^-)\): \(\mathsf{Called}(t^+) \wedge \neg \mathsf{Called}(t^-)\). The prescribed branch \(t^+\) is taken and the forbidden branch \(t^-\) is not.

• \(\mathsf{Predicate}(f)\): \(f(\tau, i, \mu) \in \mathbb{B}\), a user-defined open predicate.

10.2.3 Temporal Operators↩︎

AgentLTL supports the six standard LTL operators: globally (\(\mathsf{G}\)), finally (\(\mathsf{F}\)), next (\(\mathsf{X}\)), until (\(\mathsf{U}\)), weak until (\(\mathsf{W}\)), and release (\(\mathsf{R}\)). Let \(\tau^{\ge i}\) denote the suffix of \(\tau\) from position \(i\).

• \(\tau^{\ge i} \models \mathsf{G}(\varphi)\) iff \(\forall j \ge i.\; \tau^{\ge j} \models \varphi\) (vacuously true when \(i \ge n\)).

• \(\tau^{\ge i} \models \mathsf{F}(\varphi)\) iff \(\exists j \ge i.\; \tau^{\ge j} \models \varphi\).

• \(\tau^{\ge i} \models \mathsf{X}(\varphi)\) iff \(i+1 < n \;\wedge\; \tau^{\ge i+1} \models \varphi\). This is the strong next on finite traces (false at trace end), sometimes written \(\mathsf{X}_w\).

• \(\tau^{\ge i} \models \varphi\,\mathsf{U}\,\psi\) iff \(\exists j \ge i.\bigl(\tau^{\ge j} \models \psi \;\wedge\; \forall i \le k < j.\; \tau^{\ge k} \models \varphi\bigr)\).

• \(\tau^{\ge i} \models \varphi\,\mathsf{W}\,\psi\) iff \((\varphi\,\mathsf{U}\,\psi)\) or \(\forall j \ge i.\; \tau^{\ge j} \models \varphi\).

• \(\tau^{\ge i} \models \varphi\,\mathsf{R}\,\psi\) iff \(\forall j \ge i.\bigl(\tau^{\ge j} \models \psi \;\vee\; \exists i \le k < j.\; \tau^{\ge k} \models \varphi\bigr)\).

10.2.4 Data Quantifiers and Open Predicates↩︎

A domain extractor \(D : (\tau, \mu) \to \mathsf{List}\) supports quantification. Evaluation proceeds by computing \(D(\tau,\mu) = \{e_1,\dots,e_k\}\), substituting each \(e_i\) into \(\varphi\), and evaluating all grounded formulas \(\varphi[e_i/x]\). For example, “every number produced is processed” becomes \(\forall x \in D_{\text{numbers}}.\; \mathsf{CalledWith}(\texttt{tool\_b}, \{i:x\})\). When \(D(\tau,\mu) = \emptyset\), the universal \(\forall x \in D.\,\varphi\) is vacuously true and the existential \(\exists x \in D.\,\varphi\) is vacuously false. User-defined open predicates take the form \(f : (\tau, i, \mu) \to \mathbb{B}\).

10.3 Constraint Evaluation Procedure↩︎

10.3.1 Evaluation Algorithm↩︎

Algorithm 3 shows representative cases of the recursive evaluator; the omitted cases (\(\bot, \lor, \mathsf{G}, \mathsf{U}, \mathsf{W}, \mathsf{R}, \exists\)) follow analogously from the semantics above. Quantifiers are expanded eagerly; inner scopes shadow outer bindings.

10.3.2 Worked Example↩︎

For \(\varphi = \mathsf{Called}(\texttt{tool\_a}) \land \mathsf{F}(\mathsf{Called}(\texttt{tool\_d}))\), evaluation (i) checks \(\mathsf{Called}(\texttt{tool\_a})\), (ii) scans suffixes for \(\mathsf{Called}(\texttt{tool\_d})\), and (iii) combines via \(\land\).

10.4 Layered Constraint System (L1–L6)↩︎

The construction algorithm emits constraints in six layers, listed in 5. The layered structure is what 3 refers to throughout, and the compliance scoring of 1 aggregates per-layer pass/fail outcomes under layer weights.

6pt

10.4.0.1 Rationale.

Higher weights prioritize structural correctness; lower weights capture value precision. Changes in the weight values primarily affect value-level penalties; structural violations dominate overall scores.

10.5 Online Enforcement Mechanism↩︎

10.5.1 Prefix Evaluation and Enforceability↩︎

Online enforcement operates on the prefix \(\tau^{\le i} = \langle c_0,\dots,c_i \rangle\). A constraint \(\kappa\) is enforceable if some finite prefix witnesses its violation regardless of how execution continues: \[\exists \tau_{\text{pre}}.\; \forall \tau_{\text{ext}}.\; \tau_{\text{pre}} \cdot \tau_{\text{ext}} \not\models \kappa,\] where \(\cdot\) denotes trace concatenation. Equivalently, \(\kappa\) admits a bad prefix in the sense of runtime verification: once such a prefix has been observed, no continuation can satisfy \(\kappa\), so the violation is decided.

10.5.1.1 Liveness is deferred.

Pure liveness constraints have no bad prefix on finite traces: a formula such as \(\mathsf{F}\,\varphi\) can always be satisfied by an unseen future call, so its violation cannot be witnessed until the trace ends. Such constraints are not enforceable online and are deferred to offline evaluation. Safety constraints (e.g., \(\mathsf{G}\,\neg \varphi\), \(\mathsf{BranchCalled}\)) and bounded constraints (e.g., \(\mathsf{WithinSteps}\) once its window has elapsed) are enforceable.

10.5.2 Runtime Algorithm↩︎

function Enforce(call, tau):
    tau' = tau + call
    for kappa in enforceable_constraints:
        if violated(kappa, tau'):
            return action(severity(kappa))
    return ALLOW

10.5.3 Enforcement Settings and Escalation↩︎

Each constraint carries a severity tag drawn from four levels. Three are active in our experiments; the fourth, HARD_STOP, is defined for completeness but unused in the configurations reported in the main paper.

This design balances strict enforcement of safety-critical constraints with flexibility for recoverable errors.

11 JSON Record Examples↩︎

Listings [lst:metrics-example] and [lst:compliance-output] show the two structured records that the AgentLTL engine operates on, drawn from an actual run at difficulty 1 (seed 42, expected answer 33).

11.0.0.1 Metrics record (\(\mu\)).

The metrics dictionary produced by Agent.run() carries aggregate counters and the flat tool_calls list from which the Trace object is constructed. Each entry records the tool name, arguments, and the JSON string returned by the tool.

{
  "num_steps": 7,
  "num_tool_calls": 6,
  "input_tokens": 13268,
  "output_tokens": 127,
  "total_tokens": 13395,
  "tool_calls": [
    {
      "step": 2,
      "tool_name": "tool_a",
      "arguments": {"seed": 42},
      "tool_result": "{\"numbers\": [8, 2, 46]}"
    },
    {
      "step": 3,
      "tool_name": "tool_b",
      "arguments": {"i": 8, "j": 0},
      "tool_result": "{\"result\": 11}"
    },
    {
      "step": 4,
      "tool_name": "tool_b",
      "arguments": {"i": 2, "j": 0},
      "tool_result": "{\"result\": 11}"
    },
    {
      "step": 5,
      "tool_name": "tool_b",
      "arguments": {"i": 46, "j": 0},
      "tool_result": "{\"result\": 11}"
    },
    {
      "step": 6,
      "tool_name": "tool_d",
      "arguments": {"numbers": [11, 11, 11]},
      "tool_result": "{\"result\": 33}"
    }
  ]
}

11.0.0.2 Compliance output.

verify_trace(\(\mu\),\(G_P\)) returns the score, categorical label, the flat tool-name sequence, and a per-constraint breakdown. Weights follow the per-layer scheme of 5.

{
  "compliance_score": 1.0,
  "compliance_label": "FULL",
  "details": "All constraints satisfied.",
  "tool_sequence": ["tool_a", "tool_b", "tool_b", "tool_b", "tool_d"],
  "constraints": [
    {
      "name": "tool_a_called",
      "layer": "L1",
      "weight": 2.0,
      "passed": true,
      "detail": "\"tool_a\" was called (call #1)."
    },
    {
      "name": "tool_a_before_branches",
      "layer": "L4",
      "weight": 3.0,
      "passed": true,
      "detail": "\"tool_a\" (call #1) before \"tool_d\" (call #5)."
    },
    {
      "name": "branch_call_count",
      "layer": "L5",
      "weight": 3.0,
      "passed": true,
      "detail": "Predicate returned True (3 branch calls, expected >= 3)."
    },
    {
      "name": "tool_b_for_even",
      "layer": "L5",
      "weight": 3.0,
      "passed": true,
      "detail": "\"tool_b\" called 3 time(s); expected >= 3."
    },
    {
      "name": "tool_b_before_tool_d",
      "layer": "L3",
      "weight": 4.0,
      "passed": true,
      "detail": "\"tool_b\" (call #2) before \"tool_d\" (call #5)."
    },
    {
      "name": "tool_d_called",
      "layer": "L1",
      "weight": 2.0,
      "passed": true,
      "detail": "\"tool_d\" was called (call #5)."
    }
  ]
}

12 Benchmark and Data Generation↩︎

This appendix documents the tool vocabulary, templates, difficulty scaling, instance-generation procedure, and dataset statistics of the data discussed in 4.1. It is the underlying data used in the benchmark of 4.2 and the training corpus of 4.3.

12.1 Tool Definitions↩︎

The benchmark uses eight deterministic, stateless tools. All inputs and outputs are integers, and the same input always produces the same output. The names tool_a, tool_b, …are intentionally generic so that compliance reflects procedural reasoning rather than tool-name semantics. 6 lists each tool’s signature, output range, and exact arithmetic definition.

4pt

12.1.0.1 Vocabulary by mode.

The production mode draws from all eight tools. The simplified mode used for training restricts the vocabulary to the four-tool pool \(\{\texttt{tool\_a}, \texttt{tool\_b}, \texttt{tool\_c}, \texttt{tool\_d}\}\). Both settings share the same procedural patterns; they differ only in vocabulary, prompt phrasing, and parameter ranges (12.5).

12.2 Production Benchmark Templates↩︎

The production benchmark comprises 12 templates, grouped into the five structural types summarised in 8. 7 describes each template; tool abbreviations refer to the names in 6.

3pt

12.2.0.1 Example trace.

For loop_termination at \(D_1\) and seed \(42\):

tool_a(i=1) -> 2   [even: +=2 -> 2]
tool_a(i=2) -> 5   [odd:  +=10 -> 12]
... (stop when total >= 10)
expected_answer = 12

12.3 Difficulty Scaling↩︎

Difficulty levels \(D_1\)–\(D_5\) control trace length by varying a single structural parameter per template, never by altering the procedure. The agent never sees the difficulty index — only the resulting numbers embedded in the prompt. 9 lists the scaling parameter per template. For tool_condition_branching, the scaling parameter is the difficulty index \(d\) itself, which is passed as the second argument to tool_iterations and thereby sets the loop count.

4pt

The scaling axes group naturally: loop-driven templates (loop_termination, loop+expansion) grow their accumulation threshold; branch-driven templates (branch_selection) grow the number of binary decisions; fan-out templates (fan_*, forall_*, exists_*, forall_exists_combined) grow list length via num_items (\(= d{+}2\) for tool_a_list); nested-loop templates grow the outer count \(N\); tool_condition_branching embeds difficulty inside tool_iterations; dynamic_expansion grows BFS depth; and fan_out+loop grows both list length and inner repetition.

12.3.0.1 Resulting trace lengths.

Raw trace lengths from the parameter schedule above can in principle reach \(200{+}\) calls at \(D_5\) for loop-driven templates. To keep the benchmark tractable and to respect the per-run tool-call budget of \(10d + 10\), we filter instances to a maximum of \(50\) tool calls; the longest retained traces are capped accordingly. Approximate post-filter calls per trace are \(3\)–\(10\) at \(D_1\), \(5\)–\(20\) at \(D_2\), \(10\)–\(30\) at \(D_3\), \(20\)–\(45\) at \(D_4\), and up to \(50\) at \(D_5\).

12.4 Instance Generation Procedure↩︎

Each benchmark run is uniquely identified by the triplet \((\text{template}, \text{seed}, \text{difficulty})\). Given this triplet, the generator (i) looks up the parameter dict for the template at that difficulty; (ii) inlines all concrete numbers into a natural-language procedure to produce the prompt; (iii) simulates the procedure deterministically on the arithmetic tools to obtain expected_answer, the ordered tool_call_log of \(\{\text{name}, \text{args}, \text{result}\}\) triples, total call count, branching statistics, and iteration counts; (iv) instantiates fresh tool objects per run; and (v) compiles the layered LTL constraint set (L1–L6, 10.4) from the gold trace. The agent sees only the numbers, never the difficulty index. The structural layers L3, L4, and L5 together carry approximately \(73\%\) of the total constraint weight; L6 is downweighted to prevent a single early arithmetic error from cascading into a near-zero compliance score (cf.4.1).

12.4.0.1 Determinism from seed.

The seed controls the initial BFS node, a derived parameter \(j = (\text{seed} \bmod 10) + 1\), the list contents returned by tool_a_list, and loop counts via tool_iterations. All arithmetic is pure — given the same triplet, the prompt, gold trace, answer, and constraints are always identical.

12.4.0.2 Instance contents.

Each generated instance carries the fields listed in 10.

12.5 Production vs.Simplified Mode↩︎

The two settings share procedural primitives (loops, branches, fan-out, fan-in, conditional re-processing) but differ in vocabulary, prompt length, and parameter ranges. 11 summarises the differences.

4pt

12.5.0.1 Why two settings.

The \(3\)–\(8\) call window of simplified mode provides a tight, tractable supervision signal for GRPO; training on very long production traces (\(D_4\)/\(D_5\)) would require many more samples and GPU hours. Simplified mode preserves the structural patterns that the LTL constraints test, but at a scale where the reward signal is dense and informative. The procedure-level identity between modes allows patterns trained in simplified mode to be evaluated under the longer, richer production prompts (cross-mode transfer).

12.5.0.2 Difficulty in training data.

In the simplified-mode training corpus, difficulty is derived post hoc from tool-call count: \(\leq 5 \to D_1\), \(\leq 15 \to D_2\), \(\leq 30 \to D_3\), \(\leq 60 \to D_4\), \(> 60 \to D_5\). Almost all training instances are \(D_1\)–\(D_2\).

13 Training Data and Patterns↩︎

13.1 Simplified Training Templates↩︎

The training corpus is built from \(15\) simplified templates over the four-tool simplified-mode pool \(\{\texttt{a}, \texttt{b}, \texttt{c}, \texttt{d}\}\). Trace lengths range from \(3\) to \(7\) calls; with augmentation (13.3) the cap is \(8\) calls. 12 enumerates the 15 templates with their high-level structure. We define 17 simplified-mode templates in total; the remaining \(2\) are reserved as the unseen-pattern held-out split (see Held-out patterns below).

Four of the 15 training templates (those marked a/c) admit a transform variant: the seed transform can be performed either by tool_a or by tool_c, yielding two interchangeable instantiations of the same procedural skeleton. Tool interchangeability is restricted to the tool_a/tool_c axis; tool_value (used by dynamic_expansion) is intentionally excluded.

13.1.0.1 Held-out patterns.

In addition to the 15 training templates, two further simplified-mode patterns are reserved exclusively for the unseen-pattern evaluation split: simplified versions of loop_termination and branch_selection restricted to the 3–6 call budget. These two held-out simplified patterns happen to use only the tool_a/tool_b/tool_c subset of the four-tool simplified-mode pool; they are excluded from the training corpus.

13.2 Pattern Coverage Mapping↩︎

To evaluate generalisation, we classify each of the 12 benchmark templates by its relationship to the training set. 13 lists, for each training template, both its direct-simplification target (the benchmark template of which it is a length- and arity-reduced version) and its motif-overlap targets (benchmark templates that share structural motifs without being direct simplifications).

This induces a three-way partition of the benchmark suite used in our generalisation analysis:

• Direct-simplification (4 templates): fan_out_fan_in, forall_processing, exists_selection, nested_loops. Each has a training template that is a length-reduced version of it.

• Motif-overlap (7 templates): loop_termination, branch_selection, tool_condition_branching, forall_exists_combined, nested_loops+branching, fan_out+loop, loop+expansion. No training template is a direct simplification, but motifs (branching, fan-out, nested loops) are represented in training.

• No-coverage (1 template): dynamic_expansion. This template depends on graph-expansion motifs and on tools (tool_expand, tool_value) absent from all 15 training templates.

This partition licenses the generalisation claims of 4.3: direct-simplification measures in-distribution transfer from simplified to production prompts, motif-overlap measures compositional transfer to recombined motifs, and no-coverage measures transfer to a benchmark family with no shared tools or motifs.

13.3 Training Data Construction Pipeline↩︎

The final training set of \(300\) examples is constructed in three stages: exhaustive enumeration of trace variants, augmentation, and balanced subsampling.

13.3.0.1 Pool construction.

We first enumerate every pattern variant, each is composed of a template and a transform-choice. Of the 15 templates, \(11\) have a single fixed transform and \(4\) admit two transform variants (cf. 13.1), giving \(11 + 4 \times 2 = 19\) pattern-variant slots. For each slot we generate \(30\) core instances by varying parameter seeds, yielding a pool of \(19 \times 30 = 570\) unique cores before augmentation.

13.3.0.2 Trace augmentation.

To discourage memorization of fixed call sequences, every core trace is expanded into up to four augmentation variants, tagged in round-robin order to give exact \(1/4\) class balance per pattern:

The prompt is modified accordingly: prefix instances begin with “Call tool_a\((\text{pre\_seed})\) first — its result is an addend you will include in your final answer…”, and suffix instances append the mirror sentence. To stay within the simplified-mode \(8\)-call hard cap, traces with \(\geq 7\) core calls use only \(\texttt{none} \to \texttt{prefix}\), keeping the total \(\leq 8\) calls.

13.3.0.3 Effect on constraints.

The extra tool_a step is functionally independent of the main computation but changes the constraint profile: L3 (sequence ordering) includes the extra tool_a; L4 (pair/instance ordering) gains an additional ordering relation; L5 (call counts) sees the tool_a count \(1\)–\(2\) higher; L2 and L6 (argument constraints) cover the new step. An augmented trace looks structurally different, it has different first/last tool and a different total call, but requires the same procedural reasoning.

13.3.0.4 Balanced subsampling.

From the augmented pool we draw \(300\) examples under a per-template floor/ceiling constraint (\(\text{min\_per\_pattern} = 8\), \(\text{max\_per\_pattern} = 24\)). Quotas are computed by weighted largest-remainder allocation. Within each template’s quota, the sampler equalises across within-pattern buckets (transform variant, augmentation type) so that no axis is over-represented. With the default weights this gives \(15 \times 8 = 120\) floor allocations plus \(180\) extra slots distributed evenly (\(12\) per template), for a final target of \(20\) examples per template.

13.4 Tool Name Permutations (Diverse-Tool Split)↩︎

The diverse-tool evaluation split substitutes domain-specific aliases for the generic tool names at test time. The underlying arithmetic functions are unchanged and only the tool names and argument names change. 14 gives the pool size and an illustrative alias for each base tool. Domains covered include finance, healthcare, DevOps, data science, logistics, IoT, genomics, and legal.

6pt

A fan_out_fan_in instance might therefore present as enumerate_patients(intake_seed) \(\to\) correlate_signals(channel_a, channel_b) \(\to\) normalize_reading(reading) \(\to\) accumulate_readings(readings). This split tests whether the model has learned procedure structure versus surface-level pattern matching on tool names. The LTL constraints are restated in terms of the aliased tool names, so the compliance test is invariant under renaming.

14 Training Details (GRPO)↩︎

This appendix provides additional implementation details for the GRPO finetuning setup described in 4.3. We specify the full reward definition, the trace-distance metric used as a dense shaping reward, and the main training hyperparameters.

14.1 Reward Definition↩︎

For each sampled trajectory, the total reward is a weighted combination of three terms: compliance with the AgentLTL specification, answer correctness, and distance to the gold tool trace. The reward is defined as \[R = w_C C + w_A Acc + w_D R_{\mathrm{dist}},\] where \(C\) is the AgentLTL compliance reward, \(A\) is the shaped answer-correctness reward, and \(R_{\mathrm{dist}}\) is a dense trace-distance reward.

In the training run, the weights are \[(w_C, w_A, w_D) = \left( \alpha, \frac{1-\alpha}{2}, \frac{1-\alpha}{2} \right), \qquad \alpha = 0.5.\] Thus, the reward used in the main experiments is \[R = 0.5\,C + 0.25\,Acc + 0.25\,R_{\mathrm{dist}}.\]

The answer-correctness term is shaped to preserve a weak learning signal even when the final answer is formatted correctly but numerically incorrect. Specifically, \[\mathrm{Acc} = \begin{cases} 1.0 & \text{correct format and value},\\ 0.1 & \text{correct format, wrong value},\\ 0.0 & \text{invalid format}. \end{cases}\]

This shaping makes answer correctness an outcome anchor while avoiding an entirely sparse signal for formatted but incorrect completions.

14.2 Trace Distance Metric↩︎

The dense trace reward is based on the distance between the predicted tool trace and the gold tool trace. Let the gold trace be \[G = (g_1, \dots, g_n)\] and the predicted trace be \[P = (p_1, \dots, p_m).\] We compute a weighted Levenshtein distance \(d(G,P)\) using the dynamic program \[D(0,j) = j, \qquad D(i,0) = i,\] and \[\begin{align} D(i,j) = \min \big( & D(i-1,j) + 1, \\ & D(i,j-1) + 1, \\ & D(i-1,j-1) + s(g_i,p_j) \big). \end{align}\] where \(D(i,j)\) is the minimum edit cost between the first \(i\) elements of the gold trace and the first \(j\) elements of the predicted trace. The substitution cost \(s(g_i,p_j)\) is \[s(g_i,p_j) = \begin{cases} 0 & \text{exact match},\\ 0.5 & \text{same tool, arguments differ},\\ 1.0 & \text{tool name differs}. \end{cases}\] Insertions and deletions each have cost \(1.0\). The final distance is \[d(G,P) = D(n,m).\]

The trace-distance reward is then \[R_{\mathrm{dist}} = \exp(-d(G,P)).\]

Equivalently, the edit costs are:

• tool mismatch: \(1.0\);

• argument mismatch for the same tool: \(0.5\);

• insertion or deletion: \(1.0\).

As an example, consider the gold trace \[G = [ (\texttt{tool\_a}, \{x:1\}), (\texttt{tool\_b}, \{y:2\}) ]\] and the predicted trace \[P = \left[ \begin{align} &(\texttt{tool\_a}, \{x:9\}),\\ &(\texttt{tool\_c}, \{z:0\}),\\ &(\texttt{tool\_b}, \{y:2\}) \end{align} \right].\] The optimal alignment incurs an argument mismatch on tool_a, with cost \(0.5\), an insertion of tool_c, with cost \(1.0\), and an exact match on tool_b, with cost \(0\). Therefore, \[d(G,P) = 0.5 + 1.0 + 0 = 1.5,\] and \[R_{\mathrm{dist}} = \exp(-1.5) \approx 0.223.\]

14.3 Training Setup↩︎

The GRPO finetuning run uses Qwen/Qwen3-4B-Instruct-2507 as the base model. We finetune using LoRA adapters applied to the q_proj and v_proj modules. The LoRA rank is \[r = 8,\] with LoRA scaling parameter \[\alpha = 16\] and dropout \[0.05.\]

For each prompt, the trainer samples \[N = 16\] rollouts. Training uses a round-robin-no-repeat curriculum across pattern types. In this mode, the curriculum expands examples over epochs without repeating the same pattern consecutively, and dataset shuffling is disabled.

The pipeline uses fp32 precision. The pipeline KL coefficient is \(\beta = 10^{-3}\).

The released adapter metadata is consistent with the training configuration: LoRA rank \(r=8\), LoRA scaling parameter \(\alpha=16\), dropout \(0.05\), and target modules q_proj and v_proj.

15 Benchmark Results (Extended)↩︎

This appendix presents the full per-template, per-layer, and per-setting breakdowns of the benchmark results summarised in 5.1. Layer definitions (L1 branch, L2 argument extraction, L3 global sequence, L4 pair-order, L5 call-count, L6 exact args) follow 3.3, and the three enforcement settings (baseline, block-and-warn, soft-block) follow 4.2.

15.1 Per-Template Results↩︎

Figure 7 reports compliance and accuracy for each (model, template) cell under all three enforcement settings. The figure shows a \(2 \times 3\) grid of heatmaps: rows correspond to compliance score (top) and accuracy (bottom), and columns correspond to the baseline, soft-block, and block-and-warn settings. Within each heatmap, columns index models and rows index templates; cells are colour-coded green (high) to red (low).

15.1.0.1 Key observations.

Table 15 summarises the dominant patterns visible in Figure 7.

Compliance and accuracy diverge most sharply on composite templates (, , ) where the model satisfies per-call constraint checks but still emits incorrect call sequences. This is consistent with the L3/L4 ordering failures reported in 5.1.0.2.

15.2 Per-Layer Breakdowns↩︎

Figure 8 expands Table 4 of 5.1.0.2 into a per-setting view. The heatmap has 21 rows (7 models \(\times\) 3 settings) and 8 columns: the two summary metrics (Compliance, Accuracy) followed by per-layer pass rates (L1–L6). Dashed navy lines separate model groups, and a vertical dashed line separates the two summary columns from the layer columns. Each cell shows the mean pass rate of the constraint checks evaluated at that layer, conditional on the model having reached a callable state at that point in the run; this is the loss-contribution decomposition referenced in 5.1.0.2, where a model’s accuracy can be reconstructed as the product of pass rates across active layers.

15.2.0.1 Full numeric values.

Table 16 reports the underlying numbers for Figure 8. The best (model, setting) row by accuracy (Qwen3.5-397B-A17B baseline) and the best single-model compliance under enforcement (Gemma-4-31B block-and-warn) are highlighted in bold.

4pt

15.2.0.2 Layer-level findings.

Three observations stand out from Table 16 and complement the L3/L4 analysis in 5.1.0.2.

• L3 (global sequence) is the most consistently weak layer across all models and settings, in line with 5.1.0.2. Even the strongest models exhibit meaningful L3 gaps under baseline (Qwen3.5-397B-A17B: 0.622; Kimi-K2.6: 0.450), and DeepSeek-V4-Pro has the second-lowest baseline L3 of any model (0.153). L4 (pair-order) tracks L3 closely throughout, with L4 typically 5–20 pp above L3 (e.g.for DeepSeek-V4-Pro baseline, L3 \(=0.153\) vs.L4 \(=0.312\)), consistent with the same trace failures violating both global and pairwise ordering.

• L1 (branch) is near-perfect for strong models under baseline but collapses under soft-block for DeepSeek-V4-Flash (0.212) and Gemma-4-26B-A4B (0.424), indicating that soft-block stops disrupt branch-selection logic for weaker models before they can recover.

• Block-and-warn consistently lifts DeepSeek-V4-Flash across every layer relative to baseline (L1 +24 pp, L2 +14 pp, L3 +64 pp, L4 +61 pp), making it the setting most beneficial for weaker models. The largest gains are precisely on L3 and L4 which are the ordering layers that account for most of the weighted loss in 5.1.0.2.

15.3 Enforcement Statistics↩︎

Figure 9 reports three views of enforcement behaviour under block-and-warn: enforcement event counts per layer (stacked by model), listen-versus-insist rates, and tool-call deltas versus baseline.

15.3.0.1 (a) Enforcement events per layer.

Table 17 reports the total number of enforcement events fired at each layer, together with the number of resolved, insisted, and listened resolutions, and the resulting insist rate. An enforcement event is resolved as listened when the model abandons the violating call after a warning, and as insisted when it repeats the same call (modulo argument-equivalence) on the next turn.

Gemma-4-26B-A4B dominates L2 and L3 enforcement events (47K and 49K respectively), driven by frequent argument-extraction and ordering violations combined with a high tool-call count per run.

15.3.0.2 (b) Listen versus insist rates.

Overall, models comply with constraint warnings in the vast majority of episodes. L2 has the highest insist rate at 4.08%, meaning that models occasionally retry the same argument-extraction call after a warning. L3 and L5 insist rates are below 1.1%, indicating that models largely accept sequencing and count constraints. L1’s insist rate is essentially zero (0.16%): once warned about a wrong branch, models almost never repeat the same routing decision.

15.3.0.3 (c) Tool-call deltas versus baseline.

Block-and-warn typically adds tool calls for most models (DeepSeek-V4-Flash: \(\sim\) \(+6\) extra calls; Gemma-4-26B-A4B: \(\sim\) \(+10\)) because warning-repair cycles introduce additional retries after each warning. Soft-block reduces or barely changes tool-call counts for most models, since stopped runs terminate early and therefore contribute fewer total calls. The exception is Gemma-4-31B under soft-block, which shows a slight positive delta. This model recovers well from soft-block stops and continues executing.

15.4 Additional Analyses↩︎

15.4.1 Difficulty Scaling Curves↩︎

Figure 6 plots accuracy (top row) and compliance (bottom row) against difficulty levels D1–D5 for each enforcement setting. Each panel shows one curve per model.

1. Accuracy degrades monotonically with difficulty for most models under baseline and block-and-warn. DeepSeek-V4-Flash baseline drops from 62.5% at D1 to 56.9% at D5 (mild decline); Gemma-4-26B-A4B baseline drops from 38.9% at D1 to 25.0% at D5 (\(-13\) pp over five levels).

2. Block-and-warn amplifies difficulty sensitivity for weaker models. DeepSeek-V4-Flash under block-and-warn falls from 84.7% at D1 to 70.8% at D5 because harder instances trigger more warning cycles.

3. Soft-block dramatically suppresses accuracy at all difficulty levels. DeepSeek-V4-Flash falls to the 25–38% range under soft-block versus 50–62% under baseline, and the degradation is roughly flat across difficulty levels because stop-on-violation terminates runs regardless of difficulty.

4. Compliance is far less sensitive to difficulty than accuracy. Across all models and settings, compliance variance across D1–D5 is typically under 5 pp, consistent with compliance measuring constraint adherence per call rather than end-to-end task success.

5. Qwen3.5-397B-A17B is near-flat in accuracy (\(\sim\)​98.6%) across all difficulty levels under baseline, confirming that it is largely saturated on the benchmark.

15.4.2 Compliance vs.Correctness Correlation↩︎

We also examined the per-cell relationship between compliance and accuracy. For each enforcement setting, we computed the Pearson correlation between compliance and accuracy taken over all (model, template) cells (\(N = 84\) per setting, from \(7~\text{models} \times 12~\text{templates}\)).

15.4.2.1 Interpretations.

The moderate baseline correlation (\(r \approx 0.60\)) confirms that compliance and accuracy are correlated but not equivalent: models can satisfy constraint checks without solving the task, especially on composite templates. The higher correlation under block-and-warn (\(r \approx 0.73\)) reflects that enforcement pushes compliance and accuracy in the same direction; when the model recovers from a warning, it also tends to complete the task correctly. Cells in the high-compliance / low-accuracy region correspond predominantly to Qwen3-Next-80B-A3B-Instruct and Gemma-4-26B-A4B on complex templates, where the model follows call-by-call constraints but fails to produce the correct final answer, the same pattern reported for Qwen3-Next-80B in 5.1.0.2. Cells in the low-compliance / high-accuracy region are rare and correspond mostly to DeepSeek-V4-Pro, consistent with the main-text observation that this model produces correct answers from non-compliant traces. All settings also show a dense cluster near \((1.0, 1.0)\) populated by Qwen3.5-397B-A17B and Kimi-K2.6 on straightforward templates.

16 Finetuning Results (Extended)↩︎

This appendix complements 5.2 with full-resolution training curves and a per-template view of where the finetuned model gains and where it does not. Throughout, \(\bar{C}\) denotes empirical compliance averaged over a split, \(\tau\) a model-produced trace, and \(\tau^{*}\) the gold trace used for the distance-based reward term \(R_{\text{dist}}(\tau, \tau^{*})\) (4.3).

16.1 Training curves↩︎

5 shows the three reward components and the weighted total tracked during GRPO training, evaluated on the held-out validation set every checkpoint over \(4{,}800\) generations (\(16\) rollouts \(\times\) \(300\) prompts). 4 shows the same components on the training rollouts. The training-side and evaluation-side trajectories move in parallel, with no late-training divergence indicative of overfitting; the gap between them narrows over training and stabilises within the first half of the run.

All three reward components improve jointly. AgentLTL compliance \(\bar{C}\) rises from \(0.511\) to \(0.770\), answer correctness from \(0.296\) to \(0.728\), and gold-trace distance reward \(R_{\text{dist}}\) from \(0.301\) to \(0.782\). Joint movement rules out the failure mode of reward gaming via structurally-valid-but-wrong traces: a model maximising \(\bar{C}\) alone could trivially produce empty or near-empty traces, but the correctness and trace-distance components would not co-move.

16.2 Per-template gains↩︎

19 reports per-template accuracy and \(\bar{C}\) for every benchmark template, aggregated over the four held-out validation splits (unaugmented, augmented, unseen-pattern, and diverse-tool; \(n{=}261\) in total) and ordered by accuracy gain. The distribution of gains has three regions worth distinguishing.

16.2.0.1 Strong gains (top thirteen templates).

The thirteen templates from through all clear \(+25\)pp in accuracy and show \(\bar{C}\) gains in the same direction. The largest movers are (\(0.0 \to 100.0\)), (\(8.3 \to 100.0\)), and (\(0.0 \to 78.6\)). Compliance gains in this region are uniformly positive (\(+0.08\) to \(+0.61\)), with the largest \(\Delta\bar{C}\) attached to the templates that move from \(0\%\) accuracy: when the base model produces malformed traces, finetuning improves both axes simultaneously.

16.2.0.2 Modest gains.

Two templates show only marginal accuracy improvement: (\(+7.1\)pp) and (\(+5.6\)pp). These are also the only templates other than on which \(\bar{C}\) drops after finetuning (\(-0.015\) and \(-0.202\) respectively). The common factor is high constraint-formula depth combined with long gold traces (six or more calls); the model attempts the structure but violates one of the inner constraints, and the larger compliance drop on reflects a structural attempt that is further from the gold pattern than the base model’s shorter output.

16.2.0.3 Regression: .

The one substantial regression is , which drops from \(85.7\%\) to \(14.3\%\) (\(-71.4\)pp), with \(\bar{C}\) also falling from \(0.956\) to \(0.560\). The base model’s high accuracy on this template is, on inspection, a near-vacuous pass: the base produces very short traces that happen to satisfy the (relatively permissive) outer constraint while not actually executing the nested loop. After finetuning the model attempts the full nested-loop structure and exposes itself to the inner-loop termination constraints, on which it then fails. The same pattern, deeply nested control flow producing the model’s only consistent failure mode, is noted in the main-text discussion of on the full benchmark, of which is the training-side simplified counterpart.

16.2.0.4 unchanged.

is the one template where accuracy is flat (\(14.3\% \to 14.3\%\)). Both \(\bar{C}\) (\(+0.013\)) and \(R_{\text{dist}}\) move in the expected direction, so the model is learning structure on this template; the flat accuracy appears to be a small-\(n\) artefact (\(n{=}7\)) rather than a genuine absence of improvement.

5pt

17 Trace Grounding Study↩︎

This appendix provides implementation details, examples, and full results for the trace-grounding analysis introduced in Sections 4.4 and 5.3. We describe the two prompt variants used, the repository corpus, the implementation of the grounding predicate \(\kappa_{\mathrm{ground}}\), three worked example runs, the effect of the strict-grounding prompt, popularity stratification, and a comparison with trace-aware and trace-blind LLM judges.

17.0.0.1 Notation bridge.

Section 5.3 reports the joint distribution of correctness and grounding using four categories: CG (correct, grounded), CU (correct, ungrounded), IG (incorrect, grounded), and IU (incorrect, ungrounded). The appendix reuses these labels throughout. Where useful for comparison to an LLM judge that itself produces a binary grounded/ungrounded verdict (§17.7), we additionally report the confusion-matrix convention with \(\kappa_{\mathrm{ground}}\)-ungrounded as the positive class: TP \(=\) IU, FP \(=\) CU, FN \(=\) IG, TN \(=\) CG. Precision is \(\mathrm{TP}/(\mathrm{TP}+\mathrm{FP})\) and recall is \(\mathrm{TP}/(\mathrm{TP}+\mathrm{FN})\), both with respect to identifying incorrect answers via ungroundedness.

17.1 Prompt Details↩︎

Both prompt variants share an identical system preamble describing the available tools (list_directory, read_file) and a user turn of the form:

Repository: {repo_id}
TASK
----
{question_text}
Investigate the source code using the available tools and provide a thorough answer grounded in what you find. Cite specific files, classes, functions, and code patterns you discover.

The two variants differ only in the rules block.

17.1.0.1 Default prompt.

Four soft instructions:

1. Always explore the directory structure before reading files.

2. Read the actual source code to answer questions — do not rely on memory.

3. Cite specific files, classes, functions, and code you find.

4. If you are unsure about something, look it up in the code first.

17.1.0.2 Strict grounding prompt.

Replaces the soft instructions with three hard constraints:

1. Only state facts about files, classes, functions, or code directly read via read_file in this session. Do not use prior knowledge about this repository.

2. Every file path, class name, function name, or signature mentioned in the final answer must be one seen in a read_file result during this session. Names seen only in list_directory output do not qualify unless the file was also opened.

3. If after reasonable exploration the answer cannot be found in the source read, the final answer must be exactly "I don’t know - not found in the source I read." Refusal is a valid and preferred answer when grounding is missing.

17.2 Repository Dataset↩︎

The corpus consists of 16 Python open-source repositories, sampled across GitHub-star popularity deciles to span the spectrum of likely LLM pretraining representation. Each repository is pinned to a specific commit or tag at corpus-construction time to guarantee reproducibility. Each repository is paired with 10 authored questions, yielding 160 (repository, question) pairs. Questions follow a uniform template:

In the {repo} repository, where is the {symbol_name} defined? Provide the exact file path.

Ground truth is a human-authored (repo, file path, symbol name) triple verified against the pinned commit. Answer correctness is decided by case-insensitive substring match of all ground-truth entities against the agent’s final answer.

17.2.0.1 Repository list.

Table 20 lists all repositories with the pinned version, star count at sampling time, and assigned popularity bucket.

4pt

17.2.0.2 Popularity buckets.

The 16 repositories are partitioned into three buckets by decile: high (deciles 8–10, 5 repos: canonical libraries heavily represented in pretraining corpora), mid (deciles 5–7, 3 repos: established but less ubiquitous, likely partially memorised), and low (deciles 1–4, 8 repos: niche or recently-released projects unlikely to be memorised). The high bucket is intentionally smaller because a few canonical repositories dominate the top of the star distribution; a balanced design would over-sample them. The low bucket deliberately captures more of the diversity in the tail.

17.3 Grounding Predicate Implementation↩︎

The grounding predicate \(\kappa_{\mathrm{ground}}\) is deterministic: given the same trace it always returns the same Boolean verdict, and no LLM call or human annotation is required. It is satisfied if and only if every referential entity named in the agent’s final answer (the \(\mathrm{out}(a)\) side of the predicate) was observed in at least one read_file result during the trace (the \(\mathrm{ent}(\tau)\) side).

17.3.0.1 Entity extraction from the answer (\(\mathrm{out}(a)\)).

Three typed entity classes are extracted from the free-form answer text using regex-only patterns (no AST parsing of natural language):

• file_path — repository-relative paths ending in a known source extension (.py, .c, .h, .js, .ts, …).

• function_signature — patterns of the form ClassName.method( or bare function_name(.

• identifier — CamelCase tokens of length \(\geq 3\) and snake_case tokens of length \(\geq 3\), minus a builtin blocklist of approximately 60 entries (Python keywords, standard-library module names, common exception classes).

The blocklist suppresses spurious false positives from prose mentions of tokens such as import, return, os, json, or re that do not constitute code-level claims.

17.3.0.2 Seen-entity set from the trace (\(\mathrm{ent}(\tau)\)).

For each read_file call in the trace, the tool result (a JSON string) is parsed to recover the content field — the raw source text actually returned to the agent. From all such chunks the seen set is built in two steps:

1. File paths: every key in the read-file result dictionary (i.e., every path the agent explicitly requested and received) is added as a grounded file path.

2. Function signatures and identifiers: AST extraction is applied to each chunk to recover named symbols actually defined in the read source. We use Python’s ast.parse for .py files and libclang for C/C++ headers, with a regex fallback when libclang is unavailable.

An answer entity is grounded if it matches (case-insensitive prefix for identifiers, exact for file paths) some member of the seen set of the same type. The predicate is satisfied when every answer entity is grounded.

17.3.0.3 Edge cases.

Several non-obvious trace patterns recur in practice. Their treatment is summarised in Table 21.