LeanDojo: Prova de Teoremas com Modelos de Linguagem Aumentados por Recuperação

Resumo

Modelos de linguagem de grande escala (LLMs) têm mostrado potencial em provar teoremas formais usando assistentes de prova como o Lean. No entanto, os métodos existentes são difíceis de reproduzir ou expandir, devido a código privado, dados e grandes requisitos de computação. Isso criou barreiras substanciais para a pesquisa em métodos de aprendizado de máquina para prova de teoremas. Este artigo remove essas barreiras ao introduzir o LeanDojo: um playground de Lean de código aberto que consiste em kits de ferramentas, dados, modelos e benchmarks. O LeanDojo extrai dados do Lean e permite a interação com o ambiente de prova de forma programática. Ele contém anotações detalhadas de premissas em provas, fornecendo dados valiosos para a seleção de premissas: um gargalo crucial na prova de teoremas. Usando esses dados, desenvolvemos o ReProver (Prover Aumentado por Recuperação): o primeiro provador baseado em LLM que é aumentado com recuperação para selecionar premissas de uma vasta biblioteca matemática. Ele é econômico e precisa de apenas uma semana de treinamento em uma GPU. Nosso recuperador aproveita a capacidade de análise de programas do LeanDojo para identificar premissas acessíveis e exemplos negativos difíceis, o que torna a recuperação muito mais eficaz. Além disso, construímos um novo benchmark composto por 96.962 teoremas e provas extraídos da biblioteca matemática do Lean. Ele apresenta divisões de dados desafiadoras que exigem que o provador generalize teoremas que dependem de premissas novas que nunca são usadas no treinamento. Usamos esse benchmark para treinamento e avaliação, e os resultados experimentais demonstram a eficácia do ReProver em comparação com baselines sem recuperação e o GPT-4. Assim, fornecemos o primeiro conjunto de provadores de teoremas baseados em LLM de código aberto, sem qualquer conjunto de dados proprietário, e o liberamos sob uma licença permissiva MIT para facilitar pesquisas futuras.

English

Large language models (LLMs) have shown promise in proving formal theorems using proof assistants such as Lean. However, existing methods are difficult to reproduce or build on, due to private code, data, and large compute requirements. This has created substantial barriers to research on machine learning methods for theorem proving. This paper removes these barriers by introducing LeanDojo: an open-source Lean playground consisting of toolkits, data, models, and benchmarks. LeanDojo extracts data from Lean and enables interaction with the proof environment programmatically. It contains fine-grained annotations of premises in proofs, providing valuable data for premise selection: a key bottleneck in theorem proving. Using this data, we develop ReProver (Retrieval-Augmented Prover): the first LLM-based prover that is augmented with retrieval for selecting premises from a vast math library. It is inexpensive and needs only one GPU week of training. Our retriever leverages LeanDojo's program analysis capability to identify accessible premises and hard negative examples, which makes retrieval much more effective. Furthermore, we construct a new benchmark consisting of 96,962 theorems and proofs extracted from Lean's math library. It features challenging data split requiring the prover to generalize to theorems relying on novel premises that are never used in training. We use this benchmark for training and evaluation, and experimental results demonstrate the effectiveness of ReProver over non-retrieval baselines and GPT-4. We thus provide the first set of open-source LLM-based theorem provers without any proprietary datasets and release it under a permissive MIT license to facilitate further research.

LeanDojo: Prova de Teoremas com Modelos de Linguagem Aumentados por Recuperação

LeanDojo: Theorem Proving with Retrieval-Augmented Language Models

Resumo

Support