DeepSeek-Prover-V2：强化学习赋能的定理证明模型

DeepSeek-Prover-V2是一个开源大型语言模型，用于在Lean 4中进行形式化定理证明。它通过结合DeepSeek-V3的递归定理证明流水线和强化学习，将非形式化和形式化数学推理结合起来。该模型首先利用DeepSeek-V3将复杂问题分解成子目标，然后合成子目标的证明，创建强化学习的初始数据。最终，DeepSeek-Prover-V2-671B在MiniF2F-test上达到了88.9%的通过率，并在PutnamBench上解决了49个问题。同时，还发布了ProverBench，一个包含325个问题的基准数据集，涵盖了高中和大学水平的数学问题。