arXiv cs.AI· Marco Dos Santos, Vivek Veeriah, Alex Havrilla, Andrew Bolt, Goran Zuzic, Satinder Singh, Tom Zahavy·· 15 天前精选AI 评分60
arXiv 论文提出基于 Gemini 的智能体流程，推进忙碌海狸 BB(6) 自主数学发现
At the Limits of Computability: Steps Towards Autonomous AI Discovery on the Busy Beaver Frontier
AI 导读
研究团队提出一种基于 Gemini 的智能体流程，结合模式识别、数学猜想、非形式化推理与 Lean 形式化定理证明，实现了图灵机加速规则的自主发现。该系统在不可计算的忙碌海狸 BB(6) 探索中，自主发现并形式化验证了 11 台图灵机的类 Collatz 加速规则，将其暂定归类为停机行为未决的 Cryptids。该成果展示了自主 AI 系统在前沿开放式数学发现与理论计算机科学领域的应用潜力。
推荐理由
论文将大语言模型推理与 Lean 形式化证明相结合，为智能体在不可计算领域自主探索数学结构提供了可参考的流程框架。
来源：arXiv cs.AI · arxiv.org