TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts
Authors: name: Ruida Wang; name: Jipeng Zhang; name: Yizhen Jia; name: Rui Pan; name: Shizhe Diao; name: Renjie Pi; name: Tong Zhang
Published: 2024-07-03 15:36:18

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. 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.