DeepSeek-Prover-V2 及其形式化数学评测结果

摘要

30 秒看懂

Matthew Berman 简要介绍 DeepSeek-Prover-V2，并引用一位 DeepSeek 研究人员的基准测试说法。这些结果涉及特定评估条件下的形式化数学证明，并不意味着模型能解决所有数学问题。

1数学证明模型Berman 介绍 DeepSeek-Prover-V2，并强调其数学能力。
2miniF2F 与 PutnamBench一位 DeepSeek 研究人员报告，该模型在 miniF2F 上接近 90%，并在 PutnamBench 上取得提升。结果取决于模型和评估预算。
3形式化 AIME 问题研究人员还报告，模型在部分 AIME 2024 和 2025 问题的形式化版本上取得了一定成果。

要点建议

DeepSeek-Prover-V2 面向 Lean 4 中的形式化定理证明。
DeepSeek 报告称，671B 模型在 miniF2F 测试集上达到 88.9%，每题最多尝试 8192 次证明。
研究人员报告解决了 658 道 PutnamBench 问题中的 49 道，并给出了部分形式化 AIME 问题的结果。
视频转述了研究人员报告的结果，没有独立测试模型。

主题Mathematics AI research Benchmarks 模型与训练

全文

按章节阅读整理后的全文

对照原始文稿

只看原始文稿

DeepSeek-Prover-V2

Berman 介绍该模型及其数学领域的重点。这次发布针对形式化定理证明。

推出 DeepSeek-R1 的公司 DeepSeek 发布了 DeepSeek-Prover-V2。我对其报告的数学表现印象深刻。该模型面向 Lean 4 中的形式化定理证明，这比解决任意数学方程的范围更具体。

报告的基准测试结果

他引用一位研究人员关于 miniF2F 和 PutnamBench 的说法。这项比较使用了特定的证明搜索条件。

据一位 DeepSeek 研究人员称，该模型解决了接近 90% 的 miniF2F 问题，并显著提升了 PutnamBench 的结果。[技术报告](https://arxiv.org/abs/2504.21801)称，671B 模型在 miniF2F 测试集上达到 88.9%，每题最多尝试 8192 次证明，并解决了 658 道 PutnamBench 问题中的 49 道。这些是研究人员在特定评估条件下报告的结果，并非单次尝试的成功率。

AIME 与模型比较

Berman 强调形式化 AIME 问题的结果和模型对比图，并鼓励观众尝试该模型。

幻灯片 1 / 1DeepSeek 报告的证明基准测试图表比较报告的 miniF2F、PutnamBench 和部分 AIME 结果；各项评估设置不同。

该研究人员还报告，模型在形式化的 AIME 2024 和 2025 问题上取得了一定的成功率。报告中的 ProverBench 包含 15 道选定的 AIME 问题；所展示的比较区分了形式化证明生成与非形式化答案任务。图表显示所列模型之间存在明显差异，我鼓励观众尝试 DeepSeek-Prover-V2。这段短视频没有独立测试这些说法。