Model details
模型介绍
中文整理Model use case
DeepSeek-Prover-V2 是一个开源大语言模型，专为 Lean 4 形式化定理证明而设计。
主要能力
该模型将非形式化数学推理与形式化证明构建相结合。通过递归定理证明流程收集初始化数据，利用 DeepSeek-V3 进行子目标分解和形式化。在形式化定理证明方面达到先进水平：MiniF2F-test 通过率为 88.9%，在 PutnamBench 的 658 道题目中成功解决 49 道。
输入输出
输入：数学问题或定理
输出：Lean 4 形式化证明
运行要求
提供两种模型规模：
7B 参数版本：基于 DeepSeek-Prover-V1.5-Base，上下文长度最高支持 32K tokens
671B 参数版本：基于 DeepSeek-V3-Base 训练
基本用法
使用 Huggingface Transformers 进行模型推理。671B 版本与 DeepSeek-V3 架构相同，具体使用方法请参考 DeepSeek-V3 相关文档。
限制
本模型卡片未提供关于模型局限性的具体说明。
License
DeepSeek-Prover-V2 模型的使用需遵守模型许可证（Model License）。
优先采用原作者提供的中文模型卡片；仅有英文说明时由闲社AI翻译整理。重要参数、许可证和商用范围请以原文为准。
你将获得什么
完整仓库方式包含该固定版本中的权重、配置、分词器及说明文件；指定版本方式只下载所选文件或整组分片。多模态模型的投影文件、配置等依赖，请按作者说明配齐。
完整仓库可能包含多个权重格式，因此需要的磁盘空间可能大于单一格式的模型大小。下载文件不等于完成模型部署。
使用前须知
运行环境运行模型需要的设备、工具与依赖，以原作者说明为准。
授权范围是否允许商用、修改和分发，请查看模型许可证。
闲社提供资料与镜像下载方法，不代表已运行模型或完成安全审计。下载的代码应先检查，再执行。
Problem with the information or download?
Sign in to submit feedback.
