DeepSeek-Prover-V1.5 : Exploitation des retours d'assistant de preuve pour l'apprentissage par renforcement et la recherche arborescente Monte-Carlo

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

Résumé

Nous présentons DeepSeek-Prover-V1.5, un modèle de langage open-source conçu pour la démonstration de théorèmes dans Lean 4, qui améliore DeepSeek-Prover-V1 en optimisant à la fois les processus d'entraînement et d'inférence. Pré-entraîné sur DeepSeekMath-Base avec une spécialisation dans les langages mathématiques formels, le modèle subit un fine-tuning supervisé en utilisant un ensemble de données amélioré pour la démonstration formelle de théorèmes, dérivé de DeepSeek-Prover-V1. Un raffinement supplémentaire est obtenu grâce à l'apprentissage par renforcement basé sur les retours d'un assistant de preuve (RLPAF). Au-delà de l'approche de génération de preuves en une seule passe de DeepSeek-Prover-V1, nous proposons RMaxTS, une variante de la recherche arborescente Monte-Carlo qui utilise une stratégie d'exploitation guidée par des récompenses intrinsèques pour générer des chemins de preuve diversifiés. DeepSeek-Prover-V1.5 démontre des améliorations significatives par rapport à DeepSeek-Prover-V1, atteignant de nouveaux résultats de pointe sur l'ensemble de test du benchmark miniF2F de niveau lycée (63,5%) et du benchmark ProofNet de niveau universitaire (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%).