Determination of the fifth Busy Beaver value

这篇论文由 bbchallenge Collaboration 团队（包括 Justin Blanchard, Daniel Briggs, Georgi Georgiev (Skelet), Shawn Ligocki, mxdys, Tristan Stérin 等数十位贡献者）撰写，正式证明了 5 状态 2 符号图灵机的最大步数（Busy Beaver 值 $S(5)$）为 47,176,870。这是自 1962 年该问题提出以来，40 多年来首次确定新的 Busy Beaver 值，也是首个经过形式化验证（Formal Verification）的 Busy Beaver 值。

以下是该论文的详细技术总结：

1. 问题背景 (Problem)

• Busy Beaver 函数 $S(n)$：定义为在从全零带子开始运行时，能够执行最多步数并随后停止的 $n$ 状态 2 符号图灵机的步数。
• 不可计算性：$S(n)$ 是一个不可计算函数。如果 $S(n)$ 是可计算的，则可以通过模拟 $S(n)+1$ 步来解决停机问题。
• 历史现状：在本文之前，$S(1)$ 到 $S(4)$ 的值已被证明（分别为 1, 6, 21, 107）。对于 $S(5)$，自 1989 年 Heiner Marxen 和 Jürgen Buntrock 发现一个运行 47,176,870 步的机器以来，一直未确定是否有其他机器能超越它。
• 挑战：证明 $S(5)$ 需要分析所有可能的 5 状态机器，并确定它们是否停机。对于非停机机器，证明其“永不停机”极其困难，因为停机问题等价于许多著名的数学猜想（如哥德巴赫猜想）。

2. 方法论 (Methodology)

该研究采用了大规模协作与形式化验证相结合的方法，核心工具是 Coq 证明助手。

2.1 树形规范形式 (Tree Normal Form, TNF) 枚举

• 搜索空间缩减：5 状态 2 符号图灵机的语法总数约为 16.7 万亿（$1.67 \times 10^{13}$）。
• TNF 技术：通过引入“树形规范形式”，排除了不可达的转换和状态/符号的排列对称性。
• 结果：将需要分析的机器数量从 16.7 万亿大幅缩减至 181,385,789 台。这一枚举过程直接在 Coq 中实现并运行，确保了枚举的完整性。

2.2 判定器流水线 (Deciders Pipeline)

由于无法通过暴力模拟解决所有机器的停机问题（非停机机器可能运行极长时间），团队开发了一系列基于 闭带语言 (Closed Tape Language, CTL) 框架的判定器（Deciders）。这些判定器通过构建一个包含初始配置且对转换封闭的超集来证明机器永不停机。主要判定器包括：

1. Loops (循环检测)：检测机器是否进入循环（Cyclers）或平移循环（Translated Cyclers）。这是最基础的判定器，解决了约 95% 的非停机机器。
2. NGramCPS (n-gram 闭位置集)：基于 bbfind 的 CPS 技术改进，通过记录历史状态和符号对（n-gram）来构建状态空间。结合磁带符号增强（如固定长度历史或 LRU 历史），解决了绝大多数剩余的非停机机器。
3. RepWL (重复词列表)：将磁带内容视为正则表达式，检测重复出现的词块，构建正则配置图。
4. FAR (有限自动机归约)：一种“对偶 CTL"技术，寻找一个非确定性有限自动机（NFA）来接受所有最终停机的配置，并拒绝初始配置。
5. WFAR (加权有限自动机归约)：FAR 的扩展，使用加权自动机处理更复杂的非正则行为（如螺旋结构），解决了 17 台机器。

2.3 特殊机器处理 (Sporadic Machines)

有 13 台 机器（称为“零星机器”或 Sporadic Machines）无法被上述通用判定器解决，需要单独的非停机证明。这些机器表现出极其复杂的行为，例如：

• Skelet #1：在 $5.41 \times 10^{51}$ 步的混沌后进入平移循环。
• Skelet #10：实现双斐波那契计数器。
• Skelet #17：管理整数列表，涉及格雷码（Gray code）变换，被称为“最终 Boss"。
  这些机器的证明由团队成员（如 Kropitz, Ligocki, Yuen, Kądziołka, mxdys 等）手动构建，并在 Coq 中形式化验证。

2.4 形式化验证 (Coq-BB5)

• 所有逻辑、枚举算法和判定器均在 Coq 中实现。
• Coq-BB5 项目不仅验证了判定器的正确性，还直接运行了枚举算法。
• 证明过程利用了 Coq 的 native_compute 引擎和并行化编译，将编译时间从 13 小时缩短至 45 分钟（13 核）。
• 最终结果仅依赖于 Coq 标准库中一个广泛接受的公理（functional_extensionality_dep）。

3. 主要贡献与结果 (Key Contributions & Results)

3.1 核心定理

• $S(5) = 47,176,870$：证明了 1989 年发现的机器确实是 5 状态 Busy Beaver 冠军，且没有其他机器能超越它。
• $\Sigma(5) = 4,098$：证明了 5 状态机器停机时磁带上 1 的最大数量。
• $S(2, 4) = 3,932,964$：证明了 2 状态 4 符号图灵机的最大步数。
• $S(4) = 107$：重新形式化验证了 Brady 1983 年的结果，消除了原始证明中的不确定性。

3.2 数据产出

• 分析了 181,385,789 台 5 状态机器。
• 其中 133,005,895 台被证明永不停机。
• 48,379,894 台被证明停机（其中 183 台是长停机者，需模拟至 47,176,870 步）。
• 所有机器的停机状态和判定方法已提取并公开。

3.3 协作模式

• 展示了 大规模在线协作研究 的有效性。项目通过 Discord、Wiki 和 GitHub 聚集了数百名贡献者（包括学生、工程师和研究人员），在两年内完成了这一壮举。
• 这种“公开构建”（Build in public）的模式允许新贡献者基于现有成果快速迭代。

4. 意义与影响 (Significance)

1. 形式化验证的里程碑：这是第一个完全通过证明助手（Coq）验证的 Busy Beaver 值。它消除了对“人工证明”或“黑盒程序”的不信任，为计算复杂性理论中的极端问题提供了无可辩驳的证据。
2. 数学边界的探索：
   • 证明了 5 状态机器的停机问题在数学上是可解的，且不需要解决如哥德巴赫猜想等深层数论难题。
   • 指出真正的困难可能出现在 6 状态机器中。论文介绍了 "Cryptids"（神秘生物） 的概念，即那些停机问题极难（甚至可能独立于 ZF 公理系统）的机器。例如，6 状态的 "Antihydra" 机器与一个类似 Collatz 猜想的未解决问题相关。
3. AI 与自动推理的基准：Busy Beaver 问题生成的数学猜想（如 Antihydra 相关的猜想）已被纳入 Lean 形式化猜想数据集，作为测试 AI 推理能力的基准。Coq-BB5 的 100 个引理已被 AI 尝试证明，成功率为 58%。
4. 算法与计算理论：论文中开发的判定器（如 NGramCPS, WFAR）为分析图灵机的长期行为提供了新的数学工具，特别是处理非正则（Irregular）行为的能力。

5. 总结

这篇论文不仅解决了困扰数学界 40 多年的 $S(5)$ 问题，更重要的是展示了一种全新的科研范式：通过开源协作、形式化验证工具和算法创新，共同攻克理论计算机科学中的“不可能”任务。它标志着我们在理解计算极限和不可计算性方面迈出了坚实的一步，同时也为未来解决 $S(6)$ 及更复杂问题奠定了基础。