DeepSeek发布开源定理证明模型Prover-V2 刷新数学推理基准纪录

2月22日消息，人工智能公司DeepSeek今日正式发布其最新开源定理证明模型DeepSeek-Prover-V2，该模型在数学推理领域取得重大突破，刷新了多项基准测试纪录。

据官方介绍，DeepSeek-Prover-V2是一款专注于数学定理自动证明的大型语言模型。在业界权威的MiniF2F基准测试中，该模型达到了88.9%的准确率，创下该测试的历史最高纪录，展现出卓越的数学推理能力。

更令人瞩目的是，DeepSeek-Prover-V2成功证明了Lean 4数学库Mathlib中49个此前未被解决的数学定理。Mathlib是目前最大的形式化数学库之一，包含大量经过严格形式化验证的数学定理和证明。能够攻克其中的未解难题，充分证明了该模型在复杂数学推理方面的强大实力。

DeepSeek选择将Prover-V2完全开源，延续了其一贯的开放策略。此举将为全球数学研究者和AI开发者提供强大的工具支持，有望推动自动定理证明技术的进一步发展。

业内专家表示，自动定理证明是人工智能领域最具挑战性的任务之一，需要模型具备深度逻辑推理和符号运算能力。DeepSeek-Prover-V2的突破性表现，标志着AI在数学推理领域迈出了重要一步，未来有望在数学研究、软件验证、密码学等领域发挥重要作用。