Vom Lösen von Textaufgaben zu Beweisjurys: fünf Jahre KI-Mathematik

Die Mathematik war lange Zeit ein bösartiger Spiegel für Sprachmodelle. Das Modell könnte einen überzeugenden Aufsatz über Zahlentheorie schreiben und dann sofort die Division vermasseln, eine notwendige Bedingung mit einer hinreichenden verwechseln oder sich in der letzten Zeile selbst widersprechen. Seine Zunge klang klüger als seine Berechnung.

Doch in nur fünf Jahren hat sich fast alles verändert: Aufgaben, Metriken, Modelle und die Vorstellung, was „KI hat ein mathematisches Problem gelöst“ eigentlich bedeutet. Im Jahr 2021 haben wir gemessen, ob ein Modell beim ersten Versuch die kurze Antwort trifft. Im Jahr 2026 sehen wir uns Systeme an, die eine Population von Beweisen erstellen, sich gegenseitig kritisieren, sie korrigieren, sie durch Python oder Lean laufen lassen und erst dann in einem Turnier einen Gewinner auswählen.

Dieser Text ist eine technische Geschichte dieser Transformation. Kein Ranking von Marken, sondern eine Karte der Prinzipien: Welche Systeme haben in jedem Zeitraum gewonnen, warum sie gewonnen haben und welche scheinbar klugen Ideen immer wieder gescheitert sind. Am Ende werde ich es in ein Mathe-Modus-Design für unsere HyperFusion und Experimente mit LUMI übersetzen.

Hauptaussage: Die größten Sprünge kamen nicht nur vom größeren Modell. Sie wurden durch neue Einsatzmöglichkeiten der Berechnung hervorgerufen: detaillierte Vorgehensweise, Kandidatenvielfalt, Abstimmung, Tools, Verifizierung, gezielte Korrektur und schließlich die Orchestrierung des gesamten Beweisprozesses.

Zunächst ein Nachteil: Die Ergebnisse sind nicht direkt vergleichbar

Die Zahl „90 % in Mathematik“ kann vier sehr unterschiedliche Bedeutungen haben:

• Das Modell hat einmal die richtige Zahl generiert.
• die richtige Antwort erschien mindestens einmal unter Hunderten von Versuchen;
• die meisten der vielen Lösungen stimmten über das richtige Ergebnis überein;
• Der formale Beweis hat den Kernel-Validator lückenlos bestanden.

Dazu gehören die Modellgröße, der Zugriff auf Tools, die Anzahl der Proben, die Kontextlänge, das Zeitlimit, die Testhardware, die öffentlichen Daten und manchmal auch die menschliche Formalisierung der Aufgabe. Daher werde ich für jedes Ergebnis mindestens die folgenden Metriken unterscheiden:

Diese Unterscheidung ist wichtiger als die Reihenfolge in der Tabelle. Wenn ein System mit 2000 Samples ein Modell bei pass@1 schlägt, bedeutet das nicht automatisch, dass es sich um ein besseres Basismodell handelt. Das bedeutet, dass es eine effizientere Kombination aus Generator, Budget und Selektor gab.

2021: MATH und GSM8K zeigen, dass flüssiges Denken nicht gleichbedeutend mit logischem Denken ist

Mathe: Wettbewerbsprobleme wie eine kalte Dusche

Der MATH-Benchmark ergab 12.500 wettbewerbsfähige High-School-Aufgaben in Algebra, Geometrie, Zahlentheorie, Wahrscheinlichkeit und anderen Bereichen. Jeder hatte nicht nur eine Antwort, sondern auch eine Schritt-für-Schritt-Lösung. Die damaligen großen Transformatoren erreichten nur Einheiten von einem Prozent; Die Autoren berichteten von einer Spanne von etwa 2,9 bis 6,9 %.

Das war der Schlüsselmoment. Bei gängigen NLP-Benchmarks funktionierte die Skalierung fast wie ein Universalrezept. MATH hat gezeigt, dass ein größeres Sprachmodell die Form eines mathematischen Textes besser nachahmen kann, ohne eine lange Kette von Abhängigkeiten zuverlässig aufrechtzuerhalten. Der Fehler in der ersten Vermutung verwandelte sich im sechsten Schritt in einen elegant platzierten Unsinn.

Darüber hinaus hatte der Benchmark später große kulturelle Auswirkungen: Er legte ein gemeinsames Ziel fest, an dem die Schulung zu mathematischen Daten, Eingabeaufforderungen, Abstimmungen und Werkzeugen gemessen werden konnte. Gleichzeitig kam es jedoch allmählich zu einer Sättigung. Sobald ein Test zum Trainingskompass für ein ganzes Feld wird, ist er keine neutrale Landschaft mehr.

GSM8K: einfache Arithmetik, schwere Sprachstruktur

Im selben Jahr wurden GSM8K: 8.500 Textaufgaben für die Grundschule, typischerweise mit zwei bis acht Schritten, erstellt. Es war keine schwierige Theorie. Es ging darum, die Geschichte in die richtige Abfolge von Abläufen zu übersetzen.

Bei GSM8K tauchte eines der beständigsten Prinzipien der gesamten Geschichte auf: Es ist einfacher, zuverlässig zu generieren als auszuwählen. OpenAI ließ das Modell viele Kandidatenlösungen produzieren und trainierte einen Verifizierer, diese einzustufen. Eine Verbesserung des Verifizierers hätte einen ähnlichen Effekt haben können wie eine drastische Vergrößerung des Generators.

Doch schon damals zeichnete sich ein zukünftiges Problem ab: Mit der wachsenden Zahl an Kandidaten tauchen Lösungen auf, die fehlerhaft sind, den Prüfer aber täuschen können. Mehr Samples helfen nur so lange, bis der Selektor die Qualität schneller erkennt, als der Generator anspruchsvolle Fehler produziert.

2022: Model hat gelernt, „Arbeit zu zeigen“

Gedankenkette: Zwischenergebnisse wie Arbeitsgedächtnis

Die Arbeit Chain-of-Thought Prompting hat gezeigt, dass einige Beispiele mit einer detaillierten Vorgehensweise zu einer deutlich besseren mehrstufigen Lösung für ein großes Modell führen können. Der PaLM 540B erreichte mit acht Samples das damalige Spitzenergebnis bei GSM8K.

