TheoremLlama : Transformer les LLM généralistes en experts Lean4

TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts

July 3, 2024

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

cs.AI

Résumé

La démonstration de théorèmes mathématiques à l'aide de langages formels vérifiables par ordinateur comme Lean a un impact significatif sur le raisonnement mathématique. Une approche pour la démonstration formelle de théorèmes consiste à générer des preuves complètes en utilisant des modèles de langage de grande taille (LLMs) basés sur des preuves en langage naturel (NL). Des méthodes similaires ont montré des résultats prometteurs dans la génération de code. Cependant, la plupart des LLMs modernes présentent des performances sous-optimales en raison de la rareté des données alignées entre le NL et le langage formel (FL) pour la démonstration de théorèmes. Cette rareté entraîne un manque de méthodologies pour entraîner les LLMs et de techniques pour exploiter pleinement leurs capacités dans la composition de preuves formelles. Pour relever ces défis, cet article propose **TheoremLlama**, un cadre de bout en bout pour entraîner un LLM à usage général à devenir un expert en Lean4. Ce cadre englobe des méthodes de génération de jeux de données alignés NL-FL, des approches d'entraînement pour le démonstrateur de théorèmes formels basé sur LLM, et des techniques pour la rédaction de preuves Lean4 par LLM. En utilisant la méthode de génération de jeux de données, nous fournissons *Open Bootstrapped Theorems* (OBT), un jeu de données aligné NL-FL et bootstrapé. Une innovation clé de ce cadre est la méthode de bootstrap NL-FL, où les preuves NL sont intégrées dans le code Lean4 pour les jeux de données d'entraînement, exploitant ainsi la capacité de raisonnement NL des LLMs pour le raisonnement formel. Le cadre **TheoremLlama** atteint des précisions cumulatives de 36,48 % et 33,61 % sur les jeux de données MiniF2F-Valid et Test respectivement, surpassant les performances de référence de GPT-4 à 22,95 % et 25,41 %. Nous avons également rendu publics nos points de contrôle de modèle et le jeu de données généré, et nous rendrons bientôt tout le code disponible publiquement.

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.