PaperlayerView exact revision on arXiv

Source-linked AI summary

ToolGate: Contract-Grounded and Verified Tool Execution for LLMs

Yanming Liu, Xinyue Peng, Jiannan Cao, Xinyi Wang, Songhang Deng, Jintao Chen, Jianwei Yin, Xuhong Zhang

arXiv:2601.04688v1cs.CLcs.AIcs.FL

TL;DR

LLM tool calling lacks formal guarantees for safe invocation and trustworthy result commitment. ToolGate addresses this with typed symbolic state and Hoare-style contracts, and reports stronger reliability and robustness while maintaining competitive multi-step reasoning performance.

  • Problem

    Existing LLM tool-calling frameworks rely on natural-language reasoning without formal guarantees that invocation preconditions or result postconditions are satisfied.

  • Method

    ToolGate maintains a typed symbolic state and uses Hoare-style preconditions and postconditions to gate calls and verify results before state updates.

  • Results

    ToolGate achieves the best or near-best performance across models and benchmarks, including 3−7% improvements over ToolChain* in MCP-Universe Location Navigation and Repository Management.

  • Takeaways & Limitations

    ToolGate supports more reliable, stable, and debuggable tool-augmented reasoning by restricting state evolution to verified executions.

  • Takeaways & Limitations

    The evaluation is mainly limited to text-based and structured-data interactions in largely static environments, with limited qualitative assessment.

Abstract

from arXiv · show

Large Language Models (LLMs) augmented with external tools have demonstrated remarkable capabilities in complex reasoning tasks. However, existing frameworks rely heavily on natural language reasoning to determine when tools can be invoked and whether their results should be committed, lacking formal guarantees for logical safety and verifiability. We present \textbf{ToolGate}, a forward execution framework that provides logical safety guarantees and verifiable state evolution for LLM tool calling. ToolGate maintains an explicit symbolic state space as a typed key-value mapping representing trusted world information throughout the reasoning process. Each tool is formalized as a Hoare-style contract consisting of a precondition and a postcondition, where the precondition gates tool invocation by checking whether the current state satisfies the required conditions, and the postcondition determines whether the tool's result can be committed to update the state through runtime verification. Our approach guarantees that the symbolic state evolves only through verified tool executions, preventing invalid or hallucinated results from corrupting the world representation. Experimental validation demonstrates that ToolGate significantly improves the reliability and verifiability of tool-augmented LLM systems while maintaining competitive performance on complex multi-step reasoning tasks. This work establishes a foundation for building more trustworthy and debuggable AI systems that integrate language models with external tools.

1 Introduction

ToolGate addresses the lack of formal guarantees in LLM tool calling by constraining invocation and validating results through explicit symbolic state and Hoare-style contracts. The framework is designed to improve reliability and debuggability while retaining competitive performance on complex reasoning tasks.

  • Motivation: Existing tool-calling frameworks rely on natural-language reasoning to decide when tools are invoked and whether results are trusted.This creates challenges for logical safety and verifiability.
  • Motivation: Black-box tool execution can permit insufficient parameters, invalid results, and inconsistent world representations caused by erroneous outputs.The missing checks concern both invocation preconditions and result postconditions.
  • Framework: ToolGate maintains a typed key-value symbolic state representing trusted world information throughout reasoning.The state provides an explicit basis for checking tool-related conditions.
  • Framework: Hoare-style contracts gate invocation with preconditions and determine result commitment with postconditions.This formalizes tool calling and state updates as verifiable operations.
  • Contribution: Contract-based verification improves reliability and debuggability while maintaining competitive performance on complex multi-step reasoning tasks.This is the paper’s stated overall experimental conclusion.

2 Related Work

Related work establishes tool use as a way to extend LLM reasoning and evaluates capabilities through benchmarks, while Hoare logic supplies formal precondition-postcondition reasoning for correctness. ToolGate combines these directions for constrained tool calling.

  • LLM Tool Use: External tools extend LLMs beyond text generation through structured function calls and reasoning-acting interactions.Prior systems support retrieval, computation, and action through tools.
  • Evaluation: Tool-use benchmarks evaluate capabilities including API selection, parameter generation, and generalization.These benchmarks measure multiple dimensions of tool usage rather than a single execution outcome.
  • Formal Verification: Hoare logic reasons about program correctness using preconditions and postconditions.Formal verification has also been applied to constrain provable behaviors of neural systems.
  • ToolGate: ToolGate’s overview frames tool calling as constrained logical reasoning while continuously maintaining a trusted state S.The framework uses this state to verify conditions for tool invocation.

