DeepSeek-Prover-V1.5解读

xuebodx

808人浏览 · 2025-03-16 09:05:22

xuebodx · 2025-03-16 09:05:22 发布

1. 摘要

DeepSeek-Prover-V1.5是DeepSeek为Lean 4中的定理证明而设计的开源语言模型。该模型是在DeepSeekMath-Base 基础上训练出来的，该模型一共有三个版本，分别是DeepSeek-Prover-V1.5-Base，DeepSeek-Prover-V1.5-SFT和DeepSeek-Prover-V1.5-RL。DeepSeek-Prover-V1.5 相较于 DeepSeek-Prover-V1 有显著的提升，虽然参数量只有7B，但是在高中水平 miniF2F 基准（63.5%）和本科水平 ProofNet 基准（25.3%）的测试集上均取得了新的最优结果。

2. DeepSeek-Prover-V1.5

2.1 DeepSeek-Prover-V1.5-Base

为了提高我们的语言模型生成形式化证明和通过数学语言进行推理的能力，我们进一步预训练了基础模型DeepSeekMath-Base。这一改进涉及对包含代码和自然语言数学内容的高质量数据集进行预训练。

2.2 DeepSeek-Prover-V1.5-SFT

为了提高模型的数学定理证明能力，在DeepSeek-ProverV1.5-Base模型上进行了监督微调。微调证明数据集由 9645k个序列组成，包含大量的来自高中和本科数学竞赛问题。

2.3 DeepSeek-Prover-V1.5-RL

强化学习 (RL) 已被证明能够有效增强有监督微调语言模型的数学推理能力。为了进一步增强 DeepSeek-Prover-V1.5-SFT，我们加入了强化学习阶段，从而形成了 DeepSeek-Prover-V1.5-RL 模型。此阶段利用 RL 根据 Lean 4 证明器的验证反馈来提高性能。此 RL 过程的具体细节如下所述。
　　Prompts。在强化学习阶段，我们使用有监督微调数据集中的一组定理陈述作为RL训练的提示。我们选择 DeepSeekProver-V1.5-SFT 在多次尝试后生成正确证明的成功率适中的定理。这确保模型有改进空间，同时仍然能够收到积极的反馈。经过筛选，我们保留了大约 4.5k 个独特的定理陈述。每个定理都以 CoT 和非 CoT 提示作为前缀，以增强模型在两种模式下的证明生成能力。
　　Rewards。当通过 RL 训练 LLM 时，训练好的奖赏模型通常会提供反馈信号。相比之下，形式化定理证明受益于证明助手对生成的证明的严格验证，从而提供了显著的优势。具体来说，如果验证正确，则每个生成的证明将获得 1 的奖赏，否则将获得 0 的奖励。

　　RL。我们采用组相对策略优化 (GRPO) 作为我们的 RL 算法，与 PPO 相比，该算法表现出了卓越的有效性和效率，主要是因为它消除了训练额外critic模型的必要性。具体来说，GRPO 为每个定理提示抽取一组候选证明，并根据组内输出的相对奖励优化模型。我们的提示选择策略旨在尽可能在候选中包括正确和不正确的证明，这与 GRPO 的群组相对性质非常吻合，从而增强了训练过程。
　　Training Setting。我们基于 SFT 模型进行强化学习训练，该模型既是初始模型，也是施加 Kullback-Leibler (KL) 散度惩罚的参考模型。我们使用 5e-6 的恒定学习率，KL 惩罚系数设置为 0.02。对于每个定理，我们抽取一组 32 个候选证明，最大长度设置为 2,048。训练batch-size配置为 512。