TheoremLlama: Het transformeren van algemene LLM's naar Lean4-experts

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

Samenvatting

Het bewijzen van wiskundige stellingen met behulp van computer-verifieerbare formele talen zoals Lean heeft een aanzienlijke impact op wiskundig redeneren. Een benadering voor formeel stellingen bewijzen omvat het genereren van complete bewijzen met behulp van Large Language Models (LLMs) op basis van Natural Language (NL) bewijzen. Soortgelijke methoden hebben veelbelovende resultaten laten zien bij codegeneratie. De meeste moderne LLMs presteren echter suboptimaal vanwege de schaarste aan afgestemde NL- en Formele Taal (FL) gegevens voor stellingen bewijzen. Deze schaarste resulteert in een gebrek aan methodologieën voor het trainen van LLMs en technieken om hun mogelijkheden volledig te benutten bij het opstellen van formele bewijzen. Om deze uitdagingen aan te pakken, stelt dit artikel **TheoremLlama** voor, een end-to-end framework om een algemeen toepasbare LLM op te leiden tot een Lean4-expert. Dit framework omvat methoden voor het genereren van NL-FL afgestemde datasets, trainingsbenaderingen voor de LLM formele stellingenbewijzer, en technieken voor het schrijven van Lean4-bewijzen door LLMs. Met behulp van de datasetgeneratiemethode bieden we *Open Bootstrapped Theorems* (OBT), een NL-FL afgestemde en gebootstrapte dataset. Een belangrijke innovatie in dit framework is de NL-FL bootstrapping-methode, waarbij NL-bewijzen worden geïntegreerd in Lean4-code voor trainingsdatasets, waardoor het NL-redeneervermogen van LLMs wordt benut voor formeel redeneren. Het **TheoremLlama** framework behaalt cumulatieve nauwkeurigheden van 36,48% en 33,61% op respectievelijk de MiniF2F-Valid en Test datasets, wat de GPT-4-basislijn van 22,95% en 25,41% overtreft. We hebben ook onze modelcheckpoints en gegenereerde dataset open-source gemaakt, en zullen binnenkort alle code publiekelijk beschikbaar stellen.

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.