ToolGate: Contract-Grounded and Verified Tool Execution for LLMs

📄 arXiv: 2601.04688v1 📥 PDF

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

分类: cs.CL, cs.AI, cs.FL

发布日期: 2026-01-08

备注: First version of ToolGate

💡 一句话要点

ToolGate：为LLM工具调用提供基于合约的、可验证的执行框架

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 大语言模型 工具调用 形式化验证 Hoare逻辑 符号执行

📋 核心要点

  1. 现有LLM工具调用框架依赖自然语言推理，缺乏逻辑安全性和可验证性的形式保证。
  2. ToolGate通过Hoare风格的合约形式化工具，利用前置条件控制调用，后置条件验证结果，确保状态演化的安全性。
  3. 实验表明，ToolGate在保证性能的同时，显著提升了LLM工具调用的可靠性和可验证性。

📝 摘要（中文）

本文提出ToolGate，一个前向执行框架，为LLM工具调用提供逻辑安全性保证和可验证的状态演化。ToolGate维护一个显式的符号状态空间，作为类型化的键值映射，代表推理过程中可信的世界信息。每个工具被形式化为一个Hoare风格的合约，包含前置条件和后置条件。前置条件通过检查当前状态是否满足所需条件来控制工具调用，后置条件确定工具的结果是否可以通过运行时验证来更新状态。该方法保证符号状态仅通过验证的工具执行来演化，防止无效或幻觉结果破坏世界表示。实验验证表明，ToolGate显著提高了工具增强的LLM系统的可靠性和可验证性，同时在复杂的多步骤推理任务上保持了竞争性的性能。这项工作为构建更值得信赖和可调试的AI系统奠定了基础，这些系统将语言模型与外部工具集成。

🔬 方法详解

问题定义：现有的大语言模型（LLM）工具调用框架，在决定何时调用工具以及是否提交工具结果时，过度依赖自然语言推理。这种方式缺乏形式化的逻辑安全保证，并且难以验证推理过程的正确性，容易受到幻觉信息和错误结果的影响，导致最终结果不可靠。

核心思路：ToolGate的核心思路是将每个工具的使用形式化为一个合约，类似于软件工程中的Hoare逻辑。这个合约包含前置条件（Precondition）和后置条件（Postcondition）。前置条件定义了工具可以被安全调用的状态，后置条件定义了工具执行后状态应该如何更新。通过在运行时验证这些条件，ToolGate可以确保只有在满足条件的情况下才能调用工具，并且工具的结果能够安全地更新世界状态。

技术框架：ToolGate维护一个显式的符号状态空间，该空间以类型化的键值映射的形式表示可信的世界信息。整个推理过程是一个前向执行的过程，每一步都涉及到工具的调用和状态的更新。具体流程如下：1. LLM根据当前状态和任务目标，决定要调用的工具。2. ToolGate检查该工具的前置条件是否满足当前状态。3. 如果前置条件满足，则执行该工具。4. ToolGate验证工具的执行结果，并根据后置条件更新状态空间。5. 重复上述步骤，直到完成任务。

关键创新：ToolGate的关键创新在于引入了基于合约的工具调用机制，将形式化验证的思想引入到LLM的工具调用过程中。与传统的依赖自然语言推理的方法相比，ToolGate提供了更强的逻辑安全保证和可验证性。通过显式地维护状态空间和验证工具的执行结果，ToolGate可以有效地防止无效或幻觉结果对世界状态的污染。

关键设计：ToolGate的关键设计包括：1. Hoare风格的工具合约：定义工具的前置条件和后置条件，用于控制工具的调用和状态的更新。2. 符号状态空间：使用类型化的键值映射来表示世界状态，方便进行形式化验证。3. 运行时验证机制：在工具调用和状态更新时，对前置条件和后置条件进行验证，确保推理过程的安全性。

📊 实验亮点

实验结果表明，ToolGate在复杂的多步骤推理任务上，显著提高了工具增强的LLM系统的可靠性和可验证性。具体而言，ToolGate能够有效地防止无效或幻觉结果对世界状态的污染，从而提高最终结果的准确性。同时，ToolGate在保持竞争性的性能，没有显著增加推理时间。

🎯 应用场景

ToolGate可应用于需要高可靠性和可验证性的AI系统中，例如智能客服、自动化运维、金融风控等领域。通过确保工具调用的安全性和结果的正确性，ToolGate可以提高这些系统的稳定性和可信度，减少错误和风险。此外，ToolGate还可以用于构建可调试的AI系统，方便开发者理解和排查问题。

📄 摘要（原文）

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.