昨日，深度求索（DeepSeek）在Hugging Face平台上发布了全新模型DeepSeek-Prover-V2-671B，并同步公开了相关论文信息。这款开源大型语言模型专注于形式化数学推理，基于DeepSeek-V3-0324架构开发，旨在提升复杂定理证明能力。
DeepSeek-Prover-V2-671B通过递归定理证明管道生成初始数据，并结合子目标分解与Lean 4平台的形式化证明步骤，显著增强了数学推理能力。同时，团队还推出了规模较小的增强模型DeepSeek-Prover-V2-7B及ProverBench数据集，后者包含325个形式化数学问题，覆盖高中竞赛至本科数学多个领域。
实验结果显示，DeepSeek-Prover-V2-671B在MiniF2F-test数据集上的通过率达88.9%，并在PutnamBench数据集中解决49个难题，展现了其在神经定理证明领域的卓越表现。这一成果为形式化数学推理提供了新思路。
