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）在利用外部工具进行复杂推理时，依赖于自然语言进行推理，以决定何时调用工具以及是否采纳工具的执行结果。这种方式缺乏形式化的逻辑安全保证，容易受到LLM幻觉的影响，导致错误或不可靠的结果，进而影响后续推理过程。因此，需要一种能够保证工具调用和结果采纳安全性的机制，避免无效或错误的工具执行污染世界状态。

核心思路：ToolGate的核心思路是将每个工具的使用形式化为一个Hoare风格的合约，包含前置条件（precondition）和后置条件（postcondition）。前置条件用于判断当前状态是否满足工具调用的要求，只有满足前置条件才能执行工具。后置条件用于验证工具执行的结果是否有效，只有通过后置条件验证的结果才能被采纳并更新世界状态。通过这种方式，ToolGate能够保证只有经过验证的工具执行才能改变世界状态，从而避免了无效或错误的工具执行对推理过程的影响。

技术框架：ToolGate的整体框架包含以下几个主要模块：1) 符号状态空间：维护一个显式的符号状态空间，以类型化的键值对形式表示当前可信的世界信息。2) 工具合约：每个工具都对应一个Hoare风格的合约，包含前置条件和后置条件。3) 前向执行引擎：根据当前状态和工具合约，决定是否执行工具，并验证工具执行的结果。4) 运行时验证器：负责验证工具执行的结果是否满足后置条件，只有通过验证的结果才能更新符号状态空间。

关键创新：ToolGate的关键创新在于将形式化验证的思想引入到LLM的工具调用过程中，通过Hoare风格的合约来保证工具执行的安全性。与现有方法相比，ToolGate不再依赖于自然语言推理来判断工具的可用性和结果的有效性，而是通过形式化的逻辑推理来进行判断，从而避免了LLM幻觉的影响。此外，ToolGate还提供了一种可验证的状态演化机制，使得整个推理过程更加透明和可调试。

关键设计：ToolGate的关键设计包括：1) 符号状态空间的表示方式，需要能够有效地表示世界信息，并支持前置条件和后置条件的验证。2) 工具合约的定义方式，需要能够准确地描述工具的使用条件和执行结果。3) 运行时验证器的实现方式，需要能够高效地验证工具执行的结果是否满足后置条件。具体的参数设置、损失函数、网络结构等技术细节在论文中未详细描述，属于未知信息。

📊 实验亮点

实验结果表明，ToolGate在提高LLM工具调用的可靠性和可验证性方面取得了显著效果。具体性能数据和对比基线在摘要中未明确给出，但强调了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.