摘要
近年来，大语言模型生成形式化数学证明的能力显著提升。本文对比了多种大语言模型在 Lean 4 中生成形式化证明的有效性，旨在辅助相关项目研究。研究采用 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 美元。
AI 推荐理由
论文核心评估 LLM 在形式化数学证明中的推理能力，直接对应逻辑与数学推理主题。
研究机构
Math AI Lab, University of Washington, Seattle, WA, USA
论文信息