Discovering New Theorems via LLMs with In-Context Proof Learning in Lean

Dieser Beitrag stellt die Konjektur-Beweis-Schleife (CPL) vor, eine Pipeline, die durch iteratives Zuführen der eigenen formal verifizierten Theoreme und Beweise in Lean 4 an ein LLM kontextbasiertes Lernen nutzt, um die Entdeckungsrate und den Erfolg neuartiger, schwer zu beweisender mathematischer Vermutungen erheblich zu steigern.

Das Wesentliche

Stellen Sie sich vor, Sie versuchen, einem sehr intelligenten, aber leicht vergesslichen Roboter beizubringen, komplexe mathematische Rätsel zu lösen. Der Roboter ist ein Large Language Model (LLM), und die Rätsel sind formale mathematische Beweise, die in einer strengen Computersprache namens Lean geschrieben sind.

Die Arbeit stellt eine neue Methode vor, um diesen Roboter zu unterrichten, die als Conjecturing-Proving Loop (CPL) bezeichnet wird. Hier ist ihre Funktionsweise, erklärt durch einfache Analogien:

Das Problem: Die „Raten-und-Prüfen"-Falle

Normalerweise, wenn Menschen versuchen, KI Mathematik zu lehren, bitten sie sie, ein Rätsel zu erraten und es sofort zu lösen.

