LeanDojo ist eine Open-Source-Plattform, die das Beweisen von mathematischen Theoremen mithilfe von Sprachmodellen ermöglicht.
Das automatisierte Beweisen von Theoremen (Automated Theorem Proving, ATP) ist eine Aufgabe, bei der Beweise für in formaler Logik formulierte Theoreme erzeugt werden. Es ist nützlich für die formale Mathematik und unterstützt die formale Verifikation, die die Korrektheit und Sicherheit von Anwendungen mit beträchtlichen Risiken gewährleistet.
ATP stellt jedoch aufgrund des großen Suchraums eine Herausforderung dar. Daher hat sich Interactive Theorem Proving (ITP) als Alternative etabliert. Beim ITP werden Beweise von Mathematiker:innen in Interaktion mit Softwarewerkzeugen, sogenannten Beweisassistenten, erstellt.
Maschinelles Lernen könnte diesen Prozess automatisieren und so einen neuen Weg zum Beweisen von Theoremen eröffnen.
Große Sprachmodelle könnten das Beweisen von Theoremen automatisieren
Große Sprachmodelle in Kombination mit Beweisassistenten wie Lean sind ein Kandidat für diesen Prozess.
Bestehende Methoden lassen sich jedoch aufgrund des proprietären Codes, der Daten und der hohen Rechenanforderungen nur schwer reproduzieren oder weiterentwickeln, so ein Team aus Forschenden von Caltech, Nvidia, MIT, UC Santa Barbara und UT Austin.
Es stellt daher mit LeanDojo eine Open-Source-Plattform zur Verfügung, die es ermöglicht, mathematische Theoreme mithilfe von Sprachmodellen zu beweisen.
LeanDojo und ReProver öffnen die Tür für weitere Forschung
LeanDojo bietet zwei wesentliche Funktionen für das lernbasierte Beweisen von Theoremen: die Extraktion von Daten und die programmatische Interaktion von Modellen mit Lean, einem weit verbreiteten Beweisassistenten. Den Forschenden zufolge ist LeanDojo das erste Werkzeug, das zuverlässig mit Lean interagieren kann, wodurch Fehler beim Beweisen erheblich reduziert werden sollen.
LeanDojo adressiert auch einen zentralen Engpass beim Beweisen von Theoremen: die Auswahl der Prämissen. Dies demonstriert das Team mit ReProver (Retrieval-Augmented Prover), einem sprachmodellbasierten Beweiser, der eine Beweisstrategie generiert, die auf einer kleinen Anzahl von Prämissen basiert, die aus der mathematischen Bibliothek von Lean abgerufen werden.
Dem Team zufolge übertrifft ReProver einige andere Methoden und beweist einen signifikanten Prozentsatz der Theoreme im LeanDojo Benchmark sowie in zwei bestehenden Datensätzen, MiniF2F und ProofNet. ReProver kann auch Theoreme beweisen, für die es derzeit keine Beweise in Lean gibt, was es zu einem nützlichen Werkzeug für die Erweiterung bestehender mathematischer Bibliotheken in Lean mache.
Sprachmodelle bis 2026 als Co-Autor für Mathematik?
Das Team veröffentlicht auch einen Benchmark, der mit LeanDojo erstellt wurde und fast 97.000 Theoreme aus Mathlib enthält, sowie ein Plugin für ChatGPT.
Der Mathematiker Terence Tao prognostizierte kürzlich, dass Sprachmodelle mit externen Tools bis 2026 zu zuverlässigen Co-Autoren in der Mathematik und anderen Wissenschaften werden könnten. LeanDojo und ReProver zeigen, wie solche Werkzeuge aussehen könnten, und bieten nun anderen Forschenden eine Grundlage für Verbesserungen.
Mehr Informationen gibt es auf der LeanDojo-Seite.
