TeoremaLhama: Transformando LLMs de Uso Geral em Especialistas 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

Resumo

A comprovação de teoremas matemáticos usando linguagens formais verificáveis por computador, como o Lean, impacta significativamente o raciocínio matemático. Uma abordagem para a comprovação formal de teoremas envolve a geração de provas completas usando Modelos de Linguagem Grande (LLMs) baseados em Linguagem Natural (NL). Métodos semelhantes têm mostrado resultados promissores na geração de código. No entanto, a maioria dos LLMs modernos apresenta desempenho subótimo devido à escassez de dados alinhados de comprovação de teoremas em NL e Linguagem Formal (FL). Essa escassez resulta em uma falta de metodologias para treinar LLMs e técnicas para utilizar plenamente suas capacidades na composição de provas formais. Para enfrentar os desafios, este artigo propõe o **TheoremLlama**, um framework de ponta a ponta para treinar um LLM de propósito geral para se tornar um especialista em Lean4. Esse framework engloba métodos de geração de conjuntos de dados alinhados NL-FL, abordagens de treinamento para o provador formal de teoremas LLM e técnicas para escrever provas Lean4 com LLM. Utilizando o método de geração de conjuntos de dados, fornecemos *Teoremas Iniciais Bootstrap* (OBT), um conjunto de dados alinhado NL-FL e bootstrap. Uma inovação chave nesse framework é o método de bootstrap NL-FL, onde provas em NL são integradas ao código Lean4 para conjuntos de dados de treinamento, aproveitando a capacidade de raciocínio em NL dos LLMs para raciocínio formal. O framework **TheoremLlama** alcança acurácias cumulativas de 36,48% e 33,61% nos conjuntos de dados MiniF2F-Valid e Test, respectivamente, superando a linha de base GPT-4 de 22,95% e 25,41%. Também disponibilizamos nossos pontos de verificação de modelo e conjunto de dados gerado como código aberto, e em breve tornaremos todo o código publicamente disponível.

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.