Warum hat es funktioniert? Nicht, weil das Textverfahren automatisch ein Beweismittel ist. Durch die generierten Token wurde ein externer Desktop erstellt. Das Modell musste nicht alle Zwischenergebnisse in einer versteckten Berechnung speichern; er könnte sie in den nächsten Schritten konditionieren.

Aber CoT hat eine gefährliche Angewohnheit entwickelt: ein überzeugend klingendes Verfahren mit einer getreuen Aufzeichnung interner Überlegungen zu verwechseln. Eine Sprachkette kann eine Rationalisierung sein. Die richtige Zahl kann über den falschen Weg erreicht werden oder es kann erst bei der letzten Transkription ein Fehler auftreten. CoT ist ein leistungsstarker Kandidatengenerator, kein Zertifikat.

PAUSE 1: ACHT BEISPIELE ÄNDERT DIE BERECHNUNGSMETHODE

Gedankenkette: Das Modell erhielt mehrere gelöste Beispiele und begann, die Zwischenergebnisse in seine eigene Ausgabe zu schreiben. Der Text wurde zum externen Arbeitsgedächtnis. Es handelte sich um einen Übergang von einem einmaligen Hinweis zu einem überprüfbaren Verlauf, der noch nicht bewiesen ist.

Selbstkonsistenz: Ein Pfad ist ein Beispiel, kein Urteil

Selbstkonsistenz ersetzte die gierige Dekodierung durch eine einfache Idee: Probieren Sie mehrere verschiedene Prozesse aus und marginalisieren Sie sie gegenüber dem Endergebnis. Bei GSM8K verbesserte es die ursprüngliche Arbeit um 17,9 Prozentpunkte, bei SVAMP um 11 und bei AQuA um 12,2 Punkte.

Der Algorithmus ist fast trivial:

solutions = sample(model, problem, n=64, temperature>0)
answers   = normalize_final_answers(solutions)
winner    = most_frequent(answers)
return best_explanation_among(solutions_with(winner))

Seine Stärke liegt in der Annahme, dass die richtige Antwort viele unabhängige Pfade hat, während die Fehler verstreut sind. Wenn jedoch alle Stichproben dasselbe falsche Stereotyp haben, wird die Mehrheitsentscheidung den Fehler nur verstärken. Textvielfalt ist nicht dasselbe wie Fehlervielfalt.

DURCHBRUCH 2: +17,9 PROZENTPUNKTE BEI GSM8K

Selbstkonsistenz: Probieren Sie verschiedene Verfahren aus, extrahieren Sie die endgültige Antwort aus jedem, konvertieren Sie äquivalente Notationen in die gleiche Form und wählen Sie das häufigste Ergebnis aus. Das gleiche Prinzip führte zu 11 Punkten bei SVAMP und 12,2 Punkten bei AQuA.

Minerva: Datenspezialisierung plus Testzeitberechnung

Minerva verfolgte PaLM weiter und setzte die Schulung zu zig Milliarden technischen Inhalts-Tokens fort, darunter Mathematik-Websites und arXiv. Minerva 540B erreichte bei MATH mit Mehrheitsentscheidung 50,3 %. Im Jahr 2021 würde eine solche Zahl absurd erscheinen.

Eine Kombination aus drei Dingen hat gewonnen:

1. starkes Basismodell;
2. domänenreiches Fortsetzungs-Vortraining;
3. Dutzende bis Hunderte unabhängiger Lösungen während der Inferenz.

Dies ist das erste klare historische Muster: Training bestimmt die Verteilung der verfügbaren Strategien, Inferenz entscheidet, wie viele davon wir durchsuchen.

2022 bis 2024: Der Rechner steht wieder im Raum

Ein Sprachmodell ist gut darin, eine Prozedur zu entwerfen, aber seine Kapazität zur exakten Multiplikation zu verschwenden, ist so, als würde man einem Mathematiker nicht erlauben, Papier zu verwenden. Die nächste Generation von Systemen trennte daher die Planung von der Ausführung.

PAL: Das Modell schreibt das Programm, die Laufzeit berechnet

Programmgestützte Sprachmodelle ließ das Programm von LLM generieren und übergab das Endergebnis Python. PAL mit Codex auf GSM8K übertraf das viel größere PaLM mit Chain of Thought um 15 Prozentpunkte.

Die Arbeitsteilung ist elegant:

• das Modell erkennt Entitäten und Beziehungen;
• erstellt eine symbolische oder Programmprozedur;
• die deterministische Laufzeit führt die Arithmetik durch;
• Das System gibt das Ergebnis sowie eine überprüfbare Aufzeichnung der Berechnung zurück.

Dadurch verschwinden nicht alle Fehler. Das Modell kann die Eingabe falsch übersetzen oder ein Programm schreiben, das die falsche Menge korrekt berechnet. Das Tool entfernt jedoch die gesamte Klasse numerischer Übersprechungen und ermöglicht automatische Tests.

DURCHBRUCH 3: +15 PROZENTPUNKTE AUF GSM8K

PAL: Das Modell zählte nicht mehr jede Zahl Token für Token. Er übersetzte die Beziehungen in ein Programm, Python erledigte die Arithmetik und das Ergebnis wurde in der Antwort zurückgegeben. Die Rollenverteilung übertrifft PaLM um eine Größenordnung mit einer reinen Gedankenkette.

ToRA: abwechselnder Text und Werkzeuge

ToRA nutzt das Tool nicht erst am Ende. Das Modell wechselt zwischen natürlicher Sprache und Aufrufen von Python oder einem symbolischen Löser, beobachtet das Ergebnis und fährt fort. ToRA-7B erzielte bei MATH 44,6 % und die Variante ToRA-Code-34B übertraf 50 %.

Aus architektonischer Sicht ist dies wichtiger als die Zahl selbst. Die Lösung änderte sich von einem Monolog zu einem geschlossenen Kreislauf:

plán → kód → výsledek nástroje → revize plánu → další kód → odpověď

Diese Schleife ist der Vorläufer der heutigen Agenten. Der Unterschied besteht lediglich in der Anzahl der Rollen und darin, ob die Korrektur durch dasselbe Modell, ein anderes Modell oder ein formales System durchgeführt wird.

DeepSeekMath: Daten, GRPO und ein kleines Modell, dessen Fähigkeiten nicht mehr klein sind

