DeepSeek 发布 DeepSeek-Prover-V2，具有递归证明搜索和新的 ProverBench 基准

DeepSeek AI 发布了 DeepSeek-Prover-V2，这是一个用于在 Lean 4 中进行形式化定理证明的开源大型语言模型。它使用递归流程通过 DeepSeek-V3 生成训练数据，在 MiniF2F 和 PutnamBench 上取得了最先进的结果，并引入了包含 325 个问题的新基准 ProverBench。

DeepSeek AI 发布了 DeepSeek-Prover-V2，这是一个用于在 Lean 4 中进行形式定理证明的开源大语言模型。该模型采用递归定理证明流程，利用 DeepSeek-V3 生成高质量的初始化数据，方法是将复杂定理分解为子目标并形式化这些子目标。然后，一个 7B 参数的模型证明这些子目标，完整的证明与 DeepSeek-V3 的思维链推理配对，用于训练。基于二元反馈的强化学习进一步优化了模型。671B 参数版本在 MiniF2F 测试中达到 88.9%，并解决了 PutnamBench 658 个问题中的 49 个。DeepSeek 还引入了 ProverBench，这是一个包含来自 AIME 竞赛和教科书的 325 个问题的数据集，用于评估数学推理。该模型提供两种规模：7B 和 671B 参数。

来源: Synced — 原文