DeepSeek-Prover-V1.5：利用证明助手反馈进行强化学习与蒙特卡洛树搜索
DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search
AI总结：
本研究推出面向Lean 4的定理证明开源模型DeepSeek-Prover-V1.5，通过增强数据集微调、证明助手反馈强化学习及新型RMaxTS蒙特卡洛树搜索方法，在miniF2F、ProofNet基准上刷新最优成绩。
摘要：
我们推出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基准测试集（63.5%）和本科水平ProofNet基准（25.3%）上均取得新的最优结果。
英文摘要：
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\%$).
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
