40 年图灵机难题被业余玩家攻破，陶哲轩评价“软件辅助证明改变数学研究规则”

40 多年的计算机难题 —— 忙碌海狸难题，被一群业余爱好者攻破了！

数学大佬陶哲轩转发了这一消息，并欣慰表示：

这再一次体现了证明助手对于数学研究的协作是多么有用。

计算机科学家 Scott Aaronson 为此还写了一篇博文，并大肆赞赏：

这个发现是自 1983 年以来，忙碌海狸函数研究中最重要的进展。

具体而言，人们历经数十年努力，终于找到了第五个“忙碌海狸”图灵机：

BB (5) =47,176,870（5 状态图灵机，能在停下来之前写下 47,176,870 个“1”）

图灵机是一种抽象的计算模型，通过读取和写入 0 和 1 在无限磁带上进行计算。

早在 40 多年前，一群计算机科学家在德国多特蒙德举行竞赛，寻找“忙碌海狸”图灵机。

找出一个特定的图灵机，在它停止之前能够写下最多的 1（我们称之为忙碌海狸数）。

通过找出特定状态下能在停止前写下最多 1 的图灵机，我们能更好地理解计算理论的边界。

自从 1974 年确定了第四个忙碌海狸数后，寻找第五个成了悬而未决的问题。

而现在，来自世界各地的 20 多名贡献者（其中大多数人没有传统的学术资格），使用一款名为 Coq 证明助手的软件获得了结果 ——47,176,870，该软件证实数学证明没有错误。

这一成就瞬间令社区沸腾，其中爱尔兰梅努斯大学计算机科学家 Damien Woods 惊叹：

就像博尔特一样，我很惊讶他们的速度如此之快！

嗯，快半个世纪过去了还算快？只能说这个问题雀食有亿点难。

别着急，且看这群人如何长江后浪推前浪抓住“第 5 只海狸”~

为什么提出“忙碌海狸”？

要回答这个问题，首先需要简单了解一下二进制图灵机。

1936 年，计算机科学之父艾伦・图灵提出了图灵机 ——

由一个无限长的纸带，一个读写头（可以读取和写入纸带上的信息），以及一组内部状态等基本部分组成。

图灵机的行为由一组规则定义，这些规则可以想象成一张表。表中的每行代表一个规则，每列对应读写头读取到的符号（0 或 1）。

每条规则指定了在特定状态下，读写头遇到 0 或 1 时应该执行的操作。操作通常包括：

• 写入符号：决定在当前单元格写入什么符号（例如，将 0 替换为 1）。

• 移动方向：决定读写头是向左移动、向右移动还是保持不动。

• 状态转换：决定图灵机的下一个状态是什么。

除了处理 0 和 1 的规则外，还有一条特殊规则告诉图灵机何时停止运行。当图灵机进入这个状态时，它就不再执行任何操作，相当于“比赛结束”（这种状态一般不计算在状态集合里）。

而就在停机问题上，已经有研究观察到：

一些图灵机会相对较快地停止（比如这台 three-rule 图灵机在 11 步后停止）

其他的则陷入了很容易发现的无限循环

这也启发图灵提出了著名的“停机问题”：

图灵机是否会在有限的步骤后停止运行，或者它是否会无限期地运行下去？

他还进一步提到，停机问题没有通用的解决方案，因为人们永远无法确定适用于一台机器的方法是否也适用于另一台机器。

对于这个结论，数学家 Tibor Radó（以下简称拉多）不太满意，并由此发明了“忙碌的海狸游戏”。

为了将停机问题的本质提炼成更简单的形式，拉多提出了一种方法 —— 将图灵机根据它们拥有的规则数量进行分组。

例如，一组代表所有只有一条规则的图灵机，另一组代表所有有两条规则的图灵机，依此类推。

1962 年，拉多利用这些有限的图灵机组定义了“忙碌海狸游戏”。游戏的玩法是：

