DeepSeek-Prover: Fortschritte beim Theorembeweis in LLMs durch groß angelegte synthetische Daten

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

May 23, 2024

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

cs.AI

Zusammenfassung

Beweisassistenten wie Lean haben die mathematische Beweisüberprüfung revolutioniert und gewährleisten eine hohe Genauigkeit und Zuverlässigkeit. Obwohl große Sprachmodelle (LLMs) vielversprechend für mathematisches Denken sind, wird ihr Fortschritt in der formalen Theorembeweisführung durch einen Mangel an Trainingsdaten behindert. Um dieses Problem zu lösen, stellen wir einen Ansatz vor, um umfangreiche Lean 4 Beweisdaten zu generieren, die von mathematischen Wettbewerbsproblemen auf Gymnasial- und Bachelor-Niveau abgeleitet sind. Dieser Ansatz beinhaltet die Übersetzung von Problemsätzen in formale Aussagen, die Filterung von minderwertigen Aussagen und die Generierung von Beweisen zur Erstellung synthetischer Daten. Nach Feinabstimmung des DeepSeekMath 7B-Modells auf diesem synthetischen Datensatz, der 8 Millionen formale Aussagen mit Beweisen umfasst, erreichte unser Modell Gesamtbeweisgenerierungsgenauigkeiten von 46,3% mit 64 Beispielen und kumulativ 52% im Lean 4 miniF2F-Test, wobei der Basiswert von GPT-4 bei 23,0% mit 64 Beispielen und einer Baumsuchverstärkungsmethode bei 41,0% lag. Darüber hinaus konnte unser Modell erfolgreich 5 von 148 Problemen im Lean 4 Formalized International Mathematical Olympiad (FIMO) Benchmark beweisen, während GPT-4 keine beweisen konnte. Diese Ergebnisse zeigen das Potenzial der Nutzung von groß angelegten synthetischen Daten zur Verbesserung der Theorembeweisfähigkeiten in LLMs. Sowohl der synthetische Datensatz als auch das Modell werden zur Verfügung gestellt, um weitere Forschung in diesem vielversprechenden Bereich zu erleichtern.

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.