Technische Zusammenfassung: Risikokontrolliertes Lean-as-Judge für mathematische Schlussfolgerungen in natürlicher Sprache

1. Problemstellung

Die Arbeit adressiert die Herausforderung, formale Beweisassistenten (insbesondere Lean) als Richter für mathematische Schlussfolgerungen in natürlicher Sprache zu nutzen, die von Large Language Models (LLMs) generiert werden. Während ein erfolgreicher Lean-Beweis starke positive Evidenz für eine formale Aussage liefert, ist das Fehlen eines Beweises ein mehrdeutiges Signal. Ein gescheiterter Beweis kann auf eine mathematisch falsche Antwort hindeuten, kann aber ebenso auf eine schlecht typisierte Formalisierung, fehlende Bibliotheksfakten oder Zeitüberschreitungen bei der Beweissuche zurückzuführen sein.

Derzeitige Ansätze behandeln Beweisversagen oft als negatives Korrektheitssignal, was das Risiko birgt, mathematische Unkorrektheit mit mangelnder formaler Abdeckung zu vermischen. Die Autoren identifizieren eine „Abdeckungsklippe" (coverage cliff): Die Zuverlässigkeit der formalen Selektion hängt scharf vom Anteil der Kandidatenantworten ab, die erfolgreich formalisiert und bewiesen werden können. Bei hoher Abdeckung ist die formale Selektion hochgenau; bei niedriger Abdeckung wird das Signal unzuverlässig.

Das Kernproblem besteht darin, zu bestimmen, wann ein nachgelagertes System einem formalen Lean-Signal vertrauen sollte und wann es das Signal als außerhalb der Abdeckung (d. h. ungelöst) und nicht als falsch behandeln sollte, während gleichzeitig eine Finite-Sample-Risikogarantie für die akzeptierten Antworten bereitgestellt wird.

2. Methodik: COVCAL

Die Autoren schlagen COVCAL (Coverage-Calibrated Lean) vor, einen risikokontrollierten selektiven Wrapper, der basierend auf Abdeckungsdagnostik entscheidet, ob eine formale Antwort akzeptiert oder zurückgehalten wird.

2.1 Rahmenwerk der partiellen Beobachtung

Das System behandelt die formale Pipeline als Mechanismus der partiellen Beobachtung. Es beobachtet nicht die Wahrheit jeder Kandidatenantwort, sondern nur:

1. Welche normalisierten Antwortklassen einen wohlgeformten Lean-Ausdruck erreichen (Typisierte Abdeckung).
2. Welche dieser Klassen erfolgreich bewiesen werden (Beweis-Abdeckung).
3. Das Gewicht der höchstgewichteten bewiesenen Klasse gegenüber dem höchstgewichteten ungelösten Rivalen (Formaler Rand).

Eine Antwortklasse ist definiert als eine Gruppe von Kandidatenstrings, die dieselbe finale Antwort bezeichnen (z. B. $1/2$, $0.5$, $2/4$). Klassen, die nicht formalisiert oder nicht bewiesen werden, gelten als ungelöst, nicht automatisch als falsch.

2.2 Abdeckungsdagnostik

COVCAL berechnet vier Schlüsselmetriken für ein gegebenes Problem $x$:

• Typisierte Abdeckung ($C_{typ}$): Das Gesamtgewicht der Kandidatenklassen, die einen wohlgeformten Lean-Ausdruck erreicht haben (Status: proved, typechecked oder timeout).
• Beweis-Abdeckung ($C_{prf}$): Das Gesamtgewicht der Kandidatenklassen, die einen kernelgeprüften Beweis erhalten haben.
• Gewicht ungelöster Rivalen ($R_{unres}$): Das Gewicht der höchstgewichteten Antwortklasse, die nicht bewiesen wurde.
• Formaler Rand ($M$): Die Differenz zwischen dem Gewicht der höchstgewichteten bewiesenen Klasse und dem Gewicht der ungelösten Rivalen.

2.3 Selektion und Zertifizierung

COVCAL akzeptiert die höchstgewichtete bewiesene Klasse nur, wenn eine vorab deklarierte Regel basierend auf Schwellenwerten $(\tau_{typ}, \tau_{prf}, \tau_M)$ erfüllt ist. Wird die Regel nicht erfüllt, enthält sich das System (oder weicht auf eine nicht-formale Methode wie Selbstkonsistenz zurück).

Um Zuverlässigkeit zu gewährleisten, setzt COVCAL eine Finite-Sample-selektive Risikozertifizierung ein. Es garantiert, dass mit einer Wahrscheinlichkeit von $1-\delta$ das selektive Risiko (Fehlerrate) der akzeptierten Antworten höchstens $\epsilon$ beträgt. Zwei Zertifizierungsregime werden vorgeschlagen:

1. Bonferroni-Regime: Sucht über ein Gitter von Schwellenwerten auf einem Kalibrierungs-Split an und wendet eine Union-Bound-Korrektur ($\delta/|T|$) an, um die Mehrfachvergleiche zu berücksichtigen. Dies ist konservativ und erfordert eine hohe Signal-Dichte, um durchführbar zu sein.
2. Dev-then-Cal-Regime: Wählt den Schwellenwert auf einem unabhängigen Entwicklungs-Split aus und zertifiziert diesen einmal auf dem Kalibrierungs-Split unter Verwendung einer einzelnen Clopper-Pearson-Schranke ($\delta$). Dies ist effizienter in Bezug auf die Stichprobengröße, erfordert jedoch eine strikte Trennung zwischen Entwicklungs- und Kalibrierungsdaten.

2.4 Theoretische Grenzen