3 Methodology

ToolGate combines a typed symbolic world state, Hoare-style contracts, probabilistic tool selection, and runtime verification. Tools are filtered by logical admissibility, and only accepted outputs update the trusted state and subsequent reasoning.

  • Symbolic State: ToolGate constructs a typed symbolic state space to ground tool execution in a verifiable world model.The trusted state records structured information rather than relying only on unstructured natural-language memory.
  • Symbolic State: Each state element records a key, value, and associated type, while predicates express existence, type consistency, and semantic invariants.State satisfaction is represented as S |= φ.
  • Tool Contracts: A tool’s precondition determines whether it is legally callable, whereas its postcondition checks output validity and state-update consistency.The postcondition covers structural validity, typing correctness, and semantic consistency.
  • Tool Selection: Tool-use decisions are modeled probabilistically from the current query, history, symbolic state, and reasoning trajectory.The generated tool-call marker determines entry into the tool execution phase.
  • Tool Selection: The system forms tool requirements from the query, dialogue history, symbolic state, and reasoning trajectory, then retrieves and reranks candidate tools.Embedding-based retrieval narrows the tool space before reranking.
  • Contract Filtering: Candidate tools whose preconditions fail are eliminated, leaving a logically valid execution policy.The filtering condition requires the current state to satisfy the selected tool’s weakest precondition.
  • Runtime Verification: Runtime verification accepts a tool result only when its postcondition is satisfied before the result can affect global state.Rejected outputs are discarded, preventing propagation and creating a debugging breakpoint.
  • Trajectory Constraints: Trajectory-level constraints exclude reasoning paths that violate any tool precondition or postcondition.The remaining trajectories provide formal justification for state transitions and tool execution.

4 Experimental Setup

The evaluation uses ToolBench and MCP-Universe to assess tool invocation, planning, success, and execution stability across diverse tool environments. It compares ToolGate with representative planning baselines on proprietary and open-source language models.

  • Datasets: ToolBench contains more than 16,000 APIs organized into structured categories and assesses local invocation ability and global planning robustness.The dataset covers a wide range of functional capabilities.
  • Datasets: MCP-Universe represents realistic multi-tool environments spanning retrieval, automation, data processing, system operations, and task execution.Its tools are drawn from real-world systems and documented specifications.
  • Metrics: ToolBench evaluation reports Pass Rate for successfully completed tasks and Win Rate against Qwen-3 235B-ReACT judged by solution quality.Pass Rate measures overall task-solving capability, while Win Rate compares plans and results.
  • Metrics: MCP-Universe evaluation uses Success Rate and execution stability for tasks arising from real-world complex systems.Many tasks involve relatively few tool-invocation steps.
  • Results Presentation: Table 1 reports Pass Rate and Win Rate for ToolBench G1/G2/G3 and Success Rate for three MCP-Universe subtasks.The table provides the main benchmark results for both datasets.
  • Baselines: The comparison includes ReACT, DFSDT, LATS, ToolChain*, and Tool-Planner.These are representative tool-use and planning baselines.
  • Models: Experiments span Gemini 3 Pro, GPT-5.2, DeepSeek V3.2, and Qwen3-235B-A22B-Instruct-2507, covering proprietary and open-source models.Embedding and reranking use Qwen3-embedding-0.6B and Qwen3-Reranker-0.6B.

5 Experiments

