DeepSeek-Prover-V2-671B 現已在 Novita AI 上線

什麼是 DeepSeek-Prover 模型系列？
什麼是 DeepSeek-Prover-V2-671B？
如何在 Novita AI 上存取 DeepSeek-Prover-V2-671B
結論

DeepSeek 悄然更新了 Prover——這款專為解決數學證明與定理而設計的 AI 模型。DeepSeek-Prover-V2-671B 模型現已在 Novita AI 的 Model API 平台上線！限時活動期間，所有新用戶均可領取 $10 美元免費額度，立即探索並建置這款最先進的自動定理證明模型。

以下是 DeepSeek-Prover-V2-671B 目前在 Novita AI 的定價：

DeepSeek-Prover-V2-671B：0.7 美元 / 百萬輸入 tokens，2.5 美元 / 百萬輸出 tokens

以前所未有的方式驅動您的數學工作流程、研究與教育工具——只需一個 API 呼叫即可使用這個有史以來最先進的形式定理證明模型。

什麼是 DeepSeek-Prover 模型系列？

DeepSeek-Prover 模型系列是一系列最先進的大型語言模型（LLM），專為解決數學中的自動定理證明挑戰而設計。由 DeepSeek-AI 開發，這些模型特別針對生成、驗證和推理形式數學證明——特別是在 Lean 4 證明助理環境中——進行了優化。

為何要建立 DeepSeek-Prover？

雖然像 GPT-4 這樣的現代 LLM 在數學推理方面表現出色，但由於缺乏高品質、大規模的形式語言訓練數據，它們在形式證明任務上仍顯吃力。DeepSeek-Prover 透過從數學競賽問題自動生成數百萬個合成 Lean 4 證明，並在此獨特數據集上微調模型，解決了這個問題。

DeepSeek-Prover 如何運作？

DeepSeek-Prover 的流程包括：

自動形式化： 使用 LLM 將自然語言數學問題轉換為形式化的 Lean 4 陳述。
品質過濾： 透過模型評分和假設拒絕，過濾邏輯正確且具數學興趣的陳述。
證明生成與驗證： 嘗試證明過濾後的陳述，並僅保留具有正確、可驗證證明的陳述。
迭代訓練： 重複此過程，每次使用新的高品質證明數據進一步改進模型。

透過這種方法，DeepSeek-Prover 系列產生的模型持續進步，並得到全球最大的形式數學證明集合之一的支持。

早期 DeepSeek-Prover 模型的亮點與里程碑

規模： 生成了超過 800 萬個附有證明的形式 Lean 4 陳述。
技術基礎： 基於大型 transformer 模型（如 DeepSeekMath 7B），在大量數學數據上進行預訓練，並在合成證明上進一步微調。
最先進的效能： 在形式定理證明基準（如 miniF2F、FIMO）上取得頂尖成果，超越 GPT-4 和其他專用模型。

什麼是 DeepSeek-Prover-V2-671B？

DeepSeek-Prover-V2-671B 是 DeepSeek-Prover 系列中的旗艦模型。以下是它的與眾不同之處：

大規模參數量： 擁有約 6710 億個參數，是專為形式數學與定理證明設計的最大模型之一。
FP8 精度： DeepSeek-Prover-V2-671B 最初以 FP8（8 位元浮點數）精度訓練並發布，這是一種現代格式，能在保持高效能的同時實現高效運算與更低記憶體使用量的模型服務。
先進能力： 該模型採用最先進的 transformer 架構，支援 BF16、FP8_E4M3 和 F32 等現代張量類型，適合高效能研究與生產環境。
專為定理證明而建： 在大量高品質的合成證明數據上進行訓練，擅長複雜的數學推理與形式化 Lean 4 證明生成。

如何在 Novita AI 上存取 DeepSeek-Prover-V2-671B

在 Novita AI 上開始使用 DeepSeek-Prover-V2-671B 快速、簡單且無風險。感謝推薦計畫，您將獲得 $10 美元免費額度——足以充分探索 DeepSeek-Prover-V2-671B 的強大功能、建立原型，甚至無需預付費用即可啟動您的第一個用例。

