评测大模型在Lean 4中形式化数学命题的能力，选最优性价比方案
Evaluation of LLMs for Mathematical Formalization in Lean
- 用pass@k和refine@k指标对比多个大模型在Lean 4中的形式化能力
- Gemini 3.1 Pro在miniF2F上达92%成功率，Claude Opus 4.7在miniCTX上达86%
- NVIDIA Nemotron和GPT-OSS 120B成本低于$0.01/正确证明，效率最高
近年来，大型语言模型（LLMs）生成形式化数学证明的能力显著提升。本文比较了多种LLMs在Lean 4中生成形式化证明的有效性，旨在帮助研究者选择适合自身项目的工具。我们采用pass@$k$和refine@$k$作为评估指标，在miniF2F和miniCTX数据集的子集上进行测试。结果表明，Gemini 3.1 Pro和Claude Opus 4.7表现最佳：Gemini 3.1 Pro在miniF2F上通过refine@32达到92%成功率，Opus 4.7在miniCTX上通过refine@32达到86%成功率。从成本角度考虑，NVIDIA Nemotron 3 Super和GPT-OSS 120B最为高效，准确率可观且平均每条正确证明成本低于$0.01。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。