Technisches Resümee: IMProofBench

Problemstellung

Aktuelle Benchmarks zur Evaluierung von Large Language Models (LLMs) im Bereich Mathematik sind unzureichend, um Fähigkeiten auf Forschungsniveau zu bewerten. Bestehende Datensätze konzentrieren sich primär auf Mathematikprobleme des Gymnasial- oder Bachelor-Niveaus (z. B. AIME, MATH), die zunehmend von modernsten Modellen gelöst werden können und nicht in der Lage sind, echte Beweisführungsfähigkeiten zu testen. Darüber hinaus beschränken sich Benchmarks, die auf fortgeschrittene Mathematik abzielen, wie etwa FrontierMath und Humanity's Last Exam (HLE), oft auf die Korrektheit der Endantwort. Diese Einschränkung ermöglicht es Modellen, Abkürzungen zu nutzen oder die richtige Antwort zu erraten, ohne logisch fundierte Argumente zu konstruieren, wodurch die kritische Fähigkeit zur Erstellung rigoroser mathematischer Beweise vernachlässigt wird. Es mangelt an einem standardisierten, privaten Benchmark, der LLMs bei der Generierung mathematischer Beweise auf Forschungsniveau in einer realistischen, werkzeuggestützten Umgebung evaluiert.

Methodik

Benchmark-Konstruktion (IMProofBench)

IMProofBench ist ein privater Benchmark, der aus 77 durch Fachkollegen geprüften Problemen besteht, die in Zusammenarbeit mit über 44 professionellen Mathematikern entwickelt wurden. Die Pipeline zur Problemerstellung umfasst:

• Autorenschaft: Probleme werden von Forschern innerhalb ihrer jeweiligen Fachgebiete verfasst, das Spektrum reicht von Fragen aus mündlichen Prüfungen auf Graduate-Niveau bis hin zu offenen Forschungsproblemen.
• Peer-Review: Jede Einreichung durchläuft einen strengen Prüfungsprozess durch ein Kernteam sowie einen externen Experten auf dem relevanten Gebiet, um die mathematische Korrektheit, angemessene Schwierigkeit und Klarheit zu gewährleisten.
• Struktur: Jedes Problem besteht aus einer Hauptaufgabe zur Beweisführung und Folgefragen mit einzigartigen, automatisch bewertbaren Antworten. Diese duale Struktur unterstützt sowohl die menschliche Expertenbewertung des Beweises als auch die automatisierte quantitative Analyse der Endantworten.
• Dynamik: Der Benchmark ist als kontinuierliche Plattform konzipiert. Probleme werden laufend hinzugefügt, und Autoren werden ermutigt, Probleme zu entfernen, falls diese aufgrund neuer Forschungsergebnisse lösbar werden, um sicherzustellen, dass der Benchmark nicht gesättigt wird.

Evaluations-Framework

Die Evaluation simuliert eine realistische Forschungsumgebung unter Verwendung eines agentischen Frameworks, das auf dem Inspect-Framework basiert. Modelle operieren mit Zugriff auf:

• Rechenwerkzeuge: Python (NumPy, SciPy, SymPy), Bash (Arch Linux) und spezialisierte mathematische Software wie SageMath, GAP, Maxima, PARI/GP und Singular.
• Literaturrecherche: Web-Suchfunktionen zur Lokalisierung relevanter Theoreme, Paper oder Daten (z. B. OEIS).
• Interaktion: Modelle gehen mehrstufige Interaktionen ein und nutzen ein submit-Werkzeug, um Denkprozesse von den finalen Ausgaben zu unterscheiden.

Bewertungsprozess

Die Evaluation erfolgt in zwei Stufen:

1. Automatisierte Bewertung: Folgefragen werden bewertet, indem die Ausgaben des Modells mit den Ground-Truth-Antworten verglichen werden.
2. Menschliche Expertenbewertung: Der Hauptbeweis wird vom Autor des Problems auf einer Skala von 0 bis 3 bewertet:
   • 0/3: Kein Fortschritt.
   • 1/3: Geringfügiger Fortschritt (begrenzte Weiterentwicklung).
   • 2/3: Bedeutender Fortschritt (substanzielle Arbeit geleistet).
   • 3/3: Vollständige Lösung.
     Grader annotieren zudem spezifische Fehlertypen (logische Fehler, Halluzinationen, Rechenfehler, konzeptionelle Missverständnisse) und Leistungsindikatoren (Verständnis, korrekte Ergebnisse, Erkenntnisse, Nützlichkeit). Um Bias zu vermeiden, werden die Identitäten der Modelle während der Bewertung verborgen.

Zentrale Beiträge

1. IMProofBench: Ein privater, sich entwickelnder Benchmark, der speziell für die Generierung mathematischer Beweise auf Forschungsniveau entwickelt wurde und durch direkte Zusammenarbeit mit der mathematischen Gemeinschaft entstanden ist.
2. Systematische Analyse: Eine umfassende Evaluierung modernster LLMs hinsichtlich der Beweisführung, die von menschlichen Experten beurteilt wird und über die einfache Korrektheit der Endantwort hinausgeht.
3. Qualitative Erkenntnisse: Eine detaillierte Analyse der Stärken und Fehlermodi der Modelle, die die Lücke zwischen der Genauigkeit der Endantwort und der genuinen Fähigkeit zur Beweisführung sowie die Interaktion der Modelle mit Forschungswerkzeugen aufzeigt.

