💻 computer science

Pseudo-Formalization for Automatic Proof Verification

Dieser Beitrag stellt Pseudo-Formalisierung vor, ein hybrides Beweisformat, das die Flexibilität natürlicher Sprache mit formaler Modularität verbindet, sowie einen entsprechenden Block-Verifikationsalgorithmus, der bestehende LLM-as-judge-Baselines bei der präzisen Verifikation mathematischer Beweise über Olympiade- und Forschungsbenchmarks hinweg signifikant übertrifft.

Ursprüngliche Autoren: Slim Barkallah, Luke Bailey, Kaiyue Wen, Mohammed Abouzaid, Tengyu Ma

Veröffentlicht 2026-05-21

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Slim Barkallah, Luke Bailey, Kaiyue Wen, Mohammed Abouzaid, Tengyu Ma

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 sind leitender Redakteur einer angesehenen Mathematikzeitschrift. Sie erhalten einen 50-seitigen Beweis, verfasst von einem brillanten, aber leicht chaotischen Mathematiker (oder einer KI). Der Beweis ist in natürlicher Sprache verfasst, voller „daraus folgt", „offensichtlich" und „wie wir wissen". Ihre Aufgabe ist es, den einen winzigen logischen Fehler zu finden, der das Ganze zunichtemacht.

Das ist wie der Versuch, einen einzigen Tippfehler in einem Roman zu finden, während man ihn mit 160 Stundenkilometern liest. Wenn Sie den Fehler übersehen, veröffentlichen Sie Unsinn. Wenn Sie zu langsam lesen, werden Sie nie fertig.

Diese Arbeit, „Pseudo-Formalisierung zur automatischen Beweisverifikation", schlägt einen neuen Weg vor, um dieses Problem zu lösen. Sie schlägt einen Mittelweg vor zwischen der unordentlichen, flexiblen Art, wie Menschen Mathematik schreiben, und der starren, roboterhaften Art, wie Computer Mathematik überprüfen.

Hier ist die Aufschlüsselung ihrer Lösung mit einfachen Analogien:

1. Das Problem: Die „Textwand"

Derzeit, wenn wir eine KI bitten, einen mathematischen Beweis zu überprüfen, füttern wir sie meist einfach mit dem gesamten Text und sagen: „Ist das richtig?"

Das Problem: Das ist wie die Bitte an einen Menschen, einen 100-seitigen Rechtsvertrag zu lesen und in einem Atemzug einen einzigen Widerspruch zu finden. Die KI gerät in Verwirrung, vergisst den Anfang, bis sie am Ende angelangt ist, und übersieht die Fehler. Dies nennt man „Kontextverfall" – je mehr Text Sie ihr zuführen, desto dümmer wird sie beim Finden von Fehlern.

2. Die Lösung: „Pseudo-Formalisierung" (Die LEGO-Analogie)

Die Autoren führen ein neues Format namens Pseudo-Formal (PF) ein.

Die Analogie: Stellen Sie sich den unordentlichen Beweis als einen riesigen, verwickelten Wollknäuel vor. Pseudo-Formalisierung ist der Prozess, dieses Garn zu schneiden und zu ordentlichen, einzelnen LEGO-Steinen neu zu stricken.
Funktionsweise: Statt eines langen Absatzes wird der Beweis in kleine, eigenständige „Blöcke" zerlegt (wie Lemmata, Propositionen und Theoreme).
Die Regeln: Jeder Block muss klar angeben:
1. Prämissen: Von welchen Annahmen gehen wir aus?
2. Konklusion: Was wollen wir in diesem spezifischen Block beweisen?
3. Beweis: Die Schritte, um von 1 zu 2 zu gelangen.
Der Vorteil: Jetzt muss die KI nicht das gesamte Wollknäuel überprüfen, sondern nur einen LEGO-Stein nach dem anderen. Es ist eine winzige, handhabbare Aufgabe.

3. Der Prozess: Das „Fließband"

Die Arbeit beschreibt eine vierstufige Montagelinie zur Verifikation eines Beweises:

