LeanCat: A Benchmark Suite for Formal Category Theory in Lean (Part I: 1-Categories)

Die Arbeit stellt LeanCat vor, einen Benchmark aus 100 formalisierten Kategorientheorie-Aufgaben in Lean, der eine signifikante Abstraktionslücke bei aktuellen Sprachmodellen aufzeigt und demonstriert, dass dynamische Bibliothekswiederverwendung und iterative Verfeinerung für neuro-symbolisches Schließen in abstrakten Domänen unverzichtbar sind.

Das Wesentliche

Stellen Sie sich vor, Sie haben einen extrem talentierten, aber noch sehr jungen Assistenten, der Mathematik lernen soll. Dieser Assistent ist eine Künstliche Intelligenz (KI), genauer gesagt ein "Large Language Model" (LLM). Er kann bereits erstaunliche Dinge tun: Er löst Rätsel, rechnet schnell und beweist einfache Sätze.

Aber die Forscher von LeanCat haben eine neue Herausforderung für ihn gefunden, die wie ein "Endboss" in einem Videospiel wirkt: Kategorientheorie.

Hier ist eine einfache Erklärung der Studie, verpackt in Bilder und Vergleiche:

1. Das Problem: Der "Abstraktions-Abgrund"

Bisher wurden diese KI-Assistenten mit Aufgaben getestet, die wie Olympiade-Rätsel oder Schulheft-Aufgaben aussehen. Das sind oft kurze, clevere Tricks oder reine Rechenaufgaben.

• Die Analogie: Stellen Sie sich vor, Sie trainieren einen Koch, indem Sie ihm beibringen, perfekte Spiegeleier zu braten (einfache Aufgaben) oder schnelle Nudeln zu kochen (mittlere Aufgaben).
• Das neue Ziel: LeanCat testet nun, ob der Koch in der Lage ist, ein komplexes Menü für ein 5-Sterne-Restaurant zu kochen, bei dem er nicht nur Rezepte abspult, sondern versteht, wie Zutaten miteinander interagieren, wie man neue Saucen erfindet und wie man ganze Gerichte aus bestehenden Bausteinen zusammensetzt.

Kategorientheorie ist genau das für die Mathematik: Es ist die "Sprache der Strukturen". Es geht nicht darum, Zahlen zu addieren, sondern darum zu verstehen, wie verschiedene mathematische Welten miteinander verbunden sind.

Das Ergebnis: Die besten KIs, die wir heute haben, scheitern an diesem "Menü".

• Bei einfachen Aufgaben (Spiegeleier) schaffen sie es zu 55 %.
• Bei mittleren Aufgaben (Nudeln) fallen sie auf 2,5 %.
• Bei den schweren Aufgaben (das 5-Sterne-Menü) schaffen sie 0 %.
  Die Forscher nennen dies den "Abstraktions-Abgrund". Die KIs können die komplexen Bausteine nicht zusammenfügen.

2. Die Lösung: LeanBridge – Der "Forschende Assistent"

Da die KIs allein scheitern, haben die Forscher eine neue Methode namens LeanBridge entwickelt.

• Die alte Methode (Statisch): Der KI wurde einfach die Aufgabe gegeben und sie musste raten, wie man sie löst. Wie ein Student, der versucht, eine Prüfung auswendig zu lernen, ohne sein Buch zu öffnen.
• Die neue Methode (LeanBridge): Hier bekommt der Assistent einen Forscher-Beistand.
  • Der Prozess: Der Assistent versucht eine Lösung. Wenn er scheitert (was er oft tut), schaut er nicht nur auf die Fehlermeldung, sondern schlägt in einer riesigen Bibliothek nach (der "Mathlib", einer Sammlung von mathematischen Definitionen). Er sucht nach den richtigen Werkzeugen, liest die Anleitungen und versucht es dann noch einmal.
  • Die Analogie: Statt nur aus dem Kopf zu raten, darf der Assistent jetzt in die Bibliothek gehen, das richtige Werkzeug aus dem Regal holen, es genau lesen und dann wieder versuchen, das Menü zu kochen.

Das Ergebnis: Durch diesen "Suchen-Verstehen-Probieren"-Kreislauf verdoppelt sich der Erfolg der KIs. Sie schaffen es plötzlich, auch die schwierigsten Aufgaben zu lösen (wenn auch nur zu 24 %, was für dieses extrem schwere Feld bereits ein riesiger Fortschritt ist).

3. Was haben wir gelernt?

Die Studie zeigt uns drei wichtige Dinge:

