TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?

Die Studie stellt mit TaoBench einen neuen Benchmark vor, der zeigt, dass aktuelle automatische Theorembeweiser zwar im etablierten MathLib-Framework gut funktionieren, aber bei mathematisch äquivalenten Problemen in einem maßgeschneiderten Definitionsrahmen, der auf Terence Taos Analysis I basiert, signifikant schlechter abschneiden, was auf eine mangelnde Generalisierungsfähigkeit über verschiedene Definitionsrahmen hinweg hindeutet.

Das Wesentliche

Stell dir vor, du hast einen extrem talentierten Mathematik-Genie-Roboter. Dieser Roboter wurde jahrelang von den besten Lehrern der Welt trainiert, aber nur mit einem ganz bestimmten Lehrbuch: dem „MathLib". Das ist wie eine riesige, perfekt organisierte Bibliothek, in der jede mathematische Definition, jedes Symbol und jede Regel genau so definiert ist, wie die Bibliothekare es wollen.

Wenn du diesem Roboter eine Aufgabe aus diesem Buch gibst, ist er unschlagbar. Er findet die Lösung blitzschnell.

Das Problem: Die „echte" Mathematik ist chaotisch

Jetzt stell dir vor, du bringst diesen Roboter in ein echtes Forschungslabor. Hier arbeiten Mathematiker wie Terence Tao. Sie erfinden neue Konzepte, bauen ihre eigenen Werkzeuge und definieren Dinge oft anders als im Standard-Lehrbuch. Es ist wie der Unterschied zwischen einem Koch, der nur in einer Fabrikküche mit vorgefertigten Saucen kocht, und einem Sternekoch, der selbst Gemüse anpflanzt, Gewürze mahlt und seine eigenen Saucen mischt.

Die Forscher wollten wissen: Kann unser Roboter auch dann kochen, wenn er keine vorgefertigten Saucen (MathLib) bekommt, sondern selbst alles von Grund auf aufbauen muss?

