FormalMATH：人工智能形式化数学推理的新标杆

2025年5月，来自香港中文大学、Numina、西湖大学、M-A-P、2077AI、加州大学洛杉矶分校以及德国图宾根马克斯·普朗克智能系统研究所的研究团队联合发布了一项重要研究成果—FormalMATH，这是一个用于评估大型语言模型(LLM)形式化数学推理能力的全新基准。该研究已于2025年5月5日发布在arXiv预印本平台上，标识号为arXiv:2505.02735v1。

这项由俞周良、彭若天、丁可意等研究者共同领导的工作，旨在解决人工智能形式化数学推理领域面临的关键挑战。为什么这项研究值得关注？想象一下，我们希望计算机不仅能计算出数学问题的答案，还能像数学家一样提供严格的、无懈可击的证明。这就是形式化数学推理的核心——不仅要知道"是什么"，还要能够严格证明"为什么"。

一、形式化数学推理：AI面临的挑战与契机

形式化数学推理（FMR）是数学实践的一种特殊形式，它基于形式系统提供严格的公理化框架，对自动化证明验证至关重要。然而，这对人类专家来说都极具挑战性。例如，"Liquid Tensor实验"和"多项式Freiman-Ruzsa猜想"这样的数学难题，即使人类专家投入多年努力也尚未完全形式化证明。

想象一下，当你在解答一道复杂的数学题时，你不仅需要给出答案，还需要详细解释每一步推导的理由，不能有任何逻辑跳跃或假设——这就是形式化数学推理的严格要求。

近年来，大型语言模型(LLM)在这一领域展现出巨大潜力。研究人员通过自监督学习、思维链(CoT)微调以及可扩展的树搜索等技术，使LLM能够探索复杂的证明策略。尽管现有评估LLM形式化数学推理能力的基准如MiniF2F和ProofNet被广泛使用，但它们存在几个关键局限：

范围局限：现有基准覆盖面狭窄。例如，MiniF2F仅限于高中级别的代数和数论，而ProofNet则集中于本科级别的分析和代数。这种狭窄的范围限制了对形式化数学推理能力的全面评估。

数据集规模：目前的形式化数学基准相对较小。MiniF2F测试集仅包含244个问题，ProofNet仅有186个。这限制了基准测试的稳健性，阻碍了可泛化FMR系统的开发。

性能饱和：目前最先进的定理证明器，如Kimina-Prover，在现有基准上的成功率已超过80.7%，表明这些基准可能接近其实用效用的极限。

二、FormalMATH：一个全面的形式化数学推理基准

为了解决上述限制，研究团队引入了FormalMATH——一个基于Lean4的大规模基准，包含5,560个经过形式化验证的数学陈述。这些问题涵盖了广泛的数学领域，如代数、几何、微积分、数论和离散数学等，同时横跨多个难度级别，从高中奥林匹克难题到本科水平定理。

FormalMATH的开发面临两大主要挑战：

自动形式化难度：缺乏可靠的工具将自然语言问题转换为精确的Lean4语句，特别是对于需要严格语义保留的高级数学领域。

验证形式化语句需要确保语法正确性（通过Lean4编译器检查）和与原始问题的语义一致性——即使对人类专家来说，这也是一项技术上要求高且耗时的工作。

为应对这些挑战，研究团队提出了一个人机协作框架。这个框架通过集成以下技术大大减少了生成形式化数学语句所需的人工标注工作：

基于集成的自动形式化：通过best-of-N采样使用多个大语言模型进行自动形式化。

自动化验证：一个三层管道确保正确性——编译器语法验证、多LLM语义验证，以及基于否定的反证来过滤不可证明的定理。

这种策略在保持高准确性的同时最小化了人工验证工作，在最终的FormalMATH中保留了72.09%的翻译语句。

三、研究发现：现有定理证明器的优势与局限

当研究团队在FormalMATH基准上评估最先进的LLM定理证明器时，发现了这些系统面临的显著挑战。以最佳表现的模型Kimina-Prover为例，在FormalMATH-Full数据集上使用pass@32指标仅达到16.46%的准确率，而使用最佳优先搜索的BFS-Prover在采样预算为1×32×100的情况下仅获得11.13%的成功率。

想象一场数学竞赛，最优秀的AI选手也只能正确解决约16%的问题！这一结果表明，尽管AI在许多领域取得了令人印象深刻的进展，但在严格的形式化数学推理方面，仍有很长的路要走。

对这些结果的分析揭示了几个有趣的见解：