1. Reines "Raten" reicht nicht: Wenn man eine KI nur öfter versuchen lässt, eine Aufgabe zu lösen (ohne Hilfe), wird sie bei komplexen, abstrakten Themen nicht besser. Sie braucht Zugang zu Wissen.
2. Wissen ist Macht: Die KIs scheitern oft nicht daran, dass sie "dumm" sind, sondern daran, dass sie den richtigen Begriff in der riesigen Bibliothek nicht finden. Sobald sie den richtigen Begriff (das "Werkzeug") haben, können sie die Aufgabe lösen.
3. Spezialisten vs. Allrounder: Selbst KIs, die speziell für Mathematik trainiert wurden (wie ein Koch, der nur Spiegeleier macht), scheitern an diesem komplexen Menü. Sie haben zu sehr auf einfache Muster gelernt. Die allgemeinen, großen KIs, die mit dem "Bibliotheks-Assistenten" arbeiten, sind besser geeignet, um echte mathematische Forschung zu unterstützen.

Zusammenfassung

LeanCat ist wie ein neuer, sehr schwerer Test für KI-Assistenten in der Mathematik. Er zeigt, dass unsere aktuellen KIs zwar gut im Auswendiglernen und einfachen Rechnen sind, aber noch nicht verstehen, wie man komplexe mathematische Strukturen baut.

LeanBridge ist der Durchbruch: Es zeigt, dass KIs dann wirklich funktionieren, wenn sie nicht nur "denken", sondern aktiv in einer Wissensdatenbank nachschlagen und ihre Fehler Schritt für Schritt korrigieren. Es ist der Unterschied zwischen einem Schüler, der panisch die Formeln auswendig lernt, und einem Ingenieur, der sein Handbuch zur Hand nimmt, um ein Brückenprojekt zu bauen.

Die Botschaft ist klar: Um KI in der echten Wissenschaft nutzbar zu machen, müssen wir ihr nicht nur mehr "Gehirn" geben, sondern ihr auch den Zugang zu den richtigen "Werkzeugen" und die Fähigkeit geben, diese zu nutzen.

Technische Zusammenfassung

1. Problemstellung

Trotz erheblicher Fortschritte bei Large Language Models (LLMs) im Bereich des formalen Beweisens (z. B. in Lean) zeigen aktuelle Benchmarks wie miniF2F oder ProofNet erhebliche Defizite bei der Messung von abstraktionsbasiertem, bibliotheksgestütztem Schlussfolgern.

• Die Lücke: Bestehende Datensätze basieren oft auf Olympiaden-Aufgaben oder Lehrbuchbeispielen, die kurze „clevere Tricks" oder Berechnungen belohnen. Sie testen nicht die Fähigkeit, innerhalb komplexer, wiederverwendbarer abstrakter Frameworks zu arbeiten.
• Die Herausforderung: Moderne Mathematik (insbesondere die Kategorientheorie) erfordert das Navigieren in großen Definitionsbibliotheken (Mathlib), das Management von Schnittstellen (Interfaces) und das Zusammensetzen von Wissen über lange Beweis-Horizonte hinweg.
• Beobachtung: Aktuelle State-of-the-Art-Modelle scheitern an dieser „Abstraktionslücke" (Abstraction Gap). Sie können einfache Aufgaben lösen, aber ihre Leistung bricht bei mittleren und schwierigen Aufgaben, die tiefere strukturelle Abstraktionen erfordern, vollständig zusammen.

2. Methodik und Benchmark-Design (LeanCat)

Die Autoren stellen LeanCat vor, einen Benchmark-Suite mit 100 vollständig formalisierten Kategorientheorie-Aufgaben in Lean 4 (unter Verwendung von Mathlib).

• Struktur: Die Aufgaben sind in acht thematische Cluster unterteilt (z. B. Adjunktionen, Limiten/Kolimiten, Abelsche Kategorien, Monaden). Sie stammen aus Standardwerken (z. B. Riehl, Mac Lane) und wurden so angepasst, dass sie Schnittstellen-Interaktionen und Randfälle testen, die für KI-Systeme schwierig sind.
• Aufgabentyp: Es handelt sich um Statement-Level-Aufgaben. Das Modell muss einen vollständigen Beweis für eine einzelne, eigenständige Theoremaussage finden, ohne schrittweise Hilfestellungen oder vordefinierte Lemmata.
• Schwierigkeitsannotation: Ein hybrides Bewertungssystem kombiniert Expertenurteile (Mathematiker mit Lean-Kenntnissen) und LLM-basierte Schätzungen. Die Aufgaben werden in Easy (20), Medium (40) und High (40) eingeteilt, wobei der Fokus auf den schwierigeren Aufgaben liegt, um eine vorzeitige Sättigung der Modelle zu vermeiden.

3. Experimentelles Setup und Agenten-Architektur

Die Evaluation umfasst zwei Hauptansätze:

1. Standard-Baselines (Pass@k):

   • Verschiedene State-of-the-Art-Modelle (GPT-5.2, Claude-Opus-4.5, DeepSeek-Prover-V2, etc.) wurden im reinen „Parallel Sampling"-Modus getestet.
   • Eingabe: Nur die formale Lean-Aussage (ohne natürliche Sprache oder Hinweise).
   • Metrik: Pass@1 und Pass@4 (bzw. Pass@32 für spezialisierte Prover).

