模型详情
模型介绍
中文整理DeepSeek-Prover-V1.5 模型卡片
模型用途
用于在Lean 4形式化证明助手环境中进行定理证明。
主要能力
基于DeepSeekMath-Base预训练，专门针对形式化数学语言进行优化。经过监督微调和强化学习从证明助手反馈（RLPAF）训练。采用RMaxTS蒙特卡洛树搜索变体方法，通过内在奖励驱动的探索策略生成多样化证明路径。
输入输出
输入：数学定理描述和证明任务。输出：形式化数学证明。
运行要求
7B参数规模模型，需要支持大语言模型运行的硬件环境。
基本用法
提供Base、SFT和RL三种模型版本。Base版本为预训练基础模型；SFT版本经过监督微调；RL版本经过强化学习优化。建议根据具体任务需求选择合适的模型版本。
评估结果
在高中水平miniF2F测试集上达到63.5%准确率；在本科水平ProofNet测试集上达到25.3%准确率。
许可证
代码仓库采用MIT许可证。DeepSeekMath模型使用需遵守Model License。支持商业使用。
联系方式
如有问题，可提交issue或发送邮件至service@deepseek.com。
优先采用原作者提供的中文模型卡片；仅有英文说明时由闲社AI翻译整理。重要参数、许可证和商用范围请以原文为准。
你将获得什么
完整仓库方式包含该固定版本中的权重、配置、分词器及说明文件；指定版本方式只下载所选文件或整组分片。多模态模型的投影文件、配置等依赖，请按作者说明配齐。
完整仓库可能包含多个权重格式，因此需要的磁盘空间可能大于单一格式的模型大小。下载文件不等于完成模型部署。
使用前须知
运行环境
运行模型需要的设备、工具与依赖，以原作者说明为准。
授权范围
是否允许商用、修改和分发，请查看模型许可证。
闲社提供资料与镜像下载方法，不代表已运行模型或完成安全审计。下载的代码应先检查，再执行。
资料或下载有问题？
登录后可提交反馈。