领域偏差显著：现有证明器在不同数学领域的表现差异很大，主要擅长高中级别的代数和应用数学，而在其他数学领域如微积分方面则表现较差。这强调了它们在跨领域泛化能力方面的关键差距。

过度依赖简化自动化策略：证明器经常将多步推理简化为单一策略调用（如"aesop"和"linearith"），绕过了必要的推导严谨性。

思维链推理的反直觉影响：虽然思维链(CoT)推理提高了FormalMATH语句的性能，但添加自然语言解决方案实际上降低了成功率。这表明在形式化推理环境中，人类编写的非形式化推理可能引入的是噪声而非清晰度。

就像一个懂得基本运算但不理解数学推理原理的学生，这些AI系统可以执行某些操作，但在构建完整、严谨的证明时仍然面临困难。

四、人机协作的自动形式化流水线

FormalMATH的核心创新之一是提出了一个高效的人机协作自动形式化流水线。这个系统如同一个翻译团队，将普通数学问题转换为计算机可以理解和验证的形式化语言。

研究团队首先利用两类LLM——专门用于编码的LLM（如Qwen2.5-7B-Coder）和预训练的定理证明LLM（如Deepseek-prover-base）。通过让通用大语言模型（如GPT-4）反复将自然语言语句翻译成Lean4语句，然后将每个候选语句传递给Lean4编译器，并且只保留通过类型检查的语句，研究团队创建了一个高质量的9,260对训练示例语料库，最终用于微调他们自己的自动形式化模型。

整个流程包括以下几个关键步骤：

自动形式化：对于每个自动形式化器（由LLM实现），采用best-of-N采样策略生成N个形式候选语句。所有候选语句首先通过Lean4编译器进行语法正确性验证，只有语法有效的语句才会被保留用于后续语义验证。

基于LLM的语义验证：研究团队使用多个强大的通用LLM（如o1-mini、claude-3.5-Sonnet）来评估自然语言数学问题与其Lean4形式化之间的语义一致性。每个模型采用思维链推理完成以下程序：(1)将Lean4语句反向翻译为自然语言，(2)比较重构的描述与原始问题，(3)提供二元判断（一致/不一致）。只有通过所有LLM语义验证的Lean4语句才会被收集。

通过证明其否定来推翻错误语句：受排中律启发，研究团队进一步过滤出某些不可证明的形式化语句。对于任何形式化语句，他们执行以下步骤：(1)构造其逻辑否定，(2)对该否定进行自动化证明尝试。如果成功证明了某个语句的否定，则原语句在该形式系统中不成立。

专家验证：研究团队招募了12位国际数学奥林匹克奖牌获得者级别的人类专家，手动检查自然语言语句与其Lean4形式化之间的语义一致性。结果表明，他们的多LLM自动形式化和验证流水线具有实质性的效率，从LLM语义验证的最后阶段（从30.1%）保留了72.1%的语句（到21.7%），同时显著减少了人工验证工作。

五、深入分析现有证明器的常见错误模式

为了更好地理解现有证明器的局限性，研究团队系统分析了它们的常见错误模式。就像一位教练分析运动员比赛录像以找出改进点，研究者们仔细检查了这些AI系统在尝试证明复杂数学问题时的失误。

他们发现了四种最常见的错误模式：

不当使用自动化策略：现有的基于LLM的Lean4证明器频繁生成过度依赖自动化策略的证明，如aesop、simp和linarith，以简化策略式证明所需的低级、逐步推理。这些策略依赖于固定的启发式算法和预标记的引理，可能无法匹配每个证明的结构。当过度调用或配置不当时，它们可能会显著扩展搜索空间，导致非终止或超时，甚至将目标转换为不相关或不可解的形式。

处理复杂不等式的能力不足：当前的证明器过度依赖linarith和nlinarith来找出线性和部分非线性不等式假设之间的矛盾。使用它们的常见程序要求证明器能够(1)混合高次多项式和有理函数，(2)利用循环或对称结构，以及(3)使用特定领域的引理（如重排、Chebyshev、AM-GM变体）。

引入冗余假设：当前基于LLM的定理证明器的一个常见错误来自引入结构上冗余的假设。虽然这些本身不会导致逻辑错误，但它们会模糊证明的基本逻辑并降低可读性。

不完整的证明：另一种常见的失效模式是生成未完成的证明尝试，留下未解决的关键子目标或依赖于没有证明中间步骤的占位符策略。

