DeeperML

DeepSeek AI has unveiled DeepSeek-Prover-V2, a new open-source large language model (LLM) designed for formal theorem proving within the Lean 4 environment. This model advances the field of neural theorem proving by utilizing a recursive theorem-proving pipeline and leverages DeepSeek-V3 to generate high-quality initialization data. DeepSeek-Prover-V2 has achieved top results on the MiniF2F benchmark, showcasing its state-of-the-art performance in mathematical reasoning. The release includes ProverBench, a new benchmark for evaluating mathematical reasoning capabilities.

DeepSeek-Prover-V2 features a unique cold-start training procedure. The process begins by using the DeepSeek-V3 model to decompose complex mathematical theorems into a series of more manageable subgoals. Simultaneously, DeepSeek-V3 formalizes these high-level proof steps in Lean 4, creating a structured sequence of sub-problems. To handle the computationally intensive proof search for each subgoal, the researchers employed a smaller 7B parameter model. Once all the decomposed steps of a challenging problem are successfully proven, the complete step-by-step formal proof is paired with DeepSeek-V3’s corresponding chain-of-thought reasoning. This allows the model to learn from a synthesized dataset that integrates both informal, high-level mathematical reasoning and rigorous formal proofs, providing a strong cold start for subsequent reinforcement learning.

Building upon the synthetic cold-start data, the DeepSeek team curated a selection of challenging problems that the 7B prover model couldn’t solve end-to-end, but for which all subgoals had been successfully addressed. By combining the formal proofs of these subgoals, a complete proof for the original problem is constructed. This formal proof is then linked with DeepSeek-V3’s chain-of-thought outlining the lemma decomposition, creating a unified training example of informal reasoning followed by formalization. DeepSeek is also challenging the long-held belief of tech CEOs who've argued that exponential AI improvements require ever-increasing computing power. DeepSeek claims to have produced models comparable to OpenAI, but with significantly less compute and cost, questioning the necessity of massive scale for AI advancement.


References :

• Synced: DeepSeek Unveils DeepSeek-Prover-V2: Advancing Neural Theorem Proving with Recursive Proof Search and a New Benchmark
• iai.tv news RSS feed: DeepSeek exposed a fundamental AI scaling myth
• www.marktechpost.com: DeepSeek-AI Released DeepSeek-Prover-V2: An Open-Source Large Language Model Designed for Formal Theorem, Proving through Subgoal Decomposition and Reinforcement Learning
• syncedreview.com: DeepSeek Unveils DeepSeek-Prover-V2: Advancing Neural Theorem Proving with Recursive Proof Search and a New Benchmark
• SiliconANGLE: Xiaomi Corp. today released MiMo-7B, a new family of reasoning models that it claims can outperform OpenAI’s o1-mini at some tasks. The algorithm series is available under an open-source license. Its launch coincides with DeepSeek’s release of an update to Prover, a competing open-source reasoning model.
• MarkTechPost: DeepSeek-AI Released DeepSeek-Prover-V2: An Open-Source Large Language Model Designed for Formal Theorem, Proving through Subgoal Decomposition and Reinforcement Learning
• siliconangle.com: China AI rising: Xiaomi releases new MiMo-7B models as DeepSeek upgrades its Prover math AI
• Second Thoughts: China’s DeepSeek Adds a Weird New Data Point to The AI Race

Classification:

• HashTags: #DeepSeekAI #TheoremProving #OpenSourceAI
• Company: DeepSeek
• Target: AI researchers
• Product: DeepSeek Prover
• Feature: Theorem proving
• Malware: DeepSeek-Prover-V2
• Type: AI
• Severity: Informative