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

TL;DR
ToolGate introduces a formal framework for safe and verifiable tool execution in LLMs, ensuring logical safety and trusted state evolution during complex reasoning tasks.
Contribution
It formalizes tool invocation using Hoare-style contracts and maintains a symbolic state to guarantee verifiable and safe tool integration in LLMs.
Findings
Significantly improves reliability of tool-augmented LLMs
Ensures state evolution only through verified tool execution
Maintains competitive performance on reasoning tasks
Abstract
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsTopic Modeling · Explainable Artificial Intelligence (XAI) · Natural Language Processing Techniques
