DeepSeek-Prover-V1.5: Benutten van Feedback van Bewijsassistenten voor Reinforcement Learning en Monte-Carlo Boomzoeken

DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search

August 15, 2024

Auteurs: 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

cs.AI

Samenvatting

We introduceren DeepSeek-Prover-V1.5, een open-source taalmodel ontworpen voor stellingenbewijzen in Lean 4, dat DeepSeek-Prover-V1 verbetert door zowel de trainings- als de inferentieprocessen te optimaliseren. Het model is voorgetraind op DeepSeekMath-Base met specialisatie in formele wiskundige talen en ondergaat supervised fine-tuning met behulp van een verbeterde dataset voor formeel stellingenbewijzen, afgeleid van DeepSeek-Prover-V1. Verdere verfijning wordt bereikt door reinforcement learning op basis van feedback van een bewijsassistent (RLPAF). Naast de single-pass benadering voor het genereren van volledige bewijzen van DeepSeek-Prover-V1, stellen we RMaxTS voor, een variant van Monte-Carlo tree search die een intrinsieke-beloningsgedreven verkenningstrategie gebruikt om diverse bewijspaden te genereren. DeepSeek-Prover-V1.5 toont aanzienlijke verbeteringen ten opzichte van DeepSeek-Prover-V1 en behaalt nieuwe state-of-the-art resultaten op de testset van de middelbare schoolniveau miniF2F-benchmark (63,5%) en de bachelor-niveau ProofNet-benchmark (25,3%).

English

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%).