ToolGate is evaluated across ToolBench, MCP-Universe, ablations, efficiency, and rejection analyses. Results show strong performance, shorter tool-calling trajectories, and benefits from Hoare-based verification.

  • Main Results: ToolGate achieves the best or near-best performance across models and evaluation benchmarks.On ToolBench, it improves Pass Rate and Win Rate across G1/G2/G3 and remains model-agnostic across GPT-5.2, Qwen-3-235B, DeepSeek V3.2, and Gemini 3 Pro.
  • Main Results: ToolGate improves MCP-Universe performance by 3−7% over ToolChain* in Location Navigation and Repository Management and reaches 90.0 in Financial Analysis with GPT-5.2.It also achieves 45.45 in Repository Management and is reported to improve stability and robustness in complex tool chains.
  • Main Results: Hoare-logic constraints reduce error accumulation in ToolBench and mitigate long-horizon reasoning drift in MCP-Universe.The system maintains a trusted state set and validates each tool invocation with preconditions and postconditions.
  • Ablation Studies: Removing formal verification lowers GPT-5.2 MCP-Avg success to 37.6%, below the 38.3% DFSDT baseline.The same trend appears for DeepSeek V3.2, indicating that Hoare-based pruning is important to search efficiency.
  • Ablation Studies: Removing {Q} checks decreases GPT-5.2 MCP-Avg success by 10.8%, compared with a 4.5% decrease without {P} checks.The full {P}C{Q} loop combines precondition pruning with postcondition validation.
  • Tool Reasoning Efficiency: 37.9% efficiency improvement reduces GPT-5.2 average tool-calling steps from 6.78 to 4.21.ToolGate produces concise trajectories, while ReACT and Tool-Planner can enter trial-and-error loops; formal constraints prune infeasible branches.
  • Fine-grained Rejection Distribution: 29.4% of MCP-Universe tool-calling requests are intercepted by the formal verification layer.{P} statically prunes 17.6% of invalid paths, while {Q} dynamically rectifies 11.8% of logical drifts.

6 Conclusions

ToolGate evaluates LLM gatekeeping in tool-use scenarios, emphasizing decisions about when to invoke or refuse tools. The framework is presented as a foundation for safer and more reliable autonomous agents.

  • Conclusions: ToolGate evaluates LLM decision-making and gatekeeping beyond mere execution success, including responses to ambiguous, unauthorized, or high-risk instructions.The paper reports prevalent over-reliance by current state-of-the-art models in these situations.
  • Conclusions: ToolGate provides a diagnostic and foundational framework for safer, more reliable, and more autonomous AI agents.The stated focus is balancing functional proficiency with robust decision-making frameworks.

Limitations

The evaluation leaves important scope and realism boundaries. ToolGate is tested mainly on text-based, structured, and largely static environments, with limited qualitative assessment and possible model-specific prompt bias.

  • Scope: The benchmark primarily covers text-based and structured-data interactions, leaving multimodal tools and long-chain collaborative tasks for future work.This limits the evaluated scope of ToolGate’s current benchmark coverage.
  • Evaluation Setting: The largely static evaluation environment may not capture network latency, rate limits, or fluctuating data states in real-world APIs.These dynamics can interfere with real-time decision-making.
  • Evaluation Metrics: The predominantly quantitative metrics do not yet provide fine-grained assessment of explanatory reasoning or proactive information solicitation.The paper identifies qualitative evaluation as a future need.
  • Generalization: Prompt-based bias may prevent strategies optimized for specific models from generalizing perfectly across open-source LLMs.This is presented as a remaining limitation of generalization.

Ethics Considerations

ToolGate is evaluated in public or open-source environments without private or personally identifiable information. Its logical constraints are intended to support trustworthy tool use and can be combined with additional safeguards.

  • Data and Evaluation: Experiments use publicly available benchmarks, open-source tool environments, simulated environments, or publicly documented APIs with appropriate permissions.No private or personally identifiable information is collected, accessed, or used.
  • Data and Evaluation: ToolGate does not generate, store, or infer sensitive personal attributes or target specific demographic groups.The framework instead focuses on reliability, interpretability, and safety in model-based tool invocation.
  • Deployment: The methodology can be integrated with safety filters, auditing processes, and access-control mechanisms in real-world systems.The paper positions ToolGate as enhancing trustworthy AI behavior rather than bypassing safeguards or enabling harmful automation.
  • Benchmark Context: ToolBench evaluates tool selection, parameter planning, and executable API invocation across large API spaces.It contains more than 126K instruction–solution path pairs and uses ToolEval for execution-level assessment with metrics including Pass Rate and Win Rate.

A.2 MCP-Universe Benchmark

