模型详情
模型介绍
中文整理# DeepSeek-Prover-V1.5 模型卡片
模型用途
DeepSeek-Prover-V1.5是一个开源语言模型，专门用于在Lean 4中进行定理证明。该模型是对DeepSeek-Prover-V1的升级版本，通过优化训练和推理过程提升了性能。
## 主要能力
- 预训练于DeepSeekMath-Base模型，专门针对形式化数学语言进行优化
- 通过监督微调进一步训练，使用增强的形式化定理证明数据集
- 通过强化学习从证明助手反馈（RLPAF）进行进一步优化
- 采用RMaxTS方法，这是一种蒙特卡洛树搜索变体，使用内在奖励驱动的探索策略来生成多样化的证明路径
## 输入输出
- 输入：数学定理（以Lean 4形式化语言表述）
- 输出：定理的完整证明
运行要求
- 模型参数规模：7B（70亿）
- 提供三种模型版本：Base、SFT和RL
许可证
- 代码仓库采用MIT许可证
- DeepSeekMath模型的使用受模型许可证（Model License）约束
- DeepSeekMath支持商业使用
如需更多详细信息，请参阅LICENSE-CODE和LICENSE-MODEL文件。
优先采用原作者提供的中文模型卡片；仅有英文说明时由闲社AI翻译整理。重要参数、许可证和商用范围请以原文为准。
你将获得什么
完整仓库方式包含该固定版本中的权重、配置、分词器及说明文件；指定版本方式只下载所选文件或整组分片。多模态模型的投影文件、配置等依赖，请按作者说明配齐。
完整仓库可能包含多个权重格式，因此需要的磁盘空间可能大于单一格式的模型大小。下载文件不等于完成模型部署。
使用前须知
运行环境运行模型需要的设备、工具与依赖，以原作者说明为准。
授权范围是否允许商用、修改和分发，请查看模型许可证。
闲社提供资料与镜像下载方法，不代表已运行模型或完成安全审计。下载的代码应先检查，再执行。
资料或下载有问题？
登录后可提交反馈。
