DeepSeek-Prover-V1.5-SFT震撼发布：重新定义Lean 4定理证明的AI模型

郁如炜

363人浏览 · 2026-03-13 02:21:41

郁如炜 · 2026-03-13 02:21:41 发布

DeepSeek-Prover-V1.5-SFT震撼发布：重新定义Lean 4定理证明的AI模型

【免费下载链接】DeepSeek-Prover-V1.5-SFT DeepSeek-Prover-V1.5-SFT 是一款开源的语言模型，专为Lean 4定理证明优化设计。通过训练和推理过程的深度优化，以及基于强化学习和蒙特卡洛树搜索的探索策略，它在定理证明领域取得了卓越成果，实现了高中和本科级别基准测试的新突破。项目地址: https://ai.gitcode.com/hf_mirrors/deepseek-ai/DeepSeek-Prover-V1.5-SFT

DeepSeek-Prover-V1.5-SFT是一款开源的语言模型，专为Lean 4定理证明优化设计。通过训练和推理过程的深度优化，以及基于强化学习和蒙特卡洛树搜索的探索策略，它在定理证明领域取得了卓越成果，实现了高中和本科级别基准测试的新突破。

🌟 突破性技术：重新定义定理证明范式

DeepSeek-Prover-V1.5-SFT在DeepSeek-Prover-V1基础上实现了双重革新：

训练流程优化：基于DeepSeekMath-Base预训练模型，通过增强型形式化定理证明数据集进行监督微调，并结合证明助手反馈的强化学习（RLPAF）进一步提升性能
推理策略创新：提出RMaxTS蒙特卡洛树搜索算法，采用内在奖励驱动的探索策略，生成多样化证明路径，突破传统单路径生成的局限

📊 性能跃升：刷新多项定理证明基准

该模型在权威数学推理基准测试中表现卓越：

模型	miniF2F-test（高中级）	ProofNet（本科级）
DeepSeek-Prover-V1	50.0%	-
DeepSeek-Prover-V1.5-SFT	57.4%	22.9%
DeepSeek-Prover-V1.5-RL + RMaxTS	63.5%	25.3%

这一成绩不仅超越了前代模型，更在高中级别miniF2F测试集和本科级别ProofNet测试集上均创造了新的技术标杆。

🚀 快速开始：三步部署定理证明助手

1️⃣ 克隆项目仓库

git clone https://gitcode.com/hf_mirrors/deepseek-ai/DeepSeek-Prover-V1.5-SFT
cd DeepSeek-Prover-V1.5-SFT

2️⃣ 模型文件说明

项目包含以下核心文件：

模型权重：model-00001-of-000002.safetensors、model-00002-of-000002.safetensors
模型配置：config.json
分词器文件：tokenizer.json、tokenizer_config.json

3️⃣ 参考官方文档

完整使用指南请参阅项目中的说明文档，获取API调用示例和最佳实践建议。

📄 开源许可与学术引用

代码仓库采用MIT许可协议(LICENSE-CODE)，模型使用遵循模型许可协议(LICENSE-MODEL)。

如需在学术研究中使用，请引用以下论文：

@article{xin2024deepseekproverv15harnessingproofassistant,
      title={DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search},
      author={Huajian Xin and Z. Z. Ren and Junxiao Song and Zhihong Shao and Wanjia Zhao and Haocheng Wang and Bo Liu and Liyue Zhang and Xuan Lu and Qiushi Du and Wenjun Gao and Qihao Zhu and Dejian Yang and Zhibin Gou and Z. F. Wu and Fuli Luo and Chong Ruan},
      year={2024},
      eprint={2408.08152},
      archivePrefix={arXiv},
      primaryClass={cs.CL},
}