FormalProofBench：模型能否写出经过形式验证的研究生级数学证明？
FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?
AI总结：
FormalProofBench评估AI能否生成经过形式验证的研究生级数学证明，通过自然语言问题与Lean 4形式陈述配对，测试模型生成Lean证明的能力，结果显示最佳模型准确率为33.5%。
摘要：
我们提出了FormalProofBench，一个私有基准，用于评估AI模型能否生成经过形式验证的研究生级数学证明。每个任务配对一个自然语言问题与一个Lean~4形式陈述，模型必须输出一个被Lean 4检查器接受的Lean证明。FormalProofBench针对高级本科生和研究生数学，问题来源于资格考试和标准教材，涵盖分析、代数、概率和逻辑等主题。我们评估了多种前沿模型，并发现最佳基础模型的准确率为33.5%，性能在之后迅速下降。此外，我们还提供了工具使用、失败模式、成本和延迟的实证分析，从而全面评估了前沿模型的形式定理证明能力。
英文摘要：
We present FormalProofBench, a private benchmark designed to evaluate whether AI models can produce formally verified mathematical proofs at the graduate level. Each task pairs a natural-language problem with a Lean~4 formal statement, and a model must output a Lean proof accepted by the Lean 4 checker. FormalProofBench targets advanced undergraduate and graduate mathematics, with problems drawn from qualifying exams and standard textbooks across topics including analysis, algebra, probability, and logic. We evaluate a range of frontier models with an agentic harness, and find that the best-performing foundation model achieves 33.5% accuracy, with performance dropping rapidly after that. In addition to the accuracy numbers, we also provide empirical analysis of tool-use, failure modes, cost and latency, thereby providing a thorough evaluation of the formal-theorem proving abilities of frontier models.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
