TeoremaLlama: Transformando LLMs de Propósito General en Expertos Lean4

TheoremLlama: Transforming General-Purpose LLMs into Lean4 Experts

July 3, 2024

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

cs.AI

Resumen

Demostrar teoremas matemáticos utilizando lenguajes formales verificables por computadora como Lean impacta significativamente el razonamiento matemático. Un enfoque para la demostración formal de teoremas implica generar pruebas completas utilizando Modelos de Lenguaje Grande (LLMs) basados en pruebas de Lenguaje Natural (NL). Métodos similares han mostrado resultados prometedores en la generación de código. Sin embargo, la mayoría de los LLMs modernos muestran un rendimiento subóptimo debido a la escasez de datos alineados de demostración de teoremas en Lenguaje Natural (NL) y Lenguaje Formal (FL). Esta escasez resulta en una falta de metodologías para entrenar LLMs y técnicas para aprovechar completamente sus capacidades en la composición de pruebas formales. Para abordar los desafíos, este artículo propone **TheoremLlama**, un marco de trabajo de extremo a extremo para entrenar un LLM de propósito general para convertirse en un experto en Lean4. Este marco abarca métodos de generación de conjuntos de datos alineados NL-FL, enfoques de entrenamiento para el demostrador formal de teoremas LLM y técnicas para la escritura de pruebas Lean4 de LLM. Utilizando el método de generación de conjuntos de datos, proporcionamos *Teoremas Iniciales Abiertos* (OBT), un conjunto de datos alineado NL-FL y de arranque. Una innovación clave en este marco es el método de arranque NL-FL, donde las pruebas de NL se integran en el código Lean4 para conjuntos de datos de entrenamiento, aprovechando la capacidad de razonamiento de NL de los LLMs para el razonamiento formal. El marco **TheoremLlama** logra precisión acumulativa del 36.48% y 33.61% en los conjuntos de datos MiniF2F-Valid y Test respectivamente, superando la línea base de GPT-4 del 22.95% y 25.41%. También hemos hecho públicos nuestros puntos de control de modelo y el conjunto de datos generado, y pronto haremos que todo el código esté disponible públicamente.

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.