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·· 2 小时前精选AI 评分69
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%，方法可迁移到大模型输出的规模化评估。
正文 · 原文
Authors:Alan Sorani, Ashvni Narayanan, Michael Shalyt, Tali Monderer, Rotem Kalisch, Hila Barkan, Elyasheev Leibtag, Shachar Weinbaum, Carsten Schneider, John Campbell, Ido Kaminer
Abstract:As AI's mathematical capabilities rapidly improve, meaningful benchmarks are shifting from university-level problems and math olympiads to research-level mathematics. The Ramanujan Challenge is a benchmark comprised of research-level problems in number theory, including unpublished results and open conjectures. It presented concrete formulas for mathematical constants whose correctness can be checked numerically, while their proofs may require non-obvious mathematics. Here, we analyze the Challenge submissions, measuring the relative success of different AI models, Computer Algebra Systems (CAS), and formal tools. We find correct submissions that are conceptually distinct from the official solutions, and a proof of one of the published open conjectures. Evaluating the submissions exposed a second challenge: judging complex proofs reliably at scale. We introduce an AI-assisted evaluation pipeline for natural language proofs, CAS code, and Lean formalizations that assesses semantic and logical correctness. Compared with the conventional one-shot LLM judgment, our pipeline reduces false-positive verdicts on natural language proofs from 23% to 6% and improves judgment accuracy on supporting code from 46% to 58%. This approach provides a methodology for evaluating research-level mathematics at scale, with potential applications across mathematics and AI for science.
| Subjects: | Artificial Intelligence (cs.AI); Computation and Language (cs.CL); Symbolic Computation (cs.SC); Number Theory (math.NT) |
| Cite as: | arXiv:2610.40551 [cs.AI] |
| (or arXiv:2610.40551v1 [cs.AI] for this version) | |
| https://doi.org/10.48550/arXiv.2610.40551 arXiv-issued DOI via DataCite |
Submission history
From: Ashvni Narayanan [view email]
[v1]
Thu, 29 Oct 2026 17:39:04 UTC (301 KB)
来源：arXiv cs.AI · arxiv.org