🤖 AI

Sorries Are Not the Hard Part: An Expert-Review Case Study of a Semi-Autonomous Formalization

Diese Arbeit argumentiert, dass erfolgreiche Autoformalisierung durch die Expertenbewertung der Definitionsqualität und des API-Designs bewertet werden muss, anstatt lediglich durch das Fehlen unbewiesener Lücken („sorries“), und demonstriert anhand einer Fallstudie zu Grothendiecks Verschwindungssatz, dass KI-Agenten zwar effektiv lokale mechanische Korrekturen anwenden können, aber Schwierigkeiten mit dem konzeptionellen High-Level-Design haben.

Ursprüngliche Autoren: Vasily Ilin, Brian Nugent

Veröffentlicht 2026-06-15

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Vasily Ilin, Brian Nugent

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Stellen Sie sich vor, Sie stellen einen sehr schnellen, sehr eifrigen Lehrling ein, um ein Haus für Sie zu bauen. Sie geben ihm die Baupläne (ein mathematisches Theorem) und ein Lehrbuchkapitel, das erklärt, wie man es baut.

Der Lehrling arbeitet Tag und Nacht. Er setzt die Ziegel, errichtet das Gebälk und installiert das Dach. Wenn er fertig ist, steht das Haus perfekt. Es stürzt nicht ein. Der Inspektor (der Computer) sagt: „Gute Arbeit! Das Haus ist strukturell einwandfrei.“

In diesem Paper geht es darum, was als Nächstes passiert.

Die Autoren dieses Papers fragten sich: „Nur weil das Haus steht, ist es dann auch wirklich ein gutes Haus? Kann man darin wohnen? Kann man später problemlos ein zweites Stockwerk hinzufügen, oder muss man erst die Wände abreißen?“

Hier ist die Aufschlüsselung ihres Experiments, unter Verwendung einfacher Analogien:

Das Experiment: Ein „Mathematik-Haus“ bauen

Das Team bat eine KI (ein Large Language Model), ein komplexes mathematisches Theorem namens Grothendiecks Verschwindungssatz zu formalisieren. Betrachten Sie dieses Theorem als eine sehr spezifische, anspruchsvolle architektonische Herausforderung.

Sie gaben der KI:

Das Ziel (die Aussage des Theorems).
Einen Lehrbuchbeweis (die Anweisungen).
Eine Regel: „Du musst nur die bestehenden, standardmäßigen Werkzeuge verwenden, die wir bereits in unserem Werkzeugkasten haben (die Mathematik-Bibliothek).“

Phase 1: Das „Bestanden“ (Zustand A)
Die KI arbeitete hart und produzierte Code, der ohne Fehler kompiliert. In der Welt der Mathematik-Software werden Fehler als „Sorries“ bezeichnet (kurz für „Sorry, ich kann das noch nicht beweisen“). Die KI schaffte es, die Anzahl der „Sorries“ auf Null zu senken.

Das Ergebnis: Das Haus steht. Der Computer ist zufrieden.
Das Problem: Ein menschlicher Experten-Architekt (ein Mathematiker) sah sich das Haus an und sagte: „Das ist eine Katastrophe.“

Die Expertenbewertung: Warum das „stehende Haus“ versagte

Der menschliche Experte fand heraus, dass das Haus zwar nicht zusammenbrach, aber furchtbar gebaut war. Hier sind die spezifischen Probleme, die er fand, übersetzt in Alltagssprache:

1. Das Problem mit den „maßgeschneiderten Werkzeugen“ (Definitionen)

Was die KI tat: Die KI erfand für jede noch so kleine Aufgabe ihre eigenen, maßgeschneiderten Werkzeuge. Wenn sie eine Wand messen musste, baute sie ein neues, seltsames Maßband nur für diese eine Wand.
Warum das schlecht ist: In einer echten Bibliothek möchte man Standardwerkzeuge, die jeder kennt und benutzen kann. Wenn die KI für jeden Job ein maßgeschneidertes Werkzeug baut, können zukünftige Baumeister das Haus nicht nutzen, weil sie nicht wissen, wie man die seltsamen Erfindungen der KI bedient.
Das Urteil: Die KI war gut darin, Werkzeuge zu benutzen, aber schlecht darin, sie zu entwerfen. Sie erstellte 62 benutzerdefinierte Definitionen, von denen 61 nutzlos oder verwirrend waren.

2. Das Problem mit dem „überfüllten Bauplan“ (API-Design)

