arXiv cs.AI· Alan Sorani, Ashvni Narayanan, Michael Shalyt, Tali Monderer, Rotem Kalisch, Hila Barkan, Elyasheev Leibtag, Shachar Weinbaum, Carsten Schneider, John Campbell, Ido Kaminer·· 13 小时前AI 评分42
Ramanujan Challenge 结果：面向多格式证明的 AI 辅助评估流水线
Ramanujan Challenge Results: AI-Assisted Evaluation Pipeline for Multi-Format Proofs
AI 导读
Ramanujan Challenge 提交分析显示，不同 AI 模型、计算机代数系统（CAS）与形式化工具均取得部分正确结果，其中包括与官方解答概念不同的正确证明，以及对一项已公开开放猜想给出的证明。
正文 · AI 翻译
作者：Alan Sorani、Ashvni Narayanan、Michael Shalyt、Tali Monderer、Rotem Kalisch、Hila Barkan、Elyasheev Leibtag、Shachar Weinbaum、Carsten Schneider、John Campbell、Ido Kaminer
摘要：随着 AI 的数学能力快速提升，有意义的基准正从大学水平的问题和数学奥林匹克竞赛转向研究级数学。Ramanujan Challenge 是一个由数论研究级问题组成的基准，其中包括未发表的结果和开放猜想。它为数学常数给出了具体公式，其正确性可以通过数值方式检验，而证明这些公式可能需要非显而易见的数学。在此，我们分析了该挑战的提交内容，衡量了不同 AI 模型、计算机代数系统（CAS）和形式化工具的相对成功程度。我们发现了与官方解答在概念上不同的正确提交，以及一个已发表开放猜想的证明。评估这些提交暴露了第二个挑战：在大规模下可靠地评判复杂证明。我们引入了一个 AI 辅助的评估流水线，用于自然语言证明、CAS 代码和 Lean 形式化，以评估语义和逻辑正确性。与传统的单次 LLM 判断相比，我们的流水线将自然语言证明的假阳性判定从 23% 降至 6%，并将对支撑代码的判断准确率从 46% 提升至 58%。该方法为大规模评估研究级数学提供了一套方法论，并有望在数学和科学 AI 领域得到应用。
| 学科： | 人工智能（cs.AI）；计算与语言（cs.CL）；符号计算（cs.SC）；数论（math.NT） |
| 引用为： | arXiv:2610.40551 [cs.AI] |
| （或 arXiv:2610.40551v1 [cs.AI] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2610.40551 arXiv 颁发的 DOI 通过 DataCite |
提交历史
来自：Ashvni Narayanan [查看电子邮件]
[v1]
2026年10月29日星期四 17:39:04 UTC（301 KB）
来源：arXiv cs.AI · arxiv.org