SorryDB: Can AI Provers Complete Real-World Lean Theorems?

Die Arbeit stellt SorryDB vor, ein dynamisches Benchmark-System für reale Lean-Theoreme aus GitHub-Projekten, das zeigt, dass aktuelle KI-Ansätze wie Agenten, große Sprachmodelle und spezialisierte Beweiser komplementär sind und keine einzelne Methode alle anderen vollständig übertrifft.

Das Wesentliche

🧱 SORRYDB: Der „Flickschuster"-Test für KI-Mathematiker

Stell dir vor, du hast einen riesigen, komplexen Baukasten (wie Lego), mit dem Mathematiker auf der ganzen Welt zusammenarbeiten, um die schwierigsten Rätsel der Welt zu lösen. Aber es gibt ein Problem: Viele der Bauanleitungen sind unvollständig. An den Stellen, an denen ein wichtiger Baustein fehlt, haben die Architekten ein gelbes Klebeband mit der Aufschrift „SORRY" (Entschuldigung) geklebt. Das bedeutet: „Hier fehlt noch etwas, ich komme später darauf zurück."

Das Paper SORRYDB stellt sich genau diese Frage: Können künstliche Intelligenzen (KI) diese „Entschuldigungen" (Sorry) wirklich entfernen und die Lücken in den echten Bauplänen füllen?

1. Das Problem: Die alten Prüfungen sind zu leicht

Bisher wurden KI-Modelle für Mathematik wie Schüler getestet, die nur für die Olympiade gelernt haben (Wettbewerbsaufgaben). Das ist wie wenn man einen Autofahrer nur auf einer leeren Rennstrecke prüft. Er kann schnell fahren, aber weiß er, wie man im echten Stadtverkehr mit Baustellen, Fußgängern und Regen umgeht?

Die alten Tests sind zudem „abgenutzt". Die KIs haben die Lösungen oft schon auswendig gelernt (wie ein Schüler, der die Antworten im Internet nachschaut), statt wirklich zu verstehen.

2. Die Lösung: SORRYDB – Der echte Baustellen-Test

Die Autoren haben SORRYDB erfunden. Das ist keine statische Liste von Aufgaben, sondern ein lebendiger, sich ständig aktualisierender Markt.

• Wie es funktioniert: Sie scannen 78 echte, aktive Projekte auf GitHub (wo die Mathematiker wirklich arbeiten). Sie suchen nach allen Stellen, an denen ein „SORRY" steht.
• Der Vergleich: Stell dir vor, du hast einen riesigen Haufen unvollendeter Hauspläne. SORRYDB ist wie ein Test, bei dem du der KI einen Plan gibt und sagst: „Hier fehlt der Dachstuhl. Baue ihn jetzt, aber du musst die anderen Wände, die schon stehen, mit einbeziehen."
• Der Vorteil: Da die Projekte immer weiterentwickelt werden, gibt es immer neue, frische Aufgaben. Die KI kann nicht einfach alte Lösungen auswendig lernen, weil die Aufgaben sich jeden Monat ändern.

3. Der Test: Wer ist der beste Handwerker?

Die Forscher haben verschiedene Arten von „KI-Handwerkern" getestet, um zu sehen, wer die Lücken am besten füllen kann:

• Die „Basis-Tools" (Tactics): Das sind wie ein Hammer und eine Schraubzange. Sie können einfache Reparaturen schnell erledigen, aber bei komplexen Dingen versagen sie.
• Die „Allrounder" (Große Sprachmodelle wie Gemini, Claude, GPT): Das sind die klugen Studenten. Sie können viel, aber manchmal halluzinieren sie (erfinden Bauteile, die es gar nicht gibt).
• Die „Spezialisten" (Trainierte Mathematik-KIs): Das sind die Meisterhandwerker, die nur Mathematik gelernt haben. Sie sind gut, aber manchmal zu starr.
• Die „Agenten" (KI mit Feedback-Schleife): Das ist der wichtigste Teil des Papers. Stell dir vor, ein Handwerker baut etwas, prüft es, sieht, dass es wackelt, und baut es nochmal.
  • Ergebnis: Die KIs, die iterativ arbeiten (bauen -> prüfen -> Fehlermeldung lesen -> neu bauen), waren mit Abstand am besten. Sie haben gelernt, aus ihren Fehlern zu lernen, genau wie ein echter Mensch.

4. Die überraschende Erkenntnis: Teamwork ist alles

Das Paper zeigt etwas Wundervolles: Keine einzelne KI ist perfekt.

