DeepSeek-Prover-V1.5: Aprovechando la Retroalimentación del Asistente de Pruebas para Aprendizaje por Refuerzo y Búsqueda de Árbol Monte Carlo

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

August 15, 2024

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

Resumen

Presentamos DeepSeek-Prover-V1.5, un modelo de lenguaje de código abierto diseñado para la demostración de teoremas en Lean 4, que mejora DeepSeek-Prover-V1 al optimizar tanto los procesos de entrenamiento como de inferencia. Pre-entrenado en DeepSeekMath-Base con especialización en lenguajes matemáticos formales, el modelo se somete a un ajuste fino supervisado utilizando un conjunto de datos mejorado de demostración de teoremas formales derivado de DeepSeek-Prover-V1. Además, se logra un mayor refinamiento a través del aprendizaje por refuerzo a partir de la retroalimentación del asistente de pruebas (RLPAF). Más allá del enfoque de generación de pruebas completas de un solo paso de DeepSeek-Prover-V1, proponemos RMaxTS, una variante de la búsqueda de árboles de Monte Carlo que emplea una estrategia de exploración impulsada por recompensas intrínsecas para generar caminos de prueba diversos. DeepSeek-Prover-V1.5 muestra mejoras significativas sobre DeepSeek-Prover-V1, logrando nuevos resultados de vanguardia en el conjunto de pruebas del benchmark miniF2F de nivel de secundaria (63.5%) y en el benchmark ProofNet de nivel 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%).