2 个月前
DeepSeek-Prover-V1.5：利用证明助手反馈进行强化学习和蒙特卡洛树搜索
Huajian Xin, Z. Z. Ren, Junxiao Song, Zhihong Shao, Wanjia Zhao, Haocheng Wang, Bo Liu, Liyue Zhang, Xuan Lu, Qiushi Du, Wenjun Gao, Qihao Zhu, Dejian Yang, Zhibin Gou, Z. F. Wu, Fuli Luo, Chong Ruan
摘要
我们介绍了DeepSeek-Prover-V1.5，这是一款为Lean 4定理证明设计的开源语言模型，通过优化训练和推理过程，对DeepSeek-Prover-V1进行了增强。该模型在DeepSeekMath-Base上预训练，并专注于形式数学语言，随后使用从DeepSeek-Prover-V1派生的增强型形式定理证明数据集进行监督微调。此外，通过从证明助手反馈中进行强化学习（RLPAF），进一步提升了模型的性能。除了DeepSeek-Prover-V1采用的一次性全证明生成方法外，我们还提出了一种名为RMaxTS的蒙特卡洛树搜索变体，该方法采用内在奖励驱动的探索策略来生成多样化的证明路径。DeepSeek-Prover-V1.5在高中水平的miniF2F基准测试集（63.5%）和大学本科水平的ProofNet基准测试集（25.3%）上展示了显著的改进，取得了新的最先进成果。