1. 从“形式化”的困境谈起为什么我们需要工具增强的智能体如果你曾经尝试过将一段自然语言描述的业务逻辑或者一个数学猜想转化为能被计算机严格验证的形式化语言比如 Coq, Lean, Isabelle 等你大概率会立刻感受到一种“鸿沟”。这种鸿沟不仅仅是语法上的更是思维模式上的。我们的大脑习惯于模糊、跳跃、依赖背景知识的推理而形式化系统要求每一步都精确、完备、无歧义。这个过程被称为“形式化”Formization在数学、计算机科学和程序验证领域至关重要但它极其耗时、费力且对从业者的专业素养要求极高。这就引出了一个核心问题我们能否借助当前的人工智能特别是大语言模型LLM来降低形式化的门槛提升其效率直接让 LLM 从零生成一段正确的形式化代码成功率往往很低。因为形式化验证本质上是一个需要严谨规划、反复试错和深度推理的复杂任务。于是一个更可行的思路浮出水面不把 LLM 当作一个“全能的黑盒代码生成器”而是将其视为一个“具备规划与推理能力的智能体”并为其配备一系列专门用于形式化任务的工具。这就是“工具增强的智能体”Tool-Augmented Agents在精益形式化Lean Formalization背景下的核心价值。简单来说它试图构建这样一个工作流一个 LLM 作为“大脑”负责理解自然语言问题、制定证明策略、分解目标而一系列形式化工具如定理证明器的交互式命令、自动化策略、引理搜索器、类型检查器作为它的“手”和“眼睛”。大脑指挥手脚协同工作共同攻克形式化难题。我最近深度实践并分析了多个这类系统发现其效能并非由单一因素决定而是多个设计维度共同作用的复杂结果。本文就将基于我的实践经验对影响“工具增强智能体”在精益形式化任务中性能的关键因素进行一次“析因分析”拆解看看究竟是哪些“因子”在真正起作用。2. 核心因子一工具集的设计粒度与抽象层次给智能体配备工具听起来简单但“配备什么工具”和“如何定义工具”是首要的、也是影响最深远的决策。这直接决定了智能体的能力上限和操作效率。2.1 粗粒度工具 vs. 细粒度工具粗粒度工具例如一个名为prove_theorem的工具输入是定理的自然语言陈述输出是完整的 Lean 证明脚本。这相当于让工具包办了一切。其优点是智能体决策简单但缺点极其致命成功率极低且一旦失败智能体几乎无法进行有效的调试和干预因为不知道内部过程。细粒度工具将证明过程拆解为原子操作。例如apply_lemmalemma_name应用已知引理。use_termterm提供存在性证明的构造项。rewrite_athypothesis, target在目标处进行重写。run_tactictactic_name, args执行一个特定的 Lean 战术如simp,ring,omega。get_current_goal获取当前证明目标状态。search_libraryquery在数学库中搜索相关定义和定理。在我的实践中细粒度工具集是唯一可行的路径。它赋予了智能体与人类证明者类似的、一步步推进的能力。智能体可以观察每一步工具执行后证明状态的变化从而做出后续决策。这模仿了人类在交互式定理证明器ITP中的工作方式。2.2 工具的抽象层次语义层 vs. 语法层工具的定义还需要考虑抽象层次。语法层工具直接暴露底层证明器的原始命令或战术语法。例如工具run_tactic的参数可能就是“exact h1”或“intro h”。智能体需要自己生成正确的 Lean 语法字符串。这要求智能体对 Lean 语法有较深理解但灵活性最高。语义层工具用更高级的、领域特定的语义来封装工具。例如工具simplify_expressionexpr的内部可能调用simp但智能体无需关心simp的具体写法只需知道这个工具能化简表达式。再比如forward_reasoninghypothesis可能封装了一系列apply,have等操作。实操心得一个混合策略往往更有效。对于基础的、通用的操作如引入假设、应用等式可以提供语义层工具降低智能体的学习负担。对于复杂的、需要精确控制的战术则可以提供语法层工具或允许在语义工具中传入更详细的参数。关键在于工具的设计应当与智能体LLM的“知识”相匹配。如果 LLM 已经通过预训练熟悉了 Lean 的基本战术那么提供语法层工具可能更高效如果是从零开始训练或微调的智能体语义层工具能更快地上手。3. 核心因子二智能体的规划与反思机制有了好工具还得看“大脑”会不会用。智能体如何规划工具的使用序列以及在遇到错误时如何调整是第二个关键因子。3.1 静态规划与动态规划静态规划智能体在开始证明前就生成一个完整的、线性的工具调用序列。这类似于一次性生成整个证明脚本。其问题与粗粒度工具类似对复杂问题不现实无法应对证明过程中出现的意外分支和状态变化。动态规划反应式规划智能体采取“感知-思考-行动”的循环。在每一步它都接收当前的证明状态由工具get_current_goal等提供基于此状态和最终目标决定下一步调用哪个工具。这是目前主流且有效的方法。3.2 反思与回溯从错误中学习的关键动态规划必须配套强大的反思机制。当工具调用返回错误如“战术失败”、“类型不匹配”时智能体不能简单地崩溃或重试而需要有能力分析错误信息。错误诊断智能体需要解析 Lean 返回的错误信息。例如“tactic failed, target is not an equality” 意味着当前目标不是一个等式因此不能使用rw重写战术。智能体应能理解这类常见错误的语义。假设与上下文检查错误可能源于智能体错误地理解了某个假设的类型或者忘记使用某个可用的前提。反思机制应能驱动智能体重新检查当前的假设列表get_context工具。策略回溯与切换如果当前路径走不通智能体需要有能力回溯到之前的某个证明状态并尝试不同的策略分支。这需要系统在架构上支持保存“检查点”checkpoint。在实践中实现完全通用的回溯开销很大一个折中方案是允许智能体在有限的步骤内比如最近5步进行局部策略调整。在我的一个实验项目中我为智能体设计了一个简单的反思提示模板上一次工具调用失败。错误信息是[ERROR_MSG]。 当前证明目标是[CURRENT_GOAL]。 可用的假设有[HYPOTHESES]。 请分析失败原因并制定一个新的计划。可能的原因包括选择了错误的战术、未正确使用某个假设、需要对表达式进行先化简等。通过让 LLM 分析这个结构化的反思提示其自我修正的能力得到了显著提升。4. 核心因子三环境反馈的丰富性与实时性智能体所处的“环境”——即与 Lean 证明器的交互接口——所提供的反馈质量是第三个决定性因子。一个信息贫乏的环境会让智能体像在黑暗中摸索。4.1 状态反馈不仅仅是目标最基本的反馈是执行工具后的新证明目标。但优秀的反馈应包含更多完整的上下文所有当前可用的局部假设hypotheses及其类型。类型信息鼠标悬停在 IDE 中所能获得的所有类型信息对于智能体理解项term的结构至关重要。定义展开对于复杂的定义提供其展开形式可以帮助智能体进行化简和推理。错误信息的结构化解析将 Lean 原始的、有时晦涩的错误信息转化为更结构化、更语义化的描述。例如将“type mismatch”错误进一步标注出是哪个子表达式的类型不匹配。4.2 实时性 vs. 批量性批量执行智能体生成一系列命令一次性发送给证明器然后接收一系列结果。这种方式延迟低但一旦中间某步出错后续所有命令都可能无意义且错误定位困难。实时交互每执行一个工具命令就立即获得证明器返回的新状态和反馈。这完全模拟了人类在 IDE 中的交互体验。智能体可以根据最新状态做出最及时的决策错误也能被立即发现和纠正。毫无疑问实时交互式反馈是更优的选择尽管它对系统架构的复杂度要求更高需要维护持续的会话状态。为了实现高质量的实时反馈我通常会将智能体与一个运行着 Lean 语言服务器的后台进程连接通过其 LSPLanguage Server Protocol接口来获取精确的、实时的语法和类型信息这远比单纯解析文本输出要可靠。5. 核心因子四智能体自身的知识储备与微调策略最后一个但绝非不重要的因子是作为“大脑”的 LLM 本身。一个对形式化逻辑和特定定理证明器一无所知的基座模型即使有再好的工具和反馈也难以胜任工作。5.1 预训练知识 vs. 领域特定微调预训练知识像 GPT-4、Claude 3 这样的通用大模型已经在海量文本和代码中学习到了基本的逻辑推理模式、数学术语和编程概念。它们对“归纳法”、“反证法”、“构造函数”等概念有模糊的理解甚至可能见过一些简单的 Lean/Coq 代码片段。这些知识提供了宝贵的起点。领域特定微调这是提升性能的关键。使用高质量的定理形式化证明配对数据对模型进行监督微调SFT可以显著提升其以下能力语法准确性生成符合 Lean 语法的代码片段。战术选择偏好学习在何种证明状态下优先使用simp、ring还是apply。库知识熟悉目标数学库如 Mathlib中常用定理的名称和用途。5.2 提示工程在上下文中学习除了参数微调提示Prompt是注入知识的另一个重要手段。系统的提示词通常包含系统角色设定明确告诉模型“你是一个擅长使用工具进行 Lean 定理证明的助手”。工具描述以结构化格式如 JSON Schema详细描述每个工具的名称、功能、输入参数和输出格式。工作流程示例提供几个完整的、从自然语言定理到通过工具调用完成证明的示例。这些少样本示例Few-shot Examples能极其有效地对齐模型的输出格式和行为模式。当前任务上下文包括要证明的定理、已有的定义、以及当前的交互历史之前的工具调用、状态、错误。在我的经验中一个结合了领域微调模型与精心设计的少样本提示的智能体其表现远远超过仅使用通用模型或零样本提示的智能体。微调让模型“知道是什么”而提示中的示例则教会它“在这种情况下该怎么做”。6. 因子间的交互效应并非简单的叠加以上四个核心因子——工具设计、规划机制、环境反馈、模型知识——并非独立发挥作用。它们之间存在强烈的交互效应。工具粒度与规划能力工具越细粒度对智能体的规划能力要求就越高。智能体需要做更多、更小的决策。如果规划能力弱细粒度工具反而可能导致智能体在细节中迷失无法形成宏观证明思路。反馈质量与反思能力丰富、结构化的反馈是有效反思的前提。如果错误信息模糊不清再强的反思机制也无从下手。模型知识与工具抽象如果模型已经通过微调深刻理解了 Lean 战术那么提供语法层工具可能更直接高效。如果模型知识较弱那么语义层工具就像一个“脚手架”能引导它做出正确操作。实时反馈与模型延迟实时交互要求模型能快速响应。如果模型本身推理速度慢如使用大型模型进行复杂链式思考实时交互的体验会变得很差可能需要引入异步或缓存机制。因此设计一个高效的“工具增强智能体”系统是一个系统工程。不能只追求某一个因子的极致而需要根据任务复杂度、可用计算资源和期望的自动化程度在这四个维度上寻找平衡点。例如对于教育场景中相对简单的定理可能使用“较强模型 中等粒度工具 简单规划”的组合就够了而对于挑战前沿数学问题的形式化则可能需要“专家级微调模型 极细粒度工具 复杂反思规划 富实时反馈”的全套方案。7. 实践中的挑战与应对策略理论分析之后让我们回到地面看看在实际构建这样一个系统时会遇到哪些具体的坑以及我是如何尝试解决它们的。挑战一工具执行的“状态管理”难题。Lean 证明是高度状态依赖的。每一个战术都改变当前的目标和上下文。智能体发出的工具调用序列必须在一个持续的、状态一致的会话中执行。如果每次调用都从一个全新的 Lean 进程开始那证明永远无法推进。解决方案是维护一个持久的、有状态的 Lean 会话例如通过Lean.Server或Lean.Process交互并确保智能体的每一个请求都基于此会话的最新状态。这要求后端架构能够关联用户/任务与会话。挑战二长上下文与信息过载。随着证明步骤增多交互历史包含所有状态、工具调用和结果会变得非常长。直接将整个历史作为上下文喂给 LLM会迅速耗尽其上下文窗口且让模型难以聚焦关键信息。我的策略是选择性记忆不保存每一步的完整状态只保存关键节点如子目标开始、证明策略重大转变时的状态。摘要历史定期让模型自己对之前的证明过程做一个简短摘要然后用摘要替代冗长的原始历史。聚焦最近在提示中优先提供最近几步的详细交互和当前完整状态对于更早的历史则只提供高度概括的摘要。挑战三工具可靠性导致的智能体信心危机。如果工具本身有 Bug或者与 Lean 版本不兼容导致本应成功的调用失败会严重干扰智能体的学习与决策。必须建立一套完善的工具测试套件确保在给智能体使用前每一个工具在多种常见场景下都能返回预期结果。对于涉及外部搜索如search_library的工具还要处理网络超时、无结果等情况定义清晰的失败返回格式而不是抛出异常。挑战四评估的复杂性。如何评估这样一个系统的性能简单的“证明成功/失败”二元指标过于粗糙。我倾向于采用一个多维度的评估体系证明成功率在基准测试集上的通过率。平均证明长度步骤数衡量效率但需注意更短的证明不一定更好可能依赖了更强的前提。人类干预度在智能体“卡住”时需要人类给出提示如指定下一个战术的频率和程度。证明风格质量生成的证明是否清晰、可读、符合数学规范这可以通过有经验的开发者进行人工评分。8. 未来展望走向协同与专业化基于目前的实践和分析我认为工具增强的智能体在精益形式化领域的发展会朝着两个方向深化方向一人机协同的混合智能。最有效的模式可能不是完全自动化而是“智能体先行人类兜底与指导”。智能体负责完成繁琐的、模式化的推导步骤或者在多个可能的策略中进行快速探索。当它陷入困境时人类专家可以介入提供一个高阶的提示比如“试试用归纳法”或者直接修正某一步然后让智能体继续。系统需要设计良好的人机交互接口使得这种切换无缝自然。方向二工具与模型的共同专业化。未来的系统不会是“一个通用 LLM 一套固定工具”。而可能会出现针对不同数学领域如代数几何、数论、分析专门微调的模型以及与之配套的、更深度的领域专用工具。例如在代数拓扑领域工具集可能包含专门处理同伦群、纤维化等概念的特定策略和查询。模型和工具在特定领域的数据上共同进化形成高度专业化的“形式化专家”。这个领域仍然充满挑战但每一次将因子分析中的某个维度进行优化我们都能看到智能体在形式化这座高山上的攀登能力又提升了一小步。对于每一位从事形式化验证或对 AI 辅助推理感兴趣的朋友来说亲手搭建一个这样的智能体观察它如何笨拙地尝试、失败、反思、再尝试最终在工具的辅助下完成一个证明这个过程本身就是对于智能、工具与形式思维之间关系最深刻的理解。