使用 Playground（無需編碼）

即時存取： 註冊，領取您的免費額度，立即開始試驗 DeepSeek-Prover-V2-671B 及其他頂尖模型。
互動式 UI： 即時測試提示、思維鏈推理並視覺化結果。
模型比較： 輕鬆在 DeepSeek-Prover-V2-671B、Llama 4、DeepSeek 等模型之間切換，找到最適合您需求的模型。

透過 API 整合（適用於開發者）

使用 Novita AI 的統一 REST API，將 DeepSeek-Prover-V2-671B 無縫連接到您的應用程式、工作流程或聊天機器人——無需管理模型權重或基礎設施。Novita AI 提供多語言 SDK（Python、Node.js、cURL 等）以及為進階用戶提供的進階參數控制。

選項 1：直接 API 整合（Python 範例）

開始使用非常簡單，只需使用下面的程式碼片段：

from openai import OpenAI
  
client = OpenAI(
    base_url="https://api.novita.ai/v3/openai",
    api_key="<YOUR Novita AI API Key>",
)

model = "deepseek/deepseek-prover-v2-671b"
stream = True # or False
max_tokens = 2048
system_content = """Be a helpful assistant"""
temperature = 1
top_p = 1
min_p = 0
top_k = 50
presence_penalty = 0
frequency_penalty = 0
repetition_penalty = 1
response_format = { "type": "text" }

chat_completion_res = client.chat.completions.create(
    model=model,
    messages=[
        {
            "role": "system",
            "content": system_content,
        },
        {
            "role": "user",
            "content": "Hi there!",
        }
    ],
    stream=stream,
    max_tokens=max_tokens,
    temperature=temperature,
    top_p=top_p,
    presence_penalty=presence_penalty,
    frequency_penalty=frequency_penalty,
    response_format=response_format,
    extra_body={
      "top_k": top_k,
      "repetition_penalty": repetition_penalty,
      "min_p": min_p
    }
  )

if stream:
    for chunk in chat_completion_res:
        print(chunk.choices[0].delta.content or "", end="")
else:
    print(chat_completion_res.choices[0].message.content)

主要特色：

統一端點： /v3/openai 支援 OpenAI 的 Chat Completions API 格式。
靈活控制： 調整溫度、top-p、懲罰等參數以獲得客製化結果。
串流與批次： 選擇您偏好的回應模式。

選項 2：使用 OpenAI Agents SDK 的多智能體工作流程

透過將 Novita AI 與 OpenAI Agents SDK 整合，建置進階的多智能體系統：

隨插即用： 在任何 OpenAI Agents 工作流程中使用 Novita AI 的 LLM。
支援移交、路由和工具使用： 設計能夠委派、分流或執行函數的智能體，全部由 Novita AI 的模型提供支援。
Python 整合： 只需將 SDK 指向 Novita 的端點 (https://api.novita.ai/v3/openai) 並使用您的 API 金鑰即可。

在第三方平台上連接 DeepSeek-Prover-V2-671B API

Hugging Face：透過 Novita AI 端點在 Spaces、pipeline 或 Transformers 庫中使用 DeepSeek-Prover-V2-671B。
智能體與編排框架： 透過官方連接器和逐步整合指南，輕鬆將 Novita AI 與合作夥伴平台（如 Continue、AnythingLLM、LangChain、Dify 和 Langflow）連接。
相容 OpenAI 的 API： 享受與專為 OpenAI API 標準設計的工具（如 Cline 和 Cursor）無痛遷移與整合。

結論

DeepSeek-Prover-V2-671B 將世界級的自動定理證明直接帶到您的手中——無論您是研究人員、開發者還是教育工作者。準備好嘗試了嗎？立即在 Novita AI 上註冊，領取您的免費額度，體驗形式數學與 AI 驅動證明生成的未來！

關於 Novita AI

Novita AI 是一個 AI 雲端平台，為開發者提供使用簡單 API 部署 AI 模型的簡便方式，同時也提供價格合理且可靠的 GPU 雲端服務，用於建置和擴展應用。

DeepSeek-Prover-V2-671B 現已在 Novita AI 上線