• Die eine KI ist gut bei einfachen Aufgaben aus Lehrbüchern.
• Die andere ist gut bei komplexen, neuen Theorien.
• Die dritte ist gut darin, bestehende Bibliotheken zu nutzen.

Wenn man alle zusammenwirft (wie ein Team von Handwerkern), können sie viel mehr Aufgaben lösen als jeder einzelne für sich. Es ist wie bei einem Orchester: Die Geige allein klingt schön, aber das ganze Orchester schafft die Symphonie.

5. Warum ist das wichtig?

Früher haben wir KI nur an künstlichen Aufgaben gemessen. Mit SORRYDB testen wir sie im echten Leben.

• Es zeigt uns, wo die KI heute schon hilft (z. B. beim Überprüfen von Code).
• Es zeigt uns, wo sie noch scheitert (z. B. wenn sie zu sehr auf Suchwerkzeuge vertraut und die eigentliche Logik vergisst).

Fazit:
SORRYDB ist wie ein lebendiger Fitness-Test für KI-Mathematiker. Er zeigt uns nicht nur, wie stark sie sind, sondern zwingt sie, sich an die chaotische, echte Welt der Mathematik anzupassen. Und das Beste: Je besser die KI wird, desto schwieriger werden die Aufgaben in der Datenbank, sodass wir nie aufhören müssen, sie zu trainieren.

Kurz gesagt: Wir haben aufgehört, die KI nur in der Turnhalle trainieren zu lassen, und schicken sie jetzt direkt auf die Baustelle. Und sie lernt dort tatsächlich etwas! 🏗️🤖✨

Technische Zusammenfassung

1. Problemstellung

Die aktuelle Evaluierung von automatischen Theorembeweisern (Automated Theorem Provers, ATP) stützt sich überwiegend auf statische Benchmarks, die aus Wettbewerbsaufgaben (z. B. IMO, Putnam) oder kuratierten Datensätzen wie miniF2F oder PutnamBench bestehen. Diese Ansätze weisen mehrere kritische Mängel auf:

• Mangelnde Praxisrelevanz: Wettbewerbsaufgaben bilden nicht die Komplexität realer Formalisierungsprojekte ab, die oft von Abhängigkeiten, spezifischen Kontexten und „Unordnung" in großen Codebasen geprägt sind.
• Sättigung und Datenkontamination: Viele dieser Benchmarks sind gesättigt, und die Lösungen könnten bereits in den Trainingsdaten der großen Sprachmodelle (LLMs) enthalten sein, was die Unterscheidung zwischen Memorierung und echtem Schlussfolgern erschwert.
• Fehlende Dynamik: Statische Datensätze können nicht mit dem Fortschritt der Modelle mithalten und bieten keine Möglichkeit, die Fähigkeit von Agenten zu bewerten, zu neuen mathematischen Projekten beizutragen.

Das Ziel der Autoren ist es, einen Benchmark zu schaffen, der den tatsächlichen Arbeitsalltag von Lean-Entwicklern widerspiegelt und die praktische Nützlichkeit von KI-Systemen für die mathematische Formalisierung misst.

2. Methodik und Datensatz (SorryDB)

Die Autoren stellen SorryDB vor, einen dynamisch aktualisierten Benchmark, der auf offenen Lean-Projekten auf GitHub basiert.

