DeepSeekMath-V2 veröffentlicht – auf dem Weg zu selbstverifizierbarer mathematischer Schlussfolgerung

• Ein Modell, das auf die Verbesserung der mathematischen Schlussfolgerungsfähigkeit großer Sprachmodelle abzielt und die Überprüfbarkeit des Schlussfolgerungsprozesses stärkt, wobei es nicht nur auf die reine Korrektheit der Endantwort fokussiert
• Es behebt die Grenzen früherer auf Verstärkungslernen basierender Ansätze, die primär auf die Belohnung der Endantwort ausgerichtet waren, durch die Einführung eines Selbstverifizierungsmechanismus (self-verification)
• Bei Problemen mit Theorembeweis (theorem proving) und ähnlicher, schrittweiser logischer Herleitung ist das Generatormodell so konzipiert, dass es eigene Fehler erkennt und korrigiert
• Der Verifizierer (verifier) wird als Belohnungsmodell eingesetzt, und durch die Skalierung der Verifikationsberechnung werden schwierige Beweisdaten automatisch beschriftet, um eine kontinuierliche Leistungssteigerung zu ermöglichen
• Mit Höchstwerten bei IMO 2025, CMO 2024 und Putnam 2024 wurde die Machbarkeit selbstverifizierender mathematischer KI demonstriert

---

1. Einführung

• Große Sprachmodelle (LLM) haben im Bereich der mathematischen Schlussfolgerung große Fortschritte gemacht und fungieren als wichtiger Prüfstein der KI-Forschung
  • Durch Reinforcement Learning mit Lernen basierend auf Endantwort-Belohnung wurde in nur einem Jahr Spitzenleistung in Wettbewerben wie AIME und HMMT erreicht
• Dennoch hat der Ansatz, allein die Genauigkeit der Endantwort zu erhöhen, Grenzen
  • Selbst wenn das Endergebnis stimmt, ist die Gültigkeit des Schlussfolgerungswegs nicht gewährleistet, und für Aufgaben wie den Theorembeweis mit stufenweiser logischer Herleitung ist er nicht anwendbar
• Zur Lösung wurde das Konzept der Selbstverifikation (self-verification) eingeführt, damit die Vollständigkeit und Strenge der Schlussfolgerung bewertet werden
  • Insbesondere bei offenen Problemen (open problems) wurde es als zentrales Element vorgestellt, um bei Tests eine Erweiterung der Berechnung zu ermöglichen
• Das Forschungsteam trainierte einen genauen und vertrauenswürdigen LLM-basierten Verifizierer (verifier) und nutzte ihn als Belohnungsmodell, um den Beweisgenerator (generator) zu trainieren
  • Der Generator wird dazu angehalten, Fehler innerhalb eines Beweises selbst zu finden und zu korrigieren
• Mit steigender Leistung des Generators steigt auch der Schwierigkeitsgrad der Verifikation, daher wird die Verifikationsberechnung skaliert (scale verification compute), um neue schwierige Beweise automatisch zu labeln
  • Dadurch wird die Leistung des Verifizierers kontinuierlich verbessert
• Das Modell DeepSeekMath-V2 erreichte bei IMO 2025, CMO 2024 ein Goldmedaillen-Niveau und 118/120 Punkte im Putnam 2024
  • Diese Resultate zeigen, dass selbstverifizierendes mathematisches Schließen einen realistischen Forschungsweg darstellt

2. Evaluierungsergebnisse

• Zur Evaluierung wurden der von DeepMind’s DeepThink IMO-Gold-Team entwickelte IMO-ProofBench sowie aktuelle Mathematikwettbewerbe (IMO 2025, CMO 2024, Putnam 2024) verwendet
  • Konkrete Zahlen oder detaillierte Resultate sind im Fließtext nicht angegeben

3. Modellarchitektur

• DeepSeekMath-V2 basiert auf dem Modell DeepSeek-V3.2-Exp-Base aufgebaut
  • Unterstützungsinformationen zur Inferenz (inference) finden sich im GitHub-Repository von DeepSeek-V3.2-Exp

4. Lizenz

• Modell und Gewichte werden unter der Apache License 2.0 verteilt

5. Zitation

• Es sind Angaben zu Autoren und Paper vorhanden, der Titel lautet „DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning“ (2025)

6. Sonstige Informationen

• Downloads im letzten Monat: 4.434 Mal
• Beim Aufbau des Modellbaums bildet das Basismodell eine Selbstreferenz-Schleife und wird als „Baumerstellung nicht möglich“ angezeigt

[GN⁺]

Hacker-News-Kommentare