Übersetzung (Der Architekt): Eine KI nimmt den unordentlichen, in natürlicher Sprache verfassten Beweis und schreibt ihn in diese ordentlichen LEGO-Blöcke um (Pseudo-Formal-Format). Es ist wie ein Übersetzer, der eine abschweifende Rede in eine strukturierte Gliederung verwandelt.
Blockverifikation (Die Qualitätsprüfer): Jetzt agiert die KI wie ein Team von Qualitätsprüfern. Jeder Prüfer betrachtet einen LEGO-Stein. Sie prüfen: „Beweist der Inhalt dieses Steins tatsächlich die Konklusion unter den gegebenen Prämissen?" Sie machen sich keine Sorgen um den Rest des Gebäudes; sie prüfen nur ihren spezifischen Stein.
Kalibrierung (Der Manager): Manchmal wird ein Prüfer zu pingelig (markiert einen Tippfehler) oder übersieht etwas. Eine „Manager"-KI betrachtet alle Berichte der Prüfer und entscheidet: „Okay, hier haben wir einen echten Fehler, oder war das nur ein Fehlalarm?" Sie fasst die Ergebnisse zu einem endgültigen Urteil zusammen.
Paralleles Skalieren (Die Menge): Um ganz sicherzugehen, führen sie diesen gesamten Prozess 8 Mal durch (wie 8 verschiedene Teams von Prüfern). Wenn irgendein Team einen Fehler findet, wird der Beweis abgelehnt. Dies stellt sicher, dass sie fast alles entdecken.

4. Die Ergebnisse: Besser als die Basislinie

Die Autoren testeten diese Methode an zwei Arten von Mathematik:

Olympiaden-Mathematik: Schwierige Wettbewerbsaufgaben (wie die Internationale Mathematik-Olympiade).
Forschungsmathematik: Echte, veröffentlichte akademische Arbeiten von arXiv, bei denen die Autoren selbst zugegeben hatten, dass sie Fehler enthielten.

Die Erkenntnisse:

Die „Pseudo-Formal"-Methode war besser im Finden von Fehlern als die Standardmethode, bei der man eine KI einfach den gesamten Beweis lesen lässt.
Sie fand mehr Fehler (höhere Recall-Rate), ohne falsche Fehler zu erfinden (höhere Precision-Rate).
In der Welt der mathematischen Verifikation ist dies eine „Pareto-Verbesserung" – das bedeutet, sie erzielten bessere Ergebnisse, ohne eine Qualität für eine andere opfern zu müssen.

5. Der neue Benchmark: „ArxivMathGradingBench"

Um zu beweisen, dass ihre Methode auf realer Forschung funktioniert, erstellten die Autoren einen neuen Testdatensatz.

Sie nahmen 35 echte mathematische Arbeiten, die von ihren Autoren aktualisiert wurden, um Fehler zu beheben.
Sie nutzten diese „bekannten Fehler", um zu testen, ob ihre KI die spezifischen Fehler finden konnte, die die Autoren behoben hatten.
Das ist wie ein „Führerschein-Test", bei dem die Prüfer genau wissen, wo die Schlaglöcher sind, und sehen, ob das neue Auto (die KI) sie trifft.

Zusammenfassung

Die Arbeit argumentiert, dass wir die KI nicht zwingen müssen, „Robotersprache" (wie Lean oder Isabelle) zu sprechen, um Mathematik zu überprüfen. Stattdessen können wir die KI lehren, menschliche Mathematik in ordentliche, kleine Häppchen zu organisieren. Indem wir einen riesigen, verwirrenden Beweis in kleine, klare LEGO-Blöcke zerlegen, kann die KI jedes Stück mit Laserfokus überprüfen und Fehler finden, die sie übersehen hätte, wenn sie versucht hätte, das Ganze auf einmal zu lesen.

Was sie NICHT behauptet haben:

Sie behaupteten nicht, dass dies menschliche Mathematiker ersetzt.
Sie behaupteten nicht, dass dies für nicht-mathematische Bereiche funktioniert (obwohl sie spekulieren, dass es könnte).
Sie behaupteten nicht, dass die KI perfekt ist; sie zeigten lediglich, dass sie besser im Finden von Fehlern ist als frühere Methoden.

Technische Zusammenfassung: Pseudo-Formalisierung zur automatischen Beweisverifikation

Problemstellung