• 1.选择一个组，即确定你的图灵机将拥有的规则数量。

• 2.为组中的每台机器提供一个初始状态全是 0 的磁带。

• 3.观察这些机器的运行。一些机器可能会无限期地运行下去，而其他的则会在某个时刻停止。

• 4.在那些最终停止的机器中，有的会很快停止，有的则需要更多步骤。每个组中会有一个运行时间最长的机器，这台机器被称为“忙碌海狸”。

• 5.在有 n 条规则的组中，这台“忙碌海狸”在停止之前所执行的步数就是所谓的“忙碌海狸数”BB (n)。

• 6.游戏的目标是确定这些 BB (n) 的确切值。

拉多给这样“极度低效”的图灵机取了一个有趣且形象的名字：忙碌海狸（Busy Beaver，取自英语中的谚语 as busy as a beaver）。

而这个游戏也最终引来一众程序员和数学爱好者的疯狂试玩。

早期吃螃蟹的人

Allen Brady（以下简称布雷迪），当时的俄勒冈州立大学数学研究生，成了早期挑战者之一。

在游戏推出前，人们已经确定了 BB (1) = 1，BB (2) = 6，当时人们正尝试攻克 BB (3)。

布雷迪也投身 BB (3)，他编写了计算机程序来模拟图灵机的行为，这个程序构建了一种“家谱”，根据图灵机初始行为的相似性，对具有相同规则数量的机器进行分类。

程序只在机器之间行为差异变得重要时才将家谱树分成多个分支。如果模拟显示某条分支上的机器会停止或进入无限循环，程序就会剪掉这个分支，排除那些不会无限运行下去的图灵机。

编写程序只是第一步，布雷迪需要找到足够强大的计算机来运行它。

在 1964 年，这不是一件容易的事。最终，他在 90 英里外的灵长类动物研究实验室找到了一台 SDS 920 计算机。

只可惜 BB (3) 进行到一半，拉多的研究生 Shen Lin 已宣布证明 BB (3) = 21，不过布雷迪还是继续证实了 Lin 的结果。

毕业后，布雷迪发现了新的非停止图灵机种类，并给它们起了形象的名字。

1966 年，他发现了一个在停止前运行了 107 步的四规则图灵机，并推测这可能是第四个忙碌海狸，并最终于 1974 年证明了没有其他停止的机器能运行更久。

这是四十多年来人类所知的最后一个忙碌的海狸号码

1982 年，第一次大规模寻找 BB (5)）的 Dortmund 竞赛正式举办，其中运行时间最长的一台在超过 10 万步后停止。

1984 年，《科学美国人》对这项比赛的报道激发了新一代研究者的兴趣，有一位研究者打破了旧纪录，他发现的一台机器在超过 200 万步后停止。

这一新纪录也引来当时的研究生 Heiner Marxen 和 Jürgen Buntrock，他们在业余时间合作研究这个问题，开发了加速图灵机模拟的数学技术。

尽管未能打破 200 万步的纪录，但后来在 1989 年，Marxen 在一家公司工作时，使用一台功能强大的新计算机重新启动了他的搜索程序，并意外地发现了一个在 4700 万步后停止的图灵机。

2000 年代初，一位名叫 Georgi Ivanov Georgiev（化名 Skelet）的保加利亚计算机科学家非常接近这一目标。

经过两年的不懈努力，他开发了一个能够识别非停止机器新种类的计算机程序。尽管他的程序运行了一周并留下了约 100 个未解决的图灵机，但他手工分析后将名单减少到 43 个。

此后人们一直陷入不断尝试中。

最终确定 BB (5)

2022 年，研究生 Tristan Stérin 发起了“忙碌海狸挑战”，这是一项在线合作，旨在最终确定 BB (5)。

在这之前，Stérin 决定在传统方法的基础上进行调整，使用布雷迪的家谱方法，并计划用独立程序处理永远运行的机器。

