大模型技术进展 - DeepSeek推出数学定理证明专用模型DeepSeek-Prover-V2，参数规模达6710亿，较前代V1.5的70亿规模增长近百倍，在miniF2F测试通过率达88.9%，解决普特南测试49道题 [3] - 月之暗面同期推出形式化定理证明模型Kimina-Prover，开源1.5B和7B参数版本，miniF2F测试通过率80.7%，普特南测试解决10道题 [3] - 两家公司技术报告均采用强化学习方法，DeepSeek通过子目标分解推进数学推理，月之暗面基于强化学习技术构建形式推理模型 [4] - DeepSeek模型矩阵同步进化，Prover系列从2024年3月发布后历经三次升级，代码系列Coder从2024年4月起完成五次迭代至V3-0324版本 [10] 行业竞争格局 - DeepSeek面临阿里巴巴开源模型追赶，通义千问Qwen3参数量仅为R1的1/3但性能全面超越，阿里已开源200余个模型全球下载超3亿次 [19] - 百度发布文心4.5 Turbo和X1 Turbo，性能更强成本更低，计划6月开源文心大模型4.5系列 [19][21] - 月之暗面Kimi用户增长受挑战，腾讯元宝通过微信引流和14亿元投流费用超越Kimi成为月活第三的AI产品，Kimi月活2000万不及豆包5600万 [16] - 华为昇腾芯片被传用于DeepSeek R2模型研发，但行业人士指出其训练效果一般且生态系统不完善，更适合推理部署 [14] 技术发展路径 - DeepSeek押注数学/代码、多模态和自然语言三大AGI实现路径，认为数学和代码是封闭可验证系统，可能通过自我学习实现高智能 [9] - 推理大模型R1价格低廉且性能强劲，Prover-V2以DeepSeek-V3为基础模型进行微调，利用子目标分解和思维过程链强化推理能力 [12] - 算法专家指出R2可能侧重强化学习能力提升，研发周期较短，而V4将涉及预训练工程和方法变革，研发周期更长 [13] 市场动态 - 中国AI原生APP月活排名变化：DeepSeek以1.94亿居首，豆包1.16亿次之，腾讯元宝0.42亿超越Kimi成为第三 [16] - 行业观点认为中国需要2-3个世界领先大模型而非单一明星企业，应鼓励领域内竞争和创业 [19] - 百度指出DeepSeek存在处理单一文本、幻觉率高、响应速度慢和API价格高等局限性 [19][20]