DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search
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-AI https://github.com/deepseek-ai/DeepSeek-Prover-V1.5
Abstract
We introduce DeepSeek-Prover-V1.5, an open-source language model designed for theorem proving in Lean 4, which enhances DeepSeek-Prover-V1 by optimizing both training and inference processes. Pre-trained on DeepSeekMath-Base with specialization in formal mathematical languages, the model undergoes supervised fine-tuning using an enhanced formal theorem proving dataset derived from DeepSeek-Prover-V1. Further refinement is achieved through reinforcement learning from proof assistant feedback (RLPAF). Beyond the single-pass whole-proof generation approach of DeepSeek-Prover-V1, we propose RMaxTS, a variant of Monte-Carlo tree search that employs an intrinsic-reward-driven exploration strategy to generate diverse proof paths. DeepSeek-Prover-V1.5 demonstrates significant improvements over DeepSeek-Prover-V1, achieving new state-of-the-art results on the test set of the high school level miniF2F benchmark (63.5%) and the undergraduate level ProofNet benchmark (25.3%).
中文速览
形式化定理证明（formal theorem proving）长期面临"模型只能生成完整证明、一旦中间出错就全盘失败"的难题，DeepSeek-Prover-V1.5 针对这一痛点，在前代模型基础上同时改进了训练和推理两个环节：训练侧通过在证明代码中插入自然语言思维链注释和中间战术状态信息来做数据增强，并用来自 Lean 4 验证器的二元反馈做强化学习（RLPAF）；推理侧则提出了一种"截断-续写"机制，将整段证明生成无缝嵌入蒙特卡洛树搜索（MCTS）框架，并配合基于内在奖励驱动探索的 RMaxTS 算法来应对稀疏奖励问题，从而生成更多样的证明路径。最终，模型在高中难度的 miniF2F 测试集上达到 63.5% 通过率、在本科难度的 ProofNet 测试集上达到 25.3%，均刷新了当时的最优水平。这项工作的意义在于，它将交互式证明助手的反馈与高效的整段证明生成统一在同一框架下，为大模型辅助严格数学推理提供了可复现的开源基准。
原文 arXiv:2408.08152;中英对照 + 大白话阅读 https://aha.fim.ai/paper/2408.08152v1