这些错误模式就像数学学习过程中的常见陷阱。例如，学生可能知道某个公式但不理解何时以及如何正确应用它，或者在解题过程中遗漏关键步骤。这些观察为改进未来的AI定理证明器提供了宝贵线索。

六、测试时计算扩展的有限回报

受近期测试时计算扩展成功的启发，研究团队还研究了其对形式化数学推理能力的影响。为了简化，他们只评估了最佳优先搜索（BFS）和重复采样在FormalMATH基准上的表现。

为了进行系统评估，研究者们引入了FormalMATH-Lite，这是FormalMATH的一个精心选择的子集，包含425个问题（359个高中水平和66个本科水平问题），设计用于高效但严格的测试时扩展分析。

结果显示，在形式化定理证明上应用测试时扩展获得的回报有限。例如，STP仅获得4.58%的绝对改进（从48.59%@Pass@32到53.17%@Pass@3200），尽管采样预算增加了100倍。虽然BFS-Prover展示了更好的扩展动态，在预算扩展32倍的情况下获得18.78%的提升（从27.10%@Pass@1×32×100到45.88%@Pass@32×32×100），但相对于单次生成方法仍然表现不佳。

这与非形式推理中近乎线性的扩展性能增长形成鲜明对比。在非形式数学中，采样过程中的伪连续奖励信号创造了路径，使得不完美的推理链，尽管存在逻辑缺陷，有时也能"偶然"得到正确答案。这表明即使中间步骤不严格合理，有效结论也可能出现。

形式定理证明缺乏这种容忍度。一个错误放置的策略或类型错误会使整个证明轨迹无效，使增量采样无效。虽然验证器引导的证明搜索（例如，可访问中间证明状态的BFS）在理论上比单步生成方法更能缓解这种脆弱性，但当前实现在计算上仍不实用，缺乏扩展效率。

七、思维链推理对形式化数学的影响

研究团队还评估了不同推理策略在Lean4证明生成中的效果：(1)朴素思维链提示，(2)增强自然语言的思维链，以及(3)vanilla生成策略。目标是测量非正式数学推理在多大程度上有助于随后推导的形式化证明的严谨性和有效性。

结果显示，在SFT和RL两种配置中，解码策略的排名一致。通常，朴素思维链获得最高Pass@K（从K等于32到3200）准确率，而增强自然语言的思维链表现介于朴素思维链和vanilla解码之间。例如，在K=3200时，DeepSeek-V1.5-SFT使用思维链达到50.6%，使用增强自然语言的思维链达到49.2%，使用vanilla解码达到47.0%。

这一发现展示了一个反直觉的现象：增强自然语言的思维链并没有比简单的思维链产生更好的结果。研究表明，自然语言指导与Lean4的策略空间之间存在内在不匹配。

想象一个数学老师给学生一个解题的大致思路，但没有提供详细的步骤。对于一个理解基础数学但不熟悉特定证明技巧的学生来说，这种高层次的指导可能帮助不大，甚至可能增加混淆。这就是为什么在某些情况下，没有额外人类引导的AI可能表现得更好——它可以按照自己的"思考方式"构建证明，而不必尝试将人类的非形式化思维翻译成精确的形式化步骤。

结语：未来的方向与挑战

FormalMATH提供了一个强大的基准，用于评估形式化数学推理。研究发现揭示了当前LLM在这一领域的基本局限：(1)即使最强大的模型也只能在FormalMATH上达到16.46%的成功率，(2)现有证明器展示出严重的领域偏差，在代数等领域表现良好，但在微积分等其他领域表现不佳，(3)令人惊讶的是，在思维链场景中提供自然语言解决方案指导反而降低了证明成功率。

这些限制表明了改进基于LLM的证明器的重要潜在方向。就像人类在学习数学证明时需要逐步掌握从基础到高级的技能，AI系统也需要更复杂、更强大的方法来克服当前的局限性。

FormalMATH的创新之处在于它不仅指出了问题，还提供了一个可扩展的框架来评估和改进未来的系统。通过其全面的基准和详细的错误分析，它为研究人员提供了宝贵的见解，指导下一代AI形式化数学推理系统的开发。

想象未来，AI系统不仅能够解决数学问题，还能提供人类可理解且机器可验证的严格证明，这将在科学研究、软件验证和数学教育中开辟新的可能性。FormalMATH是朝着这一远大目标迈出的重要一步。

对于想深入了解这项研究的读者，可以通过论文项目网页、GitHub仓库或Huggingface数据集获取更多信息，这些链接都可以在原始论文中找到。