Die Arbeit beweist, dass ohne Abdeckungsdagnostik (d. h. wenn man sich ausschließlich auf das Vorhandensein eines Beweises verlässt) kein nicht-vakuelles punktuelles Korrektheitszertifikat abgeleitet werden kann, wenn eine ungelöste, nicht äquivalente Rivalenklasse existiert. Fehlende formale Evidenz ist kein Beweis für mathematische Falschheit; sie ist ein Beweis für einen ungelösten Status.

3. Hauptbeiträge

1. Charakterisierung der Abdeckungsklippe: Auf dem MATH-500-Datensatz demonstrieren die Autoren, dass die „beweisgewinnende" Antwort bei hoher Beweis-Abdeckung zu 96 % korrekt ist, bei niedriger Abdeckung jedoch nur zu 20 %. Dies etabliert, dass Lean-Beweise nur dann zuverlässig sind, wenn Abdeckung und Rand hoch sind.
2. Signal-Spärlichkeit und Treue: Das formale Signal ist spärlich und unvollkommen. Ein 7B-Auto-Formalisierer beweist eine Klasse nur für 28 % der Probleme. Darüber hinaus zeigt eine manuelle Prüfung, dass nur $\approx 43\%$ dieser Beweise treu zum ursprünglichen Problem sind (der Rest sind triviale Identitäten oder wahre, aber irrelevante Aussagen).
3. COVCAL-Methode: Ein Rahmenwerk für selektive Vorhersagen, das Risiken unter partieller Beobachtung zertifiziert. Es behandelt explizit die Asymmetrie des Beweisversagens und bietet Finite-Sample-Garantien für akzeptierte Vorhersagen.
4. Formalisierer-abhängige Durchführbarkeit: Die Arbeit zeigt, dass die Durchführbarkeit von Zertifikaten durch die Abdeckung der Auto-Formalisierung bestimmt wird. Ein 7B-Formalisierer liefert ein Signal, das für das konservative Bonferroni-Regime zu spärlich ist (Ablehnung aller 20 Bootstrap-Partitionen), während ein auf Beweise spezialisierter Formalisierer (Goedel-Prover-V2-8B) mit 79 % Abdeckung die Methode in 17/20 Partitionen durchführbar macht.

4. Experimentelle Ergebnisse

Experimente wurden auf einem gefilterten Teilbereich von MATH-500 (378 Beispiele) durchgeführt, wobei Qwen2.5-Math-7B für die Generierung und verschiedene Formalisierer für die Auto-Formalisierung verwendet wurden.

• Baseline-Leistung: Selbstkonsistenz allein erreicht ohne Zurückhaltung eine Genauigkeit von 91 %.
• COVCAL-Leistung:
  • Unter dem Bonferroni-Regime mit einem 7B-Formalisierer lehnt die Methode alle Eingaben ab (0/20 Partitionen), da das Signal zu spärlich ist, um die strikte Union-Bound zu erfüllen.
  • Unter dem Dev-then-Cal-Regime mit dem 7B-Formalisierer werden 12/20 Partitionen zertifiziert. Der akzeptierte Anteil beträgt $\approx 21\%$, mit einer akzeptierten Genauigkeit von 0,93.
  • Mit dem Goedel-Prover-V2-8B (spezialisierter Formalisierer) steigt die Beweis-Abdeckung auf 79 %. Bonferroni wird in 17/20 Partitionen durchführbar und akzeptiert $\approx 48\%$ der Probleme mit einer akzeptierten Genauigkeit von 0,98.
• Treue-Prüfung: Eine manuelle Prüfung von 45 geschichteten Beispielen zeigte, dass zwar 73,6 % der bewiesenen Aussagen nicht-trivial und korrekt waren, aber nur 43 % treu zur Problemstellung waren. Viele „bewiesene" Aussagen waren wahre Nebenfakten oder triviale Identitäten, die die Einschränkungen des Problems nicht erfassen.

5. Bedeutung und Behauptungen

Die Arbeit behauptet, dass ihr primärer Beitrag eine präzise Darstellung davon ist, wann und mit welchem Formalisierer ein partielles formales Signal unter Risikokontrolle vertrauenswürdig ist, und nicht einfach die Verbesserung der rohen Genauigkeit.

• Risikokontrolle vor roher Genauigkeit: Da Selbstkonsistenz bereits zu 91 % genau ist, liegt der Wert von COVCAL in seiner Fähigkeit, ein Zertifikat für den Teilbereich der Antworten bereitzustellen, die es akzeptiert, und zwischen „verifiziert" und „ungelöst" zu unterscheiden, anstatt zwischen „korrekt" und „falsch".
• Umgang mit partiellen Beobachtungen: Die Arbeit stellt formale Verifikation als Problem der selektiven Vorhersage neu dar, bei dem fehlende Beweise als ungelöste Kandidaten behandelt werden, wodurch eine Fehlklassifizierung korrekter Schlussfolgerungen als falsch aufgrund von Formalisierungsfehlern verhindert wird.
• Abhängigkeit von Spezialisierung: Die Ergebnisse unterstreichen, dass reine Modellgröße kein Ersatz für Spezialisierung ist. Ein auf Beweise spezialisierter Formalisierer übertrifft ein größeres Generalisten-Modell in Bezug auf die Beweis-Abdeckung signifikant, welche die bindende Einschränkung für zertifizierbare Risikokontrolle darstellt.

Die Autoren schließen, dass COVCAL als konservative Schnittstelle für die Nutzung von Lean als Richter dient: Es ist nur dann durchführbar und informativ, wenn der Auto-Formalisierer genügend Antwortmasse abdeckt, um ein Risikozertifikat zu stützen, garantiert aber nicht, dass alle Antworten verifiziert sind.