到 2021 年底，Stérin 编写了第一步的计算机程序，生成了大约 1.2 亿台可能的图灵机列表。

为了帮助分析这些机器，Stérin 构建了一个在线界面，使用“时空图”来可视化图灵机的行为。

完成这些后，鉴于个人精力有限，他在偶然的情况下拉来了 Shawn Ligocki。

Ligocki 向团队介绍了封闭磁带语言方法，这是一种 30 年前的技术，他将其应用于当前的忙碌海狸问题。

他写了一篇博客文章介绍这项技术，但最初并不知道如何编写一个能涵盖所有情况的程序。

然后，又一位 Justin Blanchard 加入了项目，他想出了如何做到这一点，但他的程序相对缓慢。

于是另外两个贡献者找到了让它运行得更快的方法，这一技术甚至可以处理前文提到的 43 个未解决图灵机中的 10 个。

取得阶段性成果后，BB (5) 终于迎来两个关键突破。

第一个是 Skelet #1，它在可预测行为和混乱行为之间不断交替，这种特性使得它非常难以分析和理解。

2023 年 3 月，Ligocki 和斯洛伐克贡献者 Pavel Kropitz（不会说英语，使用谷歌翻译与团队其他成员交流），使用 Marxen 和 Buntrock（之前挑战 200 万步记录的两位学生）30 年前的加速模拟技术的一个增强版，最终破解了 Skelet #1。

他们发现 Skelet #1 在超过一万亿步之后才进入一个异常长的重复周期，远超过一般无限循环在 1,000 步内开始重复的常规。

由于 Skelet #1 的行为极其奇怪，Ligocki 在将近五个月的时间里都不确定他们的证明结果是否正确。

后来，一位 21 岁自学成才的程序员（以“mei”为名）加入了团队，她通过学习 Coq 证明助手，将团队的一些证明翻译成 Coq 语言，提高了证明的严格性和可靠性。

第二个突破是 Skelet #17，研究者必须像破译四层加密的秘密消息一样，逐层解析其行为模式，才能证明该机器永远不会停止。

尽管研究生 Chris Xu 和其他社区贡献者做了大量工作，但大多数证明尚未翻译成 Coq。

直到 2023 年 4 月，一位名为 mxdys 的神秘新贡献者加入，并在短短几周内完成了一个 40,000 行的 Coq 证明，证实了 BB (5) 的值。

mxdys 证明第五台忙碌海狸在 4700 万步后停止，确认了 Marxen 和 Buntrock 的发现。

Coq 专家 Yannick Forster 审查了证明，他激动表示：

我仍然感到非常震惊。

故事仍未结束

BB (5) 终于确认了，目前相关研究者正在起草一份学术论文，这将是一个补充 mxdys 的 Coq 证明的人类可读版本。

但是，BB (5) 已确认，BB (6) 还会远吗？

mxdys 和另一位贡献者 Racheline 发现了一个六规则的图灵机，其停机问题与著名的数学难题“科拉茨猜想”相似。

为了避免让大家头疼，此处不再展开这个猜想，各位看官只需要知道它非常难就行。

以至于著名理论计算机科学家 Scott Aaronson 发出感慨：

BB (5) 也许是我们所知道的最后一个忙碌的海狸号码

嗯？这话有点耳熟，BB (4) 好像也是这样说的。

参考链接：

• [1]https://www.quantamagazine.org/amateur-mathematicians-find-fifth-busy-beaver-turing-machine-20240702/

• [2]https://news.ycombinator.com/item?id=40857041

• [3]https://scottaaronson.blog/?p=8088

本文来自微信公众号：微信公众号（ID：QbitAI），作者：一水，原标题《40 年图灵机难题被业余玩家攻破，陶哲轩：软件辅助证明改变数学研究规则》

广告声明：文内含有的对外跳转链接（包括不限于超链接、二维码、口令等形式），用于传递更多信息，节省甄选时间，结果仅供参考，IT之家所有文章均包含本声明。