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