主要证据
- Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-CorrectionS1 · 主要研究来源 · 论文 · 2025-08-05
- Goedel-Prover-V2 model and theorem-proving repositoryS1 · 主要研究来源 · 代码仓库
Goedel-Prover-V2 通过自我纠错扩展开放定理证明
系统采用脚手架式数据合成、验证器引导的迭代修复与模型平均。
发生了什么？
Goedel-Prover-V2-32B 报告在自我纠错模式下 miniF2F 达到 90.4%，并在其评测设置中解出 86 道 PutnamBench。
为什么重要？
它强化了“小型开放证明器通过测试时纠错而非只增大参数规模获得能力”的路线。
重要性说明：Goedel-Prover-V2 展示了分阶段合成数据与 Lean 引导自我纠错能让较小开放模型达到很强的形式证明性能。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E3 · 可检查工件
- AI 角色
- AI 主导、人类核验
- 形式保障
- 机器检查
贡献与验证
- 数学新颖性
- 基准结果
- 接口
- 形式化, 符号
- AI 贡献
- 模型生成 Lean 证明并根据编译器反馈迭代修复。
- 人类贡献
- 研究者设计分阶段数据合成、自我纠错与模型合并流程。
- 验证状态
- 论文已发布 · E3 · 可检查工件 · 机器检查
- 最后审阅
- 2026-09-11
技术细节
- 系统
- goedel-prover-v2, lean
- 机构
- princeton-university, nvidia
- 数学问题
- minif2f, putnambench
- 方法
- self-correction, synthetic-data, formal-proof
全部来源与工件
- Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-CorrectionS1 · 主要研究来源 · 论文 · 访问于 2026-09-10
- Goedel-Prover-V2 model and theorem-proving repositoryS1 · 主要研究来源 · 代码仓库 · 访问于 2026-09-11
验证历史
- 2025-08-05 · 论文已发布 · E2 · 研究记录
Chronicle 依据所引 primary / official source 记录该事件；该状态不表示 Chronicle 已完成独立验证。
- 2026-09-11 · 论文已发布 · E3 · 可检查工件
本轮 corpus 刷新增补了由作者或发布机构维护、可直接检查的公开产物。E3 表示证据已达到可检查 artifact 层级，并不等同于底层科学或数学主张已获得独立验证。
更正
当前没有记录的更正。