FormalMATH: Benchmarking Formal Mathematical Reasoning of Large Language Models

📄 arXiv: 2505.02735v1 📥 PDF

作者: Zhouliang Yu, Ruotian Peng, Keyi Ding, Yizhe Li, Zhongyuan Peng, Minghao Liu, Yifan Zhang, Zheng Yuan, Huajian Xin, Wenhao Huang, Yandong Wen, Ge Zhang, Weiyang Liu

分类: cs.AI, cs.LG

发布日期: 2025-05-05

备注: Technical Report v1 (33 pages, 8 figures, project page: https://sphere-ai-lab.github.io/FormalMATH/)

💡 一句话要点

FormalMATH：构建大规模形式化数学推理基准，揭示LLM在数学证明中的局限性。

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 形式化数学 定理证明 大型语言模型 基准测试 自动形式化

📋 核心要点

  1. 现有数学推理基准在范围和规模上存在局限性，难以全面评估LLM的形式化数学能力。
  2. 提出一种人机协同的自动形式化流程，利用LLM进行语句生成、语义验证和反证过滤，降低人工成本。
  3. 实验表明，现有LLM在形式化数学推理方面存在显著局限性，且自然语言指导可能引入噪声。

📝 摘要（中文）

形式化数学推理对人工智能而言仍然是一个关键挑战，现有基准在范围和规模上存在局限性。为了解决这个问题，我们提出了FormalMATH，这是一个大规模的Lean4基准，包含5560个经过形式验证的问题，范围从高中奥林匹克竞赛挑战到本科水平的定理，涵盖代数、应用数学、微积分、数论和离散数学等多个领域。为了减轻手动形式化的低效率，我们引入了一种新颖的人在环自动形式化流程，该流程集成了：（1）用于语句自动形式化的专用大型语言模型（LLM），（2）多LLM语义验证，以及（3）使用基于现成LLM的证明器的基于否定的反证过滤策略。这种方法在人工验证之前保留了72.09%的语句，从而降低了专家注释成本，同时确保了对原始自然语言问题的忠实性。我们对最先进的基于LLM的定理证明器的评估揭示了重大局限性：即使是最强大的模型在实际采样预算下也仅达到16.46%的成功率，表现出明显的领域偏差（例如，擅长代数但在微积分中失败）并且过度依赖简化的自动化策略。值得注意的是，我们发现自然语言解决方案指导与思维链推理场景中的证明成功之间存在违反直觉的负相关关系，这表明人工编写的非正式推理在形式推理设置中引入了噪声而不是清晰度。我们相信FormalMATH为基准化形式化数学推理提供了一个强大的基准。

🔬 方法详解

问题定义：论文旨在解决大规模形式化数学推理基准的缺失问题。现有基准的规模和覆盖范围不足以充分评估大型语言模型（LLM）在形式化数学推理方面的能力。手动形式化过程耗时且成本高昂，阻碍了基准的构建和扩展。

核心思路：论文的核心思路是利用LLM自动生成形式化数学问题，并通过多重验证和过滤机制来保证生成质量，从而降低人工成本并构建大规模基准。同时，通过对现有LLM进行评估，揭示其在形式化数学推理方面的局限性。

技术框架：FormalMATH的构建流程包含以下几个主要阶段：1) 语句自动形式化：使用专门训练的LLM将自然语言数学问题转换为Lean4形式化语言。2) 多LLM语义验证：使用多个LLM对自动形式化语句进行语义一致性验证，减少错误。3) 基于否定的反证过滤：利用LLM证明器尝试证明语句的否定，如果成功则过滤掉该语句。4) 人工验证：对剩余语句进行人工验证，确保最终基准的正确性。

关键创新：该论文的关键创新在于提出了一种人机协同的自动形式化流程，该流程能够有效地降低人工成本，并保证生成基准的质量。此外，论文还揭示了自然语言指导与形式化证明成功之间的负相关关系，挑战了传统的思维链推理方法。

关键设计：在语句自动形式化阶段，使用了专门训练的LLM，并针对数学领域的特点进行了优化。在多LLM语义验证阶段，使用了多个不同的LLM，以提高验证的可靠性。在基于否定的反证过滤阶段，使用了现成的LLM证明器，并设置了合理的阈值来控制过滤的严格程度。

🖼️ 关键图片

img_0

📊 实验亮点

实验结果表明，即使是最强大的LLM在FormalMATH基准上的成功率也仅为16.46%，且存在显著的领域偏差。研究还发现，自然语言解决方案指导与证明成功之间存在负相关关系，这表明在形式化推理中，人类的非正式推理可能会引入噪声。该基准保留了72.09%的自动形式化语句，显著降低了人工成本。

🎯 应用场景

该研究成果可应用于开发更强大的数学推理AI系统，辅助数学研究和教育。FormalMATH基准能够促进LLM在形式化验证、定理证明等领域的应用，并推动AI在科学发现中的发展。未来，该基准可以扩展到其他形式化语言和数学领域。

📄 摘要（原文）

Formal mathematical reasoning remains a critical challenge for artificial intelligence, hindered by limitations of existing benchmarks in scope and scale. To address this, we present FormalMATH, a large-scale Lean4 benchmark comprising 5,560 formally verified problems spanning from high-school Olympiad challenges to undergraduate-level theorems across diverse domains (e.g., algebra, applied mathematics, calculus, number theory, and discrete mathematics). To mitigate the inefficiency of manual formalization, we introduce a novel human-in-the-loop autoformalization pipeline that integrates: (1) specialized large language models (LLMs) for statement autoformalization, (2) multi-LLM semantic verification, and (3) negation-based disproof filtering strategies using off-the-shelf LLM-based provers. This approach reduces expert annotation costs by retaining 72.09% of statements before manual verification while ensuring fidelity to the original natural-language problems. Our evaluation of state-of-the-art LLM-based theorem provers reveals significant limitations: even the strongest models achieve only 16.46% success rate under practical sampling budgets, exhibiting pronounced domain bias (e.g., excelling in algebra but failing in calculus) and over-reliance on simplified automation tactics. Notably, we identify a counterintuitive inverse relationship between natural-language solution guidance and proof success in chain-of-thought reasoning scenarios, suggesting that human-written informal reasoning introduces noise rather than clarity in the formal reasoning settings. We believe that FormalMATH provides a robust benchmark for benchmarking formal mathematical reasoning.