FMC: Formalization of Natural Language Mathematical Competition Problems

📄 arXiv: 2507.11275v1 📥 PDF

作者: Jiaxuan Xie, Chengwu Liu, Ye Yuan, Siqi Li, Zhiping Xiao, Ming Zhang

分类: cs.CL

发布日期: 2025-07-15

备注: Accepted in ICML 2025 AI4MATH Workshop

💡 一句话要点

提出基于大语言模型和误差反馈的自动形式化方法，构建奥林匹克级数学题形式化数据集。

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

关键词: 自动形式化 大语言模型 误差反馈 形式化验证 定理证明 数学推理 Lean

📋 核心要点

  1. 现有形式化方法依赖人工标注，成本高昂且效率低下，难以处理大规模自然语言数学问题。
  2. 论文提出一种基于大语言模型和误差反馈的自动形式化流程，无需训练，实现自然语言到形式化语言的转换。
  3. 实验表明，该方法构建的数据集质量较高，可作为自动定理证明器的基准，并验证了误差反馈等策略的有效性。

📝 摘要（中文）

本文提出了一种基于大语言模型和误差反馈的自动形式化流程，旨在构建大规模自然语言数学问题及其形式化语言数据集，从而推进形式化数学推理的研究。该流程无需训练，完全自动化。利用此流程，作者构建了一个奥林匹克级别的自然语言问题与Lean形式化语言对齐的数据集，包含3922个自然语言数学问题和9787个Lean形式化问题，其中64.46%被评估为至少高于平均水平，适合作为自动定理证明器的基准。此外，研究还探讨了各种大语言模型的形式化和推理能力，并实验证明了少样本学习、误差反馈和增加采样数量可以增强自动形式化过程。在数据集上进行的自动定理证明器实验也突显了其挑战性，并证明了其作为形式推理任务基准的价值。

🔬 方法详解

问题定义：论文旨在解决自然语言数学题自动形式化的问题。现有方法主要依赖人工标注，耗时耗力，难以扩展到大规模数据集，阻碍了形式化数学推理的发展。因此，需要一种高效、自动化的方法将自然语言数学题转换为形式化语言。

核心思路：论文的核心思路是利用大语言模型强大的自然语言理解和生成能力，结合误差反馈机制，迭代优化形式化结果。通过让大语言模型生成形式化代码，并根据验证结果进行修正，逐步提高形式化的准确性和可靠性。

技术框架：该自动形式化流程主要包含以下几个阶段： 1. 问题输入：输入自然语言描述的数学问题。 2. 大语言模型生成：使用大语言模型（如GPT-3）生成对应的Lean形式化代码。 3. 形式化验证：使用Lean定理证明器对生成的代码进行验证，判断其是否正确。 4. 误差反馈：如果验证失败，则将错误信息反馈给大语言模型，指导其进行修正。 5. 迭代优化：重复步骤2-4，直到形式化代码通过验证或达到最大迭代次数。

关键创新：该方法最重要的创新点在于： 1. 全自动流程：无需人工干预，完全依赖大语言模型和误差反馈实现自动形式化。 2. 误差反馈机制：利用形式化验证的结果指导大语言模型进行修正，有效提高了形式化的准确性。 3. 训练自由：该方法无需针对特定数据集进行训练，具有良好的泛化能力。

关键设计：论文中，关键的设计包括： 1. 大语言模型的选择：选择了具有强大自然语言理解和生成能力的大语言模型，如GPT-3。 2. 误差反馈的格式：将Lean定理证明器的错误信息以结构化的方式反馈给大语言模型，方便其理解和修正。 3. 迭代次数的设置：设置了最大迭代次数，以避免无限循环。

🖼️ 关键图片

img_0

📊 实验亮点

实验结果表明，该方法构建的数据集质量较高，64.46%的数据被评估为至少高于平均水平。通过少样本学习、误差反馈和增加采样数量，可以显著提高自动形式化的准确率。在数据集上进行的自动定理证明器实验也验证了该数据集的挑战性，并突显了其作为形式推理任务基准的价值。

🎯 应用场景

该研究成果可应用于自动定理证明、形式化验证、数学教育等领域。自动形式化方法能够降低形式化验证的门槛，提高验证效率，促进形式化方法在软件和硬件系统验证中的应用。此外，该数据集可作为自动定理证明器的基准，推动相关技术的发展。在数学教育方面，该技术可以辅助学生理解数学概念，提高解题能力。

📄 摘要（原文）

Efficient and accurate autoformalization methods, which leverage large-scale datasets of extensive natural language mathematical problems to construct formal language datasets, are key to advancing formal mathematical reasoning. In this paper, we propose an autoformalization pipeline based on large language models with error feedback, achieving a fully automatic and training-free formalization approach. Using this pipeline, we curate an Olympiad-level dataset aligning natural language problems with Lean formalizations. The dataset comprises $3,922$ mathematical problems in natural language and $9,787$ in Lean, of which $64.46\%$ were assessed as at least above-average quality, making it suitable as a benchmark for automated theorem provers. Additionally, we investigate the formalization and reasoning capabilities of various LLMs and empirically demonstrate that few-shot learning, error feedback, and increasing sampling numbers enhance the autoformalization process. Experiments of three automated theorem provers on the \dataset\ dataset also highlight its challenging nature and its value as a benchmark for formal reasoning tasks.