DeepSeekMath 7B setzte das Vortraining für 120 Milliarden Mathe-Tokens fort und implementierte Group Relative Policy Optimization, später bekannt als GRPO. Ohne Tools und Abstimmung erreichte es 51,7 % bei MATH, mit einer Selbstkonsistenz von 60,9 % bei 64 Stichproben.

Während Minerva die Leistungsfähigkeit eines riesigen Spezialmodells demonstrierte, zeigte DeepSeekMath, dass ein hochwertiges mathematisches Korpus, gezielte Post-Training- und Testzeit-Stichproben ein 7B-Modell bis vor Kurzem in den Bereich von Hunderten von Milliarden Parametern bringen können.

DURCHBRUCH 4: +9,2 PROZENTPUNKTE BEI 64 VERSUCHEN

DeepSeekMath: Derselbe 7B-Checkpoint hatte 51,7 % bei pass@1 und 60,9 % bei Selbstkonsistenz über 64 Proben. Der Unterschied zeigt genau, wie viel Fähigkeit bereits im Generator vorhanden war, aber ein Versuch konnte sie nicht zuverlässig extrahieren.

Benchmark verteidigt: Robustheit, Multimodalität und wirklich schwierige Fragen

Als MATH und GSM8K zu bekannt wurden, wurden Tests entwickelt, um ihre Schwächen zu beseitigen.

OlympiadBench: Text ist nicht genug

OlympiadBench enthält 8.476 zweisprachige multimodale Mathematik- und Physikaufgaben. Das Diagramm ist keine Dekoration mehr; trägt einen Teil der Informationen. Bei der Markteinführung erreichte GPT-4V insgesamt 17,97 %. Der Benchmark trennte die Fähigkeit, das Bild zu lesen, die Situation zu formalisieren und die Berechnung durchzuführen.

GSM-Symbolisch: Ändern Sie die Nummern und sehen Sie, was übrig bleibt

GSM-Symbolic generiert symbolische Varianten derselben Vorlagen. Das Modell kann also nicht nur von der spezifischen Formulierung einer bekannten Frage profitieren. Die Autoren zeigten eine signifikante Varianz zwischen numerischen Instanzen und großen Einbrüchen nach dem Hinzufügen irrelevanter Informationen.

Dies ist ein Vorbehalt für jede Bestenliste: Ein hoher Durchschnittswert bedeutet nicht unbedingt einen invarianten Algorithmus. Ein Modell hat möglicherweise lokale Heuristiken gelernt, die auf einer typischen Datenoberfläche funktionieren, aber bei kleinen Transformationen zusammenbrechen.

FrontierMath: Gibt eine Frage zurück, die das Modell wahrscheinlich nicht gesehen hat

FrontierMath wurde als Sammlung neuer, von Experten erstellter Probleme vom höheren Universitäts- bis zum Forschungsniveau erstellt. Bei der Markteinführung im Jahr 2024 lagen die Spitzenmodelle bei höchstens rund zwei Prozent. Nur eine glatte Nachahmung des olympischen Stils half hier nicht weiter.

Auch bei FrontierMath muss die Governance geprüft werden. Epoch AI erklärte später, dass einige Fragen im Auftrag von OpenAI erstellt worden waren und das Unternehmen auf alle Fragen außer dem Holdout zugreifen konnte. Das macht den Benchmark nicht ungültig, verändert aber die Interpretation des Ergebnisses. Datenherkunft und Datenzugriff sind Teil der Metrik.

2024: AIMO 1 und der Sieg des offenen 7B-Systems

Der erste Progress Prize-Wettbewerb AI Mathematical Olympiad zog über tausend Teams an. Gewann das Numina-Projekt mit einem System, das auf DeepSeekMath-Base 7B basiert. In der öffentlichen Lösung NuminaMath lag die Magie nicht in einer einzelnen Modellherausforderung, sondern in einer präzise gestalteten Daten- und Inferenzkette.

Warum die Teilnehmer die Frontier-API nicht nutzten

Die Regeln unterschieden sich bewusst von einem normalen Chatbot-Benchmark. Bewertet wurde auf 50 verborgenen Aufgaben ähnlich AMC 12 und AIME, jeweils mit ganzzahliger Antwort. Erlaubt waren nur öffentliche Open-Weight-Modelle, die vor dem Stichtag erschienen waren. Die Submission lief als Offline-Kaggle-Notebook ohne Internet und externe APIs, auf einer P100 oder zwei T4, höchstens neun Stunden. Deshalb ergibt der 7B-Checkpoint Sinn: Gemessen wurde das gesamte lokale System unter einem festen Rechenbudget, nicht der Zugriff auf das teuerste geschlossene Modell. Details stehen im technischen Bericht des Siegerteams.

Numina sammelte etwa eine Million mathematische Probleme, bereinigte und kommentierte die Lösungen, unterteilte das Training in klassische Gedankenkette und werkzeugintegriertes Denken und nutzte SC-TIR für Schlussfolgerungen. Die öffentliche Beschreibung listet etwa 860.000 CoT-Beispiele und 70.000 TIR-Beispiele auf. Das endgültige DeepSeekMath-Base 7B wurde zunächst vollständig auf CoT und dann auf TIR abgestimmt und lief als 8-Bit-AutoGPTQ-Variante.

Reproduzierbares Erfolgsrezept: 48 Kandidaten mal 4 Zyklen

Für jede Aufgabe wurden N = 48 -Kandidaten generiert. Als der Kandidat den Python-Block öffnete, wurde die Generierung gestoppt, der Code ausgeführt und die Ausgabe oder der Traceback kehrte in den Kontext zurück. Dieser Zyklus könnte maximal M = 4 Runden lang andauern. Unvollendete Flugbahnen verworfen. Die endgültigen ganzen Zahlen wurden aus den verbleibenden Ausgaben gezogen und die häufigste normalisierte Antwort gewann. Größere N oder M halfen im Neun-Stunden-Limit nicht mehr.

for candidate in 48_parallel_samples:
    repeat at most 4 times:
        generate until Python block or final answer
        if Python block: execute and append stdout or traceback

answers = normalize(extract_integer(completed_candidates))
return most_frequent(answers)

