Ramanujan挑战赛结果：多格式证明AI评估流程
原文：Ramanujan Challenge Results: AI-Assisted Evaluation Pipeline for Multi-Format Proofs
随着AI数学能力的快速提升，有意义的基准正从大学水平问题和数学奥林匹克转向研究级数学。Ramanujan Challenge是一个由数论研究级问题组成的基准，包括未发表的结果和开放猜想。它提出了数学常数的具体公式，其正确性可以通过数值验证，而证明可能需要非显而易见的数学。在此，我们分析了该挑战的提交内容，衡量了不同AI模型、计算机代数系统（CAS）和形式化工具的相对成功率。我们发现了与官方解答在概念上不同的正确提交，以及一个已发表开放猜想的证明。评估提交内容暴露了第二个挑战：在大规模下可靠地评判复杂证明。我们引入了一个AI辅助评估流水线，用于自然语言证明、CAS代码和Lean形式化，评估语义和逻辑正确性。与传统的单次LLM判断相比，我们的流水线将自然语言证明的假阳性判定从23%降低到6%，并将对支持代码的判断准确率从46%提高到58%。该方法为大规模评估研究级数学提供了方法论，在数学和AI for Science领域具有潜在应用。作者：Alan Sorani, Ashvni Narayanan, Michael Shalyt, Tali Monderer, Rotem Kalisch。类别：cs.AI, cs.CL, cs.SC, math.NT