LeanDojo: Theorembeweis mit retrieval-augmentierten Sprachmodellen

Zusammenfassung

Große Sprachmodelle (LLMs) haben vielversprechende Ergebnisse bei der Beweisformaler Theoreme mithilfe von Beweisassistenten wie Lean gezeigt. Bestehende Methoden sind jedoch aufgrund von nicht öffentlichem Code, Daten und hohen Rechenanforderungen schwer zu reproduzieren oder darauf aufzubauen. Dies hat erhebliche Hindernisse für die Forschung zu maschinellen Lernmethoden für das Theorembeweisen geschaffen. Diese Arbeit beseitigt diese Hindernisse durch die Einführung von LeanDojo: einer Open-Source-Lean-Umgebung, die Toolkits, Daten, Modelle und Benchmarks umfasst. LeanDojo extrahiert Daten aus Lean und ermöglicht die programmatische Interaktion mit der Beweisumgebung. Es enthält detaillierte Annotationen von Prämissen in Beweisen, die wertvolle Daten für die Prämissenauswahl liefern: ein zentraler Engpass beim Theorembeweisen. Mit diesen Daten entwickeln wir ReProver (Retrieval-Augmented Prover): den ersten LLM-basierten Beweiser, der durch Retrieval ergänzt wird, um Prämissen aus einer umfangreichen mathematischen Bibliothek auszuwählen. Er ist kostengünstig und benötigt nur eine GPU-Woche Training. Unser Retriever nutzt die Programmanalysefähigkeit von LeanDojo, um zugängliche Prämissen und schwierige negative Beispiele zu identifizieren, was das Retrieval wesentlich effektiver macht. Darüber hinaus erstellen wir einen neuen Benchmark, der aus 96.962 Theoremen und Beweisen besteht, die aus der Lean-Mathematikbibliothek extrahiert wurden. Er zeichnet sich durch anspruchsvolle Datenaufteilungen aus, die vom Beweiser verlangen, sich auf Theoreme zu verallgemeinern, die auf neuen Prämissen basieren, die im Training nie verwendet werden. Wir nutzen diesen Benchmark für Training und Evaluation, und die experimentellen Ergebnisse demonstrieren die Effektivität von ReProver gegenüber nicht-retrieval-basierten Baselines und GPT-4. Somit stellen wir die erste Reihe von Open-Source-LLM-basierten Theorembeweisern ohne proprietäre Datensätze bereit und veröffentlichen sie unter einer permissiven MIT-Lizenz, um weitere Forschung zu erleichtern.

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: Theorembeweis mit retrieval-augmentierten Sprachmodellen

LeanDojo: Theorem Proving with Retrieval-Augmented Language Models

Zusammenfassung

Support