LeanDojo: Dimostrazione di Teoremi con Modelli Linguistici Aumentati dal Recupero di Informazioni

Abstract

I grandi modelli linguistici (LLM) hanno dimostrato potenzialità nel dimostrare teoremi formali utilizzando assistenti di prova come Lean. Tuttavia, i metodi esistenti sono difficili da riprodurre o sviluppare ulteriormente, a causa di codice privato, dati e requisiti computazionali elevati. Ciò ha creato barriere significative alla ricerca sui metodi di apprendimento automatico per la dimostrazione di teoremi. Questo articolo rimuove tali barriere introducendo LeanDojo: un ambiente open-source per Lean composto da toolkit, dati, modelli e benchmark. LeanDojo estrae dati da Lean e consente l'interazione con l'ambiente di prova in modo programmatico. Contiene annotazioni dettagliate delle premesse nelle dimostrazioni, fornendo dati preziosi per la selezione delle premesse: un collo di bottiglia chiave nella dimostrazione di teoremi. Utilizzando questi dati, sviluppiamo ReProver (Retrieval-Augmented Prover): il primo dimostratore basato su LLM che è potenziato con un meccanismo di recupero per selezionare premesse da una vasta libreria matematica. È economico e richiede solo una settimana di addestramento su una GPU. Il nostro sistema di recupero sfrutta la capacità di analisi programmatica di LeanDojo per identificare premesse accessibili ed esempi negativi difficili, rendendo il recupero molto più efficace. Inoltre, costruiamo un nuovo benchmark composto da 96.962 teoremi e dimostrazioni estratti dalla libreria matematica di Lean. Presenta una suddivisione dei dati impegnativa che richiede al dimostratore di generalizzare teoremi basati su premesse nuove che non vengono mai utilizzate durante l'addestramento. Utilizziamo questo benchmark per l'addestramento e la valutazione, e i risultati sperimentali dimostrano l'efficacia di ReProver rispetto ai baseline senza recupero e a GPT-4. Forniamo quindi il primo insieme di dimostratori di teoremi basati su LLM open-source senza alcun dataset proprietario e lo rilasciamo con una licenza MIT permissiva per facilitare ulteriori ricerche.

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: Dimostrazione di Teoremi con Modelli Linguistici Aumentati dal Recupero di Informazioni

LeanDojo: Theorem Proving with Retrieval-Augmented Language Models

Abstract

Support