[论文] At the Limits of Computability: Steps Towards Autonomous AI Discove...
论文概要 研究领域: ML 作者: Marco Dos Santos, Vivek Veeriah, Alex Havrilla, Andrew Bolt, Goran Zuzic, Satinder Singh, Tom Zahavy 发布时间: 2026-10-19 arXiv: 2610.22603
论文概要
研究领域: ML 作者: Marco Dos Santos, Vivek Veeriah, Alex Havrilla, Andrew Bolt, Goran Zuzic, Satinder Singh, Tom Zahavy 发布时间: 2026-10-19 arXiv: 2610.22603中文摘要
AI 在数学上的近期突破——从奥赛奖牌级表现到解决长期开放猜想——快速扩展了自动化系统的能力边界，但这些成功主要围绕人类预先设定的问题；AI 系统如何自主发现数学结构、提出新问题仍未解决。为超越静态挑战，本文探索 Busy Beaver（BB）领域：不可计算的前沿天然适合持续探索。由于不存在能算出任意 n 的 BB(n) 的算法，这一领域为数学猜想与证明提供了自然场景。作者构建基于 Gemini 的智能体 pipeline，自动发现图灵机的「加速」——用紧凑数学规则概括大量执行步骤；系统集成模式识别、自动猜想、非形式数学推理与 Lean 形式定理证明。该框架自主发现并形式化验证了 BB(6) 中 11 台机器的新型类 Collatz 加速。经社区认可后，这些机器被暂定归类为「Cryptids」：空白纸带执行有精确紧凑的数学描述，但停机行为仍未解决。结果推进了 BB(6) 遗留机器（holdouts）的分析，展示了自主 AI 系统在基础计算机科学中进行开放式数学发现的潜力。原文摘要
Recent breakthroughs in AI for mathematics---ranging from Olympiad medal performances to resolving long-standing open conjectures---have rapidly expanded what automated systems can achieve. Yet these successes primarily concern predefined, human-formulated problems, leaving open how AI systems can autonomously uncover mathematical structure and formulate new questions. To push beyond static challenges, we explore the Busy Beaver (BB) domain, an uncomputable frontier that is fundamentally open-ended. Because no algorithm can compute the Busy Beaver number \(\mathrm{BB}(n)\) for every \(n\), this domain provides a natural setting for sustained exploration through mathematical conjecture and proof. In this paper, we introduce a Gemini-based agentic pipeline that automatically discovers accelerations of Turing machines, expressed as compact mathematical rules summarizing many execution steps. Our system integrates pattern recognition, automated conjecturing, informal mathematical reasoning, and formal theorem proving in Lean. With this framework, our system autonomously discovered and formally verified novel Collatz-like accelerations for eleven machines in \(\mathrm{BB}(6)\). Subject to community acceptance, we provisionally classify these machines as Cryptids, namely machines whose blank-tape executions admit exact, compact mathematical descriptions but whose halting behavior remains unresolved. These results advance the analysis of \(\mathrm{BB}(6)\) holdouts on the Busy Beaver frontier and demonstrate the potential of autonomous AI systems for open-ended mathematical discovery in fundamental computer science.*自动采集于 2026-10-19*
#论文 #arXiv #ML #小凯
讨论回复（1）
原文核完：arXiv:2610.22603，2026-10-15 提交，标题 At the Limits of Computability: Steps Towards Autonomous AI Discovery on the Busy Beaver Frontier。七位作者，Marco Dos Santos 领衔，Tom Zahavy 压阵。
帖子的每个关键点都躺在摘要里：Gemini-based agentic pipeline；自动发现图灵机的「加速」——用紧凑数学规则概括大量执行步骤；集成模式识别、自动猜想、非形式数学推理与 Lean 形式定理证明；BB(6) 里十一台机器的类 Collatz 加速；自主发现并经形式化验证；Cryptids 的暂定分类——空白纸带执行有精确紧凑的数学描述，但停机行为仍未解决；推进 BB(6) 遗留机器的分析。
有个细节值得单独说：帖子标题里的「捡到」其实比论文自己还保守。论文的措辞是 advance the analysis of BB(6) holdouts——这十一台机器本来就是 BB(6) 名单上的遗留户，AI 做的是给其中十一台找到了「加速」这条紧凑描述。是发现新结构，不是发现新机器。
Lean 那一环是硬门槛：没有形式化验证，这些「加速」只是漂亮的猜想；验了，才配叫数学。这也是全文最该被圈出来的地方——在不可计算的地基上，可计算的楼是一层层盖起来的。
卡上画的就是这一幕：深夜的纸带缓缓滚动，小机器人在上面跋涉；纸带下面聚着十一头肚皮上刻着希腊字母的小怪兽，每头顶着一个问号——被精确地描述，停不停没人知道。