T heorem L lama: Transforming General-Purpose LLM s into Lean4 Experts (2024)

Abstract: 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. However, due to the scarcity of aligned NL and Formal Language (FL) theorem-proving data most modern LLMs exhibit suboptimal performance.This scarcity results in a paucity of methodologies for training LLMs and techniques to fully utilize their capabilities in composing formal proofs. To address these challenges, this paper proposes **TheoremLlama**, an end-to-end framework that trains a general-purpose LLM to be a Lean4 expert. **TheoremLlama** includes NL-FL dataset generation and bootstrapping method to obtain aligned dataset, curriculum learning and block training techniques to train the model, and iterative proof writing method to write Lean4 proofs that work together synergistically.Using the dataset generation method in **TheoremLlama**, we provide *Open Bootstrapped Theorems* (OBT), an NL-FL aligned and bootstrapped dataset. Our novel NL-FL bootstrapping method, where NL proofs are integrated into Lean4 code for training datasets, leverages 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%. Our code, model checkpoints, and the generated dataset is published in GitHub

## introduction the ability to perform logical reasoning has always been regarded as a cornerstone of human intelligence and a fundamental goal of machine learning * first authors systems @xcite . among these tasks, mathematical reasoning is considered crucial for evaluating the capabilities of large language models (llms). however, in modern mathematics, verifying the correctness of theorem proofs written in natural language is challenging, complicating the assessment of llms' mathematical reasoning in advanced topics. additionally, the rapid development of modern mathematics and the increasing complexity of proofs pose significant barriers to reviewing their correctness. this has led to erroneous proofs that require considerable effort to be identified by the mathematical community, as exemplified by the process of proving fermat's last theorem @xcite . to address these issues, formal mathematical languages such as lean @xcite , isabelle @xcite , and hol light @xcite have been developed. these languages allow computers to automatically verify proofs, providing a clear standard for evaluating mathematical theorem proofs and significantly impacting both the mathematical and computer science communities. however, writing mathematical proofs in formal language (fl) requires significant expertise and effort. additionally, formal proofs involve much repetitive and tedious work @xcite , which is not customary for mathematicians who are more familiar with high-level proofs. consequently, there has been significant demand for automated theorem-proving using fl, leading to a considerable number of works on this task @xcite @xcite @xcite . however, most of these works rely on searching methods in an infinite space of possible tactics to complete the proof, resulting in unaffordable computational costs (e.g., @xcite uses 2,000 a100 gpu hours for training) in finishing complex proofs and not fully leveraging nl reasoning ability of llms. recent advancements in llms, especially in reasoning @xcite and coding @xcite , have prompted researchers to explore using them to write formal proofs guided by natural language @xcite . in this paper, we focus on enabling generalpurpose llms to write formal lean4 proofs guided by natural language (nl) proofs. we have chosen lean4 because it has recently garnered considerable attention from the mathematical community @xcite @xcite , whereas lean3 and isabelle are older formal languages. despite the potential demonstrated by previous works @xcite in similar tasks using isabelle, the few-shot performance of llms in lean4 remains relatively unsatisfactory in lean 4 (details in appendix a). this is because lean4 is a more concise fl that differs significantly from nl, making the direct transfer of reasoning abilities from nl to lean4 infeasible. the situation is exacerbated by the inclusion of confusing lean3 code in the llms' pre-training data (details in appendix a). more importantly, there is a significant lack of nl-fl aligned data, making the training of llms to write lean4 proofs an overlooked and challenging task. additionally, @xcite indicates that there remains a large potential for researchers to fully utilize llms in writing formal proofs. to address these challenges, we propose the-oremllama, an end-to-end framework that transforms a general-purpose llm into a lean4 expert. the framework overview is presented in fig. 1 . our framework comprises three major components that work synergistically: we summarize our contributions in this paper as follows: (1) we propose theoremllama, an end-to-end framework that transforms a generalpurpose llm into a formal proving expert. the-oremllama spans from nl-fl aligned dataset generation to lean4 prover training techniques and iterative proof writing for lean4 prover. it amends the significant data scarcity problem by contributing to the obt dataset. additionally, it contains llm training and proof writing methods that have largely been overlooked in lean4 theorem proving. furthermore, we open-source the obt dataset, model checkpoints, and codes to support further research in the community. under a reasonable gpu footprint for theoremllama (the fine-tuning only takes about 32 hours for an 8 gpu a6000 machine) our work will significantly lower barriers to academic researchers in corresponding fields of obtaining considerably well-behaved lean4 prover. ## methodology in this section, we present the details of theo-remllama, including generation methods for the obt dataset. the key idea for our framework is to enable llms to perform well in the unfamiliar lean4 theorem proving task under the circumstances of limited or even confusing data during its pre-training. we introduce the dataset generation method in section 2.1, illustrate the training techniques for lean4 prover training using the obt dataset in section 2.2, and propose an iterative proof writing method llm prover in section 2.3. the task that this methodology works on can be defined as: "training the general purpose llm to be an expert in lean4 whole-proof generation under the guidance of natural language proofs." ## experiments we conduct extensive experiments on the minif2f-lean4 dataset @xcite to test the effectiveness of theoremllama framework on formal reasoning with nl guidance. we also conduct ablation studies (section 3.4) and case studies (section 3.7) to further validate the theoremllama. ## conclusion this paper proposes theoremllama, an end-toend framework for transforming a general-purpose llm into a lean4 expert, along with the open bootstrapped theorems (obt) dataset, a nl-fl aligned, bootstrapped dataset for training an llm lean4 prover. this work largely addresses the significant data scarcity problem by introducing the nl-fl aligned dataset generation method, which is used to create the obt dataset. subsequently, we demonstrate block training and curriculum data sorting techniques to enhance llm training. furthermore, we present the iterative proof writing tactic to better utilize the llm's capability in theorem proving. the major innovation of this work is the nl-fl bootstrapping method, which enables the llm to better transfer its natural language reasoning ability to lean4 proof writing through gen-erated data. we also conduct comprehensive experiments to evaluate the effectiveness of theorem-llama, where our framework successfully proves 36.48% and 33.61% of the theorems in minif2f-valid and test, respectively, surpassing the gpt-4 and gemini-1.5 baselines. we will open-source all the datasets to facilitate further development in the field.