DeepMind 用 Gemini 智能体在 Busy Beaver 前沿发现并形式化验证 11 台新图灵机
omarsar0 · x · 2026-10-20
Google DeepMind 发布论文《At the Limits of Computability》，展示了一条面向开放式数学发现的自主 AI 管线。
- 基于 Gemini 的智能体系统在 Busy Beaver 问题当前前沿 BB(6) 上，自主发现并经 Lean 形式化验证了 11 台未决图灵机的新型 Collatz 式「加速规则」。
- 工作流程：智能体自行挑选机器、在执行轨迹中识别模式、提出能压缩大量执行步骤的紧凑数学规则，再经非形式推理与 Lean 定理证明，只保留被证明的规则，因此结论不依赖对模型推理的信任。
- 由于 Busy Beaver 数不可计算，该领域天然「开放式」：没有固定的问题清单，智能体必须自己发现并定义新问题——这正是与以往解人类预设问题的 AI 数学研究的关键区别。
- 团队将这些机器暂命名为 Cryptids：它们的空带执行已有精确紧凑的数学描述，但是否停机仍未解决。
- 作者认为这是 AI 系统在基础计算机科学中进行开放式数学发现潜力的重要示范。
「漫话AGI」频道最新
- DeepMind 研究员更新 AI 对齐资源清单，覆盖对齐与控制全谱系 — vkrakovna · 2026-10-20
- AI Agent 评测中入侵 Hugging Face，法律如何追责成难题 — ChuckDBrooks · 2026-10-20
- PostHog 称初级开发者岗位已死，转向「Product Engineer」招聘模式 — jamesbrooksco · 2026-10-20
- 经济学教授讽高校 AI 观点文：反 AI 抄袭却用 AI 代笔 — paulnovosad · 2026-10-20
- AI 克隆太高效，独立开发者不敢再公开试玩版 — Ars Technica AI · 2026-10-20
- 15 国领袖重聚冰岛 Höfði 屋，对话 AI 全球协调 — GregCook2011 · 2026-10-20