Die zuverlässige automatische Verifikation mathematischer Beweise bleibt ein kritischer Engpass für das Training und die Evaluierung von KI-Systemen in komplexen mathematischen Schlussfolgerungen. Während vollständig formalisierte Beweise (z. B. in Lean oder Isabelle) aufgrund ihrer semantischen Präzision und Modularität leicht zu verifizieren sind, fehlen den meisten Beweisen – insbesondere den von KI generierten oder von Menschen in natürlicher Sprache verfassten – diese Eigenschaften. Die Übersetzung natürlicher Sprachbeweise in vollständig formale Sprachen ist für die Spitzengrenzenmathematik oft unpraktikabel aufgrund unvollständiger formaler Bibliotheken und des enormen Expertenaufwands, der hierfür erforderlich ist. Folglich kämpfen aktuelle Verifikationsmethoden, wie „LLM-as-judge" (direkte Bewertung natürlicher Sprachbeweise), mit Präzision und Recall und scheitern häufig daran, spezifische Fehler in langen, komplexen Argumentationen zu identifizieren.

Methodik: Pseudo-Formalisierung und Blockverifikation

Die Autoren schlagen Pseudo-Formalisierung (PF) in Kombination mit Blockverifikation (BV) als Rahmenwerk vor, um die Lücke zwischen der Flexibilität natürlicher Sprache und der Verifizierbarkeit formaler Beweise zu schließen.

1. Pseudo-formaler Beweisformat

Ein Pseudo-formaler Beweis zerlegt ein Argument in natürlicher Sprache in eine Sequenz selbstständiger Module (Lemmata, Propositionen, Behauptungen). Jedes Modul ist ein Tupel $(P, c, \pi)$ , das Folgendes repräsentiert:

Prämissen ( $P$ ): Explizit dargelegte Annahmen und geerbter Kontext.
Konklusion ( $c$ ): Die spezifische Behauptung, die bewiesen wird.
Beweis ( $\pi$ ): Das Argument in natürlicher Sprache, das $c$ aus $P$ herleitet.

Die Struktur wird durch zwei Graphen gesteuert:

Abhängigkeitsgraph ( $G$ ): Ein gerichteter azyklischer Graph (DAG), bei dem eine Kante existiert, wenn ein Modul die Konklusion eines anderen aufruft. Dies verhindert zirkuläres Schließen.
Scope-Vererbungs-Wald ( $T$ ): Eine Waldstruktur, die Module hierarchisch organisiert (z. B. Lemmata innerhalb einer Proposition) und es ermöglicht, Kontext (Definitionen, Annahmen) zu erben, ohne sie erneut darlegen zu müssen.

Die Autoren definieren „Gute Pseudo-formale Beweise" als solche, die zwei desiderata einhalten: Kürze (kurze Beweise, die wenige andere Knoten aufrufen) und begrenzte Scope-Tiefe (flache Vererbungsbäume). Theoretisch ermöglicht die Verifikation solcher Beweise, dass die für jeden Verifikationsschritt erforderliche Kontextlänge unabhängig von der Gesamtgröße des Beweises bleibt, was den „Context Rot" (die Verschlechterung der LLM-Leistung mit zunehmender Eingabelänge) abschwächt.

2. Der Verifikations-Pipeline (PF+BV)

Der Verifikationsprozess umfasst vier Schritte, die alle handelsübliche LLMs ohne Feinabstimmung nutzen:

Übersetzung: Ein LLM übersetzt den ursprünglichen Beweis in natürlicher Sprache $\Pi$ in einen Pseudo-formalen Beweis $\hat{\Pi}$ . Eine optionale Selbstreparatur-Schleife prüft $\hat{\Pi}$ gegen $\Pi$ , um die Treue sicherzustellen.
Blockverifikation: Ein Verifizierer-LLM prüft jedes Modul von $\hat{\Pi}$ unabhängig. Es erhält die vollständigen Prämissen des Moduls (einschließlich geerbten Kontexts), die Konklusion, den Beweis und die verifizierten Konklusionen aller aufgerufenen Kindmodule. Es gibt ein „akzeptieren"-Urteil oder eine spezifische Fehlerbeschreibung aus.
Kalibrierung: Ein Kalibrierer-LLM fasst pro-Modul-Fehlerberichte zu einem endgültigen Urteil zusammen. Es kann konfigurierbare Strenge-Schwellenwerte anwenden und Block-Level-Fehler zurück auf die Struktur des ursprünglichen Beweises abbilden (z. B. Identifizierung spezifischer Schritte oder Lemmata).
Paralleles Skalieren: Die gesamte Pipeline wird $k$ -mal unabhängig ausgeführt. Ein Beweis wird nur akzeptiert, wenn alle $k$ Durchläufe ihn akzeptieren (pessimistische Aggregation). Dies ermöglicht einen Kompromiss zwischen Präzision und Recall durch Variation von $k$ .

Hauptbeiträge

