StepFun-Prover: 一场机器思维的革命

摘要 (Abstract)

在追求通用人工智能的征途中，数学推理始终是衡量机器智能的黄金标准。近年来，大型语言模型（LLMs）虽在自然语言处理任务上取得了革命性突破，但在要求严谨逻辑与符号操作的形式化数学领域，其表现仍面临瓶颈。传统模型往往依赖于大量的“暴力”采样，即通过成千上万次的尝试来偶然“撞上”一个正确证明，这种方式效率低下且缺乏可解释性。本文中，我们（StepFun团队）提出了StepFun-Prover，一个专为形式化定理证明设计的创新大型语言模型。其核心突破在于引入了一种工具集成推理（Tool-Integrated Reasoning）机制，并结合了先进的强化学习管线。这一设计使模型不再是盲目地生成代码，而是能够像人类数学家一样，与Lean 4等形式化验证环境进行实时“对话”。模型会主动提出证明草图（sketch），将其提交给验证器（REPL），然后根据收到的反馈（feedback）——无论是成功信息还是错误提示——来迭代地修正和完善自己的证明策略。这种“思考-验证-反思”的闭环学习模式，极大地提升了证明的效率和准确性。在极具挑战性的miniF2F-test基准测试中，我们的32B模型在pass@1（即单次尝试成功率）指标上达到了惊人的70.0%，显著超越了以往所有同类模型。StepFun-Prover不仅在基准测试上树立了新的标杆，更重要的是，我们提出并实现了一套完整的、可复现的端到端训练框架。该框架为开发下一代具备工具集成推理能力的模型铺平了道路，预示着自动化定理证明乃至通用数学AI助手即将迎来一个全新的发展纪元。

引言：当机器学会“思考”与“试错”

大家好，我是本文的主创之一。今天，我想和大家分享一段激动人心的探索旅程——我们是如何教会一个AI模型，让它不仅仅是“计算”，而是真正地去“思考”和“证明”数学定理的。

想象一下，你面对一道复杂的数学题。你通常会怎么做？你不会一口气写下所有步骤，对吗？你会先有一个大致的思路，写下几步推导，然后检查一下：“嗯，这步对不对？方向有没有错？” 如果发现问题，你会退回去，换个角度再试试。这个过程，充满了试探、验证和修正。这，就是人类智慧的闪光点。

然而，长久以来，AI在做数学题时，更像一个蒙着眼睛的“大力士”。它们能凭借强大的算力，生成海量的解答方案，希望能有一个“蒙对”。这种方法在简单问题上或许有效，但面对真正复杂的、需要深度逻辑推理的定理时，就显得力不从心了。成功率低，资源消耗大，更重要的是，我们无法理解它的“思考”过程，它自己也无法从失败中学习。我们不禁自问：

我们能否让AI像人类一样，在证明过程中与环境互动，从错误中学习，并自主地调整策略，从而高效地找到答案呢？

这便是我们研发StepFun-Prover的初心。我们希望它不再是一个只会“背答案”的学生，而是一个懂得“如何学习”的思考者。我们为它打造了一个独特的学习框架，让它能与一个名为Lean 4的“严格的数学老师”（形式化验证环境）进行对话。我们的模型可以自由地提出自己的“草稿”，然后虚心地听取“老师”的反馈，再根据反馈进行修改。这个过程可以不断重复，直到“老师”点头认可，给出一个完整的、无懈可击的证明。

这不仅仅是一次技术上的迭代，我们认为，这是一场关于机器思维方式的“革命”。它让模型从一个封闭的、单向的输出者，变成了一个开放的、与环境双向互动的学习者。接下来，我将带大家深入了解这场革命的核心技术，以及我们是如何一步步将这个看似疯狂的想法变为现实的。

核心理念：三大支柱构建智能证明器

1. 工具集成推理：从“独白”到“对话”

传统LLM的工作模式，好比一位演员在舞台上进行一场漫长的独白。它根据剧本（输入的问题）一次性地输出所有台词（完整的证明），中间没有任何停顿或与外界的交流。如果台词说错了，只能整场戏从头再来。

而我们的工具集成推理（Tool-Integrated Reasoning），则将这场独白变成了一出精彩的互动剧。模型是主角，而Lean 4验证器（REPL）则是台下的评委。模型不再需要一次性完成所有表演，它可以先说一小段台词（生成一小段证明代码，我们称之为`sketch`），然后停下来，问问评委：“我这段表现如何？”

