数学科研梯顶C
DeepSeek-Prover-V2:把「模型说它对」换成「Lean 说它对」
DeepSeek 的形式化定理证明模型:671B MoE 底座(与 DeepSeek-V3 同源)、目标语言 Lean 4,是在旗舰级底座上做形式化对齐。核心创新是冷启动的递归子目标分解:竞赛级命题一步证成功率极低、RL 几无正样本,于是先让 DeepSeek-V3 把命题拆成子目标串,再由 7B 小模型逐个证,合成的完整证明成了训练数据,即用可分解性换数据密度;RL 奖励二元,信号来自 Lean 内核。读数(厂商自报):MiniF2F-test 88.9%(pass@8192)、PutnamBench 49/658(约 7.4%)、自建 ProverBench 325 题。三个数一起读:MiniF2F 在该采样预算下已近饱和,换普特南立刻掉一个数量级;ProverBench 自家题自家跑要打折。公开仓库(约 1304 stars)含证法 ZIP,可直接在 Lean 里跑,可核验性比闭源高一档。边界:pass@8192 意味着八千多个候选再筛,与 pass@1 不可比。与 Kimina-Prover 的 92.2% 协议不可通约,本站并列收录不排名。置信度 C(厂商宣称):未在自有 Lean 4 + mathlib 环境复算。
88.9%MiniF2F-test厂商宣称 · 2025-07
DeepSeek-Prover-V2:把「模型说它对」换成「Lean 说它对」