TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts

TL;DR

TheoremLlama is a new framework that trains general-purpose large language models to become experts in Lean4 theorem proving by generating aligned datasets and employing specialized training techniques, significantly improving formal proof accuracy.

Contribution

It introduces an end-to-end training framework with novel NL-FL dataset generation, bootstrapping, curriculum learning, and iterative proof writing for formal theorem proving.

Findings

Achieves higher accuracy than GPT-4 on MiniF2F datasets.

Provides an aligned NL-FL dataset called Open Bootstrapped Theorems.

Demonstrates the effectiveness of bootstrapping and curriculum learning in formal proof generation.

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