title: TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts
summary: 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.
paper_authors._id: 668ea53d7e35fa1925825343
paper_authors.name: Ruida Wang
paper_authors._id: 668ea53d7e35fa1925825344
paper_authors.name: Jipeng Zhang
paper_authors._id: 668ea53d7e35fa1925825345
paper_authors.name: Yizhen Jia
paper_authors._id: 668ea53d7e35fa1925825346
paper_authors.name: Rui Pan
paper_authors._id: 668ea53d7e35fa1925825347
paper_authors.name: Shizhe Diao
paper_authors._id: 668ea53d7e35fa1925825348
paper_authors.name: Renjie Pi
paper_authors._id: 668ea53d7e35fa1925825349
paper_authors.name: Tong Zhang
paper_title: TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts
paper_summary: 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.
paper_ai_summary: TheoremLlama is an end-to-end framework using Large Language Models to generate formal Lean4 proofs, demonstrating higher accuracy than GPT-4 on theorem proving tasks with an NL-FL aligned dataset.
paper_ai_keywords: Large Language Models NL-FL aligned TheoremLlama Open Bootstrapped Theorems NL-FL bootstrapping formal theorem proving Lean4 MiniF2F-Valid MiniF2F-Test GPT-4