评委（REPL）会立刻给出反馈（`feedback`）：可能是“掌声”（代码正确），也可能是“嘘声”并指出问题所在（代码有误或逻辑不通）。模型接收到这个反馈后，会立刻进行反思，调整接下来的表演策略，然后继续下一段表演。这个“表演-反馈-调整”的循环可以无限进行下去，直到整个剧目完美落幕。

2. 冷启动与响应模式融合：站在巨人的肩膀上

要让一个模型从零开始学会这种复杂的互动模式，是非常困难的。因此，我们设计了一个巧妙的“冷启动”策略。我们首先收集了大量已有的、高质量的数学证明数据，就像给新手提供了丰富的教科书和习题集。我们利用了开源数据集，并借助强大的模型（如Kimina-Autoformalizer和Claude Sonnet）生成了初始的“教学材料”。

但我们很快发现一个问题：不同的“老师”（Kimina和Claude）教学风格迥异，直接混合在一起会让模型“精神分裂”。Kimina的风格严谨但有时略显刻板，而Claude的风格则更具创造性和对话性。为了解决这个问题，我们开发了一种响应模式融合（Response Patterns Fusion）技术。

我们先让模型学习Kimina的严谨风格，然后专门收集Kimina出错的案例，再利用我们已经具备初步对话能力的模型（M₀）去“纠正”这些错误。这个过程好比，我们让学生先学习了一套标准解题范式，然后专门针对这套范式的弱点进行强化训练，教它如何在标准范式走不通时，灵活地切换到更具探索性的对话模式。通过这种方式，我们的模型（M₁）成功地融合了两种风格的优点，既有严谨的骨架，又有灵活的血肉。

3. 工具集成强化学习：在实战中进化

有了具备基础对话能力的模型 M₁，我们就进入了最关键的阶段：工具集成强化学习（Tool-Integrated Reinforcement Learning）。这好比是将一个已经掌握了基础知识和解题技巧的学生，投入到一场大型的、连续不断的模拟考试中。

在这个阶段，我们使用了一种名为GRPO (Group-based Reward Policy Optimization)的强化学习算法。它的核心思想非常直观：对于同一道题，我们让模型生成一组（比如8个）不同的解题尝试（我们称之为`rollout`）。这些尝试包含了模型与Lean 4 REPL的完整互动轨迹。然后，我们对每个尝试进行最终评判：如果最终的证明通过了验证，奖励为1（成功）；否则，奖励为0（失败）。

这个“非黑即白”的奖励机制非常重要。它避免了复杂的、可能带有偏见的过程性奖励，只关注最终结果。这鼓励模型去大胆探索各种可能的、甚至看起来有些“离经叛道”的证明路径，只要最终能成功，就会被认为是好的策略。

GRPO算法会比较一组尝试中的成功与失败案例，计算出哪些行为模式（`action`）更有可能导向成功。然后，它会更新模型的内部参数（`policy`），使得模型在下一次遇到类似问题时，更倾向于采取那些曾带来成功的策略。这个过程就像一个学生在不断刷题、对答案、总结错题本，最终内化出高效的解题直觉。

数学上，这个更新过程可以被定义为最大化一个目标函数 \(\mathcal{J}(\theta)\)。其核心是优势函数 \(A_i\)，计算公式为： \[ A_i = \frac{r_i - \text{mean}(r_1, r_2, ..., r_G)}{\text{std}(r_1, r_2, ..., r_G)} \] 这里，\(r_i\) 是第 \(i\) 个尝试的奖励（0或1），\(G\) 是一组尝试的总数。这个公式的意义是：如果一个尝试成功了（\(r_i=1\)），而组内平均成功率很低，那么这个成功的尝试就获得了很高的“优势”（positive advantage），模型会大力学习它。反之，一个失败的尝试会获得负的优势，模型会避免类似的路径。通过不断优化，模型的整体表现（`policy` \(\pi_\theta\)）就会越来越好。

成果与分析：智慧的涌现

经过上述一系列精心的设计和训练，StepFun-Prover-Preview的表现没有让我们失望。在学术界公认的miniF2F-test基准上，我们的32B参数模型取得了70.0%的pass@1成功率。这是一个什么概念呢？这意味着，对于一个从未见过的新问题，我们的模型有七成的把握在第一次尝试时就给出完全正确的证明。这在之前是难以想象的，尤其是对于一个中等规模的模型而言。

更让我们兴奋的，不是冰冷的数字，而是模型在解决问题时展现出的“智慧火花”。我们观察到，模型自主地学会了多种高级的推理模式：