Normalisierung ist kein LLM-Judge. Sie extrahiert die geforderte Ganzzahl, entfernt eine Hülle wie \boxed{...}, vereinheitlicht äquivalente Schreibweisen und verwirft ein ungültiges Format. Danach werden die Häufigkeiten gezählt. Länge oder Überzeugungskraft des Lösungswegs zählen nicht. Jedes gültige Ergebnis gibt seiner Zahl genau eine Stimme.

DURCHBRUCH 5: 48 KANDIDATEN × 4 PYTHON-ZYKLEN

Numina SC-TIR: offenes 7B-Modell, 8-Bit-Quantisierung, 48 Trajektorien, höchstens vier Rückgaben von Python und einfache Mehrheit normalisierter Zahlen. Das Ergebnis war 29 von 50 richtig.

Das Originalschema des siegreichen Numina-Teams. Quelle: project-numina/aimo-progress-prize, Apache-Lizenz 2.0.

2025: AIMO 2 und der Moment, in dem die einfache Mehrheit nicht mehr ausreichte

Den zweiten Fortschrittspreis gewann NVIDIA NemoSkills mit einer Punktzahl von 34/50. Das System wird im Dokument OpenMathReasoning und im öffentlichen Repository NeMo Skills beschrieben.

Die Regeln galten erneut lokal und offline. Der private Test umfasste 50 Aufgaben, das Notebook bekam vier L4-GPUs und fünf Stunden. Der siegreiche Checkpoint basierte auf Qwen2.5-14B-Base. Acht Epochen wurden auf 2,2 Millionen DeepSeek-R1 CoT-Lösungen trainiert. Es folgte ein kurzes TIR-Tuning an 15.000 Beispielen, 400 Schritten mit der Lernrate 1e-5. Anschließend kombinierten die Autoren die Kontrollpunkte linear im Verhältnis 0,3 × CoT + 0,7 × TIR.

Die erfolgreiche Schlussfolgerung nutzte FP8, die spekulative Dekodierung von ReDrafter, und eine nahezu gierige Temperatur von 0. Das Modell konnte bis zu 16 Kandidaten produzieren, aber das System brach den Lauf ab, sobald die ersten vier bis fünf vollständigen Antworten übereinstimmten. Er wies einer Aufgabe eine Basis von 350 Sekunden zu, übertrug die ungenutzte Zeit in die Reserve und konnte einer schwierigen Aufgabe bis zu 560 Sekunden widmen. Python war in einer einzelnen Trajektorie maximal sechs Mal erlaubt, mit einer Zeitüberschreitung von zwei Sekunden und der Rückgabe nur der ersten 200 Zeichen der Ausgabe.

DURCHBRUCH 6: 34 VON 50 UNTER DEM FÜNF-STUNDEN-LIMIT

AIMO 2-Siegerlauf: 14B-Kontrollpunkt mit 0,3 CoT und 0,7 TIR, FP8, ReDrafter, bis zu 16 nahezu gierigen Kandidaten und einem frühen Ausstieg bei Übereinstimmung von vier bis fünf Antworten. Der Schlüssel lag nicht in einem weiteren Riesenmodell, sondern darin, mit der Zeit zu arbeiten und schnell eine stabile Mehrheit zu finden.

Wichtige Korrektur: GenSelect war nicht Teil des siegreichen Laufs

Tatsächlich hat OpenMathReasoning GenSelect entwickelt, das ein Problem und mehrere vollständige Lösungen erhält und generativ den vielversprechendsten Kandidaten auswählt. Der siegreiche AIMO 2-Eintrag nutzte es jedoch aus Zeitgründen nicht. Eine frühere Version dieses Artikels kombinierte die beiden Teile des Artikels, was ungenau war.

Im GenSelect-Forschungsprotokoll arbeitete er mit 64 generierten Lösungen. Es wurden wiederholt Teilmengen von 16 Kandidaten empfangen, die Auswahl wurde 64 Mal getroffen und die endgültige Antwort wurde größtenteils anhand der ausgewählten Ergebnisse generiert. Über 32 Generationen hinweg begann es instabil zu werden, da nicht alle Flugbahnen in eine Eingabeaufforderung passten. Es ist ein wertvoller Ansatz für weitere Forschung, aber es ist nicht das Rezept, das AIMO 2 gewonnen hat.

majority:  argmax_a  sum_i 1[normalize(answer_i) = a]
GenSelect: repeat 64 times select_one(problem, subset_of_16_solutions)
           then vote over normalized answers of selected solutions

Eine spätere gemeinsame Evaluierung zeigte, wie stark die Ergebnisse mit dem Budget wachsen. Die Kombination öffentlicher Systeme erreichte in sehr vielen Versuchen den Wert 47/50.. Das ist beeindruckend, aber auch pass@very-high-k. Belastung und Auswahlmechanismus gehören ebenso in den Titel wie die Anzahl der Punkte.

Regeln von drei AIMO-Wettbewerben in einer Tabelle

Daher gewinnt das größte verfügbare Grenzmodell bei AIMO nicht automatisch. Die Regeln entfernen das Internet und proprietäre APIs, begrenzen Hardware und Zeit und erfordern ein lokal steuerbares Artefakt. Der Wettbewerb misst somit das Modell, die Quantisierung, die Bedienung, den Umgang mit Instrumenten, das Zeitmanagement und die Auswahl insgesamt.

Parallelzweig: von der Antwort zum vom Kernel akzeptierten Beweis

Klassische Benchmarks überprüfen oft die endgültige Zahl. Aber Mathematik ist nicht die einzige Antwort. Beim Beweis ist es wichtig, dass jeder Schritt aus den vorherigen Aussagen folgt.

miniF2F und PutnamBench

miniF2F ergab 488 formale Behauptungen in Systemen wie Lean, Metamath und Isabelle. PutnamBench erweiterte den Anspruch auf 1.692 Formalisierungen von 640 Wettbewerbstheoremen für Studenten.

Formale Beweise verändern den Schiedsrichter. Ein kleiner vertrauenswürdiger Kernel ersetzt das Bewertungsmodell. Der Beweis passt entweder typologisch und logisch oder nicht. Dadurch wird ein großer Teil der ästhetischen Voreingenommenheit beseitigt, es geht jedoch mit einem anderen Preis einher: der Umwandlung des natürlichen Inputs in eine formale Sprache, der Suche nach Bibliothekslemmas und einem riesigen Raum möglicher Taktiken.

