DeepSeek-Prover-V1.5：利用证明助手反馈进行强化学习与蒙特卡洛树搜索
计算与语言
2024-08-16 v1 人工智能
机器学习
计算机科学中的逻辑
摘要
我们介绍了 DeepSeek-Prover-V1.5，一个专为 Lean 4 中定理证明设计的开源语言模型，它通过优化训练和推理过程来增强 DeepSeek-Prover-V1。该模型在 DeepSeekMath-Base 上预训练，并专门针对形式化数学语言进行了优化，随后使用从 DeepSeek-Prover-V1 派生的增强形式化定理证明数据集进行监督微调。通过来自证明助手反馈的强化学习（RLPAF）进一步优化。除了 DeepSeek-Prover-V1 的单次全证明生成方法外，我们提出了 RMaxTS，这是一种利用内在奖励驱动的探索策略来生成多样化证明路径的蒙特卡洛树搜索变体。DeepSeek-Prover-V1.5 在 DeepSeek-Prover-V1 的基础上取得了显著提升，在高中水平 miniF2F 基准测试集（）和本科水平 ProofNet 基准测试集（）上取得了新的最先进结果。
引用
@article{arxiv.2408.08152,
title = {DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search},
author = {Huajian Xin and Z. Z. Ren and Junxiao Song and Zhihong Shao and Wanjia Zhao and Haocheng Wang and Bo Liu and Liyue Zhang and Xuan Lu and Qiushi Du and Wenjun Gao and Qihao Zhu and Dejian Yang and Zhibin Gou and Z. F. Wu and Fuli Luo and Chong Ruan},
journal= {arXiv preprint arXiv:2408.08152},
year = {2024}
}