70%准确率+小模型革命：StepFun-Prover如何重新定义AI数学推理-洪萨配资

70%准确率+小模型革命：StepFun-Prover如何重新定义AI数学推理

【免费下载链接】StepFun-Prover-Preview-7B项目地址: https://ai.gitcode.com/StepFun/StepFun-Prover-Preview-7B

导语

阶跃星辰团队发布的StepFun-Prover-Preview-7B模型以8B参数规模实现70% MiniF2F-test准确率，通过"生成-验证-修正"的类人推理框架，开创了小模型战胜大模型的定理证明新范式。

行业现状：大模型的数学推理困境

当前大语言模型在自然语言处理领域取得突破性进展，但在需要严格逻辑验证的数学定理证明领域仍面临重大挑战。InfoQ最新研究指出，主流模型直接生成机器可验证的形式化证明能力较弱，在MiniF2F-test等权威基准上，传统模型如DeepSeek-Prover-V2-671B和Kimina-Prover-72B的Pass@1准确率长期徘徊在60%-65%区间。

这种困境催生了"工具集成推理"新方向——让大模型像人类数学家一样，通过与定理证明助手（如Lean4）交互来完善证明过程。StepFun-Prover-Preview系列模型正是这一方向的突破性成果，尤其值得注意的是，其7B版本仅以8B参数规模就达到了与671B参数的DeepSeek-Prover-V2相当的性能。

如上图所示，表格清晰展示了StepFun-Prover系列与其他主流模型的性能对比。StepFun-Prover-Preview-7B以8B参数规模达到了与671B参数的DeepSeek-Prover-V2相当的性能，而32B版本更是以70%的准确率超越所有已知同类模型4%以上。这一"以小胜大"的突破为AI数学推理提供了新的发展思路。

核心亮点：三大技术突破实现类人推理

1. 动态推理框架：像调试代码一样修正证明

StepFun-Prover最核心的创新在于提出动态推理框架，使模型能够自主控制与Lean4环境的交互。这一过程类似程序员调试代码：生成部分证明草图并包裹在<sketch>标签中，发送至Lean4环境执行获取反馈，再分析反馈修正步骤，直至验证通过。

在最大公约数(gcd)与最小公倍数(lcm)关系证明案例中，模型最初因使用interval_casestactic导致验证超时，通过分析REPL反馈，转而采用"变量替换+因数分解"的数学方法，成功将证明时间从60秒以上缩短至3秒内。这种"生成-验证-修正"的循环机制，使模型能够处理复杂的数学推理任务。

2. 两阶段训练：从基础能力到专家水平

团队采用分阶段训练策略构建模型能力：首先通过监督微调(SFT)建立基础代码补全能力和环境交互技能，然后使用GRPO算法进行工具集成强化学习(RL)。创新性采用"RL-SFT-RL"迭代优化：将强化学习中失败率高但最终成功的推理路径，筛选后重新用于监督微调。

该图展示了StepFun-Prover-Preview的工具集成强化学习（RL）训练管道与推理流程，包含初始模型微调（SFT）、工具交互（Kimina-Prover）、迭代反馈优化及Lean Server验证证明等环节，用于形式化数学问题的定理证明。这种训练方法使模型能够高效掌握复杂的数学推理技巧。

3. 性能跃升：小模型战胜大模型的实证

在MiniF2F-test基准测试中，StepFun-Prover系列展现出显著优势。通过优化推理过程而非单纯增加参数量，模型实现了效率突破。测试数据显示，StepFun-Prover-Preview-7B在经过3-5轮环境交互后，准确率显著提升，最终达到70%的Pass@1水平，超越了参数规模大10倍的竞品模型。

行业影响：从数学证明到可信AI系统

StepFun-Prover的技术路径为AI推理能力提升提供了新思路，其影响已超出数学领域：

软件开发：模型展现的"形式化验证"能力可直接应用于代码正确性验证，特别是在区块链智能合约、自动驾驶系统等对安全性要求极高的场景。
科学发现：在物理、化学等需要复杂公式推导的领域，该技术可辅助科研人员验证假设、发现新定理。StepFun团队已基于相同技术路径开发StepFun-Formalizer模型，在数学形式化任务中实现84%准确率。
教育领域：动态推理过程可生成详细的解题步骤和错误分析，为个性化数学教育提供技术支撑。清华大学数学科学系已将其用于形式化数学教学实验，使学习效率提升50%。

快速上手指南

环境准备

StepFun-Prover已开源，可通过以下命令获取：

git clone https://gitcode.com/StepFun/StepFun-Prover-Preview-7B

模型支持vLLM推理框架，推荐配置：显存≥24GB（支持4卡张量并行），Python 3.10+, PyTorch 2.0+, Lean4环境。

基础使用示例

from vllm import LLM, SamplingParams from transformers import AutoTokenizer model_name = "Stepfun/Stepfun-Prover-Preview-7B" model = LLM( model=model_name, tensor_parallel_size=4, ) tokenizer = AutoTokenizer.from_pretrained(model_name, trust_remote_code=True) formal_problem = """ import Mathlib theorem test_theorem (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) : (x^2 - z^2) / (y + z) + (y^2 - x^2) / (z + x) + (z^2 - y^2) / (x + y) ≥ 0 := by """.strip() system_prompt = "You will be given an unsolved Lean 4 problem. Think carefully and work towards a solution. At any point, you may use the Lean 4 REPL to check your progress by enclosing your partial solution between <sketch> and </sketch>. The REPL feedback will be provided between <REPL> and </REPL>. Continue this process as needed until you arrive at a complete and correct solution." user_prompt = f"```lean4\n{formal_problem}\n```" dialog = [ {"role": "system", "content": system_prompt}, {"role": "user", "content": user_prompt} ] prompt = tokenizer.apply_chat_template(dialog, tokenize=False, add_generation_prompt=True) sampling_params = SamplingParams( temperature=0.999, top_p=0.95, top_k=-1, max_tokens=16384, stop_token_ids=[151643, 151666], # <｜end▁of▁sentence｜>, </sketch> include_stop_str_in_output=True, ) output = model.generate(prompt, sampling_params=sampling_params) output_text = output[0].outputs[0].text print(output_text)