AlphaProof: Silber bei der IMO, aber mit manueller Formalisierung

Im Jahr 2024 erzielten AlphaProof und AlphaGeometry 2 zusammen 28 von 42 Punkten bei der Internationalen Mathematikolympiade, der Silbermedaillenstufe. Sie haben vier von sechs Aufgaben gelöst.

AlphaProof nutzte Lean und Reinforcement Learning, um nach formalen Beweisen zu suchen. Allerdings mussten die Aufträge manuell in eine formale Sprache umgewandelt werden und einige Aufträge dauerten mehrere Tage, bis sie vom System verarbeitet wurden. Das Ergebnis war also nicht „ein Chatbot hat meiner Meinung nach in einem normalen Gespräch gelöst“, sondern ein Triumph aus einer Kombination aus Formalisierung, Suche und Verifizierung.

AlphaGeometry 2 hingegen profitierte von einer engen Domäne und einer symbolischen Geometrie-Engine. Das ist eine weitere Geschichtslektion: Ein spezialisierter Löser mit harten Invarianzen kann ein allgemeineres System in einer engen Klasse schlagen.

DeepSeek-Prover und Goedel-Prover: Compiler als Lehrer

DeepSeek-Prover-V2 arbeitete mit rekursiver Zerlegung in Unterziele und verstärkendem Lernen. Die Autoren berichteten von 88,9 % bei miniF2F und 49 gelösten Problemen von 658 in PutnamBench, allerdings mit dem 671B-Modell und mit einem bestimmten Sampling-Budget.

Goedel-Prover-V2 zeigte, wie schnell sich die Effizienz veränderte. Seine 8B-Variante meldet 84,6 % auf miniF2F bei pass@32; 32B mit Selbstkorrektur 90,4 %. Der Fix nutzt Lean-Compiler-Feedback: Das Modell erhält kein vages „Versuchen Sie es erneut“, sondern eine bestimmte Position und Art des Fehlers.

DURCHBRUCH 7: 90,4 % MIT COMPILER IM KONTROLLKREIS

Goedel-Prover-V2 32B: entwirft einen formalen Beweis, Lean liefert eine genaue Diagnose und das Modell korrigiert das lokalisierte Problem. Der Kernel bewertet weder Stil noch Vertrauen. Entweder besteht der Beweis oder nicht.

Das Grundprinzip ist universell:

navrhni důkaz → spusť ověřovač → přečti diagnostiku → oprav lokální chybu → znovu ověř

Dies ist viel zuverlässiger als die Aufforderung, „Ihre Antwort zu überprüfen“, da die Kritik von einem anderen Mechanismus als der Generierung herrührt.

2025: Gold in natürlicher Sprache bei IMO

Google DeepMind gab bekannt, dass das fortgeschrittene Gemini Deep Think IMO 2025 35 von 42 Punkten, die Goldmedaillenstufe] erreicht hat. Er löste fünf von sechs Aufgaben, die Lösungen wurden offiziell bewertet und innerhalb des Wettbewerbslimits von 4,5 Stunden in natürlicher Sprache erstellt.

Im Vergleich zu AlphaProof 2024 ist der qualitative Unterschied enorm: keine manuelle Eingabeformalisierung und keine mehrtägige Suche. Deep Think verwendet paralleles Denken. Auch hier geht es nicht um einen perfekt geraden Weg, sondern darum, mehrere Wege zu suchen und diese zu kombinieren.

Man kann jedoch durchaus sagen, dass es sich um ein geschlossenes System handelt. Wir kennen nicht alle Einzelheiten der Ausbildung, die Anzahl der internen Kandidaten oder die genaue Auswahl. Das Ergebnis ist offiziell, die Reproduzierbarkeit der Architektur jedoch nicht.

2026: AIMO 3 und das Ende der Illusion, dass nur ein Modell konkurriert

AIMO 3 brachte 110 neue Probleme von der Nationalen Olympiade auf IMO-Niveau, aus Algebra, Kombinatorik, Geometrie und Zahlentheorie. Die Antwort war fünfstellig. Die Konkurrenten arbeiteten in einem Offline-Laptop mit dem H100 und konnten auf offenen Waagen wie gpt-oss-120b oder Qwen3-Next aufbauen.

Die Bekanntgabe der Gewinner zählt Exalted Joseph, varianceofx, SKobayak, TAMU-TACO und yemao ye zu den Top-Preisträgern. Es hob zwei Kennzeichen der neuen Ära hervor: ein sehr starkes gemeinsames Basismodell mit hoher Varianz und gemeinsamen Notizbüchern, die die besten Geschirre schnell zwischen den Teams verteilen. Die führenden Ergebnisse haben sich gebündelt. Der Unterschied hat sich von „Ich habe ein geheimes Modell“ zu „Ich kann konsequent gute Kandidaten aus dem Modell extrahieren und sie nicht fallen lassen“ verschoben.

Für den ersten Platz gibt es in der offiziellen Zusammenfassung kein kompaktes Rezept mit einer sicher zitierfähigen Anzahl an Kandidaten. Ich möchte ihn mir nicht vorstellen. Aber das zweitplatzierte öffentliche System ist exakt reproduzierbar varianceofx: lokales gpt-oss-120b über vLLM, zustandsbehaftete Jupyter-Python-Sandbox, bis zu acht parallele Versuche und eine Kombination aus einfacher Mehrheit und entropiegewichteter Bewertung. Das ist nützlicher als die vage Behauptung, dass „das 120B-Modell gewonnen hat“.

DURCHBRUCH 8: BIS ZU 8 VERSUCHE UND ENTROPISCH GEWICHTETE STIMME

AIMO 3 2. Platz Öffentliches Rezept: gpt-oss-120b generiert bis zu acht Lösungen mit Zugriff auf Stateful Python. Die Übereinstimmung der Antworten ist das Hauptsignal, aber die Sicherheit der Token passt ihr Gewicht an. Ein Kandidat ist also nicht nur deshalb stärker, weil er groß oder stilsicher ist.

AIMO 3 bestätigte somit, dass es notwendig ist, den gesamten Versuchsvertrag zu veröffentlichen:

