布客技术评论：为什么国产模型的数学研究能力不行？

结论先行：数学能力，特别是前沿问题的解决能力，不是解应用题，而是形式化验证。国产模型数学能力不足，核心原因不是代码能力差，而是没有在Lean形式化证明方向上进行足够的特化训练。这个判断有数据支撑，而且能解释一个看似矛盾的现象——国产模型在竞赛数学和代码生成上表现不错，却在研究级数学证明上乏善可陈。

先界定“数学能力”指什么

如果“数学能力”指的是K-12竞赛题的求解，国产模型并没有那么不堪。Qwen3-Max-Thinking在AIME 25和HMMT 25上拿到了国内首个双满分，Qwen3-VL-235B-A22B-T在涵盖JMC、AMC8、JMO、IMO等竞赛的1230道题目上取得了68.81%的最高分，并在六个竞赛中拿到最佳成绩。

但前沿数学问题——那些尚未被证明的猜想、需要构造全新证明路径的定理——完全是另一回事。2026年，陶哲轩公开表示自己“已经放弃实时跟进所有新证明”，AI生成证明的速度已经远超人类消化能力，数学正在从“证明稀缺时代”进入“证明过剩时代”。真正的瓶颈已经从“如何生成证明”转移到“如何验证与理解证明”。

而目前唯一成熟到可以在研究级别使用的自动验证工具，就是Lean及其数学库Mathlib。ArXivLean基准测试的41道研究级题目全部来自2026年3月的最新arXiv论文，结果所有模型——包括最强的闭源模型和专门的Lean agent——得分都低于20%。这个数字说明的不是“AI数学不行”，而是“AI在形式化框架下解决前沿数学的能力刚刚起步”。

代码能力不是瓶颈

2026年5月，全球权威三方编程榜单Code Arena放榜，阿里Qwen3.7-Max以1541分超越GPT-5.5、Gemini-3.5-Flash，仅次于Claude系列，在大模型厂商中排名全球第二，成为唯一突破1540分大关的国产大模型。这个榜单的特点是不考孤立的算法题，而是由开发者出题、模型从零生成完整的可交互Web应用，再由全球开发者盲测投票。这比传统benchmark更接近真实工程场景。

DeepSeek在代码领域同样是第一梯队。SuperCLUE的代码生成项目中，国产头部模型与海外头部模型的差距不到2分。代码能力不是国产模型的短板。

代码能力确实能转化为实际任务能力

两个案例可以说明这一点。

网络安全。 2026年9月底至10月初，一名被CrowdStrike认定为中文使用者的攻击者，使用中国开发的开源AI渗透测试工具ARTEX，配合DeepSeek v4.1-flash（主力模型）和GLM-5.3，攻破了韩国多家金融机构的系统，包括Hana Bank、KB Kookmin Bank和Shinhan Bank，被攻入的系统涉及银行的贷款查询服务和员工移动办公支持系统。CrowdStrike在报告中明确指出，攻击者“主要使用了DeepSeek v4.1-flash，辅以GLM-5.3”。

这个案例的关键不在于“模型被用于非法用途”，而在于它证明了国产模型的代码生成能力足以支撑复杂的多步骤攻击链：从漏洞识别到工具编排到命令生成，整个流程需要模型具备可靠的代码理解和生成能力，并且能够在迭代反馈中修正错误。这本质上就是“代码生成+搜索反馈循环”在攻击场景下的应用。

量化。 广发证券的研报使用DeepSeek-v4-pro和Qwen3-VL-235B构建了全自动因子挖掘系统，框架是一个“生成-评估-进化”的迭代循环，模型生成因子代码后自动评估IC、RankIC等指标，并将反馈注入下一轮生成，全流程无需人工介入。实证结果：在沪深全市场以10个交易日为换仓周期，DeepSeek-v4-pro生成的因子IC均值为2.15%，Qwen3-VL-235B为2.95%。对于A股市场的多因子选股策略，2%-3%的IC均值是有实际价值的水平。这直接说明：代码生成和搜索反馈循环在国产模型上是有效的。

问题出在Lean特化的缺失

既然代码能力不弱，代码能力也能转化为实际任务能力，为什么数学证明不行？

Lean形式化证明和普通代码生成之间的差异，比看起来要大得多。 自然语言推理允许启发式跳跃和隐含假设，而Lean证明要求每一步都被编译器验证，不允许任何省略。一个微小的语法错误或逻辑缺口就会导致整段证明被拒绝。这种刚性反馈机制对训练数据的质量和格式提出了远比普通代码训练更严格的要求。

国内在Lean训练数据上的积累确实薄弱。Lean-zh社区虽然存在，但规模有限。北大、人大、中科院等机构有研究者在使用Lean，国家天元数学中心和上海交大也举办了Lean4的暑期学校和培训班，但这些活动的定位是“推广”和“入门”，目标是让更多人知道Lean是什么，而不是产出大规模的Lean训练数据。

有一个值得注意的反面证据：DeepSeek其实已经发布过专门的形式化证明模型DeepSeek-Prover-V2-671B，在MiniF2F-test上达到了88.9%的通过率（Pass@8192），解决PutnamBench 49/658题，性能在神经定理证明领域属于state-of-the-art。这说明技术路径是通的，能力是存在的。但Prover-V2的定位是一个专门的定理证明模型，而不是将形式化证明能力集成到通用旗舰模型中的系统性特化。MiniF2F上的高分并不直接转化为ArXivLean所测量的研究级证明能力——前者是竞赛级别的形式化，后者需要从论文摘要中提取并形式化从未被形式化过的深层数学陈述，一道题可能需要数千行Lean代码。

国内学术圈已经在有意识地推动定理证明的人才培养。CCF形式化方法专委会主办了定理证明竞赛，浙江大学和上海交通大学联合承办；深圳河套学院的博士生赵雨扬自2021年起为mathlib贡献了数百个Pull Request。但这些努力仍处于“点状突破”阶段，远未形成足以支撑大模型系统性微调的数据规模和工程化能力。