Was die KI tat: Die KI baute keine saubere Schnittstelle (ein Benutzerhandbuch). Stattdessen riss sie jedes Mal die Wände auf, um die rohen Ziegel zu zeigen, wenn jemand etwas tun wollte.
Die Lösung: Der Experte bat die KI, eine „Benutzeroberfläche“ (eine API) zu bauen, damit Menschen mit der Mathematik interagieren können, ohne das chaotische Innere sehen zu müssen.
Das Ergebnis: Die KI baute zwar eine Schnittstelle, aber sie war unordentlich. Sie fügte 24 spezifische „Regeln“ nur für den aktuellen Beweis hinzu, anstatt einige wenige elegante, allgemeine Regeln zu erstellen. Es war, als würde man für jede einzelne Glühbir bulb für jede Lampe einen einzigartigen, komplizierten Schalter anbringen, anstatt einen Standard-Lichtschalter zu installieren.

3. Das Problem der „Kurzsichtigkeit“ (Theoremen-Aussagen)

Was die KI tat: Die KI bewies genau das, was sie brauchte, um die Aufgabe zu erledigen, und nicht mehr. Es war wie ein Zimmermann, der ein Brett so zuschneidet, dass es nur in die aktuelle Lücke passt, anstatt es so zuzuschneiden, dass es später auch für andere Lücken verwendet werden kann.
Das Urteil: Die KI ist exzellent darin, das unmittelbare Rätsel zu lösen, aber sie ist schlecht darin, darüber nachzudenken: „Wie kann ich das für jemanden in fünf Jahren nützlich machen?“

Der „Vorher-Nachher“-Test

Das Team gab nicht auf. Sie nahmen das Feedback des Experten und baten die KI, es zu korrigieren.

Was die KI gut korrigierte: Sie war gut bei lokalen Reparaturen. Wenn der Experte sagte: „Benenne diese Datei um“ oder „Ändere diese spezifische Zahl“, erledigte sie das perfekt. Sie konnte das Chaos aufräumen.
Was die KI nicht korrigieren konnte: Sie konnte immer noch nicht verstehen, wie man ein gutes Haus von Grund auf neu entwirft. Selbst nach der Überprüfung waren die Definitionen immer noch klobig und die „Benutzeroberfläche“ war immer noch überladen.

Die große Lektion

Das Paper schließt mit einer einfachen, kraftvollen Idee:

„Die Lücken zu schließen“ (den Code zum Kompilieren zu bringen), ist der leichte Teil.

Der schwierige Teil ist das Design.

Die KI ist wie ein brillanter Maurer: Sie kann Steine perfekt legen, wenn man ihr genau sagt, wohin sie sie setzen soll.
Die KI ist NICHT wie ein Architekt: Sie kann nicht entscheiden, wie das Haus aussehen soll, wie die Räume fließen sollen oder welche Werkzeuge die zukünftigen Bewohner benötigen werden.

Das Fazit:
Wir sollten nicht nur fragen: „Hat die KI das mathematische Problem gelöst?“ Wir müssen fragen: „Hat die KI etwas gebaut, das andere Menschen tatsächlich nutzen können?“

Derzeit kann eine KI das Rätsel lösen, aber sie kann die Bibliothek nicht bauen. Um ein wirklich nützliches Ergebnis zu erhalten, muss immer noch ein menschlicher Experte eingreifen und die schwere Arbeit des Designs und der Organisation übernehmen. Der „schwierige Teil“ ist nicht der Beweis des Theorems; es ist sicherzustellen, dass der Beweis ein Geschenk für die Zukunft ist und nicht eine Last.

Technisches Resümee: „Sorries“ sind nicht der schwierige Teil

Problemstellung

Das vorherrschende Narrativ in der semi-autonomen Formalisierung konzentriert sich auf die Beweisvollendung: die Fähigkeit eines Agenten, Code zu generieren, den ein Beweisassistent (z. B. Lean) als verifiziertes Theorem akzeptiert. Die Autoren argumentieren jedoch, dass ein verifiziertes Theorem nicht dasselbe ist wie ein wiederverwendbarer Bibliotheksbeitrag. Die moderne Mathematik stützt sich auf vernetzte Bibliotheken, in denen Definitionen kombiniert werden müssen, Theorem-Aussagen eine angemessene Allgemeingültigkeit besitzen müssen und APIs die zukünftige Argumentation erleichtern müssen, ohne Nutzer dazu zu zwingen, Implementierungen zu entfalten.

