引言：从混乱的灵感到严谨的逻辑
大家好，我是马场 馨 (Kaito Baba)。今天，我想和大家分享一段旅程——一段始于人类直觉的火花，终于机器逻辑的坚冰的探索。这段旅程的结晶，就是我们的 Prover Agent。
不知你是否曾有过这样的经历：在解决一个复杂的数学问题时，脑海中会闪现出一些模糊的、非正式的想法。"或许可以先试试这个特例？""如果我把这个问题拆成几块，是不是就简单多了？"这些稍纵即逝的灵感，往往是通往答案的钥匙。然而，大型语言模型（LLMs）虽然在模仿这种"直觉思维"上取得了惊人的进步，却常常在严谨性上栽跟头。它们可能会"一本正经地胡说八道"，产生看似合理却充满逻辑谬误的证明。
这就好比一位才华横溢但粗心大意的艺术家，他能挥洒出壮丽的画卷草稿，却无法保证每一笔都精确无误。而另一边，我们有形式化证明助手，比如 Lean。它就像一位一丝不苟的工程师，手持精密的测量仪器，能验证每一个部件是否完美契合。但它本身缺乏创造力，无法从零开始设计蓝图。
我的梦想，就是让这位艺术家和工程师携手合作。让 LLM 的"非形式化推理"（informal reasoning）为证明过程提供宏观战略和创新思路，再由 Lean 这样的"形式化验证器"（formal verifier）来确保每一步都坚不可摧。Prover Agent 就是我们为实现这个梦想而构建的桥梁和指挥中心。它不仅仅是一个模型，更是一个协作框架，一个能让直觉与逻辑共舞的智能体。接下来，我将带大家深入了解，我们是如何教会这个智能体像人类数学家一样，在探索中犯错、从错误中学习，并最终攻克那些连它最初也感到棘手的难题的。
核心发现：Prover Agent 的五大"超能力"
1. 协同作战：非形式化与形式化的无缝衔接
我们设计的核心，在于建立一个高效的"沟通-验证-反馈"闭环。Prover Agent 不再是单一模型在战斗，而是一个由三位专家组成的团队：
- 直觉大师 (Informal LLM): 负责用自然语言进行头脑风暴，提出证明的大纲和思路。它就像团队里的策略师，不拘泥于细节，重在指明方向。
- 逻辑工匠 (Formal Prover Model): 负责将策略师的自然语言思路，翻译成 Lean 能懂的、严谨的形式化代码。它就像是工程师，将蓝图转化为精确的施工图。
- 终极裁判 (Lean Verifier): 负责检查施工图的每一行代码是否合乎逻辑、语法无误。如果发现错误，它会立刻发出"警报"，并指出问题所在。
这个过程是动态且反复的。当"裁判"发现错误，比如一个"tactic failed"（策略失败）或"goal unsolved"（目标未解决），这个反馈信息会立刻传回给"逻辑工匠"。工匠会根据错误信息，结合最初的思路，重新修改它的代码。这种即时反馈和迭代修正的机制，极大地提升了证明的成功率。它避免了传统 LLM 一条道走到黑的窘境，让模型拥有了宝贵的"反思和自我纠错"能力。
🎬 动画一：协同证明流程
生活化类比： 想象一个写作团队。作家（Informal LLM）提出故事大纲，编辑（Prover Model）将其写成章节，而校对（Lean）负责检查语法和逻辑错误。校对发现问题后，会立刻反馈给编辑修改，直到完美为止。
动画说明： 这个动画展示了 Prover Agent 的核心工作循环。一个"问题"被"直觉大师"转化为"思路"，再由"逻辑工匠"编码成"证明草稿"。草稿被送往"终极裁判"Lean 进行验证。如果验证失败，红色的"错误"信息会返回，触发新一轮的修正，直到绿色的"成功"信号出现。
2. 策略生成：通过辅助引理（Lemma）化繁为简
面对一个极其复杂的问题，人类数学家往往不会一头扎进去。他们会尝试证明一些更小的、相关的命题，我们称之为"辅助引理"（Auxiliary Lemmas）。比如，要证明一个关于所有偶数的定理，你可能会先证明它对于 2、4、6 成立，从中寻找规律。或者，你会从已知条件出发，推导一些可能用得上的中间结论。
我们的 Prover Agent 模仿了这一高级策略。当直接证明失败时，它不会固执地反复尝试，而是会启动引理生成模式。它会要求"直觉大师"提出几个可能有帮助的辅助引理，比如：
- 具体实例： 验证原问题在某个特定值下是否成立。
- 中间事实： 从问题的假设出发，推导出一个新的、可能更有用的结论。
- 弱化版本： 证明一个比原问题更简单、但结构相似的命题。
然后，智能体会逐一尝试证明这些引理。一旦某个引理被成功证明，它就会被存入"工具箱"。最后，Prover Agent 会带着这些被验证过的"新工具"，再次挑战原始问题。事实证明，这种"迂回战术"非常有效，它能帮助智能体在看似无路可走时，发现隐藏的证明路径，就像在迷宫中先点亮几盏灯，再寻找出口一样。
🎬 动画二：引理生成与解构
生活化类比： 这就像解决一个大型的乐高模型。直接搭建可能无从下手。但如果你先把说明书上的几个小组件（引理）拼好，再用这些组件去组合成最终的模型，就会容易得多。
动画说明： 一个巨大的、无法撼动的"复杂问题"方块出现在中心。点击按钮后，Prover Agent 会生成几个小型的"引理"方块。智能体逐一解决这些小方块，成功后它们会变成发光的"工具"。最后，这些工具飞向大方块，将其成功分解并解决。
3. 卓越性能：在标准测试中刷新纪录
理论说得再好，也要靠实践来检验。我们将 Prover Agent 投入到形式化证明领域的标准"考场"——MiniF2F 基准测试中。这个测试集包含了488个来自奥数竞赛和高等数学的难题，是检验模型实力的"试金石"。
结果令人振奋！在使用同等规模的小型语言模型（SLMs）的赛道上，Prover Agent 取得了 86.1% 的成功率，这在当时创造了新的 state-of-the-art 纪录。这意味着，在近乎九成的情况下，我们的智能体能够独立、自动地完成这些高难度数学题的形式化证明。这不仅仅是数字上的胜利，更证明了我们提出的"协同"与"引理"两大策略的有效性。它表明，通过智能的框架设计，我们可以让小模型的潜力得到极大的释放，实现超越其自身能力的表现。
🎬 动画三：性能对比图
数据来源: 论文 Table 1. miniF2F-test 上的性能对比。
图表说明: 这个图表直观地展示了 Prover Agent（紫色柱）与其他使用小型语言模型（SLMs）的顶尖方法在 MiniF2F 测试集上的成功率对比。可以看到，在样本预算（Sample Budget）远低于许多对手的情况下，我们的智能体取得了最高的成功率。
4. 超高效率：用更少的尝试解决问题
在AI领域，模型的性能不仅取决于"能不能做对"，还取决于"做对需要多大代价"。许多证明方法依赖于"人海战术"，即生成成千上万个证明尝试（samples），希望能"蒙对"一个。这种方法的计算成本极高，难以在实际中应用。
Prover Agent 则走了另一条路：精兵简政。由于我们的框架具有迭代修正和引理引导的能力，它不需要盲目地进行大量尝试。在我们的实验中，整个流程（包括直接证明、引理证明、最终合成）的总样本预算被控制在 2000 次以内。而之前的一些SOTA方法，为了达到高成功率，可能需要超过 8000 次甚至更多的尝试。我们的方法在某些配置下，仅用 400 次尝试就能达到 84.0% 的成功率，远超其他模型在数千次尝试下的表现。
这好比一位神枪手（Prover Agent）和一位用机枪扫射的新兵。神枪手通过精确瞄准（反馈修正）和寻找最佳射击点（引理），用更少的子弹就能命中目标。这种高效率意味着更低的推理成本和更快的解决速度，为AI在数学领域的实际应用铺平了道路。
🎬 动画四：探索与效率
生活化类比： 找人就像这样。你可以挨家挨户地敲门问（暴力搜索），也可以先打电话问问几个关键的社区中心（引理），缩小范围后再去找，效率自然更高。
动画说明： 动画展示了两种证明策略。左边是"暴力搜索"，大量的"尝试"粒子（灰色）盲目地撞向目标，消耗巨大。右边是 Prover Agent 的策略，它先派出几个"引理"探针（紫色），点亮了通往目标的路径，然后少量的"尝试"粒子（亮紫色）沿着路径高效地抵达终点。
5. 模块化设计：拥抱未来的可扩展性
我们没有试图去打造一个巨大而笨重的"万能"模型，而是采用了模块化、可插拔的架构。Prover Agent 中的"直觉大师"、"逻辑工匠"和"自动形式化器"都是独立的模块。这意味着什么？
这意味着我们的框架具有极强的未来适应性。当一个新的、更强大的通用语言模型问世时，我们不需要从头训练整个系统。我们只需要简单地"拔下"旧的"直觉大师"模块，"插上"新的模型，整个系统的推理能力就能立刻得到提升。同样，如果有人开发出更擅长 Lean 代码生成的模型，我们也可以轻松替换"逻辑工匠"。
这种设计哲学，就像组装一台高性能电脑。你可以独立升级CPU、GPU或内存，而无需更换整个主板。它让 Prover Agent 不会轻易过时，能够持续吸收整个AI领域的进步成果，保持其前沿性。这是一种更灵活、更可持续的研究范式，将问题分解，让每个部分都可以被独立优化和迭代。
🎬 动画五：模块化系统
生活化类比： 这就像一个音响系统。你可以随时把旧的功放换成新的、更强劲的型号，整个系统的音质就会立刻提升，而无需更换音箱或播放器。
动画说明： 动画展示了 Prover Agent 的模块化架构，包含"Informal LLM"、"Prover Model"等模块。点击"升级LLM模块"按钮，可以看到旧的模块被一个更大、更亮的"新LLM"模块替换，同时右侧的"性能仪表盘"指针会明显上升，直观地展示了模块化升级带来的好处。
技术细节：深入 Prover Agent 的"大脑"
现在，让我们揭开 Prover Agent 华丽外表下的硬核技术内幕。整个系统的运转，可以用一个算法流程来精确描述。这不仅仅是代码，更是我们精心设计的、模拟人类数学家思维过程的逻辑蓝图。
算法核心流程
下面是 Prover Agent 工作的伪代码，它概括了我们如何协调各个组件来解决一个给定的数学问题 $T$。
Prover Agent 核心算法 (Algorithm 1)
- 直接尝试 (Direct Attempt): 首先，系统调用
PROVE(T)函数，直接尝试证明原始问题 $T$。如果成功，皆大欢喜，任务完成。 - 引理生成 (Lemma Generation): 如果直接证明失败，系统进入策略思考阶段。
- 非形式化LLM会生成一组自然语言的辅助引理 $L_1, L_2, \dots, L_n$。
- AutoFormalizer 模型将每个 $L_i$ 转换为 Lean 语句 $F_i$。Lean 会检查其语法，确保它们是有效的"问题陈述"。
- 引理证明 (Lemma Proving): 系统再次调用
PROVE(F_i)，尝试独立证明每一个生成的引理。 - 最终合成 (Final Synthesis): 搜集所有被成功证明的引理，形成一个"已验证工具集" $P_{proven}$。然后，再次调用 Prover 模型，让它利用这些工具来证明原始问题 $T$。这一步同样会利用迭代反馈机制进行修正，直到成功或达到尝试上限。
其中，核心的 PROVE 函数自身就是一个包含两阶段的微型循环：
- 初始尝试阶段 (Initial Attempts): 生成 $N_{init}$ 个不同的证明草稿。这个阶段更像是发散思维，探索多种可能性。
- 迭代优化阶段 (Iterative Refinement): 如果初始尝试都失败了，系统会挑选一个错误最少的草稿作为"最佳候选"，然后进行 $N_{refine}$ 轮的精细打磨。这个阶段是收敛思维，针对性地修复错误。
数学公式的魅力：从概率角度看迭代
迭代修正的威力可以用一个简单的概率模型来理解。假设单次证明尝试的成功概率为一个很小的值 $p$。如果没有反馈机制，进行 $N$ 次独立尝试，那么至少成功一次的概率是： $$ P(\text{success}) = 1 - (1 - p)^N $$ 这个公式告诉我们，想要提高成功率，只能通过暴力增加 $N$ 来实现，成本很高。
公式解读： 这就像买彩票。每张彩票（一次尝试）中奖的概率是 $p$。你买 $N$ 张，至少中一张的概率就是 $1$ 减去所有 $N$ 张都没中的概率。想要中奖，就得疯狂买彩票。
而我们的迭代反馈机制，改变了这个游戏规则。每一次失败的反馈，都会给下一次尝试提供宝贵的信息，从而提高了下一次成功的概率。我们可以把第 $i$ 次迭代后的成功概率建模为 $p_i$。由于有反馈，我们有 $p_{i+1} > p_i$。假设每次反馈能让成功概率提升一个因子 $k > 1$，即 $p_{i+1} \approx k \cdot p_i$ (在概率很小时的简化)，那么成功率的增长会快得多。
一个更精确的模型是，把证明过程看作是在一个巨大的"状态空间"中搜索正确的路径。每次Lean的反馈，就像一个路标，排除了大量的错误分支，使得搜索范围急剧缩小。假设总的证明路径空间大小为 $S$，每次尝试能探索 $m$ 条路径。没有反馈时，你需要 $S/m$ 次尝试。而有反馈时，每次迭代可能将 $S$ 缩小一个数量级。这正是效率提升的关键所在。
模型选择与实现
我们精心挑选了当时在各自领域最优秀的小型开源模型来组建我们的"专家团队"：
- 非形式化LLM: 我们使用了 DeepSeek-R1-0528-Qwen3-8B，它在自然语言的数学推理上表现出色。
- 形式化Prover: DeepSeek-Prover-V2-7B，一个为 Lean 证明优化的顶尖模型。
- 自动形式化器: Kimina-Autoformalizer-7B，专门用于将数学自然语言翻译成 Lean 命题。
整个系统通过 vLLM 框架进行高效推理，部署在NVIDIA A100 GPU上。我们使用的 Lean 版本为 4.9.0，确保了实验环境的一致性和可复现性。
实验与案例：当 Prover Agent 面对难题
一个框架的真正价值，在于它如何解决那些棘手的、非显而易见的问题。让我们通过一个具体的案例，来剖析 Prover Agent 的思考过程。
案例研究: 证明 $n! < n^{n-1}$ (对于 $n \ge 3$)
这是一个典型的、需要归纳法来证明的不等式问题。我们发现，当 Prover Agent 直接尝试证明时，它会陷入困境。虽然它知道可能要用归纳法，但在没有清晰策略的情况下，生成的证明草稿充满了逻辑跳跃和未经验证的步骤，最终被 Lean 无情地驳回。
🤔 直接尝试的困境
在没有引理的帮助下，Prover Agent 生成的推理过程显得杂乱无章。它会尝试一些变换，但很快就迷失在复杂的代数表达式中，无法构建一个清晰的归纳步骤。最终生成的 Lean 代码因无法弥合归纳假设和结论之间的鸿沟而失败。
此时，引理生成机制启动了。智能体生成了几个引理，其中两个至关重要：
- 引理1 (基础情况): 证明 $n=4$ 时成立，即 $4! < 4^3$。这是一个简单的计算，24 < 64，被迅速证明。
- 引理2 (关键不等式): 证明对于 $k \ge 3$，有 $k^{k-1} < (k+1)^{k-1}$。这个引理看似简单，但它正是连接归纳步骤的关键桥梁。Prover Agent 也成功地证明了它。
带着这两个被验证过的"工具"，Prover Agent 再次挑战原问题。这一次，它的思路变得异常清晰：
归纳步骤 (从 k 到 k+1):
- 目标: 证明 $(k+1)! < (k+1)^k$。
- 展开: $(k+1)! = (k+1) \cdot k!$。
- 使用归纳假设: 因为 $k! < k^{k-1}$，所以 $(k+1) \cdot k! < (k+1) \cdot k^{k-1}$。
- 使用引理2: 我们需要证明 $(k+1) \cdot k^{k-1} < (k+1)^k$。两边同除以 $(k+1)$，就变成了证明 $k^{k-1} < (k+1)^{k-1}$。这正是我们已经证明的引理2！
瞧！原本的逻辑断层，被引理完美地填补了。这个案例生动地展示了，引理生成不只是分解问题，更是在主动寻找和构建证明策略中缺失的环节。这是从"盲目试错"到"策略性探索"的质变。
分领域性能分析
更有趣的是，我们发现Prover Agent在不同类型的数学问题上表现各异。在需要高度创造性思维的奥林匹克竞赛级别（Olympiad）问题上，它的表现尤为突出，甚至超越了那些使用更大模型和更多计算资源的方法。这再次印证了我们的猜想：结合非形式化推理的框架设计，对于解决需要"灵感"的难题至关重要。而在那些更依赖已有知识库和模式匹配的MATH和Custom类别问题上，模型大小和数据量的优势则体现得更明显。
结论与展望：迈向通用数学智能的一小步
回顾我们的探索，Prover Agent 的成功给予了我们深刻的启示：AI在数学推理领域的未来，可能不在于打造一个无所不能的"巨无霸"模型，而在于构建一个智能、高效、协同的智能体生态系统。我们的工作证明，通过让不同能力的"专家"模型各司其职、紧密合作，并赋予它们类似人类的"探索性"策略（如生成引理），我们能以更低的成本实现更高的智能。
这不仅仅是关于自动定理证明。我们所展示的模块化、反馈驱动的框架，为构建更可靠、更可解释的AI系统提供了一个范例。想象一下，未来这种框架可以应用于物理学理论的形式化验证、软件代码的自动纠错，甚至是新药研发的分子结构验证。只要一个领域存在"创造性假设"和"严格验证"的需求，我们的思想就能在那里生根发芽。
当然，这只是漫长征途的一小步。未来的路还很长：如何让引理生成得更"聪明"？如何让系统能从整个数学知识库中自动检索和学习？如何让人类数学家能更自然地与这样的AI智能体协作？这些都是我们接下来渴望探索的问题。
我坚信，我们正处在一个激动人心的时代的开端。在这个时代，AI将不再仅仅是计算的工具，而是成为人类探索科学与真理的伙伴。而Prover Agent，就是我们向着这个未来，迈出的坚定而充满希望的一步。
感谢大家的聆听。