DeepSeek-Prover-V2: The New Standard for Automatic Proofing in Formal Mathematics | Llm examples | Quick start guide to large language models pdf github | Generative ai with large language models coursera | Turtles AI

DeepSeek-Prover-V2 is an advanced open source model for automatic formal proofs in Lean 4. It combines problem decomposition, informal reasoning, and reinforcement learning, achieving excellent results on standard mathematical benchmarks and competition problems.

Key Points:

• Recursive Proof Approach: Uses DeepSeek-V3 to decompose theorems into sub-goals, facilitating step-by-step proof generation.
• Formal-Informal Integration: Combines informal thought chains with formalized proofs in Lean 4, bridging natural reasoning and symbolic logic.
• Record-Breaking Performance: DeepSeek-Prover-V2-671B achieves an 88.9% success rate on MiniF2F and solves 49 problems from PutnamBench.
• ProverBench Benchmark: Introduces a new dataset with 325 formalized problems, including exercises from AIME competitions and textbooks, broadening the scope of evaluation.

DeepSeek-Prover-V2 represents a significant step forward in automating formal theorem proving by integrating informal and formal mathematical reasoning through a large open-source language model designed for Lean 4. Developed by the DeepSeek team, the model was trained using a recursive proof pipeline based on DeepSeek-V3, which breaks down complex problems into sub-goals, synthesizing the proofs of the solved sub-goals in a thought chain process. This methodology created a cold-start dataset for reinforcement learning, improving the model’s ability to connect informal reasoning with formal proof construction. The resulting DeepSeek-Prover-V2-671B achieved state-of-the-art performance in neural theorem proving, with an 88.9% success rate in the MiniF2F test and solving 49 out of 658 problems from PutnamBench. Furthermore, ProverBench was introduced, a benchmark composed of 325 formalized problems, including 15 problems selected from recent AIME competitions (years 24-25), of which the model successfully solved 6, highlighting the reduction of the gap between formal and informal mathematical reasoning in large language models.

DeepSeek-Prover-V2 demonstrates how the synergic integration of natural language, formal logic and deep learning techniques can open new perspectives in the automation of mathematical reasoning.