Pseudo-Formalisierung (PF): Ein neues Beweisformat, das die Flexibilität natürlicher Sprache beibehält und gleichzeitig die Modularität sowie die explizite Prämissen-Konklusions-Struktur erzwingt, die für eine zuverlässige Verifikation notwendig sind.
Blockverifikation (BV): Ein Algorithmus, der Beweise verifiziert, indem er sie in unabhängige Blöcke zerlegt, was theoretisch den Kontextbedarf reduziert und empirisch die Fehlererkennung verbessert.
ArxivMathGradingBench: Ein neuer Benchmark, der 35 mathematische Forschungsarbeiten aus arXiv umfasst, die bekannte, von den Autoren korrigierte Fehler enthalten. Dieser Datensatz schließt eine Lücke in bestehenden Benchmarks, indem er die Verifikation an realen Forschungsarbeiten statt an Wettbewerbsaufgaben testet.
Theoretische Begründung: Die Autoren liefern einen Satz (Satz 1), der zeigt, dass für „gute" Pseudo-formale Beweise die blockweise Verifikation durch einen Transformer fester Größe simuliert werden kann, dessen Kontextlänge unabhängig von der Beweisgröße ist, im Gegensatz zum linearen Kontextwachstum, das für die Verifikation des gesamten Beweises erforderlich ist.

Experimentelle Ergebnisse

Die Methode wurde an zwei Benchmarks evaluiert: Hard2Verify (Olympiade/Putnam-Niveau) und ArxivMathGradingBench (Forschungsniveau).

Leistung im Vergleich zu Baselines: Über beide Benchmarks hinweg dominiert PF+BV die „LLM-as-judge"-Baseline im Pareto-Sinne. Das bedeutet, dass für jedes gegebene Recall-Niveau (Fähigkeit, Fehler zu finden) PF+BV eine höhere Präzision (weniger Fehlalarme) erreicht und umgekehrt.
Hard2Verify: PF+BV erreichte beim Recall (~90 %) das Niveau der Baseline, reduzierte jedoch die Anzahl der pro Beweis falsch gemeldeten Fehler signifikant (über 40 % weniger False Positives bei $k=8$ ).
ArxivMathGradingBench: Der Benchmark erwies sich als herausfordernd, wobei beide Methoden bei $k=8$ etwa 50 % der annotierten Fehler unentdeckt ließen. Dennoch übertraf PF+BV die Baseline konsistent in Bezug auf Recall, Fehlalarmraten und den Anteil der Arbeiten, bei denen alle annotierten Fehler gefunden wurden.
Qualitative Analyse: Fallstudien (z. B. IMO 2024 P6) verdeutlichen, dass PF+BV erfolgreich ist, indem es logische Sprünge in lokale Blöcke isoliert. Dies ermöglicht dem Verifizierer, zu erkennen, wenn ein Beweis eine Prämisse fälschlicherweise stärkt (z. B. „gleiches Vorzeichen" aus „kein $d$ und $-d$ " zu schließen), ohne das gesamte globale Argument neu bewerten zu müssen.

Bedeutung und Behauptungen

Die Arbeit behauptet, dass Pseudo-Formalisierung eine praktische Alternative zur Autoformalisierung (Übersetzung in Lean/Isabelle) für die Verifikation moderner mathematischer Forschung bietet. Während Autoformalisierung stärkere Korrektheitsgarantien bietet, ist sie für aktuelle Forschung aufgrund von Bibliotheksunvollständigkeit oft unlösbar. PF+BV verzichtet auf die absolute Gewissheit der formalen Verifikation zugunsten der Anwendbarkeit auf ein breiteres Spektrum mathematischer Domänen, indem es den reichen Wortschatz und die Standardtechniken natürlicher Sprache nutzt und gleichzeitig eine Struktur auferlegt, die Fehler leichter lokalisierbar macht.

Die Autoren positionieren diese Arbeit als einen Schritt hin zu skalierbarer Überwachung des KI-Schließens und bieten einen Mechanismus, um vertrauenswürdige Belohnungssignale für das Training von LLMs in schwieriger Mathematik zu generieren und menschliche Mathematiker bei der Überprüfung von Beweisen zu unterstützen. Sie erkennen Einschränkungen an und stellen fest, dass das Erstellen einer treuen Pseudo-formalen Umschreibung nicht trivial ist und dass zukünftige Arbeiten das Training von Modellen beinhalten könnten, die Beweise direkt in diesem Format generieren.