arXiv cs.AI· Marco Dos Santos, Vivek Veeriah, Alex Havrilla, Andrew Bolt, Goran Zuzic, Satinder Singh, Tom Zahavy·· 11 小时前AI 评分52
面向 Busy Beaver 前沿：基于 Gemini 智能体流水线的自主数学发现
At the Limits of Computability: Steps Towards Autonomous AI Discovery on the Busy Beaver Frontier
AI 导读
论文提出一条基于 Gemini 的智能体流水线，在不可计算的 Busy Beaver 领域自动发现图灵机加速规则，把多步执行压缩为紧凑的数学规则。该系统整合模式识别、自动猜想、非形式化数学推理与 Lean 形式化定理证明，自主发现并形式化验证了 BB(6) 中 11 台机器的新型 Collatz 式加速。
正文 · AI 翻译
摘要：人工智能在数学领域的最新突破——从奥赛奖牌表现到解决长期悬而未决的公开猜想——迅速拓展了自动化系统所能达到的边界。然而这些成功主要涉及预先设定、由人类提出的问题，AI 系统如何自主发现数学结构并提出新问题仍悬而未决。为超越静态挑战，我们探索忙碌海狸（BB）领域，这是一个不可计算、本质上开放的前沿。由于没有任何算法能对每个 $n$ 计算忙碌海狸数 $\mathrm{BB}(n)$，该领域为通过数学猜想与证明进行持续探索提供了天然场景。本文中，我们提出一个基于 Gemini 的智能体流水线，可自动发现图灵机的加速，并以简洁的数学规则形式表达，概括许多执行步骤。我们的系统集成了模式识别、自动猜想、非形式数学推理以及 Lean 中的形式定理证明。借助该框架，我们的系统自主发现并形式验证了 $\mathrm{BB}(6)$ 中十一台机器的新颖类 Collatz 加速。在获得社区认可的前提下，我们暂将这些机器归类为 Cryptids，即空白纸带执行具有精确、简洁数学描述但其停机行为仍未解决的机器。这些结果推进了忙碌海狸前沿上 $\mathrm{BB}(6)$ 未决机器的分析，并展示了自主 AI 系统在基础计算机科学中进行开放式数学发现的潜力。
| 学科： | 人工智能（cs.AI）；形式语言与自动机理论（cs.FL） |
| 引用为： | arXiv:2610.22603 [cs.AI] |
| （或本版本的 arXiv:2610.22603v1 [cs.AI]） | |
| https://doi.org/10.48550/arXiv.2610.22603 由 DataCite 颁发的 arXiv DOI（待注册） |
提交历史
来自：Vivek Veeriah [查看邮箱]
[v1]
2026 年 10 月 15 日星期四 19:56:48 UTC（379 KB）
来源：arXiv cs.AI · arxiv.org