TheoremLlama: Die Transformation von allgemeinen LLMs in Lean4-Experten

TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts

July 3, 2024

Autoren: Ruida Wang, Jipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao, Renjie Pi, Tong Zhang

cs.AI

Zusammenfassung

Die Beweisführung mathematischer Theoreme mithilfe von computerüberprüfbaren formalen Sprachen wie Lean hat einen signifikanten Einfluss auf mathematisches Denken. Ein Ansatz zur formalen Beweisführung beinhaltet die Generierung vollständiger Beweise mithilfe großer Sprachmodelle (LLMs), die auf natürlichsprachlichen (NL) Beweisen basieren. Ähnliche Methoden haben vielversprechende Ergebnisse bei der Codegenerierung gezeigt. Die meisten modernen LLMs weisen jedoch aufgrund der Knappheit von abgestimmten NL- und Formalen Sprach- (FL) Beweisdaten eine suboptimale Leistung auf. Diese Knappheit führt zu einem Mangel an Methoden zur Schulung von LLMs und Techniken zur vollen Nutzung ihrer Fähigkeiten bei der Erstellung formaler Beweise. Um diese Herausforderungen anzugehen, schlägt dieser Artikel **TheoremLlama** vor, ein End-to-End-Framework zur Schulung eines allgemeinen LLMs, um ein Experte für Lean4 zu werden. Dieses Framework umfasst Methoden zur Generierung von NL-FL abgestimmten Datensätzen, Schulungsansätze für den LLM formalen Theorembeweiser und Techniken für das Schreiben von LLM Lean4-Beweisen. Unter Verwendung der Datensatzgenerierungsmethode stellen wir *Open Bootstrapped Theorems* (OBT) bereit, einen NL-FL abgestimmten und gebooteten Datensatz. Eine wichtige Innovation in diesem Framework ist die NL-FL-Bootstrapping-Methode, bei der NL-Beweise in Lean4-Code für Trainingsdatensätze integriert werden, um die NL-Beweisfähigkeit von LLMs für formales Denken zu nutzen. Das **TheoremLlama**-Framework erreicht kumulative Genauigkeiten von 36,48 % bzw. 33,61 % auf den MiniF2F-Validierungs- und Testdatensätzen und übertrifft damit die GPT-4-Basislinie von 22,95 % bzw. 25,41 %. Wir haben auch unsere Modell-Checkpoints und generierten Datensätze als Open Source veröffentlicht und werden in Kürze den gesamten Code öffentlich zugänglich machen.

English

Proving mathematical theorems using computer-verifiable formal languages like Lean significantly impacts mathematical reasoning. One approach to formal theorem proving involves generating complete proofs using Large Language Models (LLMs) based on Natural Language (NL) proofs. Similar methods have shown promising results in code generation. However, most modern LLMs exhibit suboptimal performance due to the scarcity of aligned NL and Formal Language (FL) theorem-proving data. This scarcity results in a paucity of methodologies for training LLMs and techniques to fully utilize their capabilities in composing formal proofs. To address the challenges, this paper proposes **TheoremLlama**, an end-to-end framework to train a general-purpose LLM to become a Lean4 expert. This framework encompasses NL-FL aligned dataset generation methods, training approaches for the LLM formal theorem prover, and techniques for LLM Lean4 proof writing. Using the dataset generation method, we provide *Open Bootstrapped Theorems* (OBT), an NL-FL aligned and bootstrapped dataset. A key innovation in this framework is the NL-FL bootstrapping method, where NL proofs are integrated into Lean4 code for training datasets, leveraging the NL reasoning ability of LLMs for formal reasoning. The **TheoremLlama** framework achieves cumulative accuracies of 36.48% and 33.61% on MiniF2F-Valid and Test datasets respectively, surpassing the GPT-4 baseline of 22.95% and 25.41%. We have also open-sourced our model checkpoints and generated dataset, and will soon make all the code publicly available.