LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover

📄 arXiv: 2407.17227v1 📥 PDF

作者: Zijian Wu, Jiayu Wang, Dahua Lin, Kai Chen

分类: cs.AI, cs.CL

发布日期: 2024-07-24

💡 一句话要点

提出LEAN-GitHub数据集，提升Lean定理证明器在数学推理上的性能

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

关键词: 形式化定理证明 Lean 4 数据集 大语言模型 数学推理 InternLM GitHub

📋 核心要点

  1. 形式化定理证明数据稀缺限制了大语言模型在数学推理方面的性能，而大量人工编写的形式化语言语料库未被充分利用。
  2. LEAN-GitHub数据集旨在通过收集GitHub上大量的Lean 4代码，为形式化定理证明提供更丰富的训练数据。
  3. 在LEAN-GitHub上微调的InternLM-math-plus模型在多个Lean 4基准测试中取得了领先的性能，验证了数据集的有效性。

📝 摘要（中文）

本文提出了LEAN-GitHub，一个从GitHub上几乎所有Lean 4仓库中提取的大规模形式化数据的数据集。为了验证数据集的有效性，研究者在LEAN-GitHub上微调了InternLM-math-plus模型。实验结果表明，该模型在Lean 4 miniF2F测试集上，单次通过的准确率达到48.8%，64次通过的准确率达到54.5%，超过了现有最佳方法52%的准确率。此外，该模型在另外两个Lean 4基准测试（ProofNet和Putnam）上也取得了当前最佳的性能，证明了所提出的数据集对广泛数学主题的形式化推理有益。模型和数据均已开源。

🔬 方法详解

问题定义：现有的大语言模型在形式化数学推理方面表现出潜力，但受限于高质量形式化定理证明数据的匮乏。人工编写的形式化语言语料库虽然存在，但提取和利用这些数据需要大量额外的工作。因此，如何有效地利用现有的形式化语言语料库，提升大语言模型在形式化数学推理方面的能力，是一个亟待解决的问题。

核心思路：本文的核心思路是从GitHub上收集大量的Lean 4代码，构建一个大规模的形式化数据集LEAN-GitHub。通过在这个数据集上训练大语言模型，可以提升模型在形式化定理证明方面的能力。这种方法的核心在于利用开源社区的力量，收集和整理现有的形式化知识，从而为大语言模型提供更丰富的训练数据。

技术框架：该研究的技术框架主要包括以下几个步骤：1) 从GitHub上爬取Lean 4仓库；2) 对爬取到的代码进行清洗和整理，构建LEAN-GitHub数据集；3) 在LEAN-GitHub数据集上微调InternLM-math-plus模型；4) 在多个Lean 4基准测试上评估模型的性能。

关键创新：该研究的关键创新在于构建了LEAN-GitHub数据集，这是一个大规模的、高质量的Lean 4代码数据集。与以往的研究相比，LEAN-GitHub数据集包含了更广泛的数学主题和更丰富的形式化知识，可以为大语言模型提供更有效的训练数据。

关键设计：该研究的关键设计包括：1) 数据集的构建策略，如何有效地从GitHub上爬取和整理Lean 4代码；2) 模型的微调策略，如何选择合适的预训练模型和微调参数，以获得最佳的性能；3) 评估指标的选择，如何选择合适的基准测试和评估指标，以全面评估模型的性能。

🖼️ 关键图片

fig_0
fig_1
fig_2

📊 实验亮点

实验结果表明，在LEAN-GitHub数据集上微调的InternLM-math-plus模型在Lean 4 miniF2F测试集上取得了显著的性能提升，单次通过的准确率达到48.8%，64次通过的准确率达到54.5%，超过了现有最佳方法52%的准确率。此外，该模型在ProofNet和Putnam两个Lean 4基准测试上也取得了当前最佳的性能。

🎯 应用场景

LEAN-GitHub数据集和基于其训练的模型可以应用于形式化定理证明、数学知识发现、自动化代码生成等领域。该研究有助于提升人工智能在数学领域的应用水平，并为开发更智能的数学工具提供支持。未来，可以进一步探索如何利用LEAN-GitHub数据集来改进其他形式化语言的推理能力。

📄 摘要（原文）

Recently, large language models have presented promising results in aiding formal mathematical reasoning. However, their performance is restricted due to the scarcity of formal theorem-proving data, which requires additional effort to be extracted from raw formal language corpora. Meanwhile, a significant amount of human-written formal language corpora remains underutilized. To address this issue, we propose LEAN-GitHub, a dataset consisting of large-scale formal data extracted from almost all Lean 4 repositories on GitHub. After fine-tuning InternLM-math-plus on this dataset, our model achieved accuracies of 48.8% with a single pass and 54.5% with 64 passes on the Lean 4 miniF2F test, surpassing state-of-the-art method at 52%. And it also achieves state-of-the-art on two other Lean 4 benchmarks (ProofNet and Putnam) targeting different fields/levels of math. These results demonstrate that our proposed dataset is beneficial for formal reasoning on a wide range of math topics. We open-source our model at https://GitHub. com/InternLM/InternLM-Math and our data at https://huggingface.co/ datasets/InternLM/Lean-GitHub