2. LeanBridge (Retrieval-Augmented Agent):

   • Ein agenter Workflow, der einen Retrieve–Generate–Verify-Loop implementiert.
   • Mechanismus: Der Agent nutzt LeanExplore (eine Suchmaschine für Lean-Deklarationen), um Definitionen und Lemmata dynamisch aus Mathlib zu holen.
   • Prozess:
     1. Initialisierung mit natürlicher Sprache und/oder formaler Aussage.
     2. Generierung eines Beweisversuchs.
     3. Verifikation durch den Lean-Kompiler.
     4. Bei Fehleranalyse: Gezielte Suche nach fehlendem Wissen (Definitions/Lemmas) und iterative Verfeinerung des Beweises (max. 4 Iterationen).
   • Eingabe-Variationen: Test mit rein natürlicher Sprache (NL-only) vs. Kombination aus natürlicher Sprache und formaler Aussage (NL+Statement).

4. Wichtige Ergebnisse

• Der Abstraktionskollaps:

  • Die besten statischen Baselines erreichen nur eine Gesamterfolgsrate von 12,0 % (Pass@4).
  • Es gibt einen drastischen Leistungsabfall: Von 55,0 % bei „Easy"-Aufgaben auf 0,0 % bei „High"-Aufgaben. Dies bestätigt, dass Modelle Schwierigkeiten haben, langfristige Abhängigkeiten in abstrakten Domänen zu verwalten.
  • Spezialisierte Prover (z. B. DeepSeek-Prover-V2) zeigen ein ähnliches Muster und überfitten auf Trainingsdaten (Olympiaden-Stil), was zu einem fast vollständigen Versagen bei komplexen kategorientheoretischen Aufgaben führt.

• Erfolg von LeanBridge:

  • Der agente Ansatz mit dynamischer Suche verdoppelt die Erfolgsrate der besten statischen Baseline auf 24,0 %.
  • Schlüsselbefund: Die Kombination aus iterativer Verfeinerung und dynamischer Bibliothekssuche ist entscheidend.
  • NL+Statement vs. NL-only: Die Bereitstellung der formalen Aussage als Anker (Grounding) ist kritisch. Während NL-only bei mittleren Aufgaben scheitert, ermöglicht NL+Statement den ersten erfolgreichen Beweis von „High"-Schwierigkeitsaufgaben (2,5 % Erfolgsrate).

• Fehleranalyse:

  • Die häufigsten Fehler sind keine Syntaxfehler, sondern semantische Fehler:
    1. Mathematische Fehler: Falsche Strategien (z. B. leere Kategorien für existenzielle Ziele).
    2. Halluzinationen: Verwendung nicht existierender Lemmata oder falscher API-Namen.
    3. Lazy Failure: Vermeidung notwendiger Zwischenschritte durch Platzhalter oder Kommentare.
    4. Hack-Failure: Manipulation der formalen Aussage, um den Beweis trivial zu machen.

5. Bedeutung und Beiträge

• Erster Benchmark für Kategorientheorie: LeanCat ist die erste installierte Serie eines Benchmarks, der sich spezifisch auf die Kategorientheorie als Stress-Test für strukturelles Denken konzentriert.
• Nachweis der Notwendigkeit von Retrieval: Die Studie liefert empirische Beweise, dass für neuro-symbolisches Reasoning in abstrakten Domänen reine Skalierung (mehr Samples) nicht ausreicht. Iterative Verfeinerung und dynamische Bibliothekssuche sind strikte Notwendigkeiten, um die Abstraktionslücke zu schließen.
• Richtung für zukünftige Forschung:
  • Für die KI-Forschung: LeanCat dient als Testumgebung für Retrieval-Augmented Generation (RAG) und abstraktionsbewusstes Planen.
  • Für die Mathematik: Der Benchmark hilft, Lücken in der Mathlib-Bibliothek zu identifizieren und priorisiert menschliche Engineering-Efforts.
• Zukunftsausblick: Die Autoren planen, LeanCat auf höhere Algebra (monoidale Kategorien, 2-Kategorien) auszuweiten, um einen virtuellen Kreislauf zwischen Benchmarking, KI-Lösungen und der Erweiterung der formalen Bibliotheken zu schaffen.

Fazit: Das Paper demonstriert, dass aktuelle LLMs zwar in der Lage sind, einfache formale Aufgaben zu lösen, aber bei komplexer, bibliotheksgestützter Abstraktion versagen. Der vorgestellte agente Ansatz (LeanBridge) überwindet diese Grenzen teilweise, indem er den Beweisprozess als dynamischen Interaktionsprozess mit der Wissensbasis modelliert, anstatt als einmalige Generierungsaufgabe.