Follow
看到昨天 DeepSeek 开源的 DeepSeek-Prover-V2 模型官方介绍了。
该模型改变了我们处理形式化数学证明的方式，将复杂定理自动分解为简单子目标，并生成严谨的 Lean 4 证明代码。
同时结合了 DeepSeek-V3 模型的推理能力与强化学习，大幅提升了解题效率。
主要信息概括：
- 提供 7B 和 671B 两种参数规模的模型选择；
- 长上下文窗口支持（7B 模型支持 32K 令牌）；
- 在 miniF2F 测试集上达到 88.9% 的通过率，斩获第一；
- 能解决 49 个 PutnamBench 难题（共 658 个）；
- 包含 325 个形式化数学问题的 ProverBench 测试集。
GitHub: https:// 网页链接
模型下载： 网页链接
数据集： 网页链接
详细介绍可到 GitHub 上查看论文，目前模型以及数据集均已开源。