• Die Analogie: Stellen Sie sich vor, Sie bitten einen Schüler, „eine mathematische Aufgabe zu schreiben und sie sofort zu lösen".
• Das Problem: Der Schüler wird faul. Er schreibt einfache Aufgaben (wie „2 + 2 = 4"), weil diese leicht zu lösen sind. Er vermeidet schwierige Aufgaben, weil er weiß, dass er scheitern könnte. Die KI generiert am Ende Tausende von einfachen, langweiligen Beweisen und verpasst die schwierigen, interessanten.

Die Lösung: Der „Zwei-Schritte-Tanz" (CPL)

Die Autoren teilen den Prozess in zwei unterschiedliche Rollen auf: einen Vermutenden (den Ideen-Generator) und einen Beweisenden (den Löser).

1. Der Vermutende (Der Architekt): Dieser Teil der KI betrachtet eine Bibliothek bestehender mathematischer Regeln und entwickelt neue Ideen (Vermutungen). Er versucht noch nicht, sie zu lösen; er schreibt sie einfach auf.
2. Der Beweisende (Der Baumeister): Dieser Teil nimmt die Ideen und versucht, einen Beweis dafür zu erstellen. Wenn er scheitert, versucht er es erneut. Er versucht es so lange, bis er entweder erfolgreich ist oder seine Versuche aufgebraucht hat.
3. Die Bibliothek (Das Gedächtnis): Jedes Mal, wenn der Beweisende erfolgreich einen Beweis erstellt, wird dieser Beweis zur Bibliothek hinzugefügt.

Der magische Bestandteil: Kontextlernen
Hier kommt der clevere Teil ins Spiel: Der Beweisende betrachtet nicht nur die ursprünglichen mathematischen Regeln. Er betrachtet die Bibliothek der Beweise, die er während der aktuellen Sitzung bereits erfolgreich erstellt hat.

• Die Analogie: Stellen Sie sich einen Schüler vor, der eine Prüfung schreibt. Auf die alte Weise musste er sich nur auf das verlassen, was er vor Beginn der Prüfung auswendig gelernt hatte. Auf diese neue Weise darf der Schüler jedes Mal, wenn er eine Aufgabe korrekt löst, seine eigene Lösung lesen, bevor er die nächste Aufgabe angeht. Er lernt die „Tricks" und „Strategien" aus seinen eigenen jüngsten Erfolgen.

Was sie herausfanden

Die Forscher testeten dies an einigen kniffligen topologischen Konzepten (ein mathematischer Zweig, der sich mit Formen und Räumen befasst), die die KI noch nicht gut beherrschte.

• Menge vs. Qualität: Die alte Methode (gleichzeitiges Raten und Lösen) generierte mehr Theoreme insgesamt, aber sie waren meist kurz und einfach. Die neue Methode (CPL) generierte weniger Theoreme insgesamt, aber sie waren viel schwieriger und länger.
• Der große Gewinn: Die neue Methode entdeckte erfolgreich ein spezifisches, schwieriges Theorem über „alpha-offene Mengen", das die alte Methode niemals fand, selbst nach 20 Versuchen.
• Lernen vom Erfolg: Wenn die KI die Bibliothek ihrer eigenen vorherigen Beweise als „Spickzettel" (Kontext) erhielt, konnte sie schwierige Theoreme beweisen, die sie ohne diesen Kontext nicht lösen konnte. Selbst wenn die KI das Theorem nicht in plain English beweisen konnte, konnte sie es in Lean-Code beweisen, sobald sie ähnliche erfolgreiche Beweise gesehen hatte.

Das Fazit

Die Arbeit behauptet, dass wir durch die Trennung der „Ideenfindung" vom „Beweislösen" und indem wir die KI ihre eigenen verifizierten Erfolge in Echtzeit lernen lassen, sie dazu bringen können, schwierigere, komplexere mathematische Wahrheiten zu entdecken, die sie sonst verpassen würde. Es ist, als würde man der KI einen Vorsprung geben, indem man ihr erlaubt, ihre eigenen Hausaufgaben zu studieren, bevor sie die Abschlussprüfung ablegt.

Hinweis: Die Arbeit konzentriert sich streng auf diese Methode zur Generierung und Verifizierung mathematischer Theoreme. Sie behauptet nicht, dass diese Methode für medizinische Diagnosen, Finanzprognosen oder andere reale Anwendungen außerhalb der formalen Mathematik funktioniert.

Technische Zusammenfassung

Technisches Fazit: Entdeckung neuer Theoreme mittels LLMs mit kontextbasiertem Beweislernen in Lean

Problemstellung
Large Language Models (LLMs) haben vielversprechende Ergebnisse im Bereich des formalen Beweisens von Theoremen gezeigt, stehen jedoch vor erheblichen Herausforderungen: Sie können Halluzinationen produzieren, und die gleichzeitige Generierung sowohl einer mathematischen Vermutung als auch ihres Beweises führt häufig zu einer Konvergenz auf triviale oder einfache Theoreme. Bestehende Ansätze verlassen sich typischerweise auf Supervised Fine-Tuning (SFT) oder Reinforcement Learning mit verifizierten Belohnungen (RLVR), die umfangreiche Trainingsdaten erfordern und auf geschlossene Modelle schwer anwendbar sind. Darüber hinaus haben aktuelle Methoden oft Schwierigkeiten, „schwer zu beweisende" Theoreme zu entdecken, da die Wahrscheinlichkeit der Generierung eines Theorems stark durch die unmittelbare Erfolgsrate seines Beweises gewichtet wird, was dazu führt, dass die Suche in einfache, kurze Beweise kollabiert.

Methodik: Die Vermutungs-Beweis-Schleife (CPL)
Die Autoren schlagen die Vermutungs-Beweis-Schleife (Conjecturing-Proving Loop, CPL) vor, eine Pipeline, die darauf ausgelegt ist, mathematische Vermutungen automatisch zu generieren und in Lean 4 zu verifizieren. Das Framework trennt die Generierung von Vermutungen von der Generierung von Beweisen und nutzt eine Bibliothek zuvor verifizierter Theoreme als Kontext für beide Stufen.

Die Pipeline arbeitet durch vier Hauptkomponenten: ein Vermutungs-Modul (Conjecturer, LLM-Agent), ein Beweis-Modul (Prover, LLM-Agent), einen Lean-Server und eine Bibliothek (Lean-Code-Daten).

1. Vermutungsphase: Der Conjecturer generiert neue mathematische Aussagen im Lean-4-Format basierend auf der aktuellen Bibliothek. Er fragt den Lean-Server ab, um syntaktische Gültigkeit und Neuheit sicherzustellen (dass die Aussage nicht bereits durch existierende Theoreme in Mathlib4 oder der aktuellen Bibliothek beweisbar ist).
2. Beweisphase: Für jede gültige Vermutung versucht der Prover, einen formalen Beweis zu konstruieren. Entscheidend ist, dass dem Prover die Bibliothek (enthaltend zuvor verifizierte Theoreme und Beweise) als Kontext bereitgestellt wird. Dies ermöglicht dem LLM, Beweisstrategien durch kontextbasiertes Lernen (in-context learning) ohne Neutrainieren des Modells zu erlernen. Der Prover iteriert bis zu einer maximalen Anzahl von Versuchen (in den Experimenten auf 16 gesetzt) und nutzt Fehlermeldungen des Lean-Servers, um seine Versuche zu verfeinern.
3. Iteration: Verifizierte Paare aus Vermutungen und Beweisen werden zur Bibliothek hinzugefügt, die dann als Kontext für nachfolgende Iterationen dient.

Diese Trennung ermöglicht es dem System, Suchressourcen basierend auf der Beweisschwierigkeit zuzuteilen. Im Gegensatz zu einer einfachen Schleife (SL), bei der eine Aussage und ein Beweis gleichzeitig generiert werden, versucht CPL für eine einzelne Aussage mehrere Beweise, bevor sie verworfen wird. Dies verschiebt die Verteilung der generierten Theoreme hin zu solchen, die beweisbar, aber schwierig sind, anstatt zu solchen, die lediglich leicht zu beweisen sind.

Hauptbeiträge

1. Pipeline-Vorschlag: Die Einführung von CPL, eines Frameworks, das die Generierung von Vermutungen von der Generierung von Beweisen entkoppelt und die Entdeckung längerer, komplexerer Beweise ermöglicht.
2. Kontextbasiertes Lernen für geschlossene Modelle: Der Nachweis, dass geschlossene LLMs (speziell ChatGPT-o3) ihre Beweisfähigkeiten durch kontextbasiertes Lernen aus ihren eigenen zuvor verifizierten Ausgaben verbessern können, wodurch die Notwendigkeit von Parameter-Updates oder Fine-Tuning entfällt.
3. Theoretische und empirische Validierung: Die Arbeit liefert ein theoretisches Modell, das zeigt, dass CPL im Vergleich zu Frameworks zur gleichzeitigen Generierung die Wahrscheinlichkeit erhöht, schwer zu beweisende Theoreme zu generieren. Experimentell wird bestätigt, dass CPL erfolgreich ein spezifisches Theorem auf Forschungsniveau wiederentdeckt hat, das das Baseline-Framework nicht finden konnte.

Experimentelle Ergebnisse
Die Autoren bewerteten CPL gegen eine Baseline mit einfacher Schleife (SL) unter Verwendung topologischer Begriffe (halboffene Mengen, $\alpha$-offenheit und Preopenness), die innerhalb von Mathlib definiert, aber noch nicht in die Bibliothek aufgenommen waren. Das Ziel war das Theorem, das besagt, dass der Schnitt zweier $\alpha$-offener Mengen $\alpha$-offen ist.

• Entdeckungsrate: In 20 experimentellen Durchläufen entdeckte CPL das Zielftheorem 5 Mal. Im Gegensatz dazu gelang es dem SL-Framework, das im Durchschnitt signifikant mehr Theoreme generierte (328 vs. 106), nicht einmal, das Zielftheorem zu generieren. Ein exakter Fisher-Test bestätigte, dass dieser Unterschied statistisch signifikant ist ($p = 0,024$).
• Beweislänge: CPL generierte Theoreme mit signifikant längeren Beweislängen (in Zeichenanzahl) im Vergleich zu SL, was die theoretische Behauptung stützt, dass das Framework den Fokus auf schwierigere Beweise verschiebt.
• Wirksamkeit des Kontexts:
  • Wiederbeweisen: Beim Wiederbeweisen generierter Theoreme erhöhte die Bereitstellung der Bibliothek als Kontext die Erfolgsrate von 91 % auf 99 % ($p = 4 \times 10^{-35}$).
  • Zielftheorem: Beim Versuch, das Zielftheorem über den Schnitt $\alpha$-offener Mengen wiederzubeweisen, gelang dem Prover in 80 Versuchen 7 Mal der Erfolg, wenn die generierte Bibliothek als Kontext bereitgestellt wurde. Ohne die Bibliothek scheiterte er zu 100 %.
  • Baseline in natürlicher Sprache: Als ChatGPT-4o aufgefordert wurde, das Theorem in natürlicher Sprache zu beweisen, bewertete es das Theorem häufig als falsch oder lieferte falsche Beweise; ChatGPT-o3 bewertete es konsequent als falsch, was darauf hindeutet, dass das Theorem außerhalb des vorab trainierten Wissens der Modelle lag. Der Erfolg in Lean 4 wurde dem kontextbasierten Lernen von Beweisstrategien aus der generierten Bibliothek zugeschrieben.

Bedeutung und Behauptungen
Die Arbeit behauptet, dass CPL die Einschränkung von LLMs bei der Entdeckung nicht-trivialer Theoreme effektiv adressiert, indem es kontextbasiertes Lernen aus selbstgenerierten, verifizierten Beweisen nutzt. Die Autoren betonen, dass dieser Ansatz die automatische Erweiterung formaler mathematischer Bibliotheken (wie Mathlib) ermöglicht, indem er Propositionen zu gegebenen Begriffen generiert, die dem LLM möglicherweise nicht explizit bekannt sind. Die Arbeit legt nahe, dass die Trennung der Phasen Vermutungen und Beweise, kombiniert mit einer iterativen Kontextanreicherung, eine tragfähige Strategie für das neuronale Theorembeweisen ist, insbesondere für geschlossene Modelle, bei denen traditionelle Trainingsmethoden nicht anwendbar sind. Die Autoren nehmen eine bescheidene Haltung ein und stellen fest, dass zwar das Framework erfolgreich ein bekanntes Theorem auf Forschungsniveau wiederentdeckt hat, aber zukünftige Arbeiten erforderlich sind, um den Generierungsprozess für tiefere und aussagekräftigere mathematische Aussagen zu verfeinern.