• 主动解决警告：即使REPL没有报错，只是给出一个警告（warning），模型也会主动去分析并优化代码，追求代码的完美性，这像极了一个有代码洁癖的优秀程序员。
• 动态调整策略：当一个证明步骤耗时过长（例如超过60秒），模型会判断这可能是一个死胡同，并主动放弃当前路径，重构证明，尝试新的方法。
• 从反馈中深度学习：在附录的案例中可以看到，模型在多次失败后，通过仔细分析REPL返回的复杂代数表达式，最终顿悟了问题的核心——一个基于平方和的代数恒等式，从而一举解决了问题。这种从具体反馈中抽象出数学本质的能力，是通往真正数学智能的关键一步。

我们还发现，模型的性能与其“思考”的深度（即允许的最大生成长度）正相关。当我们将最大长度从4096个token增加到20480个token时，成功率从58.3%稳步提升到了70.0%。这说明，给予模型更多的思考空间和时间，它就能通过更长的“对话”链条，解决更复杂的问题。

技术附录：幕后工程的艺术

A. Lean 4 REPL 远程服务器：为大规模训练铺平道路

强化学习，尤其是需要与外部工具频繁交互的强化学习，对计算资源和系统稳定性是巨大的考验。想象一下，在训练高峰期，我们需要同时处理数千个模型实例，每个实例都在与自己的Lean 4验证器进行高频次的“对话”。任何一个环节的延迟或崩溃，都会导致整个训练流程的停滞。

为了解决这个工程难题，我们设计并实现了一个高性能、高可用的Lean4-REPL远程服务器。其架构采用了经典的“生产者-中间人-消费者”（Producer-Broker-Consumer）模式。

• 生产者 (Producer)：我们的LLM训练集群。它们源源不断地生成证明草稿（sketch）。
• 中间人 (Broker)：我们使用了一个高性能的内存数据库Redis作为消息队列。它像一个巨大的、高效的邮局，负责接收所有来自生产者的“信件”（证明任务），并将其分发给消费者。
• 消费者 (Consumer)：一个由超过1000个并发运行的Lean4-REPL进程组成的庞大集群。它们从Redis获取任务，执行验证，然后将结果（feedback）发回。

这种异步、解耦的架构带来了巨大的好处：首先，它极大地提升了效率，LLM的生成和REPL的验证可以并行不悖，互不等待，整体训练速度提升了超过10倍。其次，它增强了系统的鲁棒性，即使部分REPL进程崩溃，也不会影响整个训练大局，保证了研究的顺利进行。我们还对Lean4-REPL本身进行了内存管理优化，并贡献给了社区。

B. 训练数据筛选：只给模型“跳一跳才能够得着”的难题

在强化学习中，训练数据的质量至关重要。如果我们总是给模型太简单的问题，它会“不思进取”；如果总是给太难的问题，它又会“习得性无助”。我们需要的，是那些“恰到好处”的、能激发模型潜能的问题。

为此，我们设计了一种动态的、在训练过程中进行的数据筛选策略。我们不是在训练开始前就定好所有题目，而是在RL训练的循环中，持续评估每个问题的“价值”。我们用一个辅助模型，对备选问题池进行初步测试，并计算每个问题的成功率。

我们只保留那些成功率严格介于0和1之间的问题。这意味着，我们剔除了那些模型总能轻易解决的“送分题”（成功率=1），也剔除了那些在当前能力下无论如何也解决不了的“天书”（成功率=0）。我们只聚焦于那些模型“时而能解，时而不能解”的问题。这些问题，正是驱动模型能力提升的“最佳营养品”。随着模型能力的增强，这个“最佳问题集”也会动态地发生变化，确保训练始终在模型的“最近发展区”进行。

结论与展望：迈向数学发现的新纪元

通过StepFun-Prover，我们证明了，让大型语言模型学会像人一样“思考-验证-反思”是完全可行的，并且能带来巨大的性能提升。我们提出的端到端训练框架，包括冷启动、响应模式融合、工具集成强化学习以及高效的工程实现，为该领域的研究者提供了一套强有力的蓝图。

这仅仅是一个开始。我们的下一步，是探索如何将这种在形式化系统中锤炼出的严谨推理能力，“迁移”回通用语言模型中，以提升它们在更广泛领域的逻辑思维能力。我们还梦想着构建一个由多个AI智能体（Agent）组成的系统，它们可以互相协作、辩论，共同探索未知的数学疆域，甚至做出真正原创性的数学发现。

我们相信，一个由人类智慧引导、由机器智能驱动的数学研究新范式，正在地平线上冉冉升起。而我们，有幸成为这场伟大变革的亲历者和推动者。