DeepSeek Releases DeepSeek-Prover-V2-671B: Next-Gen Auto-Theorem-Proving Model with 671B MoE Parameters 63

小编 · 2025-04-30

DeepSeek AI released DeepSeek-Prover-V2-671B on April 30, 2025—a next-gen auto-theorem-proving model with a 671B-parameter MoE architecture that generates and verifies proofs within the Lean 4 framework. Its advantages include bringing formal math to GPT-4-level scale, efficiency gains from MoE, open-source with commercial use allowed. Compared to V1.5, it delivers significant improvements in parameter count, context length, and pass rate, and is expected to drive advances in math

DeepSeek Releases DeepSeek-Prover-V2-671B: Next-Gen Auto-Theorem-Proving Model with 671B MoE Parameters

DeepSeek ai released DeepSeek-Prover-V2-671B on April 30, 2025. It is a next-generation automated theorem proving model based on a 671-billion-parameter MoE architecture, designed to generate and verify proofs within the Lean 4 framework. Its advantages include elevating formal mathematics to a "GPT-4 level" of scale, efficiency gains from the MoE architecture, and being open-source with commercial use permitted. Compared with version V1.5, it shows significant improvements in parameter count, context length, pass rate, and other aspects. It is expected to perform excellently on benchmarks such as miniF2F and can be used in fields like formal verification and accelerating mathematical research. To use it, weights need to be downloaded from Hugging Face and the relevant setup completed.

DeepSeek releases DeepSeek-Prover-V2-671B: A next-generation automated theorem proving model based on a 671-billion-parameter MoE architecture.webp

Technical Features

Parameter Count and Architecture: The model has a total of 671 billion parameters and adopts an MoE architecture, activating approximately 37 billion parameters per token. This architecture significantly reduces memory requirements while maintaining powerful reasoning capabilities.
Context Length: Supports ultra-long context, with a maximum position embedding of 163,840, capable of handling complex mathematical proofs.
Computational Precision: Supports multiple computational precisions such as BF16, FP8, and F32, facilitating faster and more resource-efficient training and deployment.
File Format: Uses the more efficient safetensors file format.
Quantization Technology: Adopts FP8 quantization, reducing model size and improving inference efficiency through quantization techniques.

Technical Features.webp

Key Advantages

Scale and Complexity: With its massive parameter count and long context window (approximately 128k tokens), it can handle longer and more complex logical chains in mathematical proofs.
Efficiency Optimization: The MoE architecture significantly reduces memory requirements and improves inference speed compared to a fully connected 671-billion-parameter model.
Open Source and Licensing: The model is open-source, with weights available on Hugging Face, and is expected to permit commercial use.

Application Scenarios

Formal Verification: Conducting rigorous checks in cryptographic security proofs or chip design correctness proofs.
Accelerating Mathematical Research: Helping mathematicians formalize existing theorems, explore new conjectures, and solve Olympiad-level mathematical problems.
Advanced Education Tools: Creating interactive tutoring systems that guide students through formal proofs.
Safety-Critical Systems: Verifying critical software properties and invariants through Lean integration before code deployment.

Quick Start Steps

Obtain the Model: Download weights from Hugging Face: deepseek-ai/DeepSeek-Prover-V2-671B.
Set Up Lean: Install Lean 4 (recommended version ≥ 4.5) and the mathlib4 library.
Verify Hardware: Ensure that the hardware configuration meets the minimum requirements (a high-performance configuration is recommended).
Install Inference Engine: Set up an inference engine such as vLLM or other MoE-compatible frameworks.
Explore Examples: Check the evaluation scripts or example notebooks in the model repository.

Frequently Asked Questions

Is it open-source? Can it be used for commercial purposes?

Yes, DeepSeek-Prover-V2-671B is open-source (weights are available on Hugging Face), and its license is expected to permit both academic and commercial use.

Can it run on an NVIDIA 4090?

Initial reports indicate that, thanks to optimizations such as MoE, MLA, and quantization, the model can run on a single NVIDIA 4090 GPU, especially when paired with sufficient RAM and a fast NVMe SSD for dynamic loading. Performance will vary depending on the specific configuration.