DeepSeek-Prover : Faire progresser la démonstration de théorèmes dans les LLM grâce à des données synthétiques à grande échelle

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

May 23, 2024

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

cs.AI

Résumé

Les assistants de preuve comme Lean ont révolutionné la vérification des démonstrations mathématiques, garantissant une grande précision et fiabilité. Bien que les grands modèles de langage (LLM) montrent des promesses dans le raisonnement mathématique, leur avancée dans la démonstration formelle de théorèmes est entravée par un manque de données d'entraînement. Pour résoudre ce problème, nous introduisons une approche pour générer des données étendues de preuves Lean 4 dérivées de problèmes de compétitions mathématiques de niveau lycée et premier cycle universitaire. Cette approche implique de traduire des problèmes en langage naturel en énoncés formels, de filtrer les énoncés de faible qualité, et de générer des preuves pour créer des données synthétiques. Après avoir affiné le modèle DeepSeekMath 7B sur cet ensemble de données synthétiques, qui comprend 8 millions d'énoncés formels avec preuves, notre modèle a atteint des précisions de génération de preuves complètes de 46,3% avec 64 échantillons et 52% cumulativement sur le test Lean 4 miniF2F, surpassant le modèle de base GPT-4 à 23,0% avec 64 échantillons et une méthode d'apprentissage par renforcement avec recherche arborescente à 41,0%. De plus, notre modèle a réussi à prouver 5 des 148 problèmes du benchmark Lean 4 Formalized International Mathematical Olympiad (FIMO), tandis que GPT-4 n'a réussi à en prouver aucun. Ces résultats démontrent le potentiel de l'exploitation de données synthétiques à grande échelle pour améliorer les capacités de démonstration de théorèmes dans les LLM. L'ensemble de données synthétiques et le modèle seront rendus disponibles pour faciliter les recherches ultérieures dans ce domaine prometteur.

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.