Do We Need Frontier Models to Verify Mathematical Proofs?

Problemstellung

Mit dem Aufkommen von „Frontier"-Modellen (den leistungsstärksten Large Language Models, LLMs), die bei mathematischen Wettbewerben Goldmedaillen gewinnen und komplexe offene Probleme lösen, wächst die Notwendigkeit, deren Lösungen zu verifizieren. Da mathematische Beweise oft in natürlicher Sprache formuliert sind und subtile Fehler, Lücken oder implizite Annahmen enthalten können, ist eine manuelle Überprüfung teuer und zeitaufwendig.
Die zentrale Forschungsfrage des Papers lautet: Ist es notwendig, extrem große und rechenintensive Frontier-LLMs einzusetzen, um mathematische Beweise zu verifizieren, oder reichen kleinere, Open-Source-Modelle aus?
Während die Generierung von Beweisen als schwierige Aufgabe gilt, wird die Verifikation oft als einfacher angesehen. Es ist jedoch unklar, welche Modellkapazitäten für eine zuverlässige Verifikation tatsächlich erforderlich sind, insbesondere im Hinblick auf Genauigkeit und Konsistenz.

Methodik

Die Autoren führten eine systematische Evaluation durch, um die Fähigkeiten von LLMs als „Richter" (Judges) für mathematische Beweise zu vergleichen.

