策略错位训练与部署之间的核心矛盾形式化定理证明一直是LLM公认最严苛的推理试金石每一步推导都必须通过Lean 4内核的机器验证。近两年开源社区在MiniF2F、PutnamBench等benchmark上的成绩持续上升但增长路径越来越趋同扩模型、扩数据、部署阶段叠加检索和多轮修正。一个关键问题始终存在检索信号、编译器反馈和失败修复大多只在部署时作为外部流程接入模型在训练阶段并没有系统学习如何利用这些信号形成了训练与部署之间的“策略错位”。为应对这一挑战M - A - P开源社区与南京大学等团队提出OProver—— 一个将检索增强、编译器反馈与多轮修复直接内化到训练策略中的Lean 4定理证明框架。轻量、可端到端训练部署阶段有限轮次修复循环。OProver把定理证明建模为一个有限轮次的修复循环。策略基于目标形式化陈述、检索记忆库中的top - k个编译器验证证明、上一轮证明尝试和Lean 4编译器返回的诊断信息生成下一次证明尝试。任意一轮通过整条trajectory即视为成功。训练阶段两阶段训练。持续预训练CPT在约65B token的混合语料上预训练其中约30%来自OProofs的Lean 4数据20%为代码数据OpenCoder40%为数学语料Nemotron - Math - 4 - Plus10%为长CoT数据迭代后训练交替进行agentic proving rollout、SFT基于round - level修复样本和RL基于GSPO算法与难题集。关键设计在于检索结果、失败尝试和编译器反馈不再只是部署阶段临时接入的外部流程而是被纳入模型要学习的证明策略。数据与模型的协同进化OProofs语料库与prover策略在迭代中相互促进。每轮迭代中当前prover在题库上生成的新验证证明被加入OProofs并索引进检索记忆库修复trajectory成为下一轮SFT训练样本尚未解决的”难题组”为下一轮RL提供训练信号。数据、训练与策略形成持续演化的闭环。OProofs面向agentic prover的Lean 4语料。研究团队同步构建并开源了OProofs包含约1.76M条形式化陈述、6.80M条编译器验证证明。其中4.29M条证明保留了检索到的相关证明上下文859K条样本包含此前失败尝试的Lean编译器反馈。模型不只看到”最终正确证明是什么”也能学习”证明失败后如何利用检索结果和编译器反馈继续修复”。OProofs由两条构建分支组成。1、公开资源再证明以NuminaMath - LEAN、Lean - Workbook、Leanabell - Prover - FormalStmt等公开Lean资源为起点清洗去重后通过agentic proving重新生成并验证证明同时收集检索上下文、失败尝试和修复轨迹。2、自然语言到形式化从Common Crawl和GitHub挖掘数学陈述用CriticLean自动形式化为Lean 4再通过agentic proving流程生成并验证证明。从覆盖范围看OProofs横跨多个数学方向代数60.1%、分析13.7%、数论13.0%、几何6.8%。难度分布以elementary27.4%和high - school48.9%层级为主同时包含18.9%的本科水平和4.8%的研究生水平问题。五项评测三项第一、两项第二研究团队在MiniF2F、MathOlympiad、ProofNet、ProverBench、PutnamBench五个Lean 4 benchmark上评估默认报告Pass32基于n 64条独立multi - round rollouts的无偏估计。在open - weight whole - proof prover范围内OProver - 32B有三项关键结论1、32B全面超越671BOProver - 32B在全部五项评测中超越DeepSeek - Prover - V2671B在MiniF2F93.3、ProverBench58.2、PutnamBench11.3上同时领先LongCat - Flash - Prover w/ TIR560B。2、8B打平32BOProver - 8B在五个benchmark上全部超越Goedel - Prover - V2 - 32B参数量少4倍。3、迭代后训练持续增益MiniF2F - Test上OProver - 8B从79.5提升至91.812.3OProver - 32B从84.7提升至93.38.6。消融实验检索与编译器反馈协同贡献移除多轮compiler feedback会导致最大幅度下降OProver - 32B在PutnamBench从11.3降至7.0在ProofNet从33.2降至25.8。进一步移除检索后性能继续下降至5.9和24.7。这说明提升并非来自简单的best - of - N采样而是来自检索增强的证明生成与编译器反馈引导的多轮修复之间的协同。其中Lean编译器反馈提供主要修复信号检索上下文提供相关证明结构和可参考的证明片段。测试时扩展更多推理预算稳定转化随着推理预算从8增加到256OProver - 32B在五个benchmark上均呈稳定提升MiniF2F从87.5至92.8MathOlympiad从15.5至22.0ProofNet从25.6至32.8ProverBench从51.3至56.9PutnamBench从6.4至11.3。最优预算分配与benchmark难度相关多数benchmark更偏向增加refinement深度而PutnamBench这类低成功率难题需在修复深度与并行探索之间取得平衡。开源与发布研究团队同步开源了OProver的模型、数据与训练代码覆盖不同训练阶段checkpoint、OProofs语料和训练pipeline。 • m - a - p/OProver - 32B / OProver - 8B — 最终模型 • m - a - p/OProver - 32B - Base / Round1 — 32B各阶段checkpoint • m - a - p/OProver - 8B - Base / Round1 / Round2 — 8B各阶段checkpoint • m - a - p/OProofs — 1.76M statements / 6.80M proofs / 1.06M trajectories。当然OProver目前仍主要围绕Lean 4 whole - proof proving展开。后续值得观察的是这种agentic refinement框架能否迁移到Coq、Isabelle以及工程级formal methods工具以及更长的数据与模型协同进化周期中性能提升会持续多久。
OProver：内化检索与修复的Lean 4定理证明框架，五项评测多项领先，代码数据全开源
策略错位训练与部署之间的核心矛盾形式化定理证明一直是LLM公认最严苛的推理试金石每一步推导都必须通过Lean 4内核的机器验证。近两年开源社区在MiniF2F、PutnamBench等benchmark上的成绩持续上升但增长路径越来越趋同扩模型、扩数据、部署阶段叠加检索和多轮修正。一个关键问题始终存在检索信号、编译器反馈和失败修复大多只在部署时作为外部流程接入模型在训练阶段并没有系统学习如何利用这些信号形成了训练与部署之间的“策略错位”。为应对这一挑战M - A - P开源社区与南京大学等团队提出OProver—— 一个将检索增强、编译器反馈与多轮修复直接内化到训练策略中的Lean 4定理证明框架。轻量、可端到端训练部署阶段有限轮次修复循环。OProver把定理证明建模为一个有限轮次的修复循环。策略基于目标形式化陈述、检索记忆库中的top - k个编译器验证证明、上一轮证明尝试和Lean 4编译器返回的诊断信息生成下一次证明尝试。任意一轮通过整条trajectory即视为成功。训练阶段两阶段训练。持续预训练CPT在约65B token的混合语料上预训练其中约30%来自OProofs的Lean 4数据20%为代码数据OpenCoder40%为数学语料Nemotron - Math - 4 - Plus10%为长CoT数据迭代后训练交替进行agentic proving rollout、SFT基于round - level修复样本和RL基于GSPO算法与难题集。关键设计在于检索结果、失败尝试和编译器反馈不再只是部署阶段临时接入的外部流程而是被纳入模型要学习的证明策略。数据与模型的协同进化OProofs语料库与prover策略在迭代中相互促进。每轮迭代中当前prover在题库上生成的新验证证明被加入OProofs并索引进检索记忆库修复trajectory成为下一轮SFT训练样本尚未解决的”难题组”为下一轮RL提供训练信号。数据、训练与策略形成持续演化的闭环。OProofs面向agentic prover的Lean 4语料。研究团队同步构建并开源了OProofs包含约1.76M条形式化陈述、6.80M条编译器验证证明。其中4.29M条证明保留了检索到的相关证明上下文859K条样本包含此前失败尝试的Lean编译器反馈。模型不只看到”最终正确证明是什么”也能学习”证明失败后如何利用检索结果和编译器反馈继续修复”。OProofs由两条构建分支组成。1、公开资源再证明以NuminaMath - LEAN、Lean - Workbook、Leanabell - Prover - FormalStmt等公开Lean资源为起点清洗去重后通过agentic proving重新生成并验证证明同时收集检索上下文、失败尝试和修复轨迹。2、自然语言到形式化从Common Crawl和GitHub挖掘数学陈述用CriticLean自动形式化为Lean 4再通过agentic proving流程生成并验证证明。从覆盖范围看OProofs横跨多个数学方向代数60.1%、分析13.7%、数论13.0%、几何6.8%。难度分布以elementary27.4%和high - school48.9%层级为主同时包含18.9%的本科水平和4.8%的研究生水平问题。五项评测三项第一、两项第二研究团队在MiniF2F、MathOlympiad、ProofNet、ProverBench、PutnamBench五个Lean 4 benchmark上评估默认报告Pass32基于n 64条独立multi - round rollouts的无偏估计。在open - weight whole - proof prover范围内OProver - 32B有三项关键结论1、32B全面超越671BOProver - 32B在全部五项评测中超越DeepSeek - Prover - V2671B在MiniF2F93.3、ProverBench58.2、PutnamBench11.3上同时领先LongCat - Flash - Prover w/ TIR560B。2、8B打平32BOProver - 8B在五个benchmark上全部超越Goedel - Prover - V2 - 32B参数量少4倍。3、迭代后训练持续增益MiniF2F - Test上OProver - 8B从79.5提升至91.812.3OProver - 32B从84.7提升至93.38.6。消融实验检索与编译器反馈协同贡献移除多轮compiler feedback会导致最大幅度下降OProver - 32B在PutnamBench从11.3降至7.0在ProofNet从33.2降至25.8。进一步移除检索后性能继续下降至5.9和24.7。这说明提升并非来自简单的best - of - N采样而是来自检索增强的证明生成与编译器反馈引导的多轮修复之间的协同。其中Lean编译器反馈提供主要修复信号检索上下文提供相关证明结构和可参考的证明片段。测试时扩展更多推理预算稳定转化随着推理预算从8增加到256OProver - 32B在五个benchmark上均呈稳定提升MiniF2F从87.5至92.8MathOlympiad从15.5至22.0ProofNet从25.6至32.8ProverBench从51.3至56.9PutnamBench从6.4至11.3。最优预算分配与benchmark难度相关多数benchmark更偏向增加refinement深度而PutnamBench这类低成功率难题需在修复深度与并行探索之间取得平衡。开源与发布研究团队同步开源了OProver的模型、数据与训练代码覆盖不同训练阶段checkpoint、OProofs语料和训练pipeline。 • m - a - p/OProver - 32B / OProver - 8B — 最终模型 • m - a - p/OProver - 32B - Base / Round1 — 32B各阶段checkpoint • m - a - p/OProver - 8B - Base / Round1 / Round2 — 8B各阶段checkpoint • m - a - p/OProofs — 1.76M statements / 6.80M proofs / 1.06M trajectories。当然OProver目前仍主要围绕Lean 4 whole - proof proving展开。后续值得观察的是这种agentic refinement框架能否迁移到Coq、Isabelle以及工程级formal methods工具以及更长的数据与模型协同进化周期中性能提升会持续多久。