MCP-Universe evaluates LLMs through real MCP-server interactions, emphasizing long-horizon execution, tool discovery, and robustness in dynamic environments. Its broad benchmark and evaluator design supports comparisons across complex tool-use settings.

  • Benchmark scope: MCP-Universe evaluates complex tasks through interaction with real MCP servers rather than offline tool-use datasets.The benchmark emphasizes long-horizon interaction, unknown tool discovery, and robust execution under dynamic environments.
  • Benchmark composition: The benchmark spans 6 task domains, 11 MCP servers, 231 task instances, and 84 evaluators.Domains include navigation, repository management, financial analysis, 3D design, browser automation, and web searching.
  • Task structure: Tasks generally require multiple MCP tools across several rounds to complete objectives such as route planning, repository manipulation, and portfolio analysis.The task distribution is designed to remain representative and reasonably balanced across domains.
  • Evaluation: Execution-level evaluation uses Format, Static, and Dynamic Evaluators for protocol compliance, time-invariant correctness, and real-time data grounding.Dynamic evaluators support time-sensitive tasks such as financial-price and navigation evaluation.
  • Baselines and setup: Experiments compare ToolGate with ReACT, DFSDT, LATS, ToolChain*, and Tool-Planner under unified execution environments.MCP-Universe tools run in an official sandbox with latency, failure signals, and state-dependent output variation; decoding temperature is fixed at 0.2.
  • Tool retrieval: Tool descriptions and usage documentation are embedded for cosine-similarity retrieval of Top-K candidate tools, with K = 10.The retrieval representation includes functional semantics, argument specifications, and documentation.

D.1 Pre-condition {P} Validation

The precondition mechanism blocks tool calls that lack sufficient state support, especially hallucinated parameters and invalid operational sequences. It acts as an early static firewall while the execution loop searches among contract-valid candidates.

  • Precondition validation: 17.6% of all rejections arise from precondition checks that block invalid actions before execution.The precondition check functions as a static firewall.
  • Error categories: Parametric hallucination accounts for 8.4% of errors and is identified as the most prevalent error type.Models may hallucinate file IDs or directory paths instead of grounding parameters in retrieval.
  • Error categories: Symbolic link validation intercepts hallucinated file or directory parameters before execution, reducing computational overhead and token consumption.This validation targets parameters generated from intuition rather than grounded retrieval.
  • Error categories: State dependency violations account for 4.1% of errors, including attempts to modify files before obtaining required permissions or handles.The precondition mechanism enforces logical and temporal constraints on valid environmental states.
  • Execution loop: The forward-execution loop initializes state from the query, lets the LLM answer or request a tool, and iterates through valid candidates while verifying postconditions.A failed or unavailable contract path can terminate with no viable tools satisfying the contracts.
  • Execution loop: Candidate tools are skipped after failure, and accepted results update the symbolic state only when postcondition verification succeeds.The algorithm explicitly checks whether the state was updated before continuing.

F Examples

The examples demonstrate ToolGate’s contract-driven execution on successful and failed tool calls. A valid result is verified and committed, whereas a missing required field causes rejection, state preservation, and fallback to another tool.

  • Successful search: A YouTube search begins from a state containing the user’s query and invokes a search tool with machine-learning tutorial parameters.The example includes a query precondition and a concrete tool configuration.
  • Successful search: The search result passes structural and semantic checks because it contains a results list whose videos have title and URL fields.The verification result is recorded as successful before the state update.
  • Successful search: After successful verification, the symbolic state incorporates the YouTube results and result count for subsequent reasoning.The updated state retains the query, topic, platform, content type, and retrieved results.
  • Failed tool and fallback: In the weather example, the first tool satisfies the location precondition but fails postcondition verification because humidity is missing.Temperature and condition are valid, but the required humidity field is absent.
  • Failed tool and fallback: After the failed weather call, ToolGate marks the tool as failed and leaves the state unchanged before trying a second candidate.The second tool returns the required fields and passes both structural and semantic checks.
  • Failed tool and fallback: The second weather tool succeeds, updates the state with temperature, condition, humidity, wind speed, and pressure, and supports the final response.The example shows the verified result entering the subsequent reasoning trajectory.
  • Formal contract interpretation: The formal framework represents trusted information as a typed symbolic state and uses preconditions and postconditions to control tool execution and state updates.The runtime result is accepted only when structural, typing, and semantic constraints are satisfied.
  • Formal contract interpretation: An accepted result produces a well-formed state extension, while the explicit factorization makes probabilistic reasoning and logical contracts verifiable.The concrete ListFiles instantiation illustrates this accepted-update behavior.

G.5 Trajectory-Level Safety Derivation

Trajectory-level safety is defined by requiring safety at every execution step. Under sound contracts and a safe initial invariant, the framework’s induction argument establishes safety for every reachable trajectory.

  • Safety definition: A ToolGate execution is represented as a trajectory whose safety is determined by the safety of each individual step.The derivation distinguishes per-step safety from global trajectory-level safety.
  • Soundness result: If all tool contracts are sound and the initial state satisfies the global invariant, every reachable ToolGate trajectory is safe.The soundness theorem sketch uses induction on the execution step and the TOOL-STEP rule.
Loading 2601.04688v1…