形式化定理证明新范式发布 - 阶跃星辰正式发布并开源形式化定理证明大模型StepFun-Prover-Preview-7B和StepFun-Prover-Preview-32B [1] - 模型采用基于环境反馈的强化学习训练流程，模拟人类推理过程中的实时交互与修正 [2] - 模型在基准测试集miniF2F-test上表现优异，32B版本pass@1通过率达70%，领先已知模型4%以上 [9][10] 技术架构与训练方法 两阶段监督微调 - 分阶段微调策略使模型获得工具使用基础能力 [4] - 第一阶段利用开源Lean 4数据建立代码补全能力 [5] - 第二阶段通过高质量冷启动数据训练模型理解数学题求解与Lean验证的交互 [5] 工具集成强化学习 - 采用GRPO算法进行强化学习训练，赋予模型自然语言解题能力 [5] - 模型可主动插入标签生成Lean 4代码并执行，通过反馈实现调试式修正 [5][6] - 奖励函数设计为REPL验证通过得1分，失败得0分 [7] 迭代优化机制 - 采用"RL-SFT-RL"循环优化方法，逐步提升模型推理能力 [8] - 筛选强化学习中成功的高难度样本重新用于监督微调，增强推理鲁棒性 [12] 性能表现与案例 - StepFun-Prover-Preview-7B以66% pass@1准确率超越DeepSeek-Prover-V2-671B(61.9%)和Kimina-Prover-72B(63.9%) [10] - 案例显示模型能主动去除冗余证明步骤、根据超时反馈调整结构、基于环境反馈有效改错 [10][13][15] 资源与后续计划 - 模型已开源在GitHub和Huggingface平台，技术报告发布于arXiv [17] - 团队将持续探索形式化推理模型方向 [16]