Die Lösung: TAOBENCH (Der „Tao-Test")

Um das herauszufinden, haben die Autoren des Papers einen neuen Test entwickelt, den sie TAOBENCH nennen.

1. Der Test: Sie haben 150 Aufgaben aus Terence Taos Analysis-Buch genommen. In diesem Buch werden mathematische Konzepte (wie Zahlen oder Mengen) komplett neu und anders definiert als im Standard-Lehrbuch. Es ist, als würde der Koch sagen: „Vergiss die vorgefertigte Tomatensauce. Wir machen sie jetzt aus frischen Tomaten, die wir selbst geerntet haben."
2. Der Vergleich: Damit der Test fair ist, haben sie für jede dieser „frischen" Aufgaben eine zweite Version erstellt, die genau dieselbe mathematische Aufgabe ist, aber in der Sprache des Standard-Lehrbuchs (MathLib) geschrieben wurde.
3. Der Trick: Sie haben einen cleveren Roboter-Automaten gebaut, der sicherstellt, dass der Test-Roboter alle notwendigen Definitionen direkt vor sich hat, damit er nicht einfach aufgibt, weil ihm etwas fehlt.

Die überraschende Entdeckung

Das Ergebnis war schockierend, aber wichtig:

• Im Standard-Modus (MathLib): Der Roboter löste die Aufgaben sehr gut (ca. 70 % Erfolg).
• Im „Frisch-Modus" (Tao): Sobald die Aufgaben nur die Definitionen von Terence Tao benutzten, brach die Leistung dramatisch ein. Der Roboter löste nur noch etwa 40–45 % der Aufgaben.

Was bedeutet das? (Die Analogie)

Stell dir vor, du hast einen Schüler, der den Fahrkurs perfekt gelernt hat, aber nur mit einem Auto, das Pedale hat, die man mit dem linken Fuß bedient.

• Wenn du ihm ein Auto gibst, das Pedale hat, die man mit dem rechten Fuß bedient (die MathLib-Version), fährt er perfekt.
• Wenn du ihm aber ein Auto gibst, das Pedale hat, die man mit dem linken Fuß bedient, aber die Bremsen und der Lenker ganz anders angeordnet sind (die Tao-Version), dann fährt er gegen die Wand.

Der Schüler hat nicht gelernt, Fahren zu verstehen. Er hat gelernt, dieses eine spezifische Auto zu bedienen.

Die große Lektion

Das Paper zeigt uns, dass unsere aktuellen KI-Modelle für Mathematik nicht wirklich „intelligent" im Sinne von tiefem Verständnis sind. Sie sind eher wie Parrot-Imitatoren. Sie haben gelernt, Muster in der Sprache von MathLib zu erkennen. Wenn die Sprache (die Definitionen) sich ändert, auch wenn die eigentliche Mathematik dieselbe bleibt, verlieren sie die Orientierung.

Warum ist das wichtig?

Echte mathematische Forschung findet oft in diesen „neuen Sprachen" statt. Wenn wir KI-Systeme wollen, die uns bei der Entdeckung neuer Theorien helfen können, müssen wir sie nicht nur auf das eine Standard-Lehrbuch trainieren. Wir müssen sie lehren, flexibel zu sein und neue Definitionen zu verstehen, ohne in Panik zu verfallen.

Zusammenfassung in einem Satz:
Unsere aktuellen KI-Mathematiker sind wie Genies, die nur eine einzige Sprache sprechen; sobald man sie in ein Land schickt, wo die Wörter anders klingen, aber die Bedeutung dieselbe ist, verstehen sie plötzlich gar nichts mehr. Der TAOBENCH-Test ist der Weckruf, dass wir KI-Systeme brauchen, die wirklich verstehen, nicht nur auswendig lernen.

Technische Zusammenfassung

1. Problemstellung

Automatisierte Theorembeweiser (ATP) auf Basis von Large Language Models (LLMs) haben in den letzten Jahren erhebliche Fortschritte gemacht, insbesondere bei Benchmarks, die auf MathLib (der Standard-Bibliothek für Lean 4) basieren. Die aktuelle Forschung und Evaluation ist jedoch stark verzerrt, da fast alle Trainingsdaten und Testfälle innerhalb des definitorischen Rahmens von MathLib formuliert sind.

Das Kernproblem liegt darin, dass mathematische Forschung oft explorativ ist und maßgeschneiderte Konstruktionen erfordert, die von Standardbibliotheken abweichen. Wenn ATP-Modelle auf solche neuen definitorischen Frameworks treffen (Out-of-Distribution), ist unklar, ob sie ihre Beweiskapazitäten generalisieren können oder ob ihre Leistung durch die spezifische Syntax und Definitionen von MathLib limitiert ist. Bisherige Benchmarks vermischen mathematische Schwierigkeit mit der Vertrautheit zu einem bestimmten Formalismus, was die Bewertung der echten Generalisierungsfähigkeit erschwert.

2. Methodik und Aufbau von TAOBENCH

Die Autoren stellen TAOBENCH vor, den ersten Benchmark, der speziell entwickelt wurde, um die Robustheit von ATP-Modellen jenseits von MathLib zu messen.

• Datenquelle: Der Benchmark basiert auf 150 Übungen aus Terence Taos Lean-Formalisierung von Analysis I. In diesem Werk werden mathematische Konzepte (wie Mengen, reelle Zahlen, Konvergenz) von Grund auf neu definiert, oft mit maßgeschneiderten induktiven Typen und Notationen, die sich signifikant von MathLib unterscheiden.
• Agentic Pipeline für Kontextextraktion: Um faire Tests zu gewährleisten, entwickelten die Autoren eine agentenbasierte Pipeline, die für jede Übung einen selbstständigen, kompilierbaren lokalen Lean-Kontext extrahiert.
  • Sie nutzen das statische Analysetool JiXia, um Abhängigkeiten (Theoreme, Definitionen, Notationen) rekursiv zu ermitteln.
  • Ein Agent mit Datei-Such-Tool und Lean-Verifizierer baut iterativ den minimalen Kontext auf, der für die Kompilierung notwendig ist, ohne externe Importe zu benötigen. Dies verhindert Halluzinationen und sicherstellt, dass die ursprüngliche Intention der Übung erhalten bleibt.
• TAOBENCHMATHLIB (Kontrollgruppe): Um den Effekt des definitorischen Rahmens isoliert von der mathematischen Schwierigkeit zu untersuchen, wurde für jede TAOBENCH-Übung eine mathematisch äquivalente Version in MathLib-Syntax erstellt.
  • Dieser Prozess umfasst eine mehrstufige Pipeline: Umformulierung durch ein LLM (GPT-5.1) mit Web-Suche, iterative Kompilierungskorrektur und ein Äquivalenz-Check (mittels JiXia und LLM), gefolgt von manueller Expertenverifikation.
  • Dies ermöglicht einen direkten Vergleich: Gleiche mathematische Aufgabe, unterschiedliche definitorische Frameworks.

3. Wichtige Beiträge

1. TAOBENCH: Ein Benchmark, der die Generalisierungsfähigkeit von ATP-Modellen auf ein neues, nicht-Standard definitorisches Framework (Tao's Analysis I) testet.
2. TAOBENCHMATHLIB: Eine Paarung von mathematisch äquivalenten MathLib-Formulierungen, die es erlaubt, die Leistungslücke direkt auf den definitorischen Wechsel zurückzuführen.
3. Automatisierte Pipelines: Zwei skalierbare Pipelines zur Extraktion selbstständiger Kompilierungskontexte aus großen formalisierten Projekten sowie zur Erstellung äquivalenter MathLib-Formulierungen. Dies bietet eine Grundlage für die Generierung hochwertiger Trainingsdaten für zukünftige Modelle.

4. Ergebnisse

Die Autoren evaluierten mehrere State-of-the-Art ATP-Modelle (DeepSeek-Prover-V2, Goedel-Prover-V2, Kimina-Prover) sowie Frontier-Modelle (GPT-5.1, Gemini 3 Pro).

• Signifikanter Leistungsabfall: Während die Modelle auf TAOBENCHMATHLIB hohe Erfolgsquoten erzielen (oft >65–70 %), bricht die Leistung auf TAOBENCH (Tao's Framework) im Durchschnitt um ca. 26 % ein.
  • Beispiel: Goedel-Prover-V2-32B erreicht auf MathLib 72,67 %, fällt aber auf Tao-Formulierungen auf 49,33 %.
  • DeepSeek-Prover-V2-7B fällt von 69,33 % auf 41,33 %.
• Einfluss des Kontexts (Definitionen): Die Leistungslücke vergrößert sich drastisch mit der Anzahl der im Kontext bereitgestellten lokalen Definitionen.
  • Bei $n=0$ lokalen Definitionen ist die Leistung ähnlich.
  • Bei $n \ge 10$ lokalen Definitionen bricht die Pass-Rate auf Tao-Formulierungen bei allen Modellen auf unter 10 % ein, während sie auf MathLib-Formulierungen nur moderat abfällt.
• Skalierung: Größere Modelle (32B vs. 8B) verbessern die absolute Leistung, beseitigen aber die Generalisierungslücke nicht.
• Frontier-Modelle: Allgemeine LLMs (wie GPT-5.1) schneiden auf Tao-Formulierungen besser ab als spezialisierte ATP-Modelle, was darauf hindeutet, dass sie besser darin sind, kontextuelle Informationen zu nutzen, auch wenn sie keine spezialisierten Beweiser sind.

5. Fallstudien und Analyse

• Nat.backwards_induction: Auf Tao's Formulierungen (mit maßgeschneiderter Addition und Ordnung) scheitern Modelle oft, da sie die notwendigen algebraischen Lemmas nicht aus dem Kontext ableiten können. Auf MathLib nutzen sie Standard-Lemmas erfolgreich.
• Convergesto.squeeze: Hier zeigt sich ein Unterschied zwischen einer expliziten $\varepsilon$-$\delta$-Definition (Tao) und einer Filter-basierten Tendsto-Definition (MathLib). Interessanterweise performt ein Modell auf der expliziten Tao-Definition besser als auf der abstrakten MathLib-Version, was zeigt, dass die Schwierigkeit nicht nur von der Abstraktionsebene, sondern von der spezifischen Vertrautheit mit dem Framework abhängt.

6. Bedeutung und Fazit

Die Studie enthüllt eine fundamentale Schwäche aktueller ATP-Modelle: Sie generalisieren nicht zuverlässig über definitorische Frameworks hinweg.

• Hauptbottleneck: Das Problem liegt weniger in der mathematischen Schwierigkeit, sondern in der Unfähigkeit der Modelle, sich schnell an neue Definitionen und Notationen anzupassen, selbst wenn diese im Kontext bereitgestellt werden.
• Implikation für die Forschung: Die hohe Leistung auf aktuellen Benchmarks (wie MiniF2F oder MathLib-basierten Datensätzen) spiegelt oft nur die Vertrautheit mit einem spezifischen Ökosystem wider, nicht aber die Fähigkeit, echte Forschungsmathematik zu betreiben, die oft neue Definitionen erfordert.
• Zukunft: TAOBENCH bietet eine konkrete Testumgebung, um zukünftige Beweiser zu entwickeln, die robuster gegenüber definitorischen Verschiebungen sind und besser mit dem explorativen Charakter echter mathematischer Forschung übereinstimmen.

Zusammenfassend zeigt das Paper, dass die aktuelle Ära der ATP-Modelle noch stark an das MathLib-Ökosystem gebunden ist und dass ein Paradigmenwechsel notwendig ist, um Modelle zu schaffen, die echte mathematische Generalisierung leisten können.