DeepSeek-Prover-V2-671B 现已登陆 Novita AI

什么是 DeepSeek-Prover 模型系列？
什么是 DeepSeek-Prover-V2-671B？
如何在 Novita AI 上访问 DeepSeek-Prover-V2-671B
结论

DeepSeek 悄然更新了其专为数学证明和定理求解设计的 AI 模型 Prover。DeepSeek-Prover-V2-671B 模型现已上线 Novita AI 的 Model API 平台！限时活动期间，所有新用户均可领取 10 美元免费额度，用于探索和构建基于这一最先进的自动定理证明模型的应用。

以下是 DeepSeek-Prover-V2-671B 在 Novita AI 上的当前定价：

DeepSeek-Prover-V2-671B：0.7 $ / M 输入 Token，2.5 $ / M 输出 Token

用这款有史以来最强大的形式化定理证明模型之一，为你的数学工作流、研究项目和教学工具赋能——现在只需一次 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 和其他顶尖模型进行实验。
交互式界面：测试提示词、思维链推理，并实时可视化结果。
模型对比：轻松在 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 格式。
灵活控制：调整 temperature、top-p、惩罚系数等参数，以获得定制化结果。
流式与批处理：选择你偏好的响应模式。

选项 2：使用 OpenAI Agents SDK 构建多 Agent 工作流

通过将 Novita AI 与 OpenAI Agents SDK 集成，构建高级多 Agent 系统：

即插即用：在任何 OpenAI Agents 工作流中使用 Novita AI 的 LLM。
支持交接、路由和工具使用：设计能够委派任务、分类或运行函数的 Agent，全部由 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。
Agent 和编排框架：通过官方连接器和分步集成指南，轻松将 Novita AI 与 Continue、AnythingLLM、LangChain、Dify 和 Langflow 等合作伙伴平台连接。
兼容 OpenAI API：轻松迁移并集成到 Cline 和 Cursor 等工具中，这些工具专为 OpenAI API 标准设计。

结论

DeepSeek-Prover-V2-671B 将世界级的自动定理证明能力直接带到你手中——无论你是研究人员、开发者还是教育工作者。准备好尝试了吗？立即在 Novita AI 注册，领取你的免费额度，体验形式化数学和 AI 驱动的证明生成的未来！

关于 Novita AI

Novita AI 是一个 AI 云平台，为开发者提供了一种简便的方式，通过我们简单的 API 部署 AI 模型，同时还提供了经济实惠且可靠的 GPU 云用于构建应用。

DeepSeek-Prover-V2-671B 现已登陆 Novita AI