DeepSeek veröffentlicht DeepSeek-Prover-V2-671B: Next-Generation-Modell für automatisches Theorembeweisen mit 671B-MoE-Architektur 60

小编 · 2025-04-30

DeepSeek AI hat am 30. April 2025 DeepSeek-Prover-V2-671B veröffentlicht – ein Next-Generation-Modell für automatisches Theorembeweisen mit 671B-MoE-Architektur, das Beweise im Lean-4-Framework generiert und verifiziert. Zu den Vorteilen zählen die Skalierung formaler Mathematik auf GPT-4-Niveau, Effizienzgewinne durch MoE sowie Open Source mit kommerzieller Nutzung. Im Vergleich zu V1.5 wurden Parameterzahl, Kontextlänge und Pass Rate deutlich verbessert

DeepSeek veröffentlicht DeepSeek-Prover-V2-671B: Next-Generation-Modell für automatisches Theorembeweisen mit 671B-MoE-Architektur

DeepSeek ai veröffentlichte am 30. April 2025 DeepSeek-Prover-V2-671B, ein automatischen Theorembeweiser der nächsten Generation, der auf einer MoE-Architektur mit 671 Milliarden Parametern basiert und Beweise innerhalb des Lean 4-Frameworks generiert und verifiziert. Zu seinen Vorteilen gehören die Skalierung formaler Mathematik auf das Niveau „GPT-4", die durch MoE erzielten Effizienzsteigerungen sowie die Open-Source-Verfügbarkeit mit kommerzieller Nutzungserlaubnis. Im Vergleich zur Version V1.5 weist es deutliche Verbesserungen bei der Parameteranzahl, der Kontextlänge und der Bestehensquote auf. Es wird erwartet, dass es in Benchmark-Tests wie miniF2F hervorragend abschneidet und in Bereichen wie formaler Verifikation und Beschleunigung der mathematischen Forschung eingesetzt werden kann. Für die Nutzung müssen die Gewichte von Hugging Face heruntergeladen und die entsprechenden Einstellungen vorgenommen werden.

DeepSeek发布DeepSeek-Prover-V2-671B：基于6710亿参数MoE架构的下一代自动定理证明模型.webp

Technische Merkmale

Parameteranzahl und Architektur: Das Modell verfügt über insgesamt 671 Milliarden Parameter und verwendet eine MoE-Architektur, wobei pro Token etwa 37 Milliarden Parameter aktiviert werden. Diese Architektur reduziert den Speicherbedarf erheblich und behält gleichzeitig eine starke Schlussfolgerungsfähigkeit bei.
Kontextlänge: Unterstützt einen extrem langen Kontext mit einer maximalen Positions-Einbettung von 163.840, was die Verarbeitung komplexer mathematischer Beweise ermöglicht.
Rechengenauigkeit: Unterstützt mehrere Rechengenauigkeiten wie BF16, FP8 und F32, was ein schnelleres und ressourcenschonenderes Training und Deployment des Modells ermöglicht.
Dateiformat: Verwendet das effizientere safetensors-Dateiformat.
Quantisierungstechnik: Verwendet FP8-Quantisierung, um die Modellgröße durch Quantisierungstechniken zu reduzieren und die Inferenz-Effizienz zu steigern.

技术特点.webp

Wesentliche Vorteile

Skalierung und Komplexität: Die enorme Parameteranzahl und das lange Kontextfenster (ca. 128k Tokens) ermöglichen die Verarbeitung längerer und komplexerer Beweislogikketten in der Mathematik.
Effizienzoptimierung: Durch die MoE-Architektur werden der Speicherbedarf und die Inferenzgeschwindigkeit im Vergleich zu einem vollständig verbundenen Modell mit 671 Milliarden Parametern deutlich verbessert.
Open Source und Lizenzierung: Das Modell ist Open Source, die Gewichte sind auf Hugging Face verfügbar und eine kommerzielle Nutzung wird voraussichtlich erlaubt sein.

Anwendungsszenarien

Formale Verifikation: Strenge Überprüfung von Sicherheitsbeweisen in der Kryptographie oder Korrektheitsbeweisen im Chip-Design.
Beschleunigung der mathematischen Forschung: Unterstützung von Mathematikern bei der Formalisierung bestehender Theoreme, der Erforschung neuer Vermutungen und der Lösung mathematischer Probleme auf Olympiade-Niveau.
Fortgeschrittenes Bildungswerkzeug: Erstellung interaktiver Tutoring-Systeme, die Studierende durch formale Beweise führen.
Sicherheitskritische Systeme: Verifikation kritischer Software-Eigenschaften und Invarianten vor der Code-Bereitstellung durch Lean-Integration.

Schnellstart-Schritte

Modell beziehen: Gewichte von Hugging Face herunterladen: deepseek-ai/DeepSeek-Prover-V2-671B.
Lean einrichten: Lean 4 (empfohlen ≥ Version 4.5) und die mathlib4-Bibliothek installieren.
Hardware überprüfen: Sicherstellen, dass die Hardwarekonfiguration die Mindestanforderungen erfüllt (empfohlen wird eine Hochleistungskonfiguration).
Inferenz-Engine installieren: Einrichten, z. B. vLLM oder ein anderes MoE-kompatibles Framework.
Beispiele erkunden: Bewertungsskripte oder Beispiel-Notebooks im Modell-Repository prüfen.

Häufig gestellte Fragen

Ist es Open Source? Kann es kommerziell genutzt werden?

Ja, DeepSeek-Prover-V2-671B ist Open Source (Gewichte sind auf Hugging Face verfügbar) und die Lizenz wird voraussichtlich sowohl akademische als auch kommerzielle Nutzung erlauben.

Kann es auf einer NVIDIA 4090 ausgeführt werden?

Ersten Berichten zufolge kann das Modell dank Optimierungen wie MoE, MLA und Quantisierung auf einer einzelnen NVIDIA 4090 GPU betrieben werden, insbesondere in Kombination mit ausreichend RAM und einer schnellen NVMe-SSD für dynamisches Laden. Die Leistung variiert je nach konkreter Konfiguration.