这项由中科院计算技术研究所徐星教授团队联合StepFun公司完成的研究发表于2025年8月的AAAI会议，研究团队开发了名为StepFun-Formalizer的AI系统，专门解决数学自动形式化难题。有兴趣深入了解的读者可以通过arXiv:2508.04440v1访问完整论文。
要理解这项研究的重要性，我们不妨把数学想象成一种特殊的"语言"。日常生活中，我们用自然语言表达数学概念，比如说"证明任何大于2的偶数都可以表示为两个质数之和"。但在计算机的世界里，数学有着更加严格的表达方式，就像法律条文一样精确，每个符号、每个步骤都必须无懈可击。这种精确的数学语言被称为"形式化语言"，比如Lean、Coq这样的系统。
把自然语言的数学问题翻译成形式化语言，就像把一首诗翻译成另一种语言一样困难。不仅要保证意思不变，还要符合目标语言的严格语法规则。更关键的是，形式化语言容不得半点模糊或错误，就像精密仪器的图纸一样，一个小数点的位置都不能错。
研究团队发现，现有的AI系统在这项"翻译"工作上表现很糟糕。即使是最先进的大型语言模型，在处理数学形式化时也经常犯两类基本错误。第一类错误就像一个外国人想说中文，但不知道"筷子"这个词怎么说，只能比划手势——AI不熟悉形式化语言的专门词汇和语法规则。第二类错误则像一个人虽然知道所有汉字，但理解能力有问题，把"白马非马"理解成了"白色的马不是马"——AI无法正确理解自然语言数学问题的真实含义，也不知道如何在两种语言之间建立准确的对应关系。
为了解决这个问题，研究团队设计了一套名为ThinkingF的训练流程，就像为AI设计了一套完整的"语言学习课程"。这套课程分为四个环节，每个环节都有其独特的作用。
一、知识蒸馏与筛选：为AI补充"词汇量"
研究团队首先意识到，现有的AI模型在形式化数学知识方面存在严重不足，就像一个想要翻译科技文献的人却缺乏专业词汇一样。为了解决这个问题，他们采用了一种巧妙的方法——让专门的数学形式化AI模型Kimina-Autoformalizer来充当"词典编纂者"。
这个过程就像制作一本超大型词典。研究团队从NuminaMath-1.5数据集中挑选了约25.6万个数学问题，让Kimina-Autoformalizer为每个问题生成16种不同的形式化表达方式。为什么要生成这么多版本呢？这就像请16个不同的翻译家翻译同一句话，然后从中挑选最准确的版本。
接下来是严格的质量控制过程。研究团队设立了三道筛选关卡。第一关是语法检查，就像检查句子是否符合语法规则，那些有语法错误的形式化表达会被直接淘汰。第二关是"多数表决"机制，研究团队会将16个版本进行等价性验证，把它们分成不同的"意思相同"的组别，然后选择人数最多的那一组的代表。这种方法的原理很简单：如果多个独立的翻译都得出了相同的结果，那这个结果很可能是正确的。
第三关是由强大的AI模型DeepSeek-V3进行最终审核，专门筛除那些过于简单的问题（比如证明1+1=2）和逻辑矛盾的问题。经过这三轮严格筛选，最终保留了约18.3万个高质量的训练样本。这个过程就像从原矿中提炼出纯金一样，虽然数量减少了，但质量大大提升。
二、推理轨迹合成：教会AI"思考过程"
有了充足的"词汇量"还不够，AI还需要学会如何思考。研究团队发现，仅仅知道答案是不够的，AI还必须掌握从问题到答案的完整思考过程。这就像学数学不能只背答案，还要理解解题思路一样。
为此，研究团队设计了一套详细的"思维模板"，就像为学生制定学习数学的标准流程。这个模板包含两个核心部分。第一部分是"问题理解"，要求AI首先用自己的话重新表述数学问题，分析问题的逻辑结构，识别涉及的数学概念，并确定需要定义的数学对象。这就像解数学题前先要读懂题目、理清思路一样。
第二部分是"形式化分析"，AI需要预判在形式化过程中可能遇到的技术难题，然后逐步将自然语言中的数学对象映射到形式化语言中的对应表达。这个过程就像建造一座桥梁，需要仔细规划每一个构件的位置和连接方式。
研究团队使用这套模板，让Claude 3.7 Sonnet（一个擅长遵循复杂指令的AI模型）为5800个数学问题生成完整的推理过程。这些推理过程不仅包含最终答案，还详细记录了从理解问题到得出答案的每一步思考，为后续训练提供了宝贵的"思维范例"。
三、两阶段监督微调：循序渐进的技能训练
有了丰富的训练材料后，研究团队开始对基础AI模型进行专门训练。他们选择了DeepSeek-R1-Distill-Qwen作为基础模型，这是一个在数学推理和编程方面表现出色的AI系统。整个训练过程分为两个阶段，就像学习一门技能需要先打基础再提高一样。
第一阶段主要是"知识灌输"，使用前面收集的18.3万个形式化样本来训练模型。在这个阶段，AI学会了形式化语言的基本词汇和语法规则，就像学外语时先学单词和基本句型一样。训练时，研究团队在输出结果前后加上特殊标记，帮助模型保持内在的推理能力。
第二阶段是"推理能力培养"，使用包含完整思考过程的5800个样本进行训练。这些样本的特殊之处在于，每个答案前都有一段详细的推理过程，被特殊标记包围起来。通过学习这些"思维示例"，AI逐渐掌握了从理解问题到形式化表达的完整思考链条。
两个阶段结束后，AI系统已经具备了基本的数学形式化能力，但研究团队并没有就此停步。他们知道，真正的专家是在实践中不断完善技能的，AI也需要这样的"实战训练"。
四、强化学习优化：在实践中精益求精
最后一个环节是强化学习，这就像让AI在实际工作中不断改进自己的表现。研究团队使用了一种名为GRPO（Group Relative Policy Optimization）的训练算法，这种方法的核心思想是让AI通过不断试错来优化自己的表现。
训练过程是这样的：给AI一个数学问题，让它生成形式化表达，然后使用BEq（双向扩展定义等价）验证系统来检查答案是否正确。如果AI的答案与标准答案在数学上等价，就给予奖励；如果不等价，则不给奖励。通过这种"做对了有糖吃，做错了没奖励"的机制，AI逐渐学会了生成更准确的形式化表达。
这个过程就像训练一个新手翻译。一开始翻译可能磕磕绊绊，但通过大量练习和即时反馈，翻译水平会不断提升。经过450个训练步骤后，AI的奖励分数从0.232提升到0.347，平均准确率也从25.8%提升到30.3%。
经过这套完整的训练流程，研究团队最终开发出了两个版本的StepFun-Formalizer：7B参数版本和32B参数版本。这两个数字代表模型的规模大小，参数越多，模型的能力通常也越强，但计算需求也更高。
研究团队在三个权威测试集上评估了模型的性能表现。FormalMATH-Lite是一个包含425个问题的测试集，主要评估模型在已知领域的表现。ProverBench包含174个问题，专门测试模型处理新类型问题的能力。CombiBench则包含100个组合数学问题，这类问题涉及复杂的现实场景，是对AI综合能力的严峻考验。
测试结果令人振奋。在FormalMATH-Lite上，StepFun-Formalizer-32B达到了40.5%的单次尝试准确率，这意味着AI第一次尝试就能给出正确答案的概率超过四成。在更具挑战性的ProverBench上，该模型达到了26.7%的准确率。虽然这些数字看起来不算很高，但要知道这是一个极其困难的任务——即使对人类数学专家来说，将自然语言数学问题完美翻译成形式化语言也需要丰富的经验和细致的思考。
更重要的是，StepFun-Formalizer-32B的表现不仅超越了所有专门的数学形式化AI系统，甚至超过了包括GPT-4、Claude等在内的通用AI大模型。这就像一个专门训练的翻译专家不仅击败了其他翻译专家，还胜过了那些"什么都会一点"的全能型选手。
研究团队还进行了详细的错误分析，发现AI犯错主要有两大原因。一是"自然语言理解错误"，AI误解了原问题的含义；二是"形式化对齐错误"，AI理解了问题但无法准确转换为形式化表达。通过引入专门的训练数据和推理过程，StepFun-Formalizer显著减少了这两类错误的发生率。
为了验证系统的实用价值，研究团队还进行了一项有趣的实验。他们让StepFun-Formalizer将1万个数学问题形式化，然后用专门的定理证明AI来尝试证明这些形式化后的问题。结果显示，经过StepFun-Formalizer处理的问题中，有49.4%能够被成功证明，而使用其他形式化系统处理的问题只有45.5%能被证明。这个结果说明，StepFun-Formalizer不仅翻译准确率高，翻译出来的形式化表达也更容易被计算机理解和处理。
这项研究的意义远不止于技术突破本身。在人工智能快速发展的今天，如何让AI真正理解和处理复杂的数学概念一直是一个核心挑战。StepFun-Formalizer的成功为这个问题提供了一个可行的解决方案。
从更广泛的角度来看，这项研究为AI系统的训练提供了新的思路。传统的AI训练往往只关注最终结果的准确性，而忽略了思考过程的重要性。StepFun-Formalizer的成功表明，让AI学会"思考过程"比单纯追求正确答案更加重要。这种训练理念不仅适用于数学形式化，也可能推广到其他需要复杂推理的AI应用中。
研究团队在论文中还透露了一些有趣的发现。比如，他们发现单纯使用通用AI大模型来生成推理过程效果并不好，因为这些模型往往会"跑题"——花大量时间去解数学题本身，而不是专注于如何将问题转换为形式化语言。这就像请一个数学教授来做翻译工作，他可能会忍不住开始讲解数学原理，而忘记了自己的主要任务是翻译。
另一个有意思的发现是，即使是专门的数学形式化AI也经常在组合数学问题上表现不佳。组合数学涉及复杂的现实场景建模，需要AI不仅理解数学概念，还要能够处理实际应用中的各种复杂情况。StepFun-Formalizer在这类问题上的提升表明，通过系统性的训练，AI确实可以获得更强的综合理解能力。
展望未来，这项研究为数学AI的发展开辟了新的道路。随着更多高质量训练数据的积累和训练方法的进一步完善，我们有理由期待AI在数学形式化方面达到更高的准确率。更重要的是，这种能力的提升将直接推动自动定理证明、数学教育辅助、科学计算验证等应用领域的发展。
说到底，StepFun-Formalizer的成功不仅仅是一个技术突破，更是人工智能向着真正理解和处理复杂数学概念迈出的重要一步。虽然40.5%的准确率距离完美还有很大距离，但这已经是这个极具挑战性领域的一个重大进步。就像人类学习语言一样，AI也需要时间和大量练习才能真正掌握数学这门"语言"的精髓。而StepFun-Formalizer的出现，让我们看到了AI在这条路上的坚实脚步。
对于普通读者来说，这项研究的价值或许还不能直接感受到。但可以想象，当AI真正掌握了数学形式化能力后，它将能够帮助数学教师更好地设计教学内容，帮助学生理解复杂的数学概念，甚至协助科学家验证重要的数学证明。这些应用场景的实现，将让数学这门古老而美丽的学科在数字时代焕发出新的活力。
Q&A
Q1：StepFun-Formalizer是什么？它能做什么？
A：StepFun-Formalizer是由中科院计算技术研究所和StepFun公司联合开发的AI系统，专门用于数学自动形式化。它能够将自然语言表达的数学问题准确翻译成计算机可以理解和验证的严格数学语言，就像把日常数学表达转换成精密的数学"法律条文"。
Q2：为什么数学自动形式化这么困难？现有AI为什么做不好？
A：数学形式化就像把诗歌翻译成另一种语言，不仅要保证意思不变，还要符合极其严格的语法规则。现有AI主要犯两类错误：一是不熟悉形式化语言的专门词汇和语法（就像外国人不知道"筷子"怎么说），二是理解能力有问题，无法正确理解数学问题的真实含义。
Q3：StepFun-Formalizer的40.5%准确率算高吗？有什么实际意义？
A：对于这个极其困难的任务来说，40.5%是一个很大的突破，超越了所有现有系统包括GPT-4等大模型。这意味着AI在数学形式化方面迈出了重要一步，未来可以帮助数学教育、定理证明验证、科学计算等领域，让数学在数字时代发挥更大作用。
上一篇：华东师范大学团队推出Sel3DCraft：让文字变3D模型像画画一样轻松直观
下一篇：全国首个产业AI促进中心落地中山！华为云三年投10亿，助力“中山智造”领跑湾区
