这两个月的AI4Math折腾算是彻底把我从“吃瓜观众”变成了“赶路的人”。从7月初被一道简单几何题的真实得分打脸到8月底能在Lean里磕磕绊绊写完第一个完整定理的proof script这中间踩过的坑、推翻的认知比过去几年加起来都多。这篇心路历程不是教程更不是成果展示就是一个普通从业者在AI4Math这个方向上的真实记录——踩了什么坑、为什么踩、最后怎么绕过去把这些整理出来给同样在这条路上摸爬滚打的人一点参考。这一篇先聚焦2026年7月到8月两个月的时间线按我的实验记录和思考顺序来写。1. 为什么会在7月一头扎进AI4Math1.1 起因一道几何题让我从围观变成进场7月初一个开源社区的朋友发了张截图说他拿当时最热门的通用大模型去试一道初中几何题模型居然把辅助线画在了三角形外面还理直气壮地给出了答案。评论区都在玩梗说“现在的模型连初中生都不如”。但我点开那道题认真做了一遍发现题本身并不难难的是模型根本没有“几何直觉”的锚点它不知道哪条线是辅助线、辅助线该连到哪个交点。当时我手头正好在做知识库问答项目数学这块一直是用现成API顶上来的。看到那个截图之后我随手拿同一道题测了三个主流模型结果全翻车。那一刻我突然意识到AI4Math不是“能不能做对题”的问题而是整个推理链路从感知、符号理解到逻辑演绎几乎每个环节都有缺口。这让我决定不再做外围围观干脆花两个月时间专门啃这块硬骨头。1.2 起步准备先把“数学题”拆成三类再定路线7月第二周我给自己列了一个简单的分类框架把数学任务分成三类数值计算题比如解方程、求导、符号推理题比如因式分解、不等式证明、形式化证明题需要在Lean或Isabelle里写出完整proof term。这个分类看起来简单却直接影响后续所有实验的目标设定。我当时对A4Math的现状判断是这样的数值计算题通用模型只要不抽风基本能做对大半符号推理题是分水岭模型经常“会做但过程错”答案对但步骤跳跃形式化证明题则完全是另一个世界需要同时搞定搜索策略和形式化语言表达。基于这个判断我给自己定的路线是先摸清通用模型在数值题上的天花板再主攻符号推理和形式化的衔接点。那时候全网都在讨论用强化学习刷数学竞赛题但我更想搞清楚的是模型到底是在“记住题型”还是在“学会推理”。这个区别直接决定两个月后我的实验方向会不会走偏。2. 8月的“历劫”现场从数据集到训练策略的全面翻车2.1 数据准备阶段我做的第一件蠢事是拿未清洗语料直接微调7月中旬我整理了一批数学题解语料大概60万条来源很杂题库网站、竞赛真题、论坛讨论帖。当时想的是数据量够了直接在开源底座模型上做SFT有监督微调。结果训练到第三步loss就开始疯狂震荡最后模型直接学会了“看到题就先写一句这题很简单然后随便给个答案”。排查了两天才发现问题出在数据质量上——语料里有大量不完整解答比如论坛帖子里的“这题明显可以做用xxx定理”后面居然没有过程还有大量重复题、错题、甚至答案和题目对不上的残次样本。这次教训让我花了整整三天重写清洗脚本规则很简单但很管用去重、按“题目完整过程最终答案”三字段校验、过滤长度低于200字符的样本、用模型A批量做一遍题然后丢弃答案不一致的样本。清洗后数据从60万降到27万但训练loss曲线肉眼可见地稳定了下来。这里必须提醒一句数学微调的数据清洗远比文本摘要或对话任务苛刻因为数学解答是有“对错”的错一个符号就是实打实的错误样本。宁可数据少一点也不能拿噪声喂模型。2.2 评测集为了一口气复现AIME成绩我忽略了基座差异清洗完数据之后我开始微调7B规模的模型然后顺手去跑AIME竞赛题评测。结果第一轮跑下来模型分数几乎没涨而社区里有人复现出比我高两倍的分数。我一度怀疑是自己训练参数配错了后来仔细对比才发现对方的基座模型比我的大一个量级学习率还用了余弦退火加Warmup我用的则是固定学习率。这个阶段我悟到一个特别基础的道理复现成绩必须先复现环境和基线。同一个数据集放在不同规模、不同系列的基座上结果可能天差地别。后来我养成了个习惯每次跑评测之前先建一张基线记录表把基座、数据量、训练步数、学习率、评测集版本全部列出来再谈效果对比。为了进一步校准我还在评测集里加入了MiniF2F的一个子集专门用来定位模型在形式化题目上的表现。2.3 强化学习尝试奖励模型一上loss当场爆炸8月中最刺激的一次实验是尝试用强化学习RL让模型自己探索解题路径。我先用SFT版本生成了一批解题轨迹再用规则判断最终答案是否正确作为奖励信号开训。理想很丰满模型应该学会一步步试错最后找到通法。但实际跑了不到几百步训练就崩了——奖励值完全不增长策略迅速坍缩到输出固定模板。后来反思原因其实很典型规则奖励太稀疏而且AnswerJudge这个信号忽略了过程导致模型学到的是“蒙一个答案”。数学解题的过程和答案之间的因果关系远不是单纯结果比对能衡量的。于是我把奖励重新拆成三步解题中途的“式子有效性”、步骤间的“逻辑衔接得分”先不管对错只看是否构成可读推导、以及最终“答案正确性”加权组合。这个改动让训练不再爆炸但也暴露了另一个问题模型开始为了拿到中间奖励写出一堆“合理但无用的步骤”来凑数最后答案还是错。那几天我脑子一直是嗡嗡的线上讨论群里的结论几乎分成了两派一派说要用过程监督模型PRM来逐步打分另一派说干脆把问题改写成形式化语言再做搜索。两派吵了三天谁也没说服谁但对我来说这已经无所谓了——我很清楚自己已经摸到了当前技术路线的瓶颈数学推理的评估信号不能只有对错必须要有“对过程的度量”。真要做好这件事得往过程监督和形式化验证两方面下功夫。3. 两个让我彻底改观的技术方向形式化语言和解题轨迹3.1 用Lean搭建“不会说瞎话”的数学环境8月中旬我开始系统接触Lean 4。之前在社区里看过一些讨论但一直觉得门槛高每次打开教程都被一堆tactic命令劝退。这次因为要解决“模型生成步骤到底对不对”我硬着头皮把Lean装了起来试着把一些简单的不等式证明搬进去。上手之后我的最大感受是Lean就像一台数学界的单元测试框架每一步推理都必须有可执行的依据。模型如果用自然语言说“显然构造辅助圆”Lean根本不买账必须给出具体构造和后续证明。这种“不讲情面”的特性正好弥补了自然语言模型那种“看起来通顺但逻辑缺失”的毛病。我搭了一个小实验让SFT模型生成解题步骤然后把这些步骤翻译成Lean的tactic序列让Lean做验证。第一次跑下来100道题里能通过验证的只有3道。主要原因有两个一是模型压根不会写tactic命令生成的代码全是幻觉二是自然语言步骤和形式化证明之间根本没有对齐关系模型写的“第一步代换”在Lean里的含义可能是好几种操作。但看到那3道题通过验证的那一刻我整个人的思路都打开了——因为我第一次看到了“机器可验证的数学推理”的闭环路径。3.2 解题轨迹回填把“改错题”变成一种训练信号和Lean验证并行的另一条线是寻找更细粒度的过程监督。我刚被RL的稀疏奖励搞得头大就在翻代码库时看到一个老项目的思路很多人可能也见过在SFT阶段就做“错误轨迹回填”让模型同时看到正确和错误的解题过程然后训练它学会给错误步骤打标签。这个思路简单说就是拿题目生成多条解题轨迹其中有些条中途就错了用校验工具比如式子展开比对或者符号计算库定位到出错那一步然后给模型构造一个“找虫任务”——这一堆步骤里哪一步开始错的我再拿这个任务做多任务学习辅助原始解题目标。我试了两周效果简直离谱。模型做MiniF2F子集和AIME题目的正确率比单纯SFT高了大概8到12个百分点。更关键的是模型在遇到“看起来能做但中途卡住”的题目时不再硬套模板而是会尝试换一种路径。这多少有点“脑子知道错了”的意思了。这段经历让我确信对AI4Math来说标注出“哪里错了”往往比标注“哪个答案对”更重要。因为错误路径蕴含的信息量比正确答案的重复信息要大得多。4. 两个月走下来我的经验复盘和给后来者的建议4.1 评测不是跑个分就完事要拆维度8月底我重新回看自己做的所有实验最大的收获不是模型分高了多少而是我终于设计出了一套能定位问题的评测口径。以前评测得分的逻辑很简单准确率拉到70%就觉得自己行了。现在我会把每个测试题按知识板块、步骤长度、是否需要多步推理、是否有图结构分四个维度标记评测报告按维度输出。举个例子同一个模型在“一元二次方程”上准确率95%在“数列递推证明”上只有20%。前者说明计算能力没问题后者说明递归推理和归纳假设对这些模型依然是难点。这样拆完后续优化目标一下子就清楚了。千万别拿一个总分自我安慰AI4Math的死结从来藏在得分分布的不均匀里。4.2 技术路线选择上的一些个人偏见既然说经验那就直说。如果现在有人问我起步阶段应该优先走哪个方向我的排序从来都很明确形式化语言优先哪怕只是掌握Lean的基础tactic也能给你一个严格的标准去度量模型推理是否可靠过程监督优先PRM之类的方法比单纯改造结果奖励更值得投入因为数学推理中“部分正确”是常态你必须有手段度量部分正确错题回填优先与其反复刷正样本不如花力气构造高质量负样本我实测下来收益非常稳。当然这都是我两个月磕磕绊绊积累下来的偏见不一定适合所有人。但我知道有相当多的人卡在“奖励信号无法度量过程”这堵墙前面上面出场的就是我撞墙之后找到的几条窄门。4.3 给新人的实用工具箱清单根据我这两个月踩过的坑整理了一份自用工具组合仅供参考用途工具/方法我的使用心得形式化验证Lean 4别急着写复杂定理先从自然语言步骤映射到tactic序列练起数学符号计算SymPy / Mathematica用来校验中间推导步骤实时抓模型错误数据清洗自写规则 API辅助过滤字段规范化比去重更重要“题目/过程/答案”三字段缺一不可评测集MiniF2F AIME历年题必须有训练集之外的留出集别直接用训练集当评测集过程监督人工标注步骤对错或PRM初期人工标注几百条就够关键是错误样本覆盖要广训练框架开源微调框架 LoRA7B模型加LoRA训练够用但评测时必须锁定同一个基座再比4.4 这些路线后续还能怎么扩展这两个月做下来的感觉是AI4Math现在最缺的不是更大的模型而是更可靠的验证环境和更细粒度的过程信号。我个人后续打算在三个方向上继续把错题回填的覆盖面扩大到几何题看看能不能借图形库做一个几何误推导检测在Lean验证之后加一层“自然语言翻译”让模型同时输出形式化证明和自然语言解释方便人检查试一些混合奖励设计把规则判定、PRM打分和Lean通过率组合起来让RL训练不再那么脆。回头想想这六十天里真正最值得记下来的不是我跑通了哪个训练流程而是我总算弄明白了一件事所谓AI4Math不是让模型有多能算而是让模型的每一条推理链条都有被验证的可能。这条路还很长但至少从这两个月之后我已经知道下一步该往哪个方向踩了。