LEAN-GitHub：用于通用 LEAN 证明器编译的 GitHub LEAN 仓库
人工智能
2024-07-25 v1 计算与语言
摘要
最近，大型语言模型在辅助形式化数学推理方面呈现出有前景的成果。然而，其性能受限于形式化定理证明数据的稀缺，这需要额外的努力从原始形式语言语料库中提取。与此同时，大量人类编写的形式语言语料库仍未得到充分利用。为此，我们提出了 LEAN-GitHub，一个由从 GitHub 上几乎所有 Lean 4 仓库中提取的大规模形式数据组成的数据集。经过在该数据集上微调的 InternLM-math-plus 在 Lean 4 miniF2F 测试中实现 48.8% 的单次通过率和 54.5% 的 64 次通过率，超越了当前最先进的方法的 52%。它还在两个其他 Lean 4 基准测试（ProofNet 和 Putnam）上实现了最先进成绩，这些基准测试针对不同的数学领域/水平。这些结果表明，我们提出的数据集对广泛数学主题上的形式推理具有益处。我们将我们的模型开源于 https://GitHub.com/InternLM/InternLM-Math 及我们的数据开源于 https://huggingface.co/datasets/InternLM/Lean-GitHub。
引用
@article{arxiv.2407.17227,
title = {LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover},
author = {Zijian Wu and Jiayu Wang and Dahua Lin and Kai Chen},
journal= {arXiv preprint arXiv:2407.17227},
year = {2024}
}