Am Maifeiertag hat DeepSeek wieder einmal eine wichtige Nachricht für die KI-Branche gebracht - die Freigabe des neuen Modells DeepSeek-Prover-V2. Trotz der jüngsten Gerüchte, die im Internet über die bevorstehende Veröffentlichung von DeepSeek-R2 kursierten, hat DeepSeek dieses leistungsstarke Modell, das sich auf das mathematische Theorem-Proving konzentriert, veröffentlicht und bleibt dabei seinem üblichen Open-Source-Geist treu.

Zwei leistungsstarke Modelle synchronisiert mit Open Source

Diesmal hat DeepSeek zwei Versionen des Modells DeepSeek-Prover-V2 als Open Source zur Verfügung gestellt.

• DeepSeek-Prover-V2-671BBasierend auf DeepSeek-V3-Base, mit 671 Milliarden Parametern, ist es derzeit der König der Theorembeweise.
• DeepSeek-Prüfer-V2-7BBasierend auf DeepSeek-Prover-V1.5-Base, mit 7 Milliarden Parametern, unterstützt Kontextlängen bis zu 32K Token

Beide Modelle sind offiziell auf Hugging Face veröffentlicht worden:

• DeepSeek-Prover-V2-7B. https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-7B
• DeepSeek-Prover-V2-671B. https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B

Was ist DeepSeek-Prover-V2?

DeepSeek-Prover-V2 ist ein Open-Source-Großsprachenmodell für die "mathematische KI-Programmiersprache" Lean 4, das sich auf das formale Beweisen von Theoremen konzentriert. Einfach ausgedrückt, kann es abstrakte mathematische Theoreme in rigorose, computerüberprüfbare Beweise umwandeln und stellt damit ein revolutionäres Werkzeug für die mathematische Forschung dar.

Sein bestes Merkmal ist die Fähigkeit, nicht-formales mathematisches Denken (d.h. das, was Menschen üblicherweise verwenden) mit rigorosen formalen Beweisen nahtlos zu kombinieren, was es dem Modell ermöglicht, so flexibel wie ein Mensch zu denken und so rigoros wie ein Computer zu argumentieren und eine integrierte Mischung aus mathematischem Denken zu erreichen.

Erstaunliche Leistung: viele Rekorde aufgestellt

DeepSeek-Prover-V2-671B zeigt eine beispiellose Stärke in verschiedenen Benchmarks des Theorembeweisens:

• Mit 88,9% wurde beim MiniF2F-Test ein neuer Rekordwert erreicht
• Erfolgreich 49 von 658 Fragen im PutnamBench-Datensatz gelöst
• Zeigt auch gute Leistungen bei schwierigen Mathematik-Wettbewerbsaufgaben wie AIME 24 und 25

Viele Internetnutzer testeten das Modell und meinten, es sei sogar besser in der Lage, komplexe mathematische Probleme zu lösen als Spitzenmodelle wie o4-mini von OpenAI und Grok-3 von XAI. Einige Schüler, die sich in die Mathematik-Olympiade vertieft haben, riefen aus: "Die Olympiade war noch nie so einfach!"

Technologische Innovation: Kombination von rekursivem und verstärktem Lernen

In dem technischen Bericht stellt das DeepSeek-Team die zentrale Trainingsmethodik von Prover-V2 vor, die auf einer innovativen Kombination aus rekursivem und verstärktem Lernen basiert. Der Trainingsprozess für das Modell ist in mehrere Schlüsselschritte unterteilt:

1. rekursive Beweissuche durch Zerlegung von Teilzielen

DeepSeek-Prover-V2 verwendet eine ähnliche Denkweise wie ein menschlicher Mathematiker - er zerlegt komplexe Theoreme in eine Reihe kleinerer Lemmata, die zu beweisen sind. Der spezifische Implementierungsprozess umfasst:

• DeepSeek-V3 wird zunächst aufgefordert, Beweisskizzen in natürlicher Sprache zu erstellen und diese als Theoremaussagen in Lean-Sprache zu formalisieren
• Die zerlegten Teilziele werden dann unter Verwendung des 7B-Beweismodells rekursiv gelöst
• Schließlich werden die Beweise für diese Teilziele kombiniert, um einen vollständigen formalen Beweis für das ursprüngliche komplexe Problem zu erstellen

Dieser Ansatz verbessert nicht nur die Effizienz des Nachweises, sondern erweitert auch die Bandbreite der Theoreme, die das Modell behandeln kann.

2. die Harmonisierung nicht-formaler Argumentation mit formalen Beweisen

Das DeepSeek-Team hat auf geschickte Weise hochrangige natürlichsprachliche Schlussfolgerungen mit exakten Beweisverfahren auf niedriger Ebene kombiniert:

• Wählen Sie Probleme aus, die besonders schwierig zu lösen sind, und unterteilen Sie sie in kleinere Ziele
• Wenn die Mini-Ziele jeweils bewiesen sind, werden sie zu einem vollständigen rigorosen Beweis kombiniert
• Fügen Sie diesen vollständigen Beweis der von DeepSeek-V3 generierten "Gedankenkette" hinzu und erstellen Sie so Trainingsdaten, die menschliches Denken und maschinelle Überprüfung kombinieren.

Auf diese Weise sammelte das Team Hunderte von hochwertigen Trainingsdaten, die eine solide Lerngrundlage für das Modell bildeten.

3. verstärktes Lernen zur Verbesserung der Argumentationsfähigkeit

Nach einer ersten Feinabstimmung führte das Team den Verstärkungslernalgorithmus Group Relative Policy Optimization (GRPO) ein:

• Stichprobenartige Auswahl mehrerer Beweise für jede Frage und Optimierung der Strategie durch relative Belohnungen
• Verwenden Sie einen binären Belohnungsmechanismus: Lean erhält die Punktzahl 1 für eine erfolgreiche Überprüfung und 0 für einen Misserfolg.
• Der strukturelle Konsistenzbonus soll sicherstellen, dass die modellgenerierten Beweise mit den Ideen der Gedankenkettenzerlegung konsistent sind

Diese Trainingsmethode verbessert die Genauigkeit des Modells beim komplexen Theorembeweisen erheblich.

ProverBench: eine neue Reihe von Mathe-Benchmarks

Zusätzlich zum Modell selbst hat DeepSeek ProverBench veröffentlicht - einen Benchmark-Datensatz mit 325 Fragen:

• 15 Fragen zur Zahlentheorie und Algebra aus den letzten Mathematikwettbewerben wie AIME 24 und 25
• 310 Fragen aus Lehrbuchbeispielen und Tutorien, die ein breites Spektrum an Schwierigkeitsgraden und Bereichen abdecken.

Dieser Datensatz soll eine umfassende Bewertung von Modellen sowohl auf der Ebene von Schülerwettbewerben als auch auf der Ebene von Mathematikstudenten ermöglichen und eine systematischere Testplattform für die KI-Forschung in der Mathematik bieten.

ProverBench Link:https://huggingface.co/datasets/deepseek-ai/DeepSeek-ProverBench

Experimentelle Ergebnisse und hervorgehobene Befunde

Im Verlauf der Studie entdeckte das Team mehrere interessante Phänomene:

CoT vs. Nicht-CoT-Modelle

DeepSeek-Prover-V2 unterstützt zwei komplementäre Modi der Beweiserzeugung:

• Hocheffizientes Non-CoT-Modell (Non-Chain of Thought)Schnelles Generieren von schlankem Lean-Code ohne zwischengeschaltete Inferenzschritte
• Hochpräzises Modell der Gedankenkette (CoT): systematische Darstellung des Argumentationsprozesses und schrittweiser Aufbau von logisch klaren Beweisen

Experimente zeigen einen signifikanten Leistungsvorteil des CoT-Modells gegenüber dem Nicht-CoT-Modell beim formalen mathematischen Schlussfolgern, was die Wirksamkeit der Denkkette im Bereich des Theorembeweisens bestätigt.

Unerwartete Fähigkeiten von kleinen Modellen

Überraschenderweise übertraf DeepSeek-Prover-V2-7B bei Verwendung des Nicht-CoT-Modells im PutnamBench-Datensatz die Erwartungen. Es löste sogar 13 Fragen, die das 671B-Modell nicht lösen konnte!

Die Analyse ergab, dass das 7B-Modell eine einzigartige Technik erworben hat - die häufige Verwendung von Cardinal.toNat und Cardinal.natCast_inj für Probleme mit endlichen Basen - die im 671B-Modell selten ist. Dieses Ergebnis deutet darauf hin, dass das Verstärkungslernen nicht nur die Gesamtleistung verbessert, sondern es dem Modell auch ermöglicht, spezielle Problemlösungstechniken zu entwickeln.

Schnellstart-Anleitung

Möchten Sie DeepSeek-Prover-V2 ausprobieren? Hier ist ein einfaches Beispiel, das zeigt, wie man die Transformers-Bibliothek von Hugging Face für die Modellinferenz verwendet:

from transformers import AutoModelForCausalLM, AutoTokenizer
importieren Fackel

torch.manual_seed(30)
model_id = "deepseek-ai/DeepSeek-Prover-V2-7B" # oder deepseek-ai/DeepSeek-Prover-V2-671B
tokenizer = AutoTokenizer.from_pretrained(model_id)

formal_statement = """
importieren Mathlib
importieren Aesop
set_option maxHeartbeats 0
open BigOperators Real Nat Topology Rat
/-- Wie groß ist die positive Differenz zwischen $120\%$ von 30 und $130\%$ von 20? Zeigen Sie, dass sie 10 ist.-/
theorem mathd_algebra_10 : abs ((120 : ℝ) / 100 * 30 - 130 / 100 * 20) = 10 := durch
    sorry
""".strip()

prompt = """
Vervollständigen Sie den folgenden Lean4-Code.
 ``Lean4
{}

Zukunftsaussichten

Das DeepSeek-Team sagt, dass sich die zukünftige Arbeit auf die Erweiterung dieses Rahmens auf AlphaProof-ähnliche Systeme konzentrieren wird. Das ultimative Ziel ist es, mathematische Rätsel auf IMO-Ebene zu lösen, die die Spitze des automatisierten Theorembeweisens darstellen. Mit der Veröffentlichung von DeepSeek-Prover-V2 werden wir möglicherweise Zeuge einer großen Veränderung in der Art und Weise, wie Mathematik studiert wird. Dieses Modell ist mehr als nur ein technologischer Fortschritt, es stellt ein neues Paradigma für die Zusammenarbeit von Menschen und KI bei der Lösung komplexer Probleme dar.

Inzwischen ist die Vorfreude auf DeepSeek-R2 noch größer geworden. Wie ein Netizen sagte: "Klopf, klopf, dieser kleine Blauwal, wann zum Teufel wird R2 rausgeschickt!"

Wenn Sie GPT Plus, Claude Pro, Grok Super offizielles bezahltes exklusives Konto benutzen wollen, können Sie unser professionelles Team (wx: abch891) kontaktieren, wenn Sie nicht wissen, wie Sie Ihr Konto aufladen können.