• Datenerfassung: Der Datensatz wird durch das Extrahieren von sorry-Platzhaltern aus 78 aktiven Open-Source-Lean-Repositories (aus dem Lean Package Registry „Reservoir") generiert. Ein Projekt gilt als aktiv, wenn es in den letzten drei Monaten Commits erhalten hat.
• Aufgabenstellung: Die Aufgabe lautet „Fill-in-the-sorry". Das System muss den Code bereitstellen, der einen spezifischen sorry-Platzhalter in einem Theorem ersetzt, sodass der Beweisobligation (Proof Obligation) nachvollziehbar abgeschlossen wird. Es muss nicht das gesamte Theorem bewiesen werden, sondern nur der fehlende Teil.
• Kategorisierung: Die Repositories umfassen verschiedene Kategorien: Pädagogik (Lehrmaterial), Tooling, Benchmarks, Bibliotheken (z. B. Mathlib) und spezifische Formalisierungsprojekte (z. B. Fermats letzter Satz, Carlesons Theorem).
• Validierung: Ein automatisiertes Pipeline-System (unter Verwendung von LeanInteract) überprüft die Korrektheit einer Lösung, indem es den Code kompiliert und sicherstellt, dass der spezifische sorry-Platzhalter erfolgreich durch einen gültigen Beweis ersetzt wurde und keine weiteren sorry-Terme im finalen Zustand verbleiben.

3. Schlüsselbeiträge

1. Der SorryDB-Datensatz: Ein neuartiger, dynamischer Datensatz, der ungelöste Beweisziele aus realen, laufenden Projekten sammelt. Er ist konstruktiv auf praktische Anwendungen ausgerichtet und vermeidet die Sättigung durch kontinuierliche Aktualisierung.
2. Benchmarking-Framework: Eine automatisierte Validierungsmechanik, die es ermöglicht, die Genauigkeit von Theorembeweisern ohne manuelle Kuratierung von Labels zu messen.
3. Umfassende Evaluation: Eine Analyse eines statischen Schnappschusses (Januar 2026, 1000 Aufgaben) mit einer breiten Palette von Ansätzen, darunter deterministische Taktiken, allgemeine LLMs, spezialisierte Modelle und agente Architekturen.

4. Ergebnisse

Die Evaluation umfasste 1000 Aufgaben aus dem Datensatz „SorryDB-2601" und verglich verschiedene Ansätze:

• Leistungsfähigkeit:

  • Iterative Ansätze überlegen: Modelle mit Selbstkorrektur (Self-Correcting, SC) oder agenter Architektur (mit Werkzeugen wie LeanSearch) schneiden deutlich besser ab als „One-Shot"-Ansätze (pass@1).
  • Top-Performer: Ein agenter Ansatz basierend auf Gemini Flash 3 erreichte mit 30,3 % die höchste Erfolgsrate (nach 16 Iterationen).
  • Vergleich: Selbst die besten agenten Modelle waren nicht strikt überlegen gegenüber anderen Off-the-Shelf-LLMs oder spezialisierten Provern; sie ergänzen sich vielmehr.
  • Deterministische Taktiken: Einfache Taktiken (wie trivial, ring, linarith) lösten zwar nur wenige Aufgaben (8,4 %), aber sie lösten spezifische Fälle, die keine LLMs bewältigen konnten.

• Komplementarität: Die Analyse zeigte, dass verschiedene Prover unterschiedliche Teilmengen von Problemen lösen. Die Kombination aller Ansätze („Combined") löste 35,7 % der Aufgaben, was die Notwendigkeit hybrider Systeme unterstreicht.

• Fehleranalyse:

  • Spezialisierte Modelle (z. B. Goedel Prover, Kimina) hatten Schwierigkeiten, da sie oft auf älteren Lean-Versionen trainiert wurden oder sich auf Wettbewerbsmathematik spezialisiert hatten, was die Generalisierung auf reale Projekte erschwerte.
  • Agenten, die zu stark auf Suchwerkzeuge angewiesen waren, scheiterten manchmal an Aufgaben, die ein manuelles Konstruieren des Beweises erforderten, anstatt nach existierenden Lemmas zu suchen.

• Kontextabhängigkeit: Die Erfolgsrate variierte stark je nach Repository-Kategorie. Pädagogische Repositories waren am einfachsten, während komplexe Formalisierungsprojekte (z. B. Carleson) die größte Herausforderung darstellten.

5. Bedeutung und Fazit

SorryDB adressiert die Lücke zwischen theoretischen Benchmarks und der praktischen Anwendung von KI in der Mathematik.

• Dynamik: Da der Datensatz auf laufenden Projekten basiert, wird er sich mit dem Fortschritt der KI-Modelle weiterentwickeln. Sobald Modelle die aktuellen „sorrys" lösen, werden die verbleibenden Aufgaben schwieriger, was einen „moving benchmark" ohne Sättigungseffekt garantiert.
• Praxisnähe: Der Datensatz zwingt Modelle dazu, mit lokalem Kontext, Abhängigkeiten und unvollständigen Beweisen umzugehen, was für die tatsächliche Unterstützung von Mathematikern entscheidend ist.
• Zukunft: Die Autoren schlagen vor, zukünftig Leaderboards und Elo-basierte Bewertungssysteme einzuführen, um die relative Leistung von Modellen in diesem sich ständig verändernden Umfeld zu messen.

Zusammenfassend demonstriert die Arbeit, dass aktuelle KI-Systeme zwar Fortschritte machen, aber noch keine universellen Lösungen für reale Formalisierungsaufgaben darstellen. Der Erfolg hängt stark von iterativen Feedback-Schleifen, der Fähigkeit, den lokalen Kontext zu verstehen, und der Kombination verschiedener Beweisstrategien ab.