Inhalt
summary Zusammenfassung

LeanDojo ist eine Open-Source-Plattform, die das Beweisen von mathematischen Theoremen mithilfe von Sprachmodellen ermöglicht.

Anzeige

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.

Anzeige
Anzeige

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.

Empfehlung

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.

Anzeige
Anzeige
Community beitreten
Kommt in die DECODER-Community bei Discord,Reddit, Twitter und Co. - wir freuen uns auf euch!
Unterstütze unsere unabhängige, frei zugängliche Berichterstattung. Jeder Betrag hilft und sichert unsere Zukunft. Jetzt unterstützen:
Banküberweisung
Zusammenfassung
  • LeanDojo ist eine Open-Source-Plattform zur Automatisierung des Beweisens von Theoremen mit großen Sprachmodellen.
  • Das von Caltech, Nvidia, MIT, UC Santa Barbara und UT Austin entwickelte System interagiert zuverlässig mit dem Beweisassistenten Lean und ermöglicht so eine effiziente Extraktion von Daten und Interaktion.
  • Mit ReProver präsentiert das Team einen sprachmodellbasierten Beweiser, der bereits einige Theoreme beweisen konnte, für die es derzeit keine Beweise gibt.
Quellen
Max ist leitender Redakteur bei THE DECODER. Als studierter Philosoph beschäftigt er sich mit dem Bewusstsein, KI und der Frage, ob Maschinen wirklich denken können oder nur so tun als ob.
Community beitreten
Kommt in die DECODER-Community bei Discord,Reddit, Twitter und Co. - wir freuen uns auf euch!