1. 项目缘起当AI证明助手遇上成本与质量的现实难题最近在折腾一个挺有意思的项目核心是围绕Agentic Theorem Provers智能体定理证明器在Lean这个交互式定理证明环境里的表现。简单来说这玩意儿就是让大语言模型LLMs扮演一个“证明助手”的角色帮你或者引导你在Lean里完成数学定理的形式化证明。听起来很酷对吧但真正上手之后一个无法回避的、极其现实的问题就摆在了面前成本与质量的权衡。你可能会问这有什么成本不就是跑跑代码吗这里的“成本”远不止电费。对于基于LLM的Agentic Prover而言成本主要体现在两个方面计算成本和人力验证成本。计算成本很好理解调用一次GPT-4、Claude-3这样的顶级模型API生成一段证明策略tactic或者代码都是真金白银。更关键的是这些模型生成的证明建议质量参差不齐。一个质量不高的建议会导致你在Lean里反复调试、修改消耗大量本可以用于创造性思考的时间——这就是人力验证成本。有时候一个模糊的建议带来的调试时间成本远超调用API的那点费用。而“质量”在这里指的就是证明建议的有效性和指导性。一个高质量的建议应该能直接通过Lean的检查或者至少给出清晰、正确的证明思路让你能快速理解并继续推进。低质量的建议则可能包含逻辑错误、语法错误或者干脆是无关的废话把你引入歧途。所以这个项目的目标非常明确在有限的预算或计算资源下如何最大化Agentic Theorem Prover在Lean中辅助证明的整体效率和成功率这不仅仅是调个API参数那么简单它涉及到提示工程、证明状态分析、反馈循环设计、甚至多个智能体之间的协同策略。最近业界也有一些相关讨论比如关于Chimera这类面向异构LLM的、兼顾延迟与性能的多智能体服务框架的思路就给了我们很多启发。虽然Chimera主要解决的是服务部署问题但其“根据任务需求和模型能力动态调度”的核心思想与我们优化成本质量权衡的目标在底层逻辑上是相通的。2. 核心挑战拆解为什么在Lean里优化如此棘手要优化首先得明白难点在哪。在Lean中利用Agentic Prover其工作流程可以简化为用户给出一个待证明的目标Goal - AgentLLM分析当前证明状态 - 生成下一步的证明策略建议 - 用户在Lean中执行并验证。这个循环中的每一个环节都充满了不确定性。2.1 Lean证明环境的特殊性与复杂性首先Lean本身就是一个高门槛的环境。它有着严格的类型系统和复杂的语法规则。对于LLM来说理解一个Lean的证明状态Tactic State本身就是一项挑战。这个状态包含了当前所有的假设Hypotheses和需要证明的目标Goal以及可能存在的局部定义和上下文。LLM需要精确解析这些信息才能生成有效的apply,rewrite,have,exact等策略。其次证明搜索空间巨大且非结构化。与编程代码补全不同数学证明没有唯一的“正确下一步”。可能存在多种路径都能到达终点有的优雅简短有的迂回复杂。LLM需要具备一定的数学直觉和策略规划能力而不仅仅是语法模仿。2.2 LLM作为证明代理的固有缺陷当前LLM在定理证明任务上存在几个关键瓶颈上下文长度与精度要求矛盾一个复杂的证明可能需要很长的上下文来追溯定义、引理。虽然现代LLM上下文窗口很大但长上下文下的注意力机制可能导致对关键细节的忽略。同时Lean对精度要求极高一个字符的错误比如多了一个括号或少了一个点都会导致失败。幻觉与自信度错配LLM经常会“自信地”生成一段看似合理但完全错误或无效的证明策略。它无法像人类一样对自己的“不确定”进行量化表达。这直接导致了高昂的验证成本。缺乏真正的推理与回溯能力大多数基于单次提示的交互是“静态”的。LLM根据当前快照给出建议如果建议失败它通常不知道具体为什么失败也难以基于失败进行有效的、有深度的回溯和调整策略。这需要设计更复杂的交互机制。2.3 成本模型的多元化成本不仅仅是API调用的美元数。一个更全面的成本模型应包括直接经济成本 (C_econ)LLM API调用费用与使用的模型、输入/输出令牌数直接相关。时间成本 (C_time)用户等待LLM响应的时间 用户验证、调试LLM建议所花费的时间。后者往往占主导。认知负荷成本 (C_cog)糟糕的建议会增加用户的挫败感和思维中断影响整体证明效率。我们的优化目标是在总预算可能是经济预算也可能是时间预算的约束下最小化完成一个证明目标所需的C_time w * C_cog其中w是认知负荷的权重同时最大化证明成功率。这显然是一个多目标优化问题。3. 策略一构建分层的智能体调用体系直接让最强大的模型如GPT-4处理每一个证明步骤从成本上看是极其奢侈的而且对于简单步骤来说是一种浪费。因此一个自然的优化思路是引入分层策略或级联模型。3.1 轻量级“哨兵”与“校验器”角色我们可以设计一个由不同“智能度”和“成本”的模型或规则组成的流水线规则引擎/本地轻量模型第一层在将证明状态发送给昂贵的LLM之前先用一套预定义的规则或一个微调过的小型本地模型比如7B参数的模型进行过滤。它可以处理一些非常模式化的场景例如目标化简如果目标形如A ∧ B直接建议constructor。已知引理匹配如果目标与本地知识库中的某个引理结论完全匹配直接建议apply lemma_name。语法错误检查对LLM生成的结果进行基础的Lean语法合规性检查拦截明显的低级错误。 这一层的成本极低甚至是零成本可以过滤掉大量不需要动用“重武器”的简单情况。中型模型第二层对于第一层无法处理的、中等复杂度的目标调用性价比高的中型API模型如Claude Haiku, GPT-3.5-Turbo。这些模型在大多数常规证明步骤上表现尚可成本远低于顶级模型。顶级模型第三层只有当目标被判定为“非常复杂”例如涉及多层嵌套、需要创造性构造、或前两层多次尝试均失败时才调用GPT-4、Claude Opus这样的顶级模型。这里的挑战在于如何准确“判定”复杂度。我们可以基于一些启发式规则目标表达式的深度和广度。当前可用假设的数量和复杂度。前两层模型尝试的次数和失败模式。实操心得这个分层体系的关键在于“判定逻辑”的设计。一开始我们简单地用目标字符串长度作为阈值效果很差。后来改为结合目标语法树深度和假设中涉及的自定义定理数量效果提升明显。判定逻辑本身必须非常轻量否则就本末倒置了。3.2 动态预算分配与熔断机制我们不能对每个证明目标无限制地调用模型。需要引入动态预算的概念。为每个证明目标设置初始令牌预算例如10000个输出令牌。每次调用根据模型类型扣除预算调用GPT-4扣得多调用Haiku扣得少。实施熔断如果在一个目标上连续失败超过N次例如5次或者预算耗尽则暂停对该目标的自动建议转而提示用户手动干预或提供更具体的上下文。这防止了在“死胡同”里浪费大量资源。4. 策略二增强提示工程与上下文管理提示Prompt是引导LLM工作的方向盘。低质量的提示是导致高成本、低质量输出的首要原因。4.1 结构化、标准化的证明状态描述直接将Lean的原始Tactic State扔给LLM是不够的。我们需要对其进行预处理和增强。信息浓缩与去噪过滤掉当前证明无关的、来自庞大mathlib库的冗长类型定义只保留最核心的假设和目标表述。可以用自然语言对复杂的逻辑关系进行简要重述。提供相关引理提示利用Lean的#check或类似工具自动搜索当前上下文中可能相关的已知定理、引理并将其名称和类型摘要添加到提示中。这相当于给了LLM一个“工具箱清单”极大地缩小了搜索空间。-- 在提示中增加类似这样的信息 -- 相关已知事实 -- Nat.succ_ne_self (n : ℕ) : n.succ ≠ n -- List.length_map (f : α → β) (l : List α) : (l.map f).length l.length指定输出格式严格要求LLM以特定的、易于解析的格式输出。例如请生成下一步的Lean tactic。 输出格式必须严格为 TACTIC: 你的tactic代码 EXPLANATION: 简要的一行解释说明为什么使用这个tactic这方便后续程序自动化提取和执行也减少了模型输出无关废话的概率。4.2 迭代式提示与反馈集成单次提示-响应的模式效率低下。我们需要让Agent具备从失败中学习的能力。错误反馈注入当LLM生成的tactic执行失败时Lean会给出错误信息。这个错误信息是黄金般的反馈下一次提示时不仅包含新的证明状态还要附加上一次尝试的tactic和具体的错误信息。上一次尝试的Tactic: rewrite [h] at H 错误信息: rewrite tactic failed, did not find instance of the pattern in the target. 当前目标: ...这直接告诉LLM“你刚才那样做不行原因是X”引导它进行修正。多轮对话上下文保持将整个交互过程维持在一个对话上下文中让LLM能记住之前的尝试和当前的证明进展。这比每次都是全新的、孤立的提示要有效得多。但需要注意管理上下文长度避免无关历史积累导致性能下降。思维链CoT引导对于复杂目标可以明确要求LLM“先一步步推理再输出tactic”。虽然这会增加输入令牌成本但往往能显著提高最终输出tactic的质量减少试错次数从总成本上看可能是合算的。请先进行推理要证明目标 A ∨ B我们目前有假设 H: ¬A。如果我们可以证明 B那么就能用 or_inr 来完成。现在来看如何证明 B... 基于以上推理下一步的tactic是 TACTIC: apply Or.inr5. 策略三设计基于验证的智能体协同机制单一智能体能力有限。受多智能体服务框架如相关讨论中提到的Chimera的调度思想启发我们可以设计多个具有不同专长或角色的智能体进行协同工作。5.1 “提议-验证”双智能体模式这是最基础且有效的协同模式。提议者Proposer负责根据当前证明状态生成一个或多个候选的下一步tactic。它可以是我们分层体系中的任何一个模型。验证者Verifier负责快速评估候选tactic的质量。验证者不一定需要强大的生成能力但需要快速、高精度的判断力。它的任务可以简化为语法验证候选tactic在Lean中是否语法正确类型粗略检查在不完全执行的情况下基于当前上下文该tactic的输入输出类型是否大致匹配这可以通过一个简化的、不进行实际计算的类型检查来实现类似于“dry run”。简单逻辑校验对于apply lemma_name这样的tactic验证lemma_name的结论是否与当前目标在形式上可统一unifiable。验证者可以由规则引擎或一个专门微调过的小型、快速模型担任。只有通过验证者初步筛选的tactic才会被提交给用户或执行环境。这可以拦截大量明显错误的提议节省用户的调试时间。5.2 多专家智能体与仲裁机制对于特别复杂的子目标可以并行调用多个“专家”智能体。每个专家可能擅长不同的领域如代数、分析、组合逻辑或者采用不同的策略风格激进式构造、保守式化简。并行生成向多个专家智能体可以是不同模型也可以是同一模型的不同提示发送相同的证明状态收集一批候选方案。仲裁与选择设计一个“仲裁者”来整合结果。仲裁策略可以是投票法如果多个独立智能体给出了相同或相似的tactic则该tactic的可靠性更高。验证优先将所有候选tactic交给一个强大的验证智能体或通过快速模拟执行进行排序选择排名最高的。多样性选择如果当前陷入僵局故意选择一个与众不同的策略以探索新的证明路径。踩坑实录我们曾尝试让多个智能体直接“对话”协商结果发现成本激增且效率低下大量token浪费在智能体之间的客套话和重复论证上。后来改为由中央仲裁者统一收集、静默验证、选择流程清晰成本可控。这印证了在成本约束下智能体间的通信开销必须精心设计。6. 实践框架与工具链整合理论再好也需要落地。在Lean 4的生态下如何将这些策略整合成一个可用的工具6.1 与elan、lake及mathlib的协同整个工作流建立在稳定的Lean环境之上。确保使用elan管理稳定的Lean和工具链版本是基础。项目本身可以作为一个lake包来管理方便定义依赖和构建。作为Lake插件/工具可以开发一个lake插件用户通过lake exe my_prover_agent来调用。插件内部封装了与LLM API的通信、证明状态提取、提示构建、结果解析等逻辑。与Editor集成更理想的方式是集成到VSCode的Lean4插件中。可以提供一个侧边栏或命令面板允许用户在当前证明的任意位置调用Agent建议并以非侵入式的方式如代码透镜、内联建议展示结果点击即可应用。6.2 实现架构概览一个简化的系统架构可能包含以下模块状态监听器监视Lean Infoview或LSP协议捕获当前的Tactic State。状态处理器对原始状态进行清洗、浓缩、相关引文检索。策略调度器核心大脑。根据预设的成本规则、当前目标复杂度、历史记录决定调用哪个模型/智能体、使用何种提示模板。智能体执行池管理与不同LLM API或本地模型的连接处理并发请求、超时和错误重试。结果验证器对返回的tactic进行快速语法和类型预检查。反馈记录器记录每一次交互的输入、输出、结果成功/失败及错误信息用于后续分析和模型微调。6.3 成本监控与数据分析优化离不开度量。系统需要内置详细的日志和度量指标每个证明步骤消耗的API令牌数区分输入/输出。每个步骤使用的模型。建议的接受率用户最终采纳的比例。从生成建议到用户采纳/验证成功所经过的时间。失败建议的错误类型分布。定期分析这些数据可以回答关键问题在哪些类型的子目标上使用昂贵模型是“物有所值”的哪些情况下便宜模型就足够了我们的判定逻辑准确率如何提示模板哪些地方需要改进这构成了一个持续的优化闭环。在Lean中优化Agentic Theorem Prover的成本质量权衡是一个典型的工程与算法结合的问题。它没有银弹需要我们在模型能力、提示设计、系统架构和成本控制之间反复寻找最佳平衡点。从我个人的实践来看建立一个灵活可配置的分层调度策略是降低直接经济成本最有效的手段而深度整合Lean反馈的迭代式提示则是提升建议质量、降低人力时间成本的关键。将大型证明任务分解让低成本模型处理模式化工作让高成本模型聚焦于真正的难点并用自动化的验证环节为每一次调用把关这套组合拳打下来整体效率的提升是肉眼可见的。这个过程也让我更深刻地理解到让AI辅助工具真正实用化其核心往往不在于追求最强的单点能力而在于构建一个能扬长避短、高效协同的智能系统。