unsloth/deepseek-prover-v2-671b-gguf overview

{
  "metadata": {},
  "card_data": {
    "base_model": "deepseek-ai/DeepSeek-Prover-V2-671B",
    "language": [
      "en"
    ],
    "library_name": "transformers",
    "tags": [
      "deepseek",
      "unsloth",
      "transformers"
    ],
    "license": "mit",
    "frontmatter": {
      "base_model": "deepseek-ai/DeepSeek-Prover-V2-671B",
      "language": [
        "en"
      ],
      "library_name": "transformers",
      "tags": [
        "deepseek",
        "unsloth",
        "transformers"
      ],
      "license": "mit"
    },
    "hero_image_url": "https://github.com/deepseek-ai/DeepSeek-V2/blob/main/figures/logo.svg?raw=true",
    "summary": "",
    "quick_links": [],
    "benchmark_table_html": "",
    "readme_markdown": "---\nbase_model: deepseek-ai/DeepSeek-Prover-V2-671B\nlanguage:\n- en\nlibrary_name: transformers\ntags:\n- deepseek\n- unsloth\n- transformers\nlicense: mit\n---\n<p style=\"margin-top: 0;\">\n    <strong><a href=\"https://docs.unsloth.ai/basics/unsloth-dynamic-v2.0-gguf\">Unsloth Dynamic 2.0</a> achieves superior accuracy & outperforms other leading quants.</strong>\n  </p>\n  \n# deepseek-ai/DeepSeek-Prover-V2-671B\n\n<div align=\"center\">\n  <img src=\"https://github.com/deepseek-ai/DeepSeek-V2/blob/main/figures/logo.svg?raw=true\" width=\"60%\" alt=\"DeepSeek-V3\" />\n</div>\n<hr>\n<div align=\"center\" style=\"line-height: 1;\">\n  <a href=\"https://www.deepseek.com/\" target=\"_blank\" style=\"margin: 2px;\">\n    <img alt=\"Homepage\" src=\"https://github.com/deepseek-ai/DeepSeek-V2/blob/main/figures/badge.svg?raw=true\" style=\"display: inline-block; vertical-align: middle;\"/>\n  </a>\n  <a href=\"https://chat.deepseek.com/\" target=\"_blank\" style=\"margin: 2px;\">\n    <img alt=\"Chat\" src=\"https://img.shields.io/badge/🤖%20Chat-DeepSeek%20V3-536af5?color=536af5&logoColor=white\" style=\"display: inline-block; vertical-align: middle;\"/>\n  </a>\n  <a href=\"https://huggingface.co/deepseek-ai\" target=\"_blank\" style=\"margin: 2px;\">\n    <img alt=\"Hugging Face\" src=\"https://img.shields.io/badge/%F0%9F%A4%97%20Hugging%20Face-DeepSeek%20AI-ffc107?color=ffc107&logoColor=white\" style=\"display: inline-block; vertical-align: middle;\"/>\n  </a>\n</div>\n\n<div align=\"center\" style=\"line-height: 1;\">\n  <a href=\"https://discord.gg/Tc7c45Zzu5\" target=\"_blank\" style=\"margin: 2px;\">\n    <img alt=\"Discord\" src=\"https://img.shields.io/badge/Discord-DeepSeek%20AI-7289da?logo=discord&logoColor=white&color=7289da\" style=\"display: inline-block; vertical-align: middle;\"/>\n  </a>\n  <a href=\"https://github.com/deepseek-ai/DeepSeek-V2/blob/main/figures/qr.jpeg?raw=true\" target=\"_blank\" style=\"margin: 2px;\">\n    <img alt=\"Wechat\" src=\"https://img.shields.io/badge/WeChat-DeepSeek%20AI-brightgreen?logo=wechat&logoColor=white\" style=\"display: inline-block; vertical-align: middle;\"/>\n  </a>\n  <a href=\"https://twitter.com/deepseek_ai\" target=\"_blank\" style=\"margin: 2px;\">\n    <img alt=\"Twitter Follow\" src=\"https://img.shields.io/badge/Twitter-deepseek_ai-white?logo=x&logoColor=white\" style=\"display: inline-block; vertical-align: middle;\"/>\n  </a>\n</div>\n\n<div align=\"center\" style=\"line-height: 1;\">\n  <a href=\"https://github.com/deepseek-ai/DeepSeek-V3/blob/main/LICENSE-CODE\" style=\"margin: 2px;\">\n    <img alt=\"Code License\" src=\"https://img.shields.io/badge/Code_License-MIT-f5de53?&color=f5de53\" style=\"display: inline-block; vertical-align: middle;\"/>\n  </a>\n  <a href=\"https://github.com/deepseek-ai/DeepSeek-V3/blob/main/LICENSE-MODEL\" style=\"margin: 2px;\">\n    <img alt=\"Model License\" src=\"https://img.shields.io/badge/Model_License-Model_Agreement-f5de53?&color=f5de53\" style=\"display: inline-block; vertical-align: middle;\"/>\n  </a>\n</div>\n\n## 1. Introduction\n\nWe introduce DeepSeek-Prover-V2, an open-source large language model designed for formal theorem proving in Lean 4, with initialization data collected through a recursive theorem proving pipeline powered by DeepSeek-V3. The cold-start training procedure begins by prompting DeepSeek-V3 to decompose complex problems into a series of subgoals. The proofs of resolved subgoals are synthesized into a chain-of-thought process, combined with DeepSeek-V3's step-by-step reasoning, to create an initial cold start for reinforcement learning. This process enables us to integrate both informal and formal mathematical reasoning into a unified model.\n\n<p align=\"center\">\n  <img width=\"100%\" src=\"https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/main/figures/performance.png?raw=true\">\n</p>\n\n## 2. Model Summary\n\n---\n\n**Synthesize Cold-Start Reasoning Data through Recursive Proof Search**\n\n- To construct the cold-start dataset, we develop a simple yet effective pipeline for recursive theorem proving, utilizing DeepSeek-V3 as a unified tool for both subgoal decomposition and formalization. We prompt DeepSeek-V3 to decompose theorems into high-level proof sketches while simultaneously formalizing these proof steps in Lean 4, resulting in a sequence of subgoals.\n\n- We use a smaller 7B model to handle the proof search for each subgoal, thereby reducing the associated computational burden. Once the decomposed steps of a challenging problem are resolved, we pair the complete step-by-step formal proof with the corresponding chain-of-thought from DeepSeek-V3 to create cold-start reasoning data.\n\n---\n\n**Reinforcement Learning with Synthetic Cold-Start Data**\n\n- We curate a subset of challenging problems that remain unsolved by the 7B prover model in an end-to-end manner, but for which all decomposed subgoals have been successfully resolved. By composing the proofs of all subgoals, we construct a complete formal proof for the original problem. This proof is then appended to DeepSeek-V3's chain-of-thought, which outlines the corresponding lemma decomposition, thereby producing a cohesive synthesis of informal reasoning and subsequent formalization.\n\n- After fine-tuning the prover model on the synthetic cold-start data, we perform a reinforcement learning stage to further enhance its ability to bridge informal reasoning with formal proof construction. Following the standard training objective for reasoning models, we use binary correct-or-incorrect feedback as the primary form of reward supervision.\n- The resulting model, DeepSeek-Prover-V2-671B, achieves state-of-the-art performance in neural theorem proving, reaching $88.9$% pass ratio on the MiniF2F-test and solving 49 out of 658 problems from PutnamBench. The proofs generated by DeepSeek-Prover-V2 for the miniF2F dataset are available for download as a [ZIP archive](https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/master/minif2f-solutions.zip).\n\n---\n\n## 3. ProverBench: Formalization of AIME and Textbook Problems\n\nwe introduce ProverBench, a benchmark dataset comprising 325 problems. Of these, 15 are formalized from number theory and algebra questions featured in the recent AIME competitions (AIME 24 and 25), offering authentic high-school competition-level challenges. The remaining 310 problems are drawn from curated textbook examples and educational tutorials, contributing a diverse and pedagogically grounded collection of formalized mathematical problems. This benchmark is designed to enable more comprehensive evaluation across both high-school competition problems and undergraduate-level mathematics.\n\n<div align=\"center\">\n\n| Area                | Count |\n| :---------------------: | :-------: |\n| AIME 24&25          | 15    |\n| Number Theory       | 40    |\n| Elementary Algebra  | 30    |\n| Linear Algebra      | 50    |\n| Abstract Algebra    | 40    |\n| Calculus            | 90    |\n| Real Analysis       | 30    |\n| Complex Analysis    | 10    |\n| Functional Analysis | 10    |\n| Probability         | 10    |\n| Total               | 325   |\n\n</div>\n\n## 4. Model & Dataset Downloads\n\nWe release DeepSeek-Prover-V2 in two model sizes: 7B and 671B parameters. DeepSeek-Prover-V2-671B is trained on top of DeepSeek-V3-Base. DeepSeek-Prover-V2-7B is built upon DeepSeek-Prover-V1.5-Base and features an extended context length of up to 32K tokens.\n\n<div align=\"center\">\n\n|            **Model**            |                          **Download**                         |\n| :-----------------------------: | :----------------------------------------------------------: |\n|   DeepSeek-Prover-V2-7B   | [🤗 HuggingFace](https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-7B) |\n|   DeepSeek-Prover-V2-671B   | [🤗 HuggingFace](https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B) |\n\n</div>\n\n<div align=\"center\">\n\n|            **Dataset**            |                          **Download**                         |\n| :-----------------------------: | :----------------------------------------------------------: |\n|   DeepSeek-ProverBench   | [🤗 HuggingFace](https://huggingface.co/datasets/deepseek-ai/DeepSeek-ProverBench) |\n\n</div>\n\n## 5. Quick Start\n\nYou can directly use [Huggingface's Transformers](https://github.com/huggingface/transformers) for model inference. DeepSeek-Prover-V2-671B shares the same architecture as DeepSeek-V3. For detailed information and supported features, please refer to [the DeepSeek-V3 documentation on Hugging Face](https://github.com/huggingface/transformers/blob/main/docs/source/en/model_doc/deepseek_v3.md).\n\nThe following is a basic example of generating a proof for a problem from the miniF2F dataset:\n````python\nfrom transformers import AutoModelForCausalLM, AutoTokenizer\nimport torch\ntorch.manual_seed(30)\n\nmodel_id = \"DeepSeek-Prover-V2-7B\"  # or DeepSeek-Prover-V2-671B\ntokenizer = AutoTokenizer.from_pretrained(model_id)\n\nformal_statement = \"\"\"\nimport Mathlib\nimport Aesop\n\nset_option maxHeartbeats 0\n\nopen BigOperators Real Nat Topology Rat\n\n/-- What is the positive difference between $120\\%$ of 30 and $130\\%$ of 20? Show that it is 10.-/\ntheorem mathd_algebra_10 : abs ((120 : ℝ) / 100 * 30 - 130 / 100 * 20) = 10 := by\n  sorry\n\"\"\".strip()\n\nprompt = \"\"\"\nComplete the following Lean 4 code:\n\n```lean4\n{}\n```\n\nBefore producing the Lean 4 code to formally prove the given theorem, provide a detailed proof plan outlining the main proof steps and strategies.\nThe plan should highlight key ideas, intermediate lemmas, and proof structures that will guide the construction of the final formal proof.\n\"\"\".strip()\n\nchat = [\n  {\"role\": \"user\", \"content\": prompt.format(formal_statement)},\n]\n\nmodel = AutoModelForCausalLM.from_pretrained(model_id, device_map=\"auto\", torch_dtype=torch.bfloat16, trust_remote_code=True)\ninputs = tokenizer.apply_chat_template(chat, tokenize=True, add_generation_prompt=True, return_tensors=\"pt\").to(model.device)\n\nimport time\nstart = time.time()\noutputs = model.generate(inputs, max_new_tokens=8192)\nprint(tokenizer.batch_decode(outputs))\nprint(time.time() - start)\n````\n\n## 6. License\nThe use of DeepSeek-Prover-V2 models is subject to [the Model License](LICENSE-MODEL).\n\n## 7. Contact\n\nIf you have any questions, please raise an issue or contact us at [service@deepseek.com](mailto:service@deepseek.com).",
    "related_quantizations": []
  },
  "tags": [
    "transformers",
    "gguf",
    "deepseek_v3",
    "text-generation",
    "deepseek",
    "unsloth",
    "custom_code",
    "en",
    "base_model:deepseek-ai/DeepSeek-Prover-V2-671B",
    "base_model:quantized:deepseek-ai/DeepSeek-Prover-V2-671B",
    "license:mit",
    "endpoints_compatible",
    "fp8",
    "region:us",
    "conversational"
  ],
  "likes": 8,
  "downloads": 2088,
  "gated": false,
  "private": false,
  "last_modified": "2025-05-27T23:08:35.000Z",
  "created_at": "2025-05-01T07:54:27.000Z",
  "pipeline_tag": "text-generation",
  "library_name": "transformers"
}

{
  "_id": "681328b3060494e99e5e4db8",
  "id": "unsloth/DeepSeek-Prover-V2-671B-GGUF",
  "modelId": "unsloth/DeepSeek-Prover-V2-671B-GGUF",
  "sha": "112021e6465fdaaf10a051ea79caefe82bb8eb31",
  "createdAt": "2025-05-01T07:54:27.000Z",
  "lastModified": "2025-05-27T23:08:35.000Z",
  "author": "unsloth",
  "downloads": 2088,
  "likes": 8,
  "gated": false,
  "private": false,
  "pipeline_tag": "text-generation",
  "library_name": "transformers",
  "siblings_count": 230
}