Experimentelle Ergebnisse

Leistungsübersicht

Die Autoren evaluierten 10 LLMs im beweisbasierten Teil des Benchmarks:

• Spitzenreiter: GPT-5.4 erzielte die höchste Leistung und produzierte vollständige Lösungen (3/3) für 49 % der Aufgaben. GEMINI-3.1-PRO folgte dicht darauf mit 46 %.
• Schwächere Modelle: CLAUDE-OPUS-4.6 lieferte nur in 32 % der Fälle vollständige Lösungen.
• Offene Probleme: Unter den 23 offenen Forschungsfragen im Benchmark löste GPT-5 im Dezember 2025 eine Aufgabe.

Endantwort vs. Beweisführung

Auf der Teilmenge von 45 Fragen mit Folgefragen erzielte GPT-5.4 eine Genauigkeit der Endantwort von 75 %. Die Korrelation zwischen den Scores der Folgefragen und dem menschlich bewerteten Beweisfortschritt lag bei 0,51, was darauf hindeutet, dass die Genauigkeit der Endantwort zwar ein nützlicher Indikator ist, aber nicht die Nuancen besitzt, die zur Bewertung der Qualität des Denkprozesses erforderlich sind.

Fehler- und Werkzeuganalyse

• Fehlertypen: Logische Fehler waren der häufigste Fehlermodus (z. B. unbegründete Annahmen), insbesondere bei CLAUDE-OPUS-4.6 (40 % der Antworten). Auch Halluzinationen nicht existenter Theoreme wurden beobachtet.
• Werkzeugnutzung: Die Modelle variierten signifikant in der Nutzung von Werkzeugen. GEMINI-3.1-PRO tätigte fast viermal so viele Werkzeugaufrufe wie andere Modelle, nutzte jedoch die wenigsten Output-Token.
• Ablationsstudie: Eine Ablation des agentischen Setups zeigte, dass der Zugriff auf Werkzeuge die Leistung generell verbesserte (z. B. +14,4 % für GROK-4), wenngleich einige Modelle (z. B. GEMINI-2.5-PRO) leichte Rückgänge verzeichneten, was wahrscheinlich auf eine suboptimale Werkzeugwahl (z. B. übermäßige Nutzung von Code-Interpretern für mathematische Argumentation) zurückzuführen ist.

Qualitative Beobachtungen

• Literaturwissen: Führende Modelle zeigten eine starke Vertrautheit mit spezialisierter mathematischer Literatur, hatten jedoch Schwierigkeiten mit obskuren Quellen wie privaten Vorlesungsnotizen.
• Halluzination und Selbstvertrauen: Modelle halluzinierten häufig Ergebnisse, um eine Antwort zu erzwingen, und vermieden es selten, eine Lösung anzubieten, selbst wenn sie feststeckten. Sie präsentierten oft fehlerhafte Argumente mit hoher Konfidenz.
• Erkenntnisgewinn: Trotz Fehlern lieferten die Modelle häufig Erkenntnisse und Teilergebnisse, die für menschliche Forscher nützlich sein könnten; GPT-5.4 lieferte in etwa 60 % der Versuche bedeutsame Beiträge.

Bedeutung und Behauptungen

Das Paper behauptet, dass IMProofBench eine kritische Lücke in der KI-Evaluierung schließt, indem es den Fokus von wettbewerbsorientierten Problemen auf die Generierung mathematischer Beweise auf Forschungsniveau verschiebt. Die Autoren stellen fest:

1. Aktuelle Fähigkeiten: Modernste LLMs können bereits einen bedeutsamen Teil von Forschungsfragen lösen, was ihr Potenzial als mathematische Kollaborateure unterstreicht.
2. Limitierungen: Aktuelle Modelle sind noch immer unvollkommen, neigen zu logischen Fehlern sowie Halluzinationen und besitzen oft nicht die Fähigkeit, zwischen einer korrekten Endantwort und einem validen Beweis zu unterscheiden.
3. Notwendigkeit der Evaluation: Der Benchmark zeigt, dass Metriken der Endantwort nicht ausreichen, um mathematische Fähigkeiten zu messen; die menschliche Expertenbewertung des Denkprozesses ist essenziell.
4. Zukünftige Ausrichtung: Die Arbeit etabliert einen Rahmen für die kontinuierliche, dynamische Evaluierung von LLMs in realistischen Forschungsumgebungen, um die Untersuchung zu erleichtern, wie KI effektiv in mathematische Arbeitsabläufe integriert werden kann.

Die Autoren vertreten eine bescheidene Position und merken an, dass sich der Benchmark derzeit noch in der aktiven Entwicklung befindet und nur eine begrenzte Anzahl von Problemen (77) umfasst, argumentieren jedoch, dass selbst diese Größenordnung wertvolle Einblicke in die Entwicklung der KI in der mathematischen Forschung bietet.