• Checkpoint und Quantisierung;
• Probenahmeparameter;
• Anzahl und Dauer der Versuche;
• Antwortnormalisierung;
• Wiederherstellung bei unvollständiger Begründungsausgabe;
• Zeitüberschreitungen und Hardwarenutzung;
• Auswahlalgorithmus.

Ohne sie ist der Score nur das Ergebnis einer unsichtbaren Mischung aus Modell und Infrastruktur.

Proof Pilot: 25 Aufrufe eines 32B-Modells als Proof-Organisation

Nach AIMO 3 wurde der Proof Pilot gestartet, der auf menschenlesbare Beweise abzielte. Die erfolgreiche offene Lösung von Yi-Chia Chen ist gerade deshalb äußerst lehrreich, weil sie nicht auf einem riesigen proprietären Modell beruht. Das öffentliche repository und deploy bundle beschreiben ein von OLMo 3.1 32B Think abgeleitetes Modell mit einem DeepSeek-V4-Tokenizer, einer Destillation aus DeepSeek-V4-Flash und einem quantisierten Dienst.

Aber das Wichtigste ist die Schlussfolgerung. Ein Prüfpunkt wechselt die Rollen mit einer Eingabeaufforderung:

1. sechs Prüfer werden unabhängige Beweise erstellen;
2. Jeder Vorschlag erhält zwei Verifizierungsgutachten, also zwölf Kritiker.
3. Drei Refinerdurchgänge verfeinern die vielversprechendsten Kandidaten.
4. Vier Wähler stimmen über den Gewinner ab.

Die 6 / 2 / 3 / 4 -Konfiguration bedeutet insgesamt 25 Modellaufrufe pro Task. Darüber hinaus verfügt der veröffentlichte Harness über einen Watchdog, der mit einem sehr langen Kontext arbeitet, einen unvollendeten <think> -Block speichert und Fallbacks bietet. Dies sind nicht die operativen Details unter dem Strich. Im Argumentationsmodell sind sie Teil des Algorithmus.

DURCHBRUCH 9: 25 ANRUFE, AUFGETEILT IN VIER BERUFE

Proof Pilot: Unabhängige 6 -Proofe, 12 -Kritiker, 3 gezielte Korrekturen und 4 -Auswahlvoten. Dabei kommt es nicht nur auf die Anzahl der Stichproben an, sondern auch auf die Reihenfolge der Rollen und die Informationen, die sie miteinander teilen.

Das Modellpaket meldet einen IMO-ProofBench v2-Durchschnittswert von 4,48/7mit der Claude-Gegenprüfung und 3,808/7mit dem DeepSeek-Grader; Der DeepSeek-V4-Flash des Lehrers wird mit 4,83/7. gelistet. Der Unterschied zwischen den beiden Bewertern ist an sich schon eine Warnung: Natürlich handelt es sich bei dem Richter nicht nur um ein Messgerät, sondern um ein weiteres Modell mit eigenem Fehler.

Technisch gesehen ist auch der Unterschied zwischen einem Lehrer und einem Schüler interessant. Die Modellkarte listet etwa 18,74 GB für die GPTQ-Variante auf, gegenüber etwa 65 GB in BF16. Die Fähigkeit wurde also nicht nur durch harte Antworten vermittelt, sondern auch durch mehrphasige Destillation und weiche Ziele. Allerdings weisen die Autoren bei der Komprimierung auf Tendenzen zu Wiederholungen und Schleifen hin. Genau diese Art der Degradation kann ein Multiagentensystem vervielfachen, wenn es keinen Watchdog hat.

Was wirklich in der Geschichte gewonnen hat

Die Tabelle ist keine einzelne Bestenliste. Jede Zeile hat einen anderen Datensatz und ein anderes Budget. Es zeigt sich jedoch ein beständiger Trend: Systeme, die redundante Berechnungen in kontrollierte Diversität und Qualitätsauswahl umwandeln, gewinnen.

Was im Gegenteil immer wieder nicht funktionierte

1. „Lassen Sie das Modell länger nachdenken“, ohne es zu überprüfen

Längeres Nachdenken kann zu Korrekturen, aber auch Grübeleien, Wiederholungen und Selbstverstärkung führen. Ein besonders quantisiertes Modell kann immer wieder Tausende von Token desselben Fehlers erzeugen. Ein Budget ohne Prüfung ist keine Garantie für Qualität.

2. Mehr Proben ohne Oracle-Gap-Messung

Wenn oracle@64 = 90 % aber der Selektor 65 % erreicht, liegt das Problem nicht beim Generator. Zusätzliche Samples können den Selektor noch mehr überfordern. Zunächst gilt es zu analysieren, warum die richtige Lösung nicht gewinnt.

3. Die meisten Modelle mit demselben Fehler

Drei Kontrollpunkte derselben Familie, die auf ähnlichen Daten trainiert und von derselben Eingabeaufforderung gesteuert werden, sind keine drei unabhängigen Stimmen. Es handelt sich um drei Messungen mit demselben Bias. Für die Fusion ist manchmal ein schwächerer, aber anderer Löser wertvoller als eine weitere Kopie des stärksten.

4. Der generative Richter als einzige Quelle der Wahrheit

Ein LLM-Richter verwechselt leicht Länge, Selbstvertrauen oder vertrauten Stil mit Korrektheit. Könnte die gleiche Reaktion der Familie bevorzugen. Wo es Python, SymPy, Unit Test oder Lean gibt, muss das harte Signal Vorrang vor dem ästhetischen Urteil haben.

5. Eine Synthese, die das richtige Fundament bis zur Unkenntlichkeit „anreichert“.

Bei internen HyperFusion-Tests auf DRACO sahen wir einen extremen Fehler der alten generativen Fusion: Eine mit 88,7 % bewertete GPT-5.5-Antwort sank nach aggressiver Komprimierung auf 13,9 %, sodass 295 Zeichen von etwa 27.000 Zeichen übrig blieben. Der Synthesizer hat keinen winzigen Fehler gemacht; Beweisinhalte vernichtet.

Die neuere v3augment -Strategie wählt zunächst die stärkste Basis aus, bewahrt sie und fügt nur gezielt nicht widersprüchliches Wissen hinzu. Der Durchschnitt lag im gesamten Set bei 84,9 %, während die beste einzelne Rohantwort bei 81,6 % lag. Für die Mathematik folgt daraus eine strengere Regel: wählen und überprüfen; Überschreiben Sie nicht, es sei denn, Sie haben einen lokalisierten Fehler.

