💬 NLP

Monotonic Reference-Free Refinement for Autoformalization

Dieser Beitrag stellt ein referenzfreies, iteratives monotonisches Verfeinerungsframework für die Autoformalisierung ganzer Sätze vor, das komplementäres Feedback von Theorembeweisern und LLM-Bewertern nutzt, um gleichzeitig formale Validität, logische Erhaltung, mathematische Konsistenz und formale Qualität zu optimieren, und erzielt damit State-of-the-Art-Leistung auf den miniF2F- und ProofNet-Benchmarks ohne Ground-Truth-Daten oder menschliches Eingreifen.

Ursprüngliche Autoren: Lan Zhang, Marco Valentino, André Freitas

Veröffentlicht 2026-05-08

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Lan Zhang, Marco Valentino, André Freitas

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 versuchen, eine komplexe Geschichte, die in einer lockeren, alltäglichen Sprache verfasst ist (wie ein Blogbeitrag über Mathematik), in eine strenge, für Computer lesbare Sprache zu übersetzen (wie einen Programmcode für einen Roboter-Mathematiker). Dieser Prozess wird als Autoformalisierung bezeichnet.

Das Problem besteht darin, dass Computer zwar hervorragend darin sind zu prüfen, ob Code „syntaktisch korrekt" ist (enthält er die richtige Zeichensetzung?), sie jedoch Schwierigkeiten haben zu verstehen, ob die Geschichte immer noch Sinn ergibt oder ob die Logik standhält. Bestehende Methoden beheben oft die Grammatik, verlieren dabei aber die Bedeutung, oder sie treffen die Bedeutung richtig, doch der Code stürzt ab.

Dieser Artikel stellt eine neue Methode namens Monotone Referenzfreie Verfeinerung vor. So funktioniert sie, unter Verwendung einfacher Analogien:

1. Das Ziel: Eine perfekte Übersetzung

Die Autoren möchten eine Übersetzung schaffen, die in vier Hinsichten perfekt ist:

Formale Gültigkeit (Der „Syntax-Check"): Der Code muss fehlerfrei ausgeführt werden können. Wenn nicht, lehnt ihn der Roboter sofort ab.
Logische Bewahrung (Der „Handlungs-Check"): Die Übersetzung muss die Logik der ursprünglichen Geschichte bewahren. Man kann das Ende nicht einfach ändern, nur weil es einfacher zu schreiben ist.
Mathematische Konsistenz (Der „Fakten-Check"): Alle Zahlen, Variablen und Regeln müssen exakt mit der ursprünglichen Geschichte übereinstimmen.
Formale Qualität (Der „Stil-Check"): Der Code sollte sauber, prägnant und für Menschen später leicht lesbar sein.

2. Das Problem: Ein Werkzeug kann nicht alles leisten

Normalerweise verwenden Forscher ein einziges KI-Modell, um die gesamte Aufgabe zu erledigen. Aber es ist, als würde man eine einzelne Person bitten, gleichzeitig Grammatiker, Logiker, Faktenprüfer und Redakteur zu sein. Sie mag hervorragend in Grammatik sein, aber schrecklich in Logik. Außerdem erfordert die Korrektur eines ersten Fehlers normalerweise eine „Goldstandard"-Antwort (den korrekten Code) zum Vergleich. Die Autoren wollten eine Methode, die ohne den Lösungsschlüssel funktioniert.

3. Die Lösung: Eine spezialisierte Fließbandproduktion

Die Autoren entwickelten ein System, das wie eine spezialisierte Fabrik mit verschiedenen Arbeitern funktioniert, von denen jeder das tut, worin er am besten ist. Sie benötigen keinen Lösungsschlüssel; sie müssen lediglich den Entwurf verbessern, bis er perfekt ist.

Hier sind die drei Arten von „Arbeitern" (KI-Modellen) in ihrer Fabrik:

Die „Erstentwurf"-Schreiber (Einmal-Generatoren): Dies sind spezialisierte Mathematik-KIs, die die rohe Geschichte nehmen und die allererste Version des Codes schreiben. Sie sind gut darin, die Struktur richtig zu bekommen.
Die „Syntax-Reparateure" (FV-Repairer): Wenn der Erstentwurf Codefehler enthält (der Roboter lehnt ihn ab), greifen diese Arbeiter ein. Sie sind Experten darin, defekten Code zu reparieren, damit er ausgeführt werden kann, und sorgen dafür, dass die Punktzahl für „Formale Gültigkeit" steigt.
Die „Verfeinerer" (Recurrent Generators): Sobald der Code ausgeführt werden kann, betrachten diese Arbeiter den Entwurf und versuchen, ihn zu verbessern. Sie beheben nicht nur Fehler; sie verbessern die Logik, die Fakten und den Stil. Sie erhalten Feedback von „Richtern" (anderen KIs), die sagen: „Dieser Teil ist logisch schwach" oder „Das ist zu wortreich".

4. Die „Monotone" Regel: Nie einen Schritt zurück

Der wichtigste Teil dieses Systems ist die Akzeptanzrichtlinie. Stellen Sie sich vor, Sie besteigen einen Berg.

In vielen KI-Systemen machen Sie vielleicht einen Schritt nach oben, dann einen nach unten, dann wieder nach oben, in der Hoffnung, den Gipfel zu finden.
In diesem System lautet die Regel Monoton: Sie akzeptieren eine neue Version des Codes nur, wenn sie streng besser (oder zumindest nicht schlechter) ist als die vorherige.

Wenn ein neuer Entwurf in der Logik etwas besser, aber im Stil etwas schlechter ist, prüft das System einen „Sicherheitspuffer" (eine mathematische Garantie namens Untere Konfidenzgrenze). Es akzeptiert die Änderung nur, wenn es zuversichtlich ist, dass sich die Gesamtqualität verbessert hat. Dies stellt sicher, dass der Prozess niemals in einer Schleife feststeckt, in der es immer schlechter wird.

5. Das Ergebnis: Eine sich selbst verbessernde Schleife

Das System läuft in einer Schleife ab:

Einen Entwurf generieren.
Prüfen, ob er ausgeführt wird (Gültigkeit). Wenn nicht, senden Sie ihn an den Syntax-Reparateur.
Wenn er ausgeführt wird, senden Sie ihn an die Verfeinerer, um Logik und Stil zu verbessern.
Vergleichen Sie die neue Version mit der alten unter Verwendung des „Sicherheitspuffers".
Wenn die neue als besser zertifiziert ist, behalten Sie sie. Wenn nicht, behalten Sie die alte und versuchen Sie einen anderen Ansatz.

Das Ergebnis:
Die Autoren testeten dies an zwei schwierigen Mathematik-Benchmarks (miniF2F und ProofNet).

Beim einfacheren Benchmark erreichten sie 100 % Gültigkeit (der Code wird immer ausgeführt) und eine sehr hohe Gesamtqualitätsbewertung.
Beim schwierigeren Benchmark erreichten sie immer noch eine hohe Gültigkeit und deutlich bessere Gesamtwerte als frühere Methoden.

Zusammenfassend:
Dieser Artikel stellt einen „team-basierten" Ansatz zur Übersetzung von Mathematik in Code vor. Anstatt sich auf eine Super-KI zu verlassen, nutzt er ein Team spezialisierter KIs, die in einer Schleife arbeiten, mit einer strengen Regel, dass jeder Schritt eine Verbesserung sein muss. Dies ermöglicht es ihnen, hochwertige, fehlerfreie mathematische Beweise zu erstellen, ohne die korrekten Antworten im Voraus sehen zu müssen.

Technische Zusammenfassung: Monotone referenzfreie Verfeinerung für die Autoformalisierung

1. Problemstellung

Während Large Language Models (LLMs) das mathematische Schlussfolgern vorangebracht haben, bleibt die Autoformalisierung ganzer Theoreme – die Umwandlung von Theoremen in natürlicher Sprache und deren begleitenden Beweise in vollständige, mechanisch verifizierbare formale Aussagen und Beweise – weitgehend unerforscht. Bestehende Ansätze konzentrieren sich häufig ausschließlich auf die Formalisierung der Aussage und verlassen sich dabei auf „sorry"-Platzhalter für Beweise oder behandeln die Generierung von Aussagen und den Theorembeweis als isolierte Aufgaben.

Die Kernherausforderung liegt in der multidimensionalen Natur einer hochwertigen Autoformalisierung. Eine erfolgreiche Formalisierung muss gleichzeitig folgende Kriterien erfüllen:

Formale Gültigkeit (FV): Syntaktische Korrektheit und mechanische Verifizierung durch einen Theorembeweiser (z. B. Lean4).
Logische Erhaltung (LP): Semantische Übereinstimmung mit der logischen Struktur der ursprünglichen Aussage in natürlicher Sprache.
Mathematische Konsistenz (MC): Korrekte Darstellung mathematischer Objekte und Operationen.
Formale Qualität (FQ): Strukturelle Klarheit, Prägnanz und Wiederverwendbarkeit.

Aktuelle iterative Verfeinerungsmethoden haben Schwierigkeiten, diese Dimensionen gemeinsam zu optimieren, und verbessern häufig einen Aspekt (z. B. Syntax) auf Kosten anderer (z. B. semantische Ausrichtung). Darüber hinaus verlassen sich bestehende Methoden oft auf formale Referenzlösungen (Ground Truth) oder menschliche Eingriffe zur Auswahl, was ihre Anwendbarkeit in referenzfreien Szenarien einschränkt.

2. Methodik

Die Autoren schlagen einen referenzfreien, iterativen, monotonen Optimierungsprozess vor, der zur Testzeit ohne Zugriff auf formale Referenzlösungen oder menschliche Auswahl arbeitet. Das Framework integriert Rückmeldungen von Theorembeweisern und LLM-basierten Bewertern, um ein Ensemble spezialisierter LLMs zu steuern.

2.1 Zielfunktion

Die Autoren definieren eine maskierte zusammengesetzte Zielfunktion $J_{OA}(x)$ , um die vier Dimensionen auszugleichen. Die formale Gültigkeit ( $\pi_{FV}$ ) wirkt als harte Einschränkung (Maske), während die logische Erhaltung ( $\pi_{LP}$ ), die mathematische Konsistenz ( $\pi_{MC}$ ) und die formale Qualität ( $\pi_{FQ}$ ) als weiche Dimensionen behandelt werden:
$J_{OA}(x) = \frac{1}{3}\pi_{FV}(x) \left( \pi_{LP}(x) + \pi_{MC}(x) + \pi_{FQ}(x) \right)$
Diese Formulierung stellt sicher, dass ungültige Formalisierungen (bei denen $\pi_{FV}=0$ ), unabhängig von ihren weichen Scores, nicht ausgewählt werden.

2.2 LLM-Bewerter und Unsicherheit

Da weiche Dimensionen nicht exakt berechenbar sind, setzt das Framework LLM-Bewerter ein, um Scores zu schätzen. Um das inhärente Rauschen und die Verzerrung von LLMs zu handhaben, gehen die Autoren von folgenden Annahmen aus:

Asymptotische Stabilität: Bewertungen stabilisieren sich nach der Kalibrierung.
Messbare Unsicherheit: Eine einseitige Untere Konfidenzgrenze (LCB) kann für die wahren Scores etabliert werden.
Das Ziel wird unter Verwendung eines auf LCB basierenden Schätzers optimiert, wodurch Auswahlentscheidungen konservativ und robust gegenüber Bewertungsrauschen bleiben.

2.3 Generatorrollen und Reaktionsfähigkeit

Das Framework zerlegt LLM-Rollen in drei Kategorien, geleitet durch eine Reaktionsfähigkeitskarte, die erwartete Verbesserungen pro Dimension modelliert:

Einmal-Generatoren (OOGs): Erzeugen initiale Formalisierungen von Grund auf (z. B. spezialisierte Mathematik-Modelle wie DeepSeek-Prover).
FV-Reparierer (FVRs): Zielen spezifisch auf formal ungültige Kandidaten ab und korrigieren diese (z. B. Modelle, die zur iterativen Beweisrevision fähig sind).
Rekurrente Generatoren (REGs): Verfeinern den aktuellen besten Kandidaten basierend auf Rückmeldungen von LLM-Bewertern bezüglich spezifischer weicher Dimensionen (LP, MC oder FQ).

2.4 Monotone Akzeptanzrichtlinie

Der Prozess iteriert durch die Generierung und Auswahl von Kandidaten. Eine konservative Akzeptanzrichtlinie wird angewendet: Ein neuer Kandidat wird nur akzeptiert, wenn sein geschätzter Zielscore (basierend auf der LCB) strikt höher ist als der des aktuellen Besten. Dies garantiert eine zertifizierte monotone Verbesserung, was bedeutet, dass die Qualität der ausgewählten Formalisierung über die Iterationen hinweg niemals abnimmt. Es wird bewiesen, dass der Prozess unter bestimmten Bedingungen konvergiert und terminiert.

3. Hauptbeiträge

Formale Definition und Framework: Das Papier definiert erstmals die Autoformalisierung ganzer Theoreme als einheitliche Aufgabe formal und schlägt einen referenzfreien, iterativen monotonen Prozess zu deren Lösung vor.
Maskierte zusammengesetzte Zielfunktion: Einführung einer Zielfunktion, die die formale Gültigkeit als harte Einschränkung durchsetzt und gleichzeitig mehrere weiche Dimensionen (LP, MC, FQ) optimiert.
Rollen-spezialisiertes Ensemble: Zerlegung der Autoformalisierungsaufgabe in OOG-, FVR- und REG-Rollen unter Verwendung einer Reaktionsfähigkeitskarte zur Auswahl von Generatoren, die für bestimmte Qualitätsdimensionen am effektivsten sind.
Theoretische Garantien: Bereitstellung theoretischer Beweise für zertifizierte Monotonie, Konvergenz und Prozess-Terminierbarkeit, die auch unter realistischem Bewerterrauschen einen nicht-abnehmenden Fortschritt sicherstellen.
Empirische Validierung: Nachweis, dass das Framework die Stärken spezialisierter und allgemeiner LLMs effektiv kombiniert, um auf Standard-Benchmarks hochwertige Ergebnisse zu erzielen.

4. Experimentelle Ergebnisse

Die Methode wurde auf miniF2F-Test und ProofNet-Test unter Verwendung von Lean4 evaluiert. Das Framework setzte ein Ensemble von Modellen ein, darunter DeepSeek-Prover-V2-7B, Goedel-Prover-V2-8B, Seed-Coder-8B, Qwen2.5-7B und GPT-4.1-mini (als Bewerter).

Wichtige Leistungsmetriken:

miniF2F: Erzielte 100,00 % formale Gültigkeit und einen Gesamtscore von 90,27 %. Die Rate „perfekter" Formalisierungen (alle Dimensionen mit Score 1) erreichte 49,18 %.
ProofNet: Erzielte 77,96 % formale Gültigkeit und einen Gesamtscore von 52,45 %, mit 17,74 % perfekten Formalisierungen.

Vergleichende Befunde:

Monoton vs. Baselines: Der monotone Prozess schnitt signifikant besser ab als sowohl Best-of-k (Sampling von $k$ Ausgaben) als auch Iterative Selbstverfeinerung (ISR) ohne Akzeptanzrichtlinien.
Ensemble vs. Einzelmodell: Während ein einzelnes starkes Modell (GPT-5.4) Verbesserungen zeigte, erzielte das Ensemble kleinerer, spezialisierter Modelle, die spezifischen Rollen zugewiesen waren, überlegene Leistungen, insbesondere bei der formalen Gültigkeit.
Robustheit: Der monotone Trend blieb auch bei der Bewertung durch verschiedene LLM-Bewerter-Familien (z. B. Qwen vs. GPT) und menschliche Experten bestehen, was darauf hindeutet, dass die Verbesserungen keine Artefakte von Bewertungsverzerrungen sind.

5. Bedeutung und Behauptungen

Das Papier behauptet, dass diese Arbeit einen praktischen und theoretisch fundierten Schritt hin zu einer zuverlässigen Autoformalisierung darstellt. Durch die Arbeit in einer referenzfreien Weise ist der Ansatz auch in Domänen anwendbar, die keine umfangreichen formalen Bibliotheken besitzen, und könnte potenziell die Formalisierung unerforschter Bereiche der Mathematik und Wissenschaft unterstützen.

Die Autoren betonen, dass das Framework eine prinzipielle Methodik für die KI-gestützte Autoformalisierung bietet, die:

Den Bedarf an menschlicher Aufsicht in großskaligen formalen Verifizierungspipelines reduziert.
Unsicherheit in Bewertungen durch LCB-Annahmen explizit quantifiziert und steuert.
Zeigt, dass die Kombination komplementärer LLMs mit Feedback formaler Verifizierer Formalisierungen mit nachweislich nicht-abnehmender Qualität hervorbringen kann.

Die Arbeit schließt, dass die Rechenkosten zwar höher sind als bei der Inferenz in einem einzigen Durchgang, dieser Trade-off jedoch durch die signifikanten Gewinne in Leistung und Stabilität gerechtfertigt ist und den Weg für zukünftige Forschung in sicherer, zuverlässiger KI-gestützter formaler Schlussfolgerung ebnet.