1. 国产大模型数学推理的真实差距先从一道题说起前阵子我在一个技术群里看到有人抛了一道题用国产大模型去证明一个中等难度的数学命题要求输出能被 Lean 形式化验证器接受的代码。群里几个人分别试了不同模型结果差异大得离谱——有的模型连题目里的数学符号都理解错了有的能写出看起来像模像样的证明但一跑 Lean 就报错还有的干脆在中间步骤偷偷引入了一个未经证明的假设。这件事让我意识到讨论国产大模型的数学推理能力不能只看跑分榜单上的百分比得看它在真实约束下到底能做什么、不能做什么。这篇文章想聊的就是这件事国产大模型在数学推理这条路上真实的差距到底在哪里。我会从形式化验证这个最硬核的检验标准切入聊到显存这个绕不开的工程约束再落到实际部署和调试中会遇到的具体问题。适合正在做数学推理相关应用开发的工程师、想了解国产模型真实水平的技术决策者以及那些被跑分榜单搞得一头雾水的普通开发者。不管你是刚接触这个领域还是已经在调模型跑实验下面这些从实际项目里踩出来的经验应该都能给你一些参考。2. 数学推理的检验标准为什么形式化验证器是照妖镜2.1 自然语言答案的看起来对陷阱大部分模型在数学题上的评测用的是自然语言答案比对或者最终结果匹配。这种方式有个致命问题模型可以写出一个逻辑链条看起来完整、但中间某一步是错的证明只要最终答案碰巧对了评测就给它满分。我见过太多这样的情况——模型在第三步用了一个显然可得跳过了关键推导而那个显然其实根本不成立。自然语言证明的另一个问题是不可验证性。你没法用程序去检查一段中文写的数学证明是否严谨只能靠人工审阅。这在规模化的模型评测里根本不现实所以大家退而求其次用最终答案匹配但这又回到了刚才说的陷阱。2.2 Lean 这类形式化验证器到底在验什么Lean 是一个交互式定理证明器它的核心机制是你写的每一步推导都必须能被内核的类型检查器验证通过。这意味着模型不能跳过任何步骤不能引入未经证明的假设不能使用显然这种模糊表述。每一步要么是公理要么是之前已经证明过的定理要么是通过合法的推理规则从已有条件推导出来的。这就把数学推理的门槛从看起来有道理拉高到了机器可验证的严谨。一个模型如果能稳定输出 Lean 能接受的证明代码那它的数学推理能力就是实打实的。反过来如果模型在 Lean 验证下频繁失败那它在自然语言评测里的高分就有很大水分。2.3 国产模型在 Lean 任务上的真实表现分层从我实际测试和收集到的反馈来看国产模型在 Lean 任务上的表现大致可以分成三个层次。第一层是能理解 Lean 的基本语法能写出结构正确的证明框架但具体步骤经常出错这个层次的模型占了大多数。第二层是能在简单命题上给出完整且正确的证明但遇到需要多步归纳或者复杂构造的题目就力不从心。第三层是能处理中等难度的数学命题证明步骤基本正确偶尔需要人工微调目前能达到这个层次的国产模型屈指可数。这个分层和模型参数量、训练数据里数学内容的占比、以及是否针对形式化证明做过专门微调都有关系。但更关键的是很多模型在预训练阶段见过的数学文本大多是自然语言的Lean 代码的占比极低导致它们在形式化推理上的泛化能力天然就弱。3. 显存约束下的数学推理工程现实比理论更骨感3.1 为什么数学推理对显存的需求特别大数学推理任务和普通的文本生成有个本质区别它需要模型在生成过程中保持很长的推理链条而且每一步都要和前面的步骤保持逻辑一致性。这意味着模型需要更大的上下文窗口来容纳完整的证明过程同时注意力机制的计算量会随着序列长度平方级增长。再加上 Lean 形式化证明的代码通常比自然语言证明长得多一个中等难度的命题Lean 证明代码可能有好几百行。模型要一次性生成或者分段生成这些代码对显存的压力就上来了。我实测过一个 7B 参数的模型在处理长度超过 2000 token 的 Lean 证明任务时显存占用比处理同样长度的普通文本高出将近 40%。3.2 低显存运行模型的几种现实方案如果你手头的显卡显存有限比如只有 8G 或者 12G直接跑全精度的模型基本不现实。我试过几种方案各有优劣。量化是最直接的手段。把模型权重从 FP16 量化到 INT8 或者 INT4显存占用能降到原来的二分之一到四分之一。但量化对数学推理的影响比对普通文本生成大得多因为数学推理对数值精度更敏感量化误差可能在多步推理中被放大。我的经验是INT8 量化对数学推理的影响还在可接受范围内INT4 量化就需要谨慎评估了简单命题可能没问题复杂证明很容易出错。模型切分是另一种思路。把模型的不同层分配到不同的设备上或者用流水线并行的方式让多个小显存设备协同工作。这种方式的好处是不损失精度坏处是通信开销大推理速度会明显下降。如果只是做实验验证不在乎速度这是个可行的方案。还有一种方式是使用专门为低显存场景优化的推理框架比如一些支持动态卸载和按需加载的框架。这些框架会把暂时不用的层卸载到内存里需要的时候再加载回显存。实测下来这种方式在显存 8G 的卡上能跑动 13B 左右的模型但生成速度会慢很多适合做批量离线推理不适合交互式使用。3.3 显存分配策略对推理稳定性的影响显存分配不只是够不够的问题还有怎么分的问题。我遇到过好几次这样的情况显存明明够但推理到一半就崩了报显存不足。后来发现是 KV Cache 的分配策略有问题。KV Cache 是注意力机制里用来缓存之前计算的键值对的结构它的占用会随着生成序列的长度线性增长。如果一开始就把显存全部分配给模型权重没有给 KV Cache 留足空间生成长证明的时候就会爆显存。我的做法是在加载模型的时候预留至少 20% 的显存给 KV Cache如果预期生成序列很长这个比例还要提高。另外批处理大小也会影响显存分配。做数学推理评测的时候很多人喜欢用大的 batch size 来提高吞吐但每个样本的证明长度不一样长的样本会把整个 batch 的显存占用拉高。我通常会把 batch size 设成 1用梯度累积来模拟大 batch 的效果这样显存占用更可控。4. 从实际案例看国产模型的数学推理短板4.1 一个具体命题的完整测试记录我选了一个中等难度的数论命题来做测试证明对于任意正整数 n如果 n 是奇数那么 n 的平方减一能被 8 整除。这个命题在数学上不算难但需要用到模运算和因式分解能较好地检验模型的推理能力。测试了几个国产模型结果很有意思。模型 A 直接给出了自然语言的证明思路是对的但中间跳了一步因为 n 是奇数所以 n 可以写成 2k1 的形式这一步其实需要说明 k 是整数但模型没写。模型 B 尝试输出 Lean 代码语法基本正确但在使用 ring 策略化简表达式的时候用错了参数导致证明失败。模型 C 给出了完整的 Lean 证明我拿去验证居然通过了但仔细看代码发现它用了一个库里的定理直接得出了结论相当于把核心步骤外包给了现成的定理没有展示自己的推理过程。这个测试说明了一个问题国产模型在数学推理上的差距不只是能不能做对还有怎么做对的。有的模型是靠扎实的推理一步步推出来的有的模型是靠记忆或者模式匹配蒙对的这两者在面对新命题时的表现会天差地别。4.2 模型在长链条推理中的注意力衰减数学证明往往需要很长的推理链条每一步都依赖前面的步骤。我观察到国产模型在推理链条超过一定长度后会出现注意力衰减的现象前面几步的结论在后面的推理中被遗忘或者扭曲了。举个例子在一个需要五步归纳的证明里模型在第三步的时候还能正确使用第一步的假设但到了第五步它引用的第一步假设已经变了样加了一些原本没有的条件。这种错误在自然语言证明里很难被发现因为读起来很流畅但在 Lean 验证下会立刻暴露。这个问题和模型的上下文窗口大小、注意力机制的设计、以及训练时长序列数据的比例都有关系。目前国产模型在这方面和头部模型相比差距还是比较明显的。4.3 形式化验证器反馈的利用能力Lean 在验证失败时会给出错误信息指出哪一步出了问题。一个理想的数学推理模型应该能根据这些反馈来修正自己的证明。但我测试下来国产模型在这方面的能力普遍偏弱。具体表现是模型收到 Lean 的错误信息后要么完全忽略继续生成同样的错误代码要么做出过度修正把原本正确的部分也改错了。能根据错误信息精准定位问题并做出有效修正的模型我目前还没遇到。这个能力其实很关键因为在实际应用中模型很难一次就生成完全正确的证明通常需要多轮交互。如果模型不能有效利用验证器的反馈那整个交互过程的效率就会很低。5. 提升国产模型数学推理能力的实操路径5.1 数据层面的针对性补充国产模型在数学推理上的短板很大程度上是训练数据的问题。大部分预训练语料里形式化数学证明的占比极低模型没见过足够多的 Lean 代码自然写不好。一个可行的做法是在微调阶段引入大量的形式化证明数据。这些数据可以从开源的形式化数学库中提取比如 Lean 的数学库 mathlib 里就有大量的定理和证明。把这些数据转换成指令微调的格式让模型学习给定一个命题输出对应的 Lean 证明这个映射关系。但要注意直接拿 mathlib 的数据来微调效果可能有限因为 mathlib 里的证明往往使用了大量的辅助引理和高级策略模型很难直接学会。更好的做法是构建一个难度递进的训练集从最简单的命题开始逐步增加复杂度让模型循序渐进地学习。5.2 推理策略的工程优化除了模型本身的能力推理策略的优化也能显著提升数学推理的成功率。我试过几种策略效果比较明显的是分步生成加验证。具体做法是不让模型一次性生成完整的证明而是让它先生成证明的大纲然后逐步填充每一步的细节。每生成一步就用 Lean 验证一下这一步是否合法。如果验证失败就让模型重新生成这一步而不是从头再来。这种方式的好处是把一个长链条的推理任务拆成了多个短任务降低了模型出错的概率也方便定位问题。另一种策略是多路径采样加筛选。让模型对同一个命题生成多个不同的证明然后用 Lean 逐一验证取第一个通过验证的。这种方式能提高成功率但计算成本会成倍增加。如果显存和算力允许这是个简单有效的办法。5.3 显存优化的具体参数配置针对显存受限的场景我整理了一套具体的参数配置方案在 12G 显存的卡上实测能跑动 13B 级别的模型做数学推理。参数项推荐值说明模型精度INT8在数学推理上精度损失可接受最大序列长度2048覆盖大多数中等难度证明KV Cache 预留比例25%防止长序列生成时爆显存Batch Size1配合梯度累积使用梯度累积步数8模拟大 batch 效果显存卸载阈值80%超过此比例触发卸载这套配置的核心思路是牺牲一定的推理速度来换取显存空间的稳定。实测下来生成一个 500 行左右的 Lean 证明耗时大约 3 到 5 分钟对于离线评测和实验验证来说是可以接受的。注意量化到 INT8 后模型的数学推理能力会有一定下降建议在关键任务上先用 FP16 验证结果再用 INT8 做批量处理。6. 数学推理评测中容易踩的坑6.1 评测集选择的偏差很多人在评测国产模型的数学推理能力时用的评测集本身就有问题。比如有些评测集里的题目在训练数据里出现过模型是靠记忆答对的不是真的会推理。还有些评测集的答案标注有误导致模型答对了反而被扣分。我的建议是尽量用新发布的、模型训练时不可能见过的评测集而且最好能人工抽查一部分题目的答案是否正确。如果条件允许自己构建一个小规模的评测集针对性地测试模型在你关心的那类数学问题上的表现。6.2 验证器配置的细节陷阱用 Lean 做验证的时候有几个细节很容易被忽略。一个是 Lean 的版本问题不同版本的语法和策略可能有差异模型在一个版本上能通过的证明换一个版本可能就失败了。另一个是导入的库不同有些证明依赖特定的库如果验证环境里没有这个库证明就无法通过。我踩过的一个坑是模型生成的证明里用了一个 mathlib 里的定理但我的验证环境里 mathlib 的版本比较旧没有这个定理导致验证失败。后来统一了版本才解决。所以做验证之前一定要确保验证环境和模型训练时用的环境一致。6.3 显存监控与异常处理做数学推理的时候显存监控很重要。我遇到过好几次推理进程突然被系统杀掉的情况查日志发现是显存溢出。后来养成了习惯在推理脚本里加上显存监控当显存占用超过阈值时自动保存当前状态并优雅退出避免丢失已经生成的部分结果。另外长时间跑推理任务的时候显存碎片化也是个问题。连续生成多个证明后显存里会留下很多碎片导致后续的分配失败。解决办法是定期重启推理进程或者使用支持显存碎片整理的推理框架。7. 一些实际测试中的观察和体会我在实际测试国产模型数学推理能力的过程中有一个很深的体会模型在简单题上的表现和复杂题上的表现差距比想象中大得多。简单题上几个主流国产模型都能给出正确答案差距不明显。但到了需要多步推理的中等难度题差距就拉开了有的模型能稳定做对有的模型十次里错八次。另一个观察是模型对数学符号的理解能力普遍偏弱。比如把题目里的变量名换一下或者把数学表达式换一种等价但不同的写法模型的正确率就会明显下降。这说明模型可能是在做模式匹配而不是真正理解了数学结构。还有一个有意思的现象模型在生成 Lean 代码的时候倾向于使用它见过的常见策略比如 simp、ring、linarith 这些。对于需要自定义策略或者复杂构造的证明模型的表现就差很多。这反映出模型在形式化推理上的灵活性和创造性还有很大的提升空间。显存方面我的经验是不要追求在单卡上跑最大的模型。一个在 12G 显存上能稳定运行的 13B 模型比一个在 24G 显存上勉强跑起来但经常崩溃的 34B 模型在实际项目里更有价值。稳定性比峰值性能重要得多。最后分享一个小技巧做数学推理评测的时候把模型的温度参数调低一些比如 0.2 到 0.3能让输出更稳定减少随机性带来的波动。但也不能太低太低会导致模型陷入重复循环生成一堆无意义的重复步骤。这个参数需要根据具体模型和任务来调没有万能值。