TheoremLlama: Trasformare LLM generici in esperti di Lean4

TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts

July 3, 2024

Autori: Ruida Wang, Jipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao, Renjie Pi, Tong Zhang

cs.AI

Abstract

Dimostrare teoremi matematici utilizzando linguaggi formali verificabili al computer come Lean ha un impatto significativo sul ragionamento matematico. Un approccio alla dimostrazione formale di teoremi prevede la generazione di prove complete utilizzando Modelli Linguistici di Grande Dimensione (LLMs) basati su dimostrazioni in Linguaggio Naturale (NL). Metodi simili hanno mostrato risultati promettenti nella generazione di codice. Tuttavia, la maggior parte dei moderni LLMs presenta prestazioni subottimali a causa della scarsità di dati allineati tra NL e Linguaggio Formale (FL) per la dimostrazione di teoremi. Questa scarsità si traduce in una carenza di metodologie per l'addestramento degli LLMs e di tecniche per sfruttare appieno le loro capacità nella composizione di dimostrazioni formali. Per affrontare queste sfide, questo articolo propone **TheoremLlama**, un framework end-to-end per addestrare un LLM generico a diventare un esperto di Lean4. Questo framework comprende metodi di generazione di dataset allineati NL-FL, approcci di addestramento per il dimostratore di teoremi formali basato su LLM, e tecniche per la scrittura di dimostrazioni Lean4 con LLM. Utilizzando il metodo di generazione del dataset, forniamo *Open Bootstrapped Theorems* (OBT), un dataset allineato NL-FL e bootstrappato. Un'innovazione chiave in questo framework è il metodo di bootstrapping NL-FL, in cui le dimostrazioni NL vengono integrate nel codice Lean4 per i dataset di addestramento, sfruttando la capacità di ragionamento NL degli LLMs per il ragionamento formale. Il framework **TheoremLlama** raggiunge accuratezze cumulative del 36,48% e 33,61% rispettivamente sui dataset MiniF2F-Valid e Test, superando la baseline di GPT-4 del 22,95% e 25,41%. Abbiamo inoltre reso open-source i checkpoint del nostro modello e il dataset generato, e presto renderemo disponibile tutto il codice pubblicamente.

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.