6. Benchmark ohne Datenherkunft

Das Ergebnis ohne Angaben zu Datum, Datensatzversion, Zugang zum Test und Auswertungsmethode altert stark. Bei mathematischen Benchmarks ist die Kontamination besonders gefährlich: Eine vertraute Aufgabe kann wie eine Verallgemeinerung aussehen, obwohl es sich um eine Rekonstruktion einer auswendig gelernten Vorlage handelt.

Wie würde ich HyperFusion Math daraus erstellen?

Die aktuelle HyperFusion verwendet eine Gruppe von Modellen, einen anonymisierten Richter und einen Synthesizer. Für allgemeine Suchen ist Select-and-Augment sinnvoll. Für die genaue Berechnung würde ich jedoch einen separaten Modus mit Konfidenzrang hinzufügen:

1. deterministischer Test: Berechnung, Substitution, numerische Kontrolle, Invarianz;
2. Formeller Test: ob die Aufgabe formalisierbar und die Bibliothek verfügbar ist;
3. unabhängige Kritik: Suche nach Fehlern in Prämisse und Vollständigkeit;
4. gewichtete Übereinstimmung: nur als zusätzliches Signal;
5. Stil und Klarheit: der letzte Filter, nicht der erste.

Die Punktzahl eines Kandidaten kann beispielsweise wie folgt aussehen:

score(c) = α · V_exec(c)
         + β · V_formal(c)
         + γ · log P_selector(c)
         + δ · Σ_i w_i · 1[answer_i = answer_c]
         - λ · risk(c)

Wo:

• V_exec ist das Ergebnis eines Codes, einer Substitution oder eines Tests;
• V_formal ist die Akzeptanz durch einen formellen Prüfer;
• P_selector ist die Wahrscheinlichkeit des generativen Selektors;
• w_i ist das im Trainingsteil geschätzte Solver-Gewicht;
• risk bestraft einen Analysefehler, eine unvollständige Argumentation, einen unbegründeten Schritt oder einen Widerspruch zwischen dem Beweis und der Antwort.

Beim Abschlusstest dürfen keine Koeffizienten erstellt werden. Es ist notwendig, den Datensatz nach Aufgabenfamilien zu unterteilen, nicht zufällig nach Zeilen, da sonst fast dieselben Vorlagen in Training und Test gelangen.

Das Experiment würde ich als nächstes auf LUMI durchführen

Wenn wir die Antworten mehrerer lokaler Modelle gespeichert haben, müssen wir nicht zuerst zusätzliche Schlussfolgerungen ziehen. Wir können offline messen, welche Kombinationen überhaupt Potenzial haben.

Phase A: kein Richter, nur anhand vorhandener Antworten

Für jedes Modell und jeden Speichermodus:

• normalisierte endgültige Antwort;
• Korrektheit;
• Parse schlägt fehl und schneidet ab;
• Länge, Zeit, Token und Speicher;
• Modellfamilie und Modus-ID think/nothink.

Berechnen Sie dann für alle Paare, Tripel und Vierlinge:

1. Einzelpass@1;
2. Mehrheiten/weightedAbstimmung;
3. oracle@k: ob mindestens ein Mitglied Recht hatte;
4. Uneinigkeitsquote;
5. paarweise Korrelation von Fehlern;
6. Leistung in Kategorien und Schwierigkeiten;
7. Preis um einen weiteren Prozentpunkt.

Die Kombination mit der höchsten Summe der Einzelwerte ist nicht die interessanteste. Es handelt sich um eine Kombination mit einer hohen Oracle-Obergrenze und einer geringen Fehlerkorrelation.

Phase B: Selektortraining ohne Datenleck

Ich würde die Aufteilung wie folgt vorschlagen:

Wenn der Datensatz klein ist, würde ich eine verschachtelte Kreuzvalidierung nach Jobtypen verwenden. Für die 60 Elemente des GPQA-Diamond-Typs ist das Unsicherheitsintervall breit; Ein Unterschied von ein paar Punkten kann eine einzige Frage sein. Für mathematische Benchmarks ist ein deutlich größerer Holdout ideal.

Phase C: teurer Judge nur dort, wo er Informationswert hat

Ich würde nicht immer Richter anrufen. Ich würde es nur ausführen, wenn:

• überlebende Kandidaten geben unterschiedliche Antworten;
• harte Tests haben nicht entschieden;
• Die Oracle-Analyse zeigt, dass die richtige Lösung oft existiert, aber durch einfache Abstimmung nicht gefunden werden kann.

Dadurch entsteht eine Kaskade: Einfache Fragen werden durch billigen Konsens, rechnerische Python-Aufgaben und formale Lean-Aufgaben gelöst, und nur echte Konflikte bekommen eine teure Jury.

Das spezifische erste Panel

Für das erste Experiment würde ich unser vorgeschlagenes Trio-Panel Gemma-4-31B think + Qwen-27B nothink + GLM-5.2 Q4 nothink beibehalten, da es verschiedene Modi und Familien kombiniert. Aber ich würde Gemma nicht automatisch zur Richterin ernennen, nur weil sie die beste Einzelpunktzahl hat. Zunächst würde ich anhand historischer Reaktionen messen:

• Wie oft korrigiert Gemma den Streit richtig?
• wie oft bevorzugt er seinen eigenen Stil;
• Was ist der Unterschied zwischen der Auswahlgenauigkeit und der einfachen Mehrheit?
• ob nicht ein kleinerer spezialisierter Prüfer das gleiche Ergebnis günstiger bringen wird.

Der stärkste Löser und der beste Richter sind zwei verschiedene Rollen. Die Geschichte von GSM8K, GenSelect und Proof Pilot ist darin überraschend konsistent.

Was Sie statt einer einzelnen Nummer sehen sollten

Für jedes Experiment würde ich mindestens diesen Vektor veröffentlichen:

pass@1
oracle@k
maj@k
selector@k
formal_or_exec_pass
mean_tokens
p95_latency
peak_memory_gb
parse_fail_rate
cost_per_correct

Es kann verwendet werden, um zu diagnostizieren, wo das System verliert:

• niedrig oracle@k → mangelhafter Generator oder Diversität;
• hoch oracle@k, niedrig selector@k→ Richter versagt;
• hoch selector@k, niedrig formal_or_exec_pass→ Richter schätzt Plausibilität;
• hohe Punktzahl, hoch parse_fail_rate → Pipeline ist labortechnisch stabil, betrieblich anfällig;
• kleiner Gewinn für um ein Vielfaches höhere Token → Testzeitberechnung hat bereits eine abnehmende Rendite.

Was ist mit der Forschung aus dem Jahr 2026?

Die Forschung bewegt sich schnell von einfachen Best-of-N-Analysen hin zu Evidenzpopulationen. MaxProof beschreibt beispielsweise ein Modell in vier Rollen: Generator, Prüfer, Verfeinerer und Rangierer. Es nutzt Bevölkerungssuche und Turnierauswahl. Die Autoren des Preprint-Berichts 35/42auf der IMO 2025 und 36/42auf der USAMO 2026. Es ist wichtig hinzuzufügen, dass es sich hierbei um das Ergebnis des Preprints des Autors und nicht um das offizielle Wettbewerbsurteil handelt.

DeepMind für das System Aletheia beschreibt den Generierungs-, Verifizierungs- und Revisionszyklus sowie das Leistungswachstum mit Testzeitberechnungen. Der Trend ist derselbe: Das Modell wandelt sich von einem Responder zu einem Prozess.

Gleichzeitig stellt sich heraus, dass generative Verifizierer nicht neutral sind. Die Arbeit an Skalierung generativer Verifizierer lenkt die Aufmerksamkeit auf die Sensitivität der Eingabeaufforderung und den Unterschied zwischen der Auswahl der richtigen Antwort und der Bewertung der Qualität der Evidenz. Reinforcement Learning kann Verfahrensmetriken verbessern, ohne die Genauigkeit der endgültigen Antwortauswahl zu verbessern.

Daher wird meiner Meinung nach der nächste entscheidende Schritt weniger effektiv sein als „ein noch größeres Argumentationsmodell“: kalibrierte, heterogene und überprüfbare Verifizierung.

Fazit: Die Mathematik wurde nicht durch ein Modell gewonnen, sondern durch eine neue Art, die Berechnung zu organisieren

Von 2021 bis 2026 wiederholt sich eine große Geschichte.

MATH und GSM8K zeigten, dass Sprachkenntnisse nicht ausreichen. Die Gedankenkette hat einen Jobpfad geschaffen. Durch Selbstkonsistenz wurde aus einer einzelnen Spur eine Population. PAL und ToRA haben die genaue Berechnung den Tools überlassen. Numina hat die Leistungsfähigkeit eines offenen Modells, von Daten und Abstimmungen gezeigt. Die siegreichen NeMo-Skills kombinierten TIR, Checkpoint-Merge, schnelle Dekodierung und frühen Stopp; Sein GenSelect-Forschungszweig zeigte eine intelligentere Auswahl für zukünftige Systeme. Lean verwandelte den Compiler in einen Schiedsrichter. AlphaProof kombinierte Formalisierung mit RL-Suche. Gemini Deep Think ist in der natürlichen Sprache fündig geworden. Proof Pilot hat gezeigt, dass ein einzelner 32B-Kontrollpunkt eine Organisation aus vier Berufen sein kann.

Für HyperFusion bedeutet dies nicht, dass wir 25 Aufrufe pro Frage blind kopieren müssen. Dies führt zu etwas Praktischerem:

1. Kultivieren Sie echte Fehlervielfalt und nicht nur mehr Text.
2. Messen Sie die Orakeldecke, bevor wir einen teureren Richter kaufen.
3. Bevorzugen Sie harte Validierung gegenüber LLM-Flair;
4. einen lokalisierten Fehler korrigieren, nicht die korrekte Basis neu schreiben;
5. separater Generator, Prüfer, Verfeinerer und Selektor, auch wenn sie physisch von einem Modell gespielt werden;
6. Geben Sie das Inferenzbudget ebenso deutlich an wie die Punktzahl.
7. Schützen Sie den Test beim Erlernen von Gewichten und Routing vor Leckagen.

Das beste mathematische System der Zukunft ist möglicherweise nicht das Modell, das „am meisten weiß“. Es wird das System sein, das am besten weiß, wenn es nicht weiß, wer von den anderen einfach mehr weiß und wie es es überprüfen kann, bevor es die Antwort weiterleitet.

---

Primärquellen und Reproduktionsmaterialien

• Hendrycks et al.: MATH
• Cobbe et al.: GSM8K und geschulte Prüfer
• Wei et al.: Chain-of-Thought Prompting
• Wang et al.: Selbstkonsistenz
• Lewkowycz et al.: Minerva
• Gao et al.: PAL
• Gou et al.: ToRA
• Shao et al.: DeepSeekMath
• He et al.: OlympiadBench
• Mirzadeh et al.: GSM-Symbolic
• Epochen-KI: FrontierMath
• Numina: AIMO 1 Gewinnerlösung und technische Analyse 48 × 4 SC-TIR
• NVIDIA: AIMO 2 paper und NeMo Skills
• AIMO-Preis: Regeln und Start von AIMO 3 und Bekanntgabe der Gewinner
• varianceofx: Zuchtrezept 2. Platz AIMO 3
• DeepMind: AlphaProof und AlphaGeometry 2
• DeepMind: Gemini Deep Think bei IMO 2025
• Zheng et al.: miniF2F
• Tsoukalas et al.: PutnamBench
• Ren et al.: DeepSeek-Prover-V2
• Goedel-LM: Goedel-Prover-V2
• Yi-Chia Chen: Proof Pilot code und Bundle bereitstellen
• Jiang et al.: LLM-Blender
• Wang et al.: Mixture-of-Agents
• DeepSeek-AI: DeepSeek-R1
• Chen et al.: MaxProof

Anmerkung zu den Abbildungen: Jedes Ergebnis im Text gehört zu einem bestimmten Protokoll der Autoren. Pass@1, Selbstkonsistenz, Pass@k, offizielle olympische Punkte und LLM-Richterergebnisse sind nicht austauschbar. Bei Vorabdrucken präsentiere ich die Ergebnisse als Behauptungen der Autoren und nicht als unabhängig bestätigte Aufzeichnungen.