1. Evaluierte Modelle:
   • Frontier-Modelle: GPT-5.2 und Gemini 3.1 Pro (jeweils mit Varianten für niedrigen und hohen „Reasoning"-Aufwand).
   • Open-Source-Modelle: GPT-OSS (20B und 120B Parameter) und Qwen3.5 (35B und 122B Parameter).
2. Datensätze:
   • Drei Benchmarks mit Olympiade-Level-Problemen und menschlich bewerteten Beweisen: IMO-GradingBench, ProofArena und ProofBench.
   • Die Beweise wurden von menschlichen Experten auf einer Skala von 0–7 bewertet. Für die binäre Verifikation (Korrekt/Falsch) wurden nur perfekte Beweise (7 Punkte) als korrekt gewertet.
3. Metriken:
   • Balanced Accuracy (BA): Das arithmetische Mittel aus True Positive Rate und True Negative Rate (Maß für die Richtigkeit der Urteile).
   • Self-Consistency: Der Anteil der Fälle, in denen ein Modell bei drei wiederholten Abfragen mit demselben Prompt das gleiche Urteil fällt (Maß für die Reproduzierbarkeit).
4. Prompt-Strategien:
   • Zunächst wurden drei Standard-Prompts (IMOBench, GIMO, ProofBench7pt) getestet.
   • Anschließend wurde eine Prompt-Ensemble-Methode entwickelt. Dabei wurde ein automatisierter Suchprozess (unterstützt durch Claude Code) genutzt, um eine Sammlung von 12 spezialisierten Prompts zu synthetisieren, die verschiedene Fehlermodi abdecken (z. B. „Logic Chain Verifier", „Proof Repair", „Extreme Skeptic").
   • Die Urteile dieser Prompts wurden durch eine Schwellenwert-Abstimmung (Threshold Voting) aggregiert: Ein Beweis gilt als korrekt, wenn mindestens 8 von 12 Aufrufen „Korrekt" melden.

Hauptergebnisse

1. Lücke in der Genauigkeit vs. Konsistenz:

   • Kleinere Open-Source-Modelle liegen in der Balanced Accuracy nur ca. 10 % hinter den Frontier-Modellen zurück. Dies deutet darauf hin, dass die reine mathematische Fähigkeit zur Fehlererkennung in kleineren Modellen bereits vorhanden ist.
   • Der entscheidende Unterschied liegt jedoch in der Self-Consistency: Kleinere Modelle sind bis zu 25 % inkonsistenter als Frontier-Modelle. Sie neigen dazu, bei wiederholten Abfragen unterschiedliche Urteile zu fällen.

2. Empfindlichkeit gegenüber Prompts:

   • Die Verifikationsgenauigkeit ist stark von der Prompt-Wahl abhängig. Bestimmte Prompts (wie GIMO) führen bei allen Modellen zu einer hohen Rate an falsch-negativen Urteilen (Ablehnung korrekter Beweise), während andere zu falsch-positiven Urteilen neigen.

3. Analyse der Fehlermodi:

   • Kleinere Modelle scheitern oft nicht am mangelnden mathematischen Verständnis, sondern daran, dass sie mit Standard-Prompts nicht zuverlässig auf die relevanten Fehlermodi (z. B. logische Brüche, fehlende Fallunterscheidungen) fokussieren.
   • Qualitative Analysen zeigten zwei Hauptfehlerarten:
     • Das Modell reproduziert fehlerhafte Logik wortwörtlich und validiert sie fälschlicherweise.
     • Das Modell erfindet eigene Argumente, um Lücken zu füllen, statt den Fehler zu melden.

4. Wirksamkeit des Prompt-Ensembles:

   • Durch den Einsatz des spezialisierten Prompt-Ensembles konnten die Leistungen der kleineren Modelle drastisch verbessert werden:
     • Steigerung der Balanced Accuracy um bis zu 9,1 %.
     • Steigerung der Self-Consistency um bis zu 15,9 %.
   • Ergebnis: Modelle wie Qwen3.5-35B erreichen mit dem Ensemble eine Leistung, die mit Frontier-Modellen wie Gemini 3.1 Pro gleichzieht oder diese in bestimmten Metriken sogar übertrifft.

Wichtige Beiträge

1. Systematische Evaluation: Eine umfassende Studie, die die Verifikationsfähigkeiten von Frontier- und kleineren Open-Source-Modellen über mehrere Datensätze und Prompt-Strategien hinweg vergleicht.
2. Identifikation der Kapazitätslücke: Der Nachweis, dass die Leistungslücke bei der Verifikation primär durch Inkonsistenz und nicht durch mangelnde mathematische Intelligenz der kleineren Modelle verursacht wird.
3. Entwicklung eines Prompt-Ensembles: Die Synthese einer Methode, die durch die Kombination komplementärer, spezialisierter Prompts (anstatt eines einzelnen allgemeinen Prompts) die Zuverlässigkeit kleinerer Modelle signifikant erhöht.
4. Praktische Implikation: Die Demonstration, dass kleine, kostengünstige Open-Source-Modelle durch Inference-Time-Techniken (wie Prompt-Ensembling) für hochzuverlässige Beweisverifikation eingesetzt werden können, ohne auf teure Frontier-Modelle angewiesen zu sein.

Bedeutung und Fazit

Das Paper widerlegt die Annahme, dass für die Verifikation komplexer mathematischer Beweise zwingend Frontier-Modelle erforderlich sind. Es zeigt auf, dass kleinere Modelle die notwendige mathematische Kompetenz bereits besitzen, diese aber mit Standard-Prompts nicht konsistent abrufen können.

Die vorgeschlagene Prompt-Ensemble-Methode fungiert als effektiver „Inference-Time-Booster", der die Schwächen kleinerer Modelle ausgleicht. Dies hat weitreichende Konsequenzen:

• Kosteneffizienz: Verifikation kann mit deutlich günstigeren Open-Source-Modellen durchgeführt werden.
• Reproduzierbarkeit: Die Methode erhöht die Stabilität der Urteile, was für automatisierte Bewertungssysteme entscheidend ist.
• Zukunftsperspektive: Die Erkenntnisse könnten genutzt werden, um das Post-Training (RLHF) von LLMs für mathematisches Reasoning zu verbessern und die Methodik auf andere Domänen wie Recht oder Finanzen zu übertragen.

Zusammenfassend lässt sich sagen: Wir brauchen keine Frontier-Modelle für die Beweisverifikation, solange wir die richtigen Inferenz-Strategien (spezialisierte Prompt-Ensembles) anwenden.