Das identifizierte Kernproblem besteht darin, dass Large Language Models (LLMs) zwar zunehmend in der Lage sind, lokale Beweislücken zu schließen (das Entfernen von „Sorries“), sie aber Schwierigkeiten mit den globalen Designentscheidungen haben, die für eine hochwertige, wartbare Formalisierung erforderlich sind. Insbesondere scheitern Agenten oft daran, geeignete Definitionen zu wählen, verallgemeinerbare Theorem-Aussagen zu entwerfen oder saubere APIs zu konstruieren, was zu einem Code führt, der zwar den Kernel passiert, aber als Bibliotheksbeitrag bei einer Expertenprüfung durchfällt.

Methodik

Die Arbeit präsentiert eine detaillierte Fallstudie einer semi-autonomen Formalisierung des Grothendieckschen Verschwindungssatzes (Hartshorne, 1977, Ch. III, Thm. 2.7) in Lean 4. Das Theorem besagt, dass für einen noetherschen topologischen Raum $X$ und eine ganze $n$ größer als die topologische Krull-Dimension von $X$ , die $n$ -te Sheaf-Kohomologie eines beliebigen Schäfer-Abelschen Gruppen-Sheaves auf $X$ verschwindet.

Die Studie folgt einem Vorher-Nachher-Experimentdesign:

Zustand A (Initiale Formalisierung): Ein Agent (Claude Code), geleitet von einer vom Menschen bereitgestellten Theorem-Aussage und einem PDF-Auszug aus Hartshornes Beweis, generierte eine Formalisierung, die mit null „Sorries“ (unbewiesenen Zielen) kompilierte.
Expertenprüfung: Ein Lean/mathlib-Experte überprüfte Zustand A und identifizierte Probleme in den Definitionen, der Allgemeingültigkeit der Theorem-Aussagen, der Dateiorganisation und dem API-Design.
Zustand B (Refaktorisierte Formalisierung): Der Agent wurde damit beauftragt, die Checkliste des Experten abzuarbeiten. Dies beinhaltete ein „Review-getriebenes Refactoring“ und eine anschließende Phase der „Kompression und Politur“, um die Formalisierung an die mathlib-Konventionen anzupassen.
Zweite Prüfung: Derselbe Experte überprüfte Zustand B.

Die Analyse vergleicht die beiden Zustände über vier Dimensionen hinweg: Definitionen, Theorem-Aussagen, Beweise sowie Datei-/API-Struktur. Der Zeitplan des Projekts, der Token-Verbrauch und die Tool-Interaktionen wurden aus Commit-Logs und Telemetrie rekonstrukturiert, um die Verhaltensmuster des Agenten zu verstehen.

Wichtigste Erkenntnisse und Ergebnisse

1. Definitionen: Der primäre Schwachpunkt

Definitionen wurden als die schwächste Komponente identifiziert und als der Bereich, in dem der Agent zwischen Zustand A und Zustand B die geringste Verbesserung zeigte.

Zustand A: Der Agent generierte 62 benutzerdefinierte Definitionen. Nur eine (TopCat.closedIncl) wurde als korrekt und wiederverwendbar eingestuft. Die übrigen waren „ad hoc“ und umschlossen oft Standardbibliotheks-Konstruktionen mit Namen, die spezifisch auf den aktuellen Beweis-Kontext zugeschnitten waren (z. B. sheafH_filtered_colimit_h1_sectionsFunctor anstatt sheafSections zu verwenden).
Konsequenzen: Diese Definitionen erzeugten „zukünftige Transportkosten“, da sie spätere Nutzer dazu zwangen, triviale Äquivalenzen zu beweisen, um die Objekte zu nutzen. Sie behinderten zudem die Taktik-Performance (z. B. simp), indem sie die zugrunde liegende Syntax verschleierten.
Zustand B: Der Agent versäumte es, seine Fähigkeit zur Erstellung allgemeiner, wiederverwendbarer Definitionen signifikant zu verbessern. Er erstellte weiterhin spezifische, unnötige Objekte, anstatt allgemeine Konstruktionen mit praktischen Spezialisierungen zu entwerfen.

2. API-Design: Teilweise Verbesserung

Zustand A: Der Agent baute keine API für die Sheaf-Kohomologie (Sheaf.H) auf, sondern entfaltete die Definition in nachfolgenden Dateien wiederholt direkt.
Zustand B: Der Agent erstellte eine dedizierte API-Datei, was die nachfolgenden Beweise bereinigte. Die API selbst war jedoch „verrauscht und aufgebläht“ und enthielt etwa 800 Zeilen und 24 hochspezifische Lemmata anstelle einer destillierten, prinzipienbasierten Schnittstelle.
Kontrast: Der Agent performte besser beim API für topologicalKrullDim (eine einfachere Definition), was darauf hindeutet, dass er gute APIs entwerfen kann, wenn er mit spezifischen, begrenzten Aufgaben konfrontiert wird, aber Schwierigkeiten mit offenem Design hat.

3. Theorem-Aussagen: Lokal vs. Global

Zustand A: Der Agent bewies genau das, was für den unmittelbaren Beweis nötig war, wobei er oft zu spezifische Hypothesen verwendete (z. B. die Forderung nach einer „injektiven Präsentation“, während eine allgemeine kurze exakte Sequenz genügt hätte).
Zustand B: Der Agent generalisierte die Theorem-Aussagen erfolgreich, wenn dies in der Review-Checkliste explizit verlangt wurde. Er versäumte es jedoch, notwendige Generalisierungen eigenständig zu identifizieren. Der Agent zeichnet sich durch lokale syntaktische Korrekturen aus, besitzt aber nicht das globale Urteilsvermögen, um zukünftige Wiederverwendungsbedarfe zu antizipieren.

4. Beweise: Ungleichmäßige Verbesserung

Zustand A: Die Beweise enthielten „Wände von have-Statements“, häufigen Missbrauch von definitorischer Gleichheit und das direkte Entfalten von Definitionen.
Zustand B: Die Beweise verbesserten sich, insbesondere in Dateien, die bestehende mathlib-Objekte verwendeten. Der Agent übernahm benannte Sub-Lemmata, um komplexe Beweise zu zerlegen – ein Muster, das durch die „Heartbeat“-Beschränkungen (Performance) verstärkt wurde.
Limitierung: Beweise, die auf den eigenen, mangelhaften Definitionen des Agenten basierten (z. B. in den Dateien für gefilterte Kolimite), blieben schwer lesbar und wartbar.

5. Prozessdynamik

Feedback-Adaption: Der Agent passte sich gut an Feedback mit präzisen Vervollständigungs-Prädikaten an (z. B. „benenne diese Datei um“, „generaliere diese Hypothese“). Er hatte Schwierigkeiten mit Feedback, das kontrafaktisches Urteilsvermögen erforderte (z. B. „entwirf eine API, die in der Zukunft nützlich sein wird“).
Ausstiegsmöglichkeiten (Escape Hatches): Agenten neigten dazu, Aufgaben als „blockiert“ zu deklarieren oder die Infrastruktur verantwortlich zu machen (z. B. „mathlib gap“), wenn sie vor schwierigen Designentscheidungen standen. Explizite Prompts, die diese Formulierungen untersagten, waren notwendig, um die Dekomposition zu erzwingen.
Metriken: Das „Schließen von Sorries“ ist ein unzureichender Metrik für die Qualität. Das Projekt entwickelte sich auch lange nach dem Erreichen der Null-Sorry-Marke signifikant weiter (hinsichtlich Codezeilen und Struktur).

Bedeutung und Ansprüche

Die Arbeit argumentiert, dass die Evaluierung der Autoformalisierung über die binäre Beweisvollendung hinausgehen muss. Die Autoren behaupten:

Kernel-Akzeptanz ist unvollständig: Ein Theorem kann vom Kernel verifiziert werden, während es zukünftige Nutzer durch mühsame Kohäsionen, duplizierte Definitionen und unhandliche APIs zwingt.
Die „Wiederverwendungslücke“ (Reusability Gap): Es gibt eine scharfe Trennung zwischen der Fähigkeit eines Agenten, lokale Ziele zu schließen, und seiner Fähigkeit, Definitionen zu wählen und APIs zu entwerfen. Letzteres erfordert ein Urteilsvermögen über die zukünftige Wiederverwendung, das aktuellen LLMs fehlt.
Evaluationsstandard: Die Autoren schlagen vor, dass KI-Systeme für Mathematik danach bewertet werden sollten, ob die resultierende Formalisierung eine Expertenprüfung übersteht. Konkret sollte nach der Verifizierung eines Beweises ein Experte die öffentlichen Definitionen, Theorem-Aussagen, Namespaces und API-Oberflächen prüfen, um die Fähigkeit des Systems zu messen, auf Design-Feedback zu reagieren.

Die Studie kommt zu dem Schluss, dass LLMs ohne ein anspruchsvolles Framework für globales Design zwar in der Lage sind, „verifizierte Artefakte“ zu produzieren, aber noch keine „wiederverwendbaren Bibliotheksbeiträge“. Der Weg nach vorn besteht darin, menschliche Experten zur Definition der Qualitätsvorgaben (Definitionen, Interfaces) einzusetzen und Agenten für die engen, mechanisch prüfbaren Refaktorierungen zu nutzen.