arXiv:2606.14000 — KI-Agent formalisiert Mathematik-Lehrbuch: Kompilierung garantiert keine Korrektheit

Großer Ehrgeiz: Das gesamte Lehrbuch in Lean 4

Formale Mathematiküberprüfung — das Beweisen von Sätzen in Systemen wie Lean 4, Coq oder Isabelle — erfordert traditionell Tausende von Stunden fachkundiger manueller Arbeit. Die Forscher Theodore Meek, Siyuan Ge, Di Qiu Xiang, Simon Chess und Vasily Ilin wendeten eine automatisierte agentische Pipeline auf ein ambitioniertes Ziel an: das gesamte Lehrbuch der numerischen Methoden für gewöhnliche Differentialgleichungen in Lean 4 mit der Mathlib-Bibliothek zu formalisieren.

Numerische Analysis ist ein besonders anspruchsvolles Ziel, da dieser Mathematikzweig in bestehenden formalen Bibliotheken relativ schwach vertreten ist — was bedeutet, dass der Agent nicht einfach bereits bewiesene Lemmata aufrufen kann, sondern formalisierte Grundlagen von Grund auf aufbauen muss.

Ist Kompilierung ein ausreichender Korrektheitsbeweis?

Die Standardmetrik zur Evaluierung von Agenten, die formalen mathematischen Code schreiben, ist die Kernel-Akzeptanz — ob der Code den Lean-Verifikator ohne Fehler durchläuft. Auf den ersten Blick erscheint dies als starkes Signal: Wenn der Kernel eine Aussage akzeptiert, ist sie formal korrekt bewiesen.

Die Studie widerlegt diese Annahme. Die Autoren entdeckten, dass Kernel-Akzeptanz im Wesentlichen semantische Fehler verdeckt — Agenten produzieren regelmäßig Aussagen, die kompilieren, aber mathematisch inkorrekt sind. Darüber hinaus überschätzen kompilierungsbasierte Metriken die tatsächliche Qualität der Formalisierung erheblich, was die Zuverlässigkeit von Evaluierungsprotokollen in Frage stellt, die ausschließlich auf diesem Signal basieren.

Drei systematische Fehlermuster

Die agentische Pipeline zeigte drei wiederkehrende Fehlermuster, die die Kompilierung nicht erfasst.

Hinzugefügte Hypothesen, die Sätze abschwächen. Der Agent formuliert einen Satz mit zusätzlichen Voraussetzungen, die der ursprüngliche Satz nicht hat. Die Aussage ist technisch korrekt innerhalb dieser Voraussetzungen — beweist aber eine schwächere Behauptung. Ein allgemeiner Konvergenz-Satz über eine numerische Methode kann beispielsweise auf einen Spezialfall mit positiven Koeffizienten eingeschränkt werden, den Lean akzeptiert, ein Forscher aber nicht.

Unvollständige Abdeckung mehrteiliger Aussagen. Wenn ein Satz mehrere Schlussfolgerungen oder Fälle hat, kann der Agent nur einen Teil formalisieren. Lean akzeptiert dies als gültige, aber partielle Formalisierung. Die Abdeckung des ursprünglichen Satzes bleibt unvollständig, ohne dass der Verifikator eine Diagnosemeldung ausgibt.

Phantom-Imports. Der Agent referenziert Mathlib-Definitionen oder Lemmata, die nicht existieren oder unterschiedliche exportierte Namen haben. In bestimmten Kontexten toleriert Lean solche Imports oder löst sie partiell auf, lässt den Fehler durch den Kernel durch und hinterlässt einen falschen Eindruck von Gültigkeit.

Dreidimensionales Qualitätsrahmenwerk

Als Antwort schlagen die Autoren ein dreidimensionales Evaluierungsrahmenwerk vor, das über den binären Akzeptanz-oder-Ablehnung-Ansatz hinausgeht.

Die erste Dimension ist semantische Korrektheit — entspricht die formalisierte Aussage der Semantik des ursprünglichen Lehrbuch-Satzes, unabhängig davon, ob sie die Kernel-Überprüfung besteht. Die zweite ist Mathlib-Wiederverwendung — nutzt der Agent bestehende Definitionen, Lemmata und Strukturen aus der Mathlib-Bibliothek, oder erfindet er bereits bewiesene Behauptungen neu. Die dritte ist dateiübergreifende Wiederverwendung — sind die Definitionen über verschiedene Projektdateien hinweg konsistent, oder gibt es inkonsistente Paare, die logische Lücken verbergen.

Alle drei Dimensionen werden mit dem LLM-as-Judge-Ansatz bewertet — einer automatisierten Evaluierung, die reproduzierbar und skalierbar ist. Das Rahmenwerk ist darauf ausgelegt, auf zukünftige agentische Formalisierungssysteme anwendbar zu sein, nicht nur auf diese spezifische Pipeline.

Breitere Implikationen für KI-Coding-Benchmarks

Die Arbeit hat Konsequenzen, die weit über die formale Mathematik hinausgehen. Kompilierung als primäres Erfolgssignal wird auch bei der Evaluierung von KI-Coding-Agenten für Standard-Software eingesetzt — Benchmarks wie HumanEval oder SWE-bench verlassen sich auf das Bestehen von Tests als Proxy für Korrektheit.

Wenn dasselbe Problem dort ebenfalls vorhanden ist — Agenten, die Tests bestehen, aber semantisch abgeschwächte oder teilweise korrekte Implementierungen produzieren — dann sind Standard-KI-Coding-Benchmarks unzureichende Qualitätssignale. Diese Forschung liefert ein formales Argument für diese Sorge, unterstützt durch konkrete Fehlermuster, die an einem realen Formalisierungsprojekt katalogisiert wurden.

Für Teams, die KI-Agenten zum Schreiben oder Verifizieren kritischen Codes einsetzen, ist die Kernbotschaft klar: Kompilierungsüberprüfung und das Bestehen von Tests sind notwendige, aber nicht hinreichende Korrektheitsindikatoren. Semantische Evaluierung — so kostspielig und schwer zu automatisieren sie auch sein mag — bleibt ein unverzichtbarer Schritt.