• Das diesmal veröffentlichte Modell hat seine Gewichte als Open Source unter der Apache-2.0-Lizenz offengelegt.
  Die IMO-Goldmedaillen-Modelle von OpenAI oder DeepMind sind weiterhin nicht öffentlich.

  • So wie AI-Unternehmen mit dem Urheberrecht an Trainingsdaten umgehen, sollten wir meiner Meinung nach auch das Urheberrecht an Gewichten behandeln.
  • Wenn jedoch nur die Gewichte offengelegt werden, nicht aber Trainingscode oder Daten, bleibt es weiterhin ein geschlossenes Modell.

• Die vorherige Diskussion findet sich unter diesem Link.

  • Diesen Link hatte ich verpasst, danke fürs Teilen.

• Beeindruckend ist, wie schnell Open-Weight-Modelle in spezialisierten Bereichen wie Mathematik oder Reasoning aufholen.
  Ich frage mich, ob jemand es auch mit komplexer Logik oder Coding-bezogenen Tests ausprobiert hat. Modelle mit starker Mathematikleistung sind oft auch gut beim Debugging oder bei der Algorithmusgenerierung.

  • Dass auf bestimmte Domänen spezialisierte Modelle aufholen, ist ein natürlicher Effekt, weil ihr kommerzieller Wert geringer ist und das Training großer LLMs eher Allgemeingültigkeit bevorzugt.
  • kimi-k2 ist fürs Coding ziemlich ordentlich, erreicht aber nicht das Niveau der SOTA-Modelle von Anthropic, OpenAI oder Google.

• Ich denke, gegenüber den Ergebnissen dieses Modells ist auch eine skeptische Sichtweise nötig.
  Es wurde ausdrücklich erwähnt, dass Probleme, die aus dem Internet gesammelt wurden, direkt zum Training verwendet wurden, aber es wurde nicht gesagt, ob eine Bereinigung von Benchmark-Kontamination stattgefunden hat oder ob Probleme aus 2024/2025 ausgeschlossen wurden.
  OpenAI und Google haben ihre experimentellen Modelle getestet, ohne vorab Zugang zu den Aufgaben von 2025 zu haben.

• Ich frage mich, warum OpenAIs Goldmedaillen-Modell noch nicht veröffentlicht wurde.

  • Das war einfach nur Werbung. Die dort gewonnenen Erkenntnisse sollen im nächsten allgemeinen Modell berücksichtigt werden.

• Wichtig ist, dass dieses Modell kein allgemeines Modell ist. Die Modelle von Google und OpenAI waren allgemeine Modelle.

  • Tatsächlich haben sowohl OpenAI als auch Google für die IMO spezialisierte Forschungsmodelle verwendet.
    • OpenAI kündigte in diesem Tweet die Veröffentlichung von GPT-5 an und erklärte, dass das IMO-Modell experimentell sei und vorerst nicht veröffentlicht werden solle.
    • DeepMind erklärt im offiziellen Blog, dass Gemini mit RL-basiertem mehrstufigem Reasoning und Theorem-Proving-Daten trainiert wurde.
  • Auch DeepSeeks offizieller Post wurde dazu geteilt.

• Ich frage mich, wie man so ein Modell zu Hause laufen lassen könnte.
  Die Frage ist, ob das CPU-basiert mit etwa 1 TB RAM möglich wäre.

  • Allein die Download-Daten sind 690 GB groß, daher dürfte wohl 1 TB RAM nötig sein. Selbst mit meinen zwei Strix-Halo-Maschinen ist das nicht möglich.
  • Mit ik_llama.cpp, genug RAM und einer einzelnen GPU lässt es sich zumindest langsam ausführen. Normales llama.cpp geht auch, aber der ik-Fork ist effizienter.
  • Es soll sogar mit zwei per Thunderbolt 5 verbundenen Mac Studio mit je 512 GB möglich sein.

• Ich vermute, dass dieses Modell vielleicht direkt aus den Outputs von OpenAI oder Google destilliert wurde.

• Ich frage mich, ob geplant ist, dieses Modell bei OpenRouter bereitzustellen.

• Wenn OpenAI Werbung in ChatGPT einbaut, würden die Leute dann nicht sofort zu anderen Modellen wechseln?

  • Ich fände es eher wünschenswert, wenn mehrere Anbieter allgemeine Modelle im Wettbewerb zum Marktpreis anbieten würden.
  • Unabhängig von Werbung vertraue ich OpenAI nicht. Bevor sie ihren Namen nicht in CloseAI ändern, fällt es mir schwer, ihnen zu glauben.
  • ChatGPT ist einfach nur eine Website. Dass Websites Werbung enthalten, ist nichts Ungewöhnliches. Bei Instagram ist es genauso.
  • Über GPU-Rechenzentren und APIs haben sie bereits ein funktionierendes Geschäftsmodell. Selbst wenn Konkurrenz entsteht, werden sie wohl vorerst die erste Wahl bleiben.
  • Google hat jahrzehntelang Werbung geschaltet, und trotzdem ist kaum jemand zu einer anderen Suchmaschine gewechselt.