主要证据
- InternLM2.5-StepProver: Advancing Automated Theorem Proving via Expert Iteration on Large-Scale LEAN ProblemsS1 · 主要研究来源 · 论文 · 2024-10-21
- InternLM-Math repository containing StepProver release links and resourcesS1 · 主要研究来源 · 代码仓库
InternLM2.5-StepProver 在大规模 Lean 问题集上扩展专家迭代
系统在大规模 Lean 数据上执行专家迭代，并使用 critic 选择相对容易的问题、引导更深证明搜索。
发生了什么？
InternLM2.5-StepProver 报告 miniF2F-test 65.9%，并证明或反驳 Lean-Workbook-Plus 中 17.0% 的问题。
为什么重要？
它提供了一个开放实证案例，显示形式证明性能如何随数据、搜索和算力扩展。
重要性说明：StepProver 展示了大规模问题库与高算力专家迭代如何持续提升开放形式定理证明性能。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E3 · 可检查工件
- AI 角色
- AI 主导、人类核验
- 形式保障
- 机器检查
贡献与验证
- 数学新颖性
- 基准结果
- 接口
- 形式化, 符号
- AI 贡献
- 证明器搜索 Lean 证明、用成功结果继续训练，并通过学习式 critic 分配搜索资源。
- 人类贡献
- 研究者构建大规模专家迭代管线并整理 Lean 数据。
- 验证状态
- 论文已发布 · E3 · 可检查工件 · 机器检查
- 最后审阅
- 2026-09-11
技术细节
- 系统
- internlm2.5-stepprover, lean
- 机构
- shanghai-ai-laboratory
- 数学问题
- minif2f, lean-workbook-plus, putnambench
- 方法
- expert-iteration, critic-model, proof-search
全部来源与工件
- InternLM2.5-StepProver: Advancing Automated Theorem Proving via Expert Iteration on Large-Scale LEAN ProblemsS1 · 主要研究来源 · 论文 · 访问于 2026-09-10
- InternLM-Math repository containing StepProver release links and resourcesS1 · 主要研究来源 · 代码仓库 · 访问于 2026-09-11
验证历史
- 2024-10-21 · 论文已发布 · E2 · 研究记录
Chronicle 依据所引 primary / official source 记录该事件；该状态不表示 Chronicle 已完成独立验证。
- 2026-09-11 · 论文已发布 · E3 · 可检查工件
本轮 corpus 刷新增补了由作者或发布机构维护、可直接检查的公开产物。E3 表示证据已达到可检查 artifact 层级，并不等同于底层科学或数学主张已获得独立验证。
更正
当前没有记录的更正。