LeanDojo: Stellingen Bewijzen met Retrieval-Augmenteerde Taalmodellen

Samenvatting

Grote taalmodellen (LLMs) hebben potentie getoond in het bewijzen van formele stellingen met behulp van proof assistants zoals Lean. Bestaande methoden zijn echter moeilijk te reproduceren of op te bouwen vanwege privécode, data en grote rekenkrachtvereisten. Dit heeft aanzienlijke barrières gecreëerd voor onderzoek naar machine learning-methoden voor stellingenbewijzen. Dit artikel verwijdert deze barrières door LeanDojo te introduceren: een open-source Lean-speelplaats bestaande uit toolkits, data, modellen en benchmarks. LeanDojo extraheert data uit Lean en maakt interactie met de bewijsomgeving programmatisch mogelijk. Het bevat gedetailleerde annotaties van premissen in bewijzen, wat waardevolle data biedt voor premisse-selectie: een belangrijk knelpunt in stellingenbewijzen. Met deze data ontwikkelen we ReProver (Retrieval-Augmented Prover): de eerste LLM-gebaseerde prover die is versterkt met retrieval voor het selecteren van premissen uit een uitgebreide wiskundebibliotheek. Het is kosteneffectief en heeft slechts één GPU-week training nodig. Onze retriever maakt gebruik van LeanDojo's programma-analysecapaciteit om toegankelijke premissen en moeilijke negatieve voorbeelden te identificeren, wat retrieval aanzienlijk effectiever maakt. Bovendien construeren we een nieuwe benchmark bestaande uit 96.962 stellingen en bewijzen die zijn geëxtraheerd uit Lean's wiskundebibliotheek. Het bevat uitdagende datasplits die vereisen dat de prover generaliseert naar stellingen die afhankelijk zijn van nieuwe premissen die nooit in de training worden gebruikt. We gebruiken deze benchmark voor training en evaluatie, en experimentele resultaten tonen de effectiviteit van ReProver aan ten opzichte van niet-retrieval-baselines en GPT-4. We bieden hiermee de eerste set open-source LLM-gebaseerde stellingenprovers zonder enige propriëtaire datasets en geven deze vrij onder een permissieve MIT-licentie om verder onderzoek te faciliteren.

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: Stellingen Bewijzen met Retrieval-Augmenteerde Taalmodellen

LeanDojo: Theorem Proving with Retrieval-Augmented Language Models

Samenvatting

Support