DeepSeek-Prover-V2-671B发布 - 公司于4月30日正式推出DeepSeek-Prover-V2-671B模型，标志着AI数学推理能力进入新阶段 [2][4] - 该模型基于6710亿参数混合专家（MoE）架构，专为Lean 4证明辅助框架优化 [4] 技术架构特性 - 采用动态参数激活机制，单次推理仅调用约370亿参数，平衡性能与计算效率 [4][6] - 上下文窗口约128k tokens，支持高阶数学证明中的复杂长逻辑链处理 [6][7] - 可能延续多头潜在注意力机制（MLA），显著降低KV缓存需求并提升吞吐量 [7] 核心突破价值 - 实现形式化数学的"GPT-4级"突破，处理复杂数学证明能力显著提升 [7] - MoE架构相比稠密模型大幅降低内存需求并提高运算速度 [7] - 开放商用许可，预计在Hugging Face开源权重，支持学术与工业应用 [7] 应用场景拓展 - 形式化验证：应用于密码学安全证明、芯片设计验证等自动化流程 [7] - 数学研究加速：辅助定理形式化、新猜想探索及奥赛级难题证明 [7] - 智能教育工具：构建可验证步骤的交互式数学教学系统 [7] - 关键系统安全：通过Lean集成验证核心代码逻辑的正确性 [7] 基础训练数据 - 基础预训练可能超过14.8万亿tokens（基于V3基础），提供广泛知识储备 [6]