模型介绍
中文整理模型用途
DeepSeek-Prover-V2 是一个开源大语言模型，专门用于在 Lean 4 环境中进行形式化定理证明。
主要能力
该模型通过递归定理证明流程收集初始化数据。冷启动训练程序首先引导 DeepSeek-V3 将复杂问题分解为一系列子目标，然后将已解决子目标的证明与 DeepSeek-V3 的逐步推理结合，形成冷启动推理数据。模型整合了非形式化和形式化数学推理，并通过强化学习进一步增强连接非形式化推理与形式化证明构建的能力。
在性能方面，DeepSeek-Prover-V2-671B 在 MiniF2F-test 上达到 88.9% 的通过率，并在 PutnamBench 的 658 个问题中成功解决 49 个。
输入输出
输入：数学问题或定理
输出：Lean 4 形式化证明
运行要求
模型提供两个版本：7B 参数版本和 671B 参数版本。7B 版本基于 DeepSeek-Prover-V1.5-Base，扩展上下文长度达 32K tokens。671B 版本基于 DeepSeek-V3-Base 训练。
基本用法
可直接使用 Huggingface Transformers 进行模型推理。671B 版本与 DeepSeek-V3 共享相同架构。
限制
模型性能受限于问题的复杂度和形式化证明的难度。
许可证
DeepSeek-Prover-V2 模型的使用受模型许可证约束。
优先采用原作者提供的中文模型卡片；仅有英文说明时由闲社AI翻译整理。重要参数、许可证和商用范围请以原文为准。
你将获得什么
完整仓库方式包含该固定版本中的权重、配置、分词器及说明文件；指定版本方式只下载所选文件或整组分片。多模态模型的投影文件、配置等依赖，请按作者说明配齐。
完整仓库可能包含多个权重格式，因此需要的磁盘空间可能大于单一格式的模型大小。下载文件不等于完成模型部署。
使用前须知
运行模型需要的设备、工具与依赖，以原作者说明为准。
是否允许商用、修改和分发，请查看模型许可证。
闲社提供资料与镜像下载方法，不代表已运行模型或完成安全审计。下载的代码应先检查，再执行。
资料或下载有问题？
登录后可提交反馈。