DeepSeek发布开源定理证明模型Prover-V2 MiniF2F基准测试准确率达88.9%

2月22日，人工智能公司DeepSeek正式发布并开源其最新定理证明模型DeepSeek-Prover-V2。该模型专为Lean 4形式化数学证明设计，在权威基准测试中刷新多项纪录，标志着AI在数学推理领域取得重要突破。

据DeepSeek官方技术文档介绍，DeepSeek-Prover-V2采用创新的递归定理证明流程，由DeepSeek-V3提供子目标分解和形式化支持。模型通过强化学习将非形式推理与形式化证明统一到单一框架中，实现了推理能力的显著提升。

在性能表现方面，DeepSeek-Prover-V2-671B版本在MiniF2F-test基准测试中达到88.9%的通过率，创下该测试历史最高纪录。此外，该模型还成功解决了PutnamBench中658道题目中的49道，展现出在高难度数学竞赛题目上的强大能力。

DeepSeek同步发布了ProverBench基准数据集，包含325道形式化数学题目。其中15道来自2024和2025年美国数学邀请赛（AIME），310道来自教科书示例，为学术界提供了更全面的评估工具。

业内人士分析，自动定理证明是人工智能最具挑战性的任务之一，需要模型具备深度逻辑推理和符号运算能力。DeepSeek-Prover-V2的开源将为数学研究、软件验证、密码学等领域提供有力工具支持。

目前，该模型已在GitHub开源，开发者可通过官方仓库获取完整代码和模型权重。

信息来源

• DeepSeek官方GitHub仓库：github.com/deepseek-ai/DeepSeek-Prover-V2
• 官方技术论文：DeepSeek_Prover_V2.pdf

可信度：95/100（官方一手来源，技术论文验证）