A Lean Dataset for International Math Olympiad: Small Steps towards Writing Math Proofs for Hard Problems

📄 arXiv: 2411.18872v2 📥 PDF

作者: Roozbeh Yousefzadeh, Xuenan Cao, Azim Ospanov

分类: cs.LG

发布日期: 2024-11-28 (更新: 2025-03-03)

🔗 代码/项目: GITHUB

💡 一句话要点

构建国际数学奥赛Lean证明数据集，推动AI自动数学证明研究

🎯 匹配领域: 支柱五：交互与反应 (Interaction & Reaction)

关键词: 形式化证明 Lean 国际数学奥林匹克 数据集构建 AI数学推理

📋 核心要点

  1. 现有AI在数学证明方面面临挑战，尤其是在形式化证明语言（如Lean）的自动生成上，缺乏高质量的训练数据和评估基准。
  2. 该研究通过人工编写IMO问题的Lean形式化证明，并将其分解为更小的引理，构建了一个新的数据集，旨在促进AI模型在数学证明方面的学习和评估。
  3. 该数据集包含5880行Lean证明和1329个引理，为评估和诊断AI模型在数学证明方面的能力提供了新的资源，并对SOTA LLM进行了初步评估。

📝 摘要（中文）

利用人工智能编写数学问题的形式化证明是一项具有挑战性的任务，近年来取得了一些进展。Lean等自动化系统可以验证用形式化语言编写的证明的正确性，但对人类和机器来说，用形式化语言编写证明可能具有挑战性。miniF2F基准测试集包含20个IMO问题，但只有6个问题有形式化证明（其中3个仅由数学家编写）。目前最佳的模型只能证明20个IMO问题中的2个，且其训练集是保密的。本文为剩余的IMO问题以及2022年和2023年的3个额外问题编写了完整的、原创的Lean形式化证明。这项工作通过创建5880行Lean证明，扩展了当前公共领域中可用的证明。本文的目标是通过提供一个评估基准，为开发能够自动编写miniF2F及其他所有IMO问题的形式化证明的AI模型铺平道路。为此，我们设计了一种方法将这些问题的证明分解为构建块，构建了一个包含1329个引理的数据集，其中包含超过4万行Lean代码。这些引理并非微不足道，但易于理解，为评估和诊断AI模型的失败和成功提供了机会。我们在我们的数据集上评估了SOTA LLM的能力，并从不同的角度分析了它们的成功和失败模式。我们的数据集和代码可在https://github.com/roozbeh-yz/IMO-Steps获得。

🔬 方法详解

问题定义：该论文旨在解决AI自动生成数学形式化证明的问题，特别是在国际数学奥林匹克（IMO）级别的问题上。现有方法的痛点在于缺乏足够规模和质量的形式化证明数据集，特别是使用Lean等形式化语言编写的证明，这限制了AI模型在该领域的训练和评估。

核心思路：论文的核心思路是通过人工编写IMO问题的Lean形式化证明，并将其分解为更小的、可管理的引理（lemmas）。这种分解使得问题更易于理解和解决，同时也为AI模型提供了更细粒度的学习目标。通过构建包含大量引理的数据集，为AI模型提供了一个学习和评估的平台。

技术框架：该研究的技术框架主要包括以下几个步骤：1) 人工编写IMO问题的完整Lean形式化证明；2) 将这些证明分解为一系列引理，每个引理代表证明中的一个逻辑步骤；3) 构建包含这些引理的数据集，并提供相应的Lean代码；4) 使用该数据集评估现有SOTA LLM在数学证明方面的能力，并分析其成功和失败模式。

关键创新：该研究的关键创新在于构建了一个专门针对IMO问题的Lean形式化证明数据集，并将其分解为引理级别。这种分解不仅降低了问题的难度，也为AI模型提供了更细粒度的学习目标。此外，该研究还对SOTA LLM在数学证明方面的能力进行了初步评估，并分析了其局限性。

关键设计：该研究的关键设计包括：1) 选择IMO问题作为研究对象，因为它们具有挑战性且具有代表性；2) 使用Lean作为形式化证明语言，因为它具有强大的验证能力；3) 将证明分解为引理，以便于AI模型学习和评估；4) 使用SOTA LLM作为评估对象，以了解现有AI模型在数学证明方面的能力。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

该研究构建了一个包含5880行Lean证明和1329个引理的IMO问题数据集，显著扩展了公开可用的形式化证明资源。通过对SOTA LLM的初步评估，揭示了现有模型在复杂数学证明方面的局限性，为未来研究指明了方向。

🎯 应用场景

该研究成果可应用于开发自动数学证明系统，辅助数学家进行研究，并用于数学教育，帮助学生理解和掌握数学证明的技巧。此外，该数据集和方法论也可推广到其他需要形式化验证的领域，如软件验证和硬件验证。

📄 摘要（原文）

Using AI to write formal proofs for mathematical problems is a challenging task that has seen some advancements in recent years. Automated systems such as Lean can verify the correctness of proofs written in formal language, yet writing the proofs in formal language can be challenging for humans and machines. The miniF2F benchmark has 20 IMO problems in its test set, yet formal proofs are available only for 6 of these problems (3 of which are only written by mathematicians). The model with best accuracy can only prove 2 of these 20 IMO problems, from 1950s and 60s, while its training set is a secret. In this work, we write complete, original formal proofs for the remaining IMO problems in Lean along with 3 extra problems from IMO 2022 and 2023. This effort expands the availability of proof currently in the public domain by creating 5,880 lines of Lean proof. The goal of the paper is to pave the way for developing AI models that can automatically write the formal proofs for all the IMO problems in miniF2F and beyond by providing an evaluation benchmark. In this pursuit, we devise a method to decompose the proofs of these problems into their building blocks, constructing a dataset of 1,329 lemmas with more than 40k lines of Lean code. These lemmas are not trivial, yet they are approachable, providing the opportunity to evaluate and diagnose the failures and successes of AI models. We evaluate the ability of the SOTA LLMs on our dataset and analyze their success and failure modes from different perspectives. Our dataset and code is available at: https://github.com/roozbeh-yz/IMO-Steps.