DeepSeek开源新模型

五一期间，DeepSeek有新动作，开源了Prover-V2模型。该模型在定理证明赛道表现出色，在MiniF2F测试中通过率达88.9%。4月30日晚，HuggingFace平台更新了其技术细节。

模型版本与特点

DeepSeek团队发布了两个版本，参数规模分别为7B和671B。Prover-V2是为Lean 4打造的开源大语言模型，专注形式化定理证明。其初始化数据通过特定流程收集，能融合非形式化和形式化数学推理。

训练与实验结果

模型经历两阶段训练，建立了两种证明生成模式。实验表明，671B版模型准确率高、效率更高。DeepSeek还发布了ProverBench基准数据集。

网友评价

网友对该模型评价颇高，有人称其把o4-mini和Grok-3都比下去了，处理数学问题的思路对代码问题也适用。大家对DeepSeek-R2也满怀期待。