Ramanujan Challenge 结果发布：AI 辅助多格式数学证明评估流水线

Ramanujan Challenge Results: AI-Assisted Evaluation Pipeline for Multi-Format Proofs

AI 导读

团队公布 Ramanujan Challenge 基准结果，该基准由研究级数论问题构成，含未发表结果和公开猜想，并分析了各 AI 模型、计算机代数系统和形式化工具的表现。提交中出现了与官方解答思路不同的正确证明，并证明了其中一个已发表的公开猜想。团队还提出 AI 辅助评估流水线，将自然语言证明的误报率从 23% 降至 6%，辅助代码判断准确率从 46% 提升至 58%。

推荐理由

论文提出研究级数学基准和 AI 辅助评审流程，把自然语言证明误判率从 23% 降到 6%，方法可迁移到大模型输出的规模化评估。

正文 · AI 翻译

作者：Alan Sorani、Ashvni Narayanan、Michael Shalyt、Tali Monderer、Rotem Kalisch、Hila Barkan、Elyasheev Leibtag、Shachar Weinbaum、Carsten Schneider、John Campbell、Ido Kaminer

查看 PDF HTML（实验性）

摘要：随着 AI 的数学能力快速提升，有意义的基准正从大学水平的题目和数学奥林匹克转向研究级数学。Ramanujan Challenge 是一个由研究级数论问题组成的基准，其中包括未发表的结果和公开猜想。它给出了数学常数的具体公式，其正确性可以通过数值检验，而其证明可能需要非显而易见的数学方法。我们分析了本次挑战的提交结果，衡量了不同 AI 模型、计算机代数系统（CAS）和形式化工具的相对成功率。我们发现了在概念上与官方解答不同的正确提交，以及对其中一个已发表公开猜想的证明。对这些提交的评估暴露了第二个挑战：如何可靠地大规模评判复杂的证明。我们引入了一套 AI 辅助的评估流水线，针对自然语言证明、CAS 代码和 Lean 形式化，评估其语义和逻辑正确性。与传统的单次 LLM 评判相比，我们的流水线将自然语言证明的误判率从 23% 降至 6%，并将辅助代码评判的准确率从 46% 提升至 58%。这一方法为大规模评估研究级数学提供了一种方法论，在数学以及 AI for Science 领域具有潜在应用。

学科分类：	人工智能 (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 通过 DataCite 获取 arXiv 签发的 DOI

提交历史

来自：Ashvni Narayanan [查看邮件]
[v1] 2026年10月29日星期四 17:39:04 UTC (301 KB)