Google DeepMind 用 Gemini 智能体发现并验证 Busy Beaver 新加速规则
DeepMind 让 Gemini 智能体自己挑数学问题做发现，11 台 BB(6) 图灵机的规则还过了 Lean 证明，论文可读性很高。
Google DeepMind 发布论文，一个基于 Gemini 的智能体在 BB(6)——Busy Beaver 问题的当前前沿——中为 11 台未解决的图灵机找到并形式化验证了新的加速规则。智能体自行挑选图灵机、从执行轨迹中发现模式、提出压缩多步执行的规则，每条规则都要经过非形式推理和 Lean 形式证明双重把关，只保留被证明的规则。作者将这些机器暂命名为 Cryptids：从空白纸带开始的运行已有精确描述，但是否停机仍未知。
Banger paper from Google DeepMind on open-ended math discovery with agents. This is one of the early, exciting works I have seen on autonomous AI-powered discoveries. (bookmark it) A Gemini-based agent found and formally verified new acceleration rules for eleven unresolved Turing machines in BB(6), the current frontier of the Busy Beaver problem. Busy Beaver is uncomputable, so no fixed list of problems exists. The agent has to pick machines, spot patterns in their execution traces, and propose compact rules that summarize many steps at once. Each proposed rule then goes through informal reasoning and a Lean proof. Only proved rules are kept, so the result does not depend on trusting the model's reasoning. The authors provisionally call these machines Cryptids. Their runs from a blank tape now have exact, compact descriptions, but whether they halt is still open. This is a good example of an agent producing new, formally checked mathematical results on problems it chose itself. arxiv.org/abs/2610.22603 Chat with Paper: academy.dair.ai/papers/at-the-… 💬 13 🔄 2 ❤️ 28 👀 2016 📊 15 ⚡
