DeepSeek-Prover-V1.5: Sfruttare il Feedback degli Assistenti di Dimostrazione per l'Apprendimento per Rinforzo e la Ricerca ad Albero Monte-Carlo

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

August 15, 2024

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

Abstract

Presentiamo DeepSeek-Prover-V1.5, un modello linguistico open-source progettato per il teorema proving in Lean 4, che migliora DeepSeek-Prover-V1 ottimizzando sia i processi di addestramento che di inferenza. Pre-addestrato su DeepSeekMath-Base con specializzazione nei linguaggi matematici formali, il modello viene sottoposto a fine-tuning supervisionato utilizzando un dataset potenziato di teorema proving formale derivato da DeepSeek-Prover-V1. Un ulteriore affinamento è ottenuto attraverso il reinforcement learning basato sul feedback dell'assistente di prove (RLPAF). Oltre all'approccio di generazione dell'intera prova in un singolo passaggio di DeepSeek-Prover-V1, proponiamo RMaxTS, una variante della ricerca ad albero Monte-Carlo che impiega una strategia di esplorazione guidata da ricompense intrinseche per generare percorsi di prova diversificati. DeepSeek-Prover-V1.5 dimostra miglioramenti significativi rispetto a DeepSeek-Prover-V1, raggiungendo nuovi risultati all'avanguardia sul test set del benchmark miniF2F di livello liceale (63,5%) e del benchmark ProofNet di livello universitario (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%).