Evaluation of LLMs for Mathematical Formalization in Lean

作者: Tyson Klingner, Drew Bladek, Escher Crawford, Bohao Chen, Ariel Fu, Kaira Nair, Jarod Alper, Giovanni Inchiostro, Vasily Ilin

分类: cs.AI

发布日期: 2026-06-04

备注: 15 pages, 13 figures, 10 tables. Comments welcome!

💡 一句话要点

评估大型语言模型在Lean中的数学形式化能力

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

关键词: 大型语言模型 数学证明 Lean 4 模型评估 成本效益 自动定理证明 机器学习

📋 核心要点

现有大型语言模型在生成正式数学证明时的有效性和效率存在差异，影响了其在实际应用中的推广。
本文通过比较不同LLMs在Lean 4中的表现，提出了一种基于pass@$k$和refine@$k$的评估方法，旨在为研究者提供参考。
实验结果显示，Gemini 3.1 Pro和Claude Opus 4.7在成功率和成本效益上表现优异，推动了LLMs在数学证明生成中的应用潜力。

📝 摘要（中文）

近年来，大型语言模型（LLMs）在生成正式数学证明方面的能力显著提升。本文比较了多种LLMs在Lean 4中生成正式证明的有效性，旨在帮助希望利用LLMs支持项目的研究者。我们采用pass@$k$和refine@$k$指标作为比较基准，并在miniF2F和miniCTX数据集的子集上进行评估。测试结果表明，Gemini 3.1 Pro和Claude Opus 4.7表现最佳，前者在miniF2F上通过refine@32达到了92%的成功率，而后者在miniCTX上达到了86%的成功率。在考虑成本的情况下，NVIDIA Nemotron 3 Super和GPT-OSS 120B表现出较高的效率，准确率竞争力强，平均每个正确证明的成本低于0.01美元。

🔬 方法详解

问题定义：本文旨在评估不同大型语言模型在Lean 4中生成正式数学证明的能力，现有方法在有效性和成本方面存在不足，限制了其应用。

核心思路：通过对多种LLMs进行系统比较，采用pass@$k$和refine@$k$指标，提供量化的评估结果，帮助研究者选择合适的模型支持其项目。

技术框架：研究首先选择了多个LLMs进行测试，然后在miniF2F和miniCTX数据集上进行评估，最后通过分析成功率和成本效益得出结论。

关键创新：本文的创新在于系统性地比较了不同LLMs在数学证明生成中的表现，特别是在Lean 4环境下的应用，填补了相关领域的研究空白。

关键设计：在评估过程中，采用了pass@$k$和refine@$k$作为主要指标，确保了评估的全面性和准确性，同时考虑了模型的成本效益。实验中还对成功率进行了详细分析，确保结果的可靠性。

🖼️ 关键图片

fig_0

fig_1

fig_2

📊 实验亮点

实验结果显示，Gemini 3.1 Pro在miniF2F数据集上通过refine@32达到了92%的成功率，而Claude Opus 4.7在miniCTX上达到了86%的成功率。此外，NVIDIA Nemotron 3 Super和GPT-OSS 120B在成本效益方面表现突出，平均每个正确证明的成本低于0.01美元，显示出较高的效率。

🎯 应用场景

该研究的潜在应用领域包括数学教育、自动定理证明、以及计算机辅助证明等。通过提高LLMs在数学证明生成中的有效性，可以为研究人员和学生提供更强大的工具，促进数学研究和教育的发展。未来，随着模型的进一步优化，LLMs在更复杂的数学问题处理中的应用前景广阔。

📄 摘要（原文）

Within the past few years, the ability of Large Language Models (LLMs) to generate formal mathematical proofs has improved drastically. We provide a comparison of various LLMs' effectiveness in producing formal proofs in Lean 4 with the goal of assisting those seeking to use LLMs to support their own projects. We utilize both pass@$k$ and refine@$k$ metrics as the benchmark for our comparison and evaluate on subsets of both miniF2F and miniCTX datasets. Our testing shows that overall, Gemini 3.1 Pro and Claude Opus 4.7 perform best. Gemini 3.1 Pro achieved a 92\% success rate on miniF2F via refine@32 whereas Opus 4.7 achieved a 86\% success rate on miniCTX via refine@32. When taking cost into account, NVIDIA Nemotron 3 Super and GPT-OSS 120B were the most efficient, with competitive accuracies and average costs of $<\$0.01$ per correct proof.