DeepSeek-Prover: Avanzando en la demostración de teoremas en LLMs mediante datos sintéticos a gran escala

DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data

May 23, 2024

Autores: Huajian Xin, Daya Guo, Zhihong Shao, Zhizhou Ren, Qihao Zhu, Bo Liu, Chong Ruan, Wenda Li, Xiaodan Liang

cs.AI

Resumen

Los asistentes de pruebas como Lean han revolucionado la verificación de demostraciones matemáticas, garantizando una alta precisión y fiabilidad. Aunque los modelos de lenguaje extenso (LLMs) muestran potencial en el razonamiento matemático, su avance en la demostración formal de teoremas se ve obstaculizado por la falta de datos de entrenamiento. Para abordar este problema, presentamos un enfoque para generar datos extensos de pruebas en Lean 4 derivados de problemas de competiciones matemáticas de nivel secundario y universitario. Este enfoque implica traducir problemas en lenguaje natural a enunciados formales, filtrar enunciados de baja calidad y generar pruebas para crear datos sintéticos. Tras ajustar el modelo DeepSeekMath 7B en este conjunto de datos sintéticos, que comprende 8 millones de enunciados formales con pruebas, nuestro modelo logró precisiones en la generación de pruebas completas del 46.3% con 64 muestras y del 52% acumulativamente en la prueba miniF2F de Lean 4, superando la línea base de GPT-4 con un 23.0% con 64 muestras y un método de aprendizaje por refuerzo con búsqueda en árbol con un 41.0%. Además, nuestro modelo demostró con éxito 5 de 148 problemas en el benchmark Formalized International Mathematical Olympiad (FIMO) de Lean 4, mientras que GPT-4 no logró demostrar ninguno. Estos resultados demuestran el potencial de aprovechar datos sintéticos a gran escala para mejorar las capacidades de demostración de teoremas en LLMs. Tanto el conjunto de datos sintéticos como el modelo estarán disponibles para facilitar futuras investigaciones en este prometedor campo.

English

Proof assistants like Lean have revolutionized mathematical proof verification, ensuring high accuracy and reliability. Although large language models (LLMs) show promise in mathematical reasoning, their advancement in formal theorem proving is hindered by a lack of training data. To address this issue, we introduce an approach to generate extensive Lean 4 proof data derived from high-school and undergraduate-level mathematical competition problems. This approach involves translating natural language problems into formal statements, filtering out low-quality statements, and generating proofs to create synthetic data. After fine-tuning the DeepSeekMath 7B model on this synthetic dataset, which comprises 8 million formal statements with proofs, our model achieved whole-proof generation accuracies of 46.3% with 64 samples and 52% cumulatively on the Lean 4 miniF2F test, surpassing the baseline GPT-4 at 23.0% with 64 samples and a tree search reinforcement learning method at 41.0%. Additionally, our model successfully proved 5 out of 148 problems in the Lean 4 Formalized International Mathematical Olympiad (FIMO) benchmark, while GPT-4 failed to prove any. These results demonstrate the potential of leveraging large-scale synthetic data to enhance theorem-proving capabilities in LLMs. Both the synthetic dataset and the model will be made available to facilitate further research in this promising field.