模型介绍
中文整理模型用途
DeepSeek-Prover 是一个用于形式化定理证明的大语言模型，基于 Lean 4 证明助手生成的高中和本科级数学竞赛问题数据进行训练。
主要能力
该模型能够自动生成完整的 Lean 4 形式化证明。在 miniF2F-test 基准测试中，使用 64 个采样时达到 46.3% 的准确率，累积准确率为 52%，优于 GPT-4（23.0%）和树搜索强化学习方法（41.0%）。在 Lean 4 FIMO（形式化国际数学奥林匹克）基准测试中，成功证明了 148 道题中的 5 道，而 GPT-4 未能证明任何题目。
输入输出
输入：自然语言数学问题被翻译为 Lean 4 形式化陈述
输出：Lean 4 形式化证明
运行要求
模型基于 DeepSeekMath 7B 构建，训练数据包含 800 万条形式化陈述及其证明。
基本用法
模型和合成数据集已发布在 HuggingFace 上，可供下载使用。
限制
模型主要针对高中和本科级数学竞赛问题，在更高级的数学问题上的能力有限。FIMO 基准测试中仅有 5/148 的问题被成功证明。
许可证
代码仓库采用 MIT 许可证。DeepSeek-Prover 模型使用需遵守模型许可证，支持商业用途。
优先采用原作者提供的中文模型卡片；仅有英文说明时由闲社AI翻译整理。重要参数、许可证和商用范围请以原文为准。
你将获得什么
完整仓库方式包含该固定版本中的权重、配置、分词器及说明文件；指定版本方式只下载所选文件或整组分片。多模态模型的投影文件、配置等依赖，请按作者说明配齐。
完整仓库可能包含多个权重格式，因此需要的磁盘空间可能大于单一格式的模型大小。下载文件不等于完成模型部署。
使用前须知
运行模型需要的设备、工具与依赖，以原作者说明为准。
是否允许商用、修改和分发，请查看模型许可证。
闲社提供资料与镜像下载方法，不代表已运行模型或完成安全审计。下载的代码应先检查，再执行。
资料或下载有问题？
登录后可提交反馈。