综合头条

当前位置/ 首页/ 综合头条/ 正文

陶哲轩转赞!40多年「忙碌海狸」数学难题获突破,4万行Coq代码立大功

导读 【新智元导读】「忙碌海狸」难题困扰了计算机科学家40多年。如今,来自全球各地20+业余开发者和数学家们,终于取得了突破性进展。他们抓到...

【新智元导读】「忙碌海狸」难题困扰了计算机科学家40多年。如今,来自全球各地20+业余开发者和数学家们,终于取得了突破性进展。他们抓到了第五只忙碌海狸——用Coq辅助证明,得到答案47176870。对此陶哲轩激动地表示,这再次体现了证明助手对数学研究协作的重要性。

40多年的计算机难题——「忙碌海狸」难题,今天获得了重大突破了!

著名数学家陶哲轩转发了这一消息,欣慰地表示:这再一次体现了证明助手对于数学研究的协作是有多么有用。

计算机科学家Scott Aaronson为此还写了一篇博文,并称「这个发现是自1983年以来『忙碌海狸』函数研究中最重要的进展」。

40年前,100多名计算机科学家在西德的多特蒙德市,参加了这样一场奇怪的竞赛,选手需要捕捉一种难以捉摸的目标——忙碌海狸。

这次竞赛难度极大,因为只有四只海狸被成功捕获,第五只忙碌海狸逃脱了。

其实,这些海狸其实是一种看起来简单、运行时间奇长的计算机程序。这些程序异常活跃,对它们的搜索过程,涉及到了一些最著名的数学未解之谜。

甚至可以说,海狸难题直接根植于一个和计算机科学本身一样古老的不可解问题。

两年前,一位名叫Tristan Stérin的研究生建起一个网站,再次向全世界发起忙碌海狸挑战赛。

今天,有团队宣布——他们成功捕捉到了「第五只忙碌海狸」!这是由20多位来自世界各地业余爱好者组成的团队。

答案是47176870

具体来说,他们验证了一个名为BB(5)的数字的真值,这个数字量化了第五只海狸的忙碌程度。

获得这个结果的过程中,团队使用一个名为Coq的证明助手软件,后者可以确保数学证明没有错误。

圣塔菲研究所的计算机科学家Cristopher Moore这样评价:「他们为了达到目标所进行的社会学和数学工程,实在令人印象深刻」

「我惊讶于他们完成得如此之快,」爱尔兰梅努斯大学的计算机科学家、Stérin的导师Damien Woods说。「这简直达到了Usain Bolt的水平。」

可以说,寻找忙碌海狸最终是一场为了荣誉的狩猎。

因为,BB(5)的具体数值在计算机科学的其他领域并没有任何用处。

但对于捕捉忙碌海狸的猎人来说,战胜数学不可能性后取得的胜利,本身就是回报。

停机,还是不停机

牵动广大忙碌海狸猎人的程序,不是用普通编程语言编写的,而是为图灵机编写的指令。

计算机科学家艾伦·图灵在1936年设计了图灵机,从而以数学方式为计算过程建模。

图灵机的计算方式,是在无限长的磁带上读取和写入0和1。磁带被划分为多个方形单元格,一个「读写头」一次可以操作一个单元格。

每台图灵机都有一套独特的规则。

每条规则规定了读写头在进入一个新的单元格时应该做什么,取决于它遇到的是0还是1。

这意味着,图灵机的指令可以用一个表格来总结,每条规则占一行,两列分别对应读写头遇到0和遇到1的情况。

一条规则可能是:「如果读到0,将其替换为1,向右移动一步,并参照规则C」,这是第一列。

「如果读到1,保持不变,向左移动一步,并参照规则A」,这是第二列。

所有规则都如此,除非某个特殊规则告诉机器何时停止运行。

不过,虽然图灵机有停机的方法,但并不意味着它会停。

在最简单的情况下,它可能会陷入一个无限循环中,不断循环几个状态。

是否存在这样一种方法,可以判断具有特定规则集的图灵机是会停机,还是会永远运行下去呢?

这,就是著名的停机问题的本质,也是使得海狸难题如此迷人的原因。

图灵证明了停机问题没有普遍的解决方案——我们永远无法确定,对一台机器有效的方法是否对另一台机器也同样有效。

好在,停机问题并不总是对特定的机器来说很难。

比如下面这个视频中,有些机器会相对较快地停机。

而有的机器却很快陷入了无限循环。

这台三规则图灵机很快陷入了无限循环

我们总会遇到一些难以轻易分类的图灵机——它的运行会很快结束,还是会在磁带上永远徘徊?

是的,除非它运行足够长的时间,否则我们根本不知道,它会做什么。

忙碌海狸,在不可知边缘探索

忙碌海狸的故事,始于数学家Tibor Radó。

1895年出生于匈牙利,大学学习的是土木工程。一战爆发后,在西伯利亚战俘营的同伴指导下开始学习数学

后来他重返校园,在俄亥俄州立大学任教35年。

关于停机问题,他对图灵的证明并不满意。

为了将这个问题的本质提炼得更简单,Radó希望根据图灵机的规则数量进行分类——所有一规则图灵机为一组,所有二规则图灵机为另一组,依此类推。

如此一来,虽然会因图灵机可以有任意数量的规则而被分成无限多的组,但由于规则的组合是有限的,所以每组中的不同机器数量也是有限的。

这样推理,就比考虑所有的机器容易多了。

在1962年的一篇论文中,Radó基于此提出了「忙碌海狸游戏」。

要进行这个游戏,首先需要选择一个组——也就是你机器的规则数量。

给组中的每台机器提供一条每个单元格都是0的磁带后,有些机器会一直运行下去,其余的最终会停机。

其中有些会很快停机,有些会花更长时间,而有一台会是最后一个停机的。每个组都会有一个运行时间最长的成员,这些特别勤奋的机器,就被称为「忙碌海狸」。

在拥有n条规则的组中,忙碌海狸机器在停机前所需的步数,就是相应的忙碌海狸数BB(n)。而游戏的目标,是确定这些数字的确切值。

仔细一想就知道,解决「忙碌海狸」需要考虑众多问题。

要成功的话,你必须确定每台停机机器的运行时间,看看哪台花费的时间最长。你还必须证明所有其他的机器永远不会停机。

测量运行时间当然很简单,因为在普通计算机上模拟图灵机很容易。

但是,想要证明一台机器永远运行下去,相当于为它解决停机问题的具体版本——在最一般形式下,这几乎是不可能完成的任务。

「我们在不可知的边缘进行探索,」软件工程师、海狸难题的贡献者Shawn Ligocki这样说。

但不可知性究竟从哪里开始?

只有几个规则的图灵机看起来非常简单。理解一个可以放在索引卡上的程序有多难?

数学研究生的海狸团队

单一规则的情况很简单,因为实际上只有两种可能性。

如果规则告诉图灵机在看到0时停机,它会在第一步就停止。任何其他规则都会导致机器永远在磁带上前进,因为它会在每个单元格中遇到0。这意味着BB(1) =1。

除了这个小海狸,一个只用铅笔和纸装备的猎人很快就会遇到问题。对于两规则的情况,已经有超过6000个不同的图灵机需要考虑;这个数字在三规则时膨胀到数百万,在四规则时膨胀到数十亿。

手工处理所有这些情况是不可能的。「显然,你不可能做到这一点,」Ligocki说。「即使你能做到,也没有人会相信你。」

这意味着,这个根植于计算基础的问题只能在计算机的帮助下解决。

是的,一个相当简单的程序足以证明BB(2) =6,但从BB(3)起,就开始变得困难多了。

而Radó介绍这个游戏后不久,一小部分研究人员开始了这场狩猎。

Oregon State University的数学研究生Allen Brady很快就意识到,取得进展的关键,就是忽略图灵机之间不重要的差异。

例如,考虑一个有许多规则的图灵机,其中第一个规则告诉它如果读取到0就停机。

「其余那些转换中的内容并不重要,因为它会立即停机,」Ligocki说。就忙碌海狸游戏而言,这些机器大多数是多余的,因此可以直接一次性排除它们。

研究生Brady将这个过程,整合到一个用于模拟图灵机的计算机程序中。

基于机器初始行为的相似性,这个程序为具有相同规则数量的机器构建了一个类似家族树的结构。

只有当机器之间的差异变得相关时,程序才会将树分成多个分支,并删除在模拟中停机或进入无限循环的整个分支。

程序是编出来了,但找到能运行它的计算机,在1964年时并不容易。

终于,Brady获得了90英里外一个灵长类研究实验室计算机的使用权。

没想到,工作进行到一半,Brady发现自己被半路截胡了:Radó的研究生Shen Lin已经证明了第三个忙碌海狸数BB(3) =21。

Brady并未气馁,不仅确认了Lin的结果,而且在BB(4)上取得了部分突破——此前,Radó认为BB(4)「完全无望」解决。

BB(4)之所以难解,不仅是因为问题数量庞大,更因为四条规则的机器能够表现出的行为,实在是太丰富了!

所有不停机的两规则机器,都会陷入容易检测的无限循环。

在三规则的情况下,有几十台机器会永远运行而不进入循环,而证明这些机器永不停机,需要不同的方法。

对于四规则的机器,则有成千上万台这种非循环机器。

毕业后,Brady识别出了一些新的非停机图灵机种类,并给它们起了「影树」和「尾食龙」之类的奇幻名字。

1966年,他发现了一台四规则机器,在停机前运行了107步,他猜测:这就是难以捉摸的第四个忙碌海狸。

他的猜想是对的,但直到1974年,他才证明没有其他停机机器能运行得更久。

他在一份内部技术报告中写下了证明,但直到九年后,报告才在学术期刊上发表。

这是人类在超过40年里,所知道的最后一个忙碌海狸数。

第五只忙碌海狸诞生!

Brady发表证明的那一年,也是多特蒙德比赛——第一次寻找第5个忙碌海狸的大型竞赛的那一年。

对于五规则机器,可能的图灵机数量接近17万亿。即使以每毫秒一个的速度列出所有这些机器,也需要超过500年。

用Brady家谱方法来缩小搜索空间仍然必不可少,但程序必须运行得非常快,才有希望成功。

参赛者们各自开发了自己的程序,并且找到了运行时间最长的五规则图灵机——最忙的那台,在超过100,000步后停机。

《科学美国人》1984年对比赛报道后,不久后就有一位研究者打破了多特蒙德的纪录:一台机器在超过200万步后才停机。

柏林的研究生Heiner Marxen和Jürgen Buntrock,也开始利用业余时间研究这个问题。

几年后,在1989年Marxen成为了程序员,在公司中获得了一台强大的计算机。

竟然凭自己的程序找到了一台惊人的机器,在47176870步后才停机。

起初,他认为代码中肯定有错误。

但调试了几个小时后,他开始有一种奇怪的感觉:自己捕获到了忙碌海狸。

Buntrock很快复现了这一结果,两人发表了论文。

虽然Marxen捕获了忙碌海狸,但证明所有剩余的机器都不会停机,则花了超过30年。

在2000年初,一位名叫Georgi Ivanov Georgiev的保加利亚计算机科学家几乎成功了。

当时,他在一家国有电信公司担任系统管理员。他痴迷于BB(5)的研究,花了两年时间,每天花数小时改进一个可以识别新型非停机机器的程序。

最终的程序有6000行密集且没有注释的代码,运行时间超过一周。它留下了大约100台未决的图灵机。

手工分析这些机器后,他将名单缩减到43台。

2003年,Georgiev在网上发布了成果。

Marxen鼓励Georgiev继续努力,但两年的高强度工作已经让他筋疲力尽。

「这段时间结束时,我无法再产生任何新想法,我非常疲惫。」

这也是忙碌海狸研究者所共同面临的困境。

几十年来,他们或独自或成对地辛勤工作,却没有得到广泛学术界的太多认可。但是要完成这项工作,显然需要集体的努力。

召集所有猎手

召集所有猎手的努力,始于Tristan Stérin。

2000年代末,他最初通过IM结识了一位编程竞赛爱好者,从而早早精通了计算机编程。

但他很快意识到编程竞赛的文化,并不适合自己。

2022年,Tristan Stérin发起了忙碌海狸挑战赛,这是一项在线合作,旨在最终确定第五个忙碌海狸数量的价值

他表示,「我不是一个喜欢竞争的人。我喜欢看到一个问题,然后花3个月时间思考它,而不是只花30分钟」。

在好奇心的驱使下,Stérin决定从法国来到爱尔兰攻读研究生,在那里他与Woods一起研究DNA计算,即如何使用DNA链实现算法。

2020年夏天,Woods给他发了一篇关于「忙碌海狸」的综述论文,作者是计算机科学家Scott Aaronson。

Stérin立即被这篇文章吸引了。

论文地址:https://dl.acm.org/doi/10.1145/3427361.3427369

在与Woods合作撰写了一篇关于大型图灵机能力的论文后,他转向研究BB(5)问题,并下定决心要最终证明——Marxen和Buntrock的4700万步机器,确实是第五个「忙碌海狸」。

Stérin说,「我有强烈的直觉,自己做不到。但我也有一种直觉,这件事是可以做到的」。

论文地址:https://arxiv.org/pdf/2107.12475

从一开始,Stérin就知道,要有结论性的证明,必须有良好的文档记录和可重复性,因为任何微小的软件错误都会对整个研究造成致命打击。

Georgiev的程序极其复杂,但其他研究人员发现它难以解析。

参与「忙碌海狸」挑战赛的软件开发人员Justin Blanchard表示,「当你回头试图审查代码时,你会马上放弃。任何新的方法实际上都得从头开始」。他曾是一名数学专业的研究生。

Stérin决定在传统方法的基础上进行一些改进。

他首先使用Brady的家族树(Brady’s family-tree)方法,来消除冗余的图灵机,并识别出哪些机器在4700万步内停机。

但与Brady或其后继者不同的是,Stérin没有包含任何用于剔除永远运行的机器的代码。

相反,他计划使用独立的程序来解决这些问题,每种方法对应一个程序,证明图灵机永远不会停机。

这样分块处理任务,将使合作伙伴更容易独立地完成每个部分,并交叉检查结果。

2021年底,Stérin编写了第一步的计算机程序。

它生成了大约1.2亿台图灵机的列表,这些图灵机足以确定BB(5)的值——其余的都是冗余的。

在这1.2亿台图灵机中,大约1/4在Marxen和Buntrock的机器之前就停机了,剩下的8800万台仍在考虑范围内。

为了帮助分析这些图灵机,Stérin构建了一个在线界面,用于在「时空图」上可视化它们的行为,时空图是由代表0和1的黑白方格组成的二维网格。

图中的每一行记录了图灵机演化过程中的一步。

第一行代表第一步后的纸带状态,第二行显示第二步后的纸带状态,依此类推。

以这种方式查看,Stérin收集的图灵机仿佛活了过来,展示出令人眼花缭乱的各种不同模式。

要证明Marxen和Buntrock确实找到了第五个忙碌海狸,就意味着要证明这些机器中的每一个都会永远运行下去。

Stérin知道,自己无法单独完成这项任务。

2022年春天,Stérin和一些早期加入者在独立平台Discord上,创建了一个论坛和一个单独的聊天服务器。

然后,是时候寻找贡献者了。

「忙碌海狸」的魅力

Shawn Ligocki很快加入了团队。

也许这是命运:他1985年出生在Beaverton,虽然他第一次听说「忙碌海狸」是在2004年,当时在他大学第一学期结束时。

寒假期间,他和他的父亲Terry一起开始研究海狸搜索算法,Terry是劳伦斯伯克利国家实验室的一名应用数学家。

一个月后,当Ligocki回到大学忙于课程时,他的父亲兴奋地打电话给他。

他决定在Brady发明的原始忙碌海狸游戏的一个变体上,测试他们的一个算法,并发现了一台打破Brady记录的图灵机。

他们联系了已经退休的Brady,Brady很高兴并在他的网站上公布了这个结果。

随之,Shawn Ligocki很快与世界各地的「忙碌海狸」研究人员通过电子邮件进行交流。

有一次难忘的经历发生在Ligocki大二暑假访问德国期间,他顺道去了柏林与Marxen见面。

忙碌海狸的魅力,伴随着Ligocki整个大学期间,但毕业找到工作后,生活琐事让他分心。

他偶尔会重新投入忙碌海狸的研究,但从未持续太久。

2022年初,他建立了一个在线讨论组,帮助研究人员保持联系。5月时,Stérin发现了这个邮件列表,并发出加入忙碌海狸挑战的邀请。Ligocki毫不犹豫地接受了邀请。

他对项目的首次贡献之一,是复兴了Marxen发明的一种技术,这是他们16年前在柏林酒吧讨论过的技术。

这种技术被称为「封闭磁带语言」(the closed tape language)方法。这是一种新方法,用于识别图灵机磁带上永不停止的模式。

这是识别循环程序和许多其他图灵机不停机的基本策略,但「封闭磁带语言」方法有潜力通过统一的数学框架识别更广泛的模式类别。

Ligocki写了一篇博客文章,向他的新合作者介绍了这项技术,但尽管理论上的想法非常通用,他并不知道如何编写一个涵盖所有情况的程序。

Justin Blanchard在秋天加入项目后不久,就找到了方法,但他的程序相对较慢。然后另外两位贡献者找到了让它运行更快的方法。

在几个月内,「封闭磁带语言」技术从一个有前途的想法变成了他们最强大的工具之一。

它甚至可以处理Georgiev的43个未解决问题中的10个,为纪念他而被称为「Skelet图灵机」。

怪物「图灵机」来袭

随着时间的推移,新的贡献者们发现了「忙碌海狸」挑战,并开始逐步解决问题的不同部分。

但许多图灵机仍未解决,其中有两台图灵机尤其声名狼藉。

第一台是Skelet #1,它在可预测和混乱的行为之间不断交替。

在2023年3月,Ligocki和Pavel Kropitz——一位不会说英语的斯洛伐克贡献者,通过谷歌翻译与团队其他成员交流——提出了一系列想法,终于破解了它。

使用Marxen和Buntrock30年前的加速模拟技术的升级版,他们发现秩序与混乱之间的拉锯战确实结束了,但只有在超过一万亿亿步之后。

然后它最终进入了一个异常长的重复循环周期。

实际上,几乎所有的无限循环在1000步内就会开始重复;而Skelet #1的循环超过了80亿步之长。

这台图灵机的行为非常诡异,证明过程融合了许多不同的想法,以至于Ligocki在近5个月内都无法确定结果。

不过,这一不确定重复周期,被一位新贡献者打破了——一位21岁的自学成才的程序员,名叫Maja Kądziołka,多数情况在她只用一个字mei。

mei在波兰长大,并在2021年秋季在华沙大学学习了一个学期后辍学。

随后,她在一家软件公司工作了一年多,但越来越觉得工作令人筋疲力尽,开始寻找更具智力挑战的工作。

偶然的机会,她在软件Coq中找到了这种兴趣,这是一款设计用于编码和验证数学证明有效性的软件。

当时,忙碌海狸挑战的贡献者们已经在证明中使用计算机程序,但就像纸笔证明一样,计算机程序也容易出错。

而在Coq证明中,代码只有在每一行逻辑上都能从前一行推导出来时才能运行,这使得错误几乎不可能发生。

对mei来说,弄清楚如何制作这些证明开始变得像一场游戏。

在学习了Coq之后,mei开始寻找一个开放的问题来测试它。就在那时,她发现了忙碌海狸挑战。

几周后,她将团队的几项证明用Coq重新编写,包括Ligocki和Kropitz关于Skelet #1永不停止的证明——Ligocki终于可以确定这一点了。

突然间,比Stérin强调的可重复性更高的严格标准,似乎成为可能。

项目地址:https://github.com/meithecatte/busycoq

而这一切都是由一个没有正式训练的人——一个业余数学家做出来的。

突破性进展

大约在同一时间,一位名叫Chris Xu的研究生,在第二台怪物图灵机——Skelet #17上取得了突破。

通常,即使是复杂的五规则图灵机(five-rule Turing machines),一旦理解了其工作原理,总结其行为也不难。

通过研究Skelet #17磁带上的模式来理解它,就像解密四层加密的秘密信息一样:破解一个代码只是揭示了另一个完全不相关的代码,并且下面还有两个。

Xu必须解密所有这些代码,才能最终证明这台机器从未停止。

Xu的证明非常出色,但它涉及一些无人知道,如何用Coq所要求的精确术语形式化的数学直觉。

而且,忙碌海狸挑战的工作还远未完成:虽然Skelet #1和#17是看起来最难对付的两台图灵机,但还有其他一些图灵机需要解决,还有一些只使用低效程序解决的图灵机。

这不足以说服世界。

在接下来的几个月里,社区慢慢拼凑出剩余图灵机的证明,但大多数还没有被翻译成Coq。

然后在四月,一个神秘的新贡献者出现了,他用化名mxdys来完成这项工作。

团队中没有人知道mxdys的所在地或其他个人信息。在一次Discord私信交流中,他提到对数学游戏有长期兴趣,但拒绝提供更多关于他背景的信息。

5月10日,mxdys在Discord服务器上发布了一条简短的消息:「BB(5)的Coq证明已经完成」。

一分钟后,Stérin回复了一串七个感叹号。

在几周内,mxdys完善了社区的技术,并将他们的结果综合成一个40,000行的Coq证明。

法国国家研究院Inria的Coq专家Yannick Forster在审查证明后表示,「这不是一件容易形式化的事,我仍对此感到惊讶」。

Marxen和Buntrock在30多年前发现的那台在4700万步后停止运转的图灵机,确实是第五个忙碌海狸。

「这个消息对我来说非常令人兴奋,」Georgiev在一封电子邮件中写道。「我从未想到这个问题会在我有生之年得到解决。」

但对另一位忙碌海狸挑战的开创者来说,这个消息来得太晚了。

Allen Brady于4月21日去世,距离证明完成不到一个月,享年90岁。

贡献人员名单

以下是所有参与这次证明BB(5)=47176870的贡献人员名单。

下一步探索

忙碌海狸挑战的参与者们已经开始起草一篇正式的学术论文,描述他们的成果,并用更易理解的证明来补充mxdys的Coq证明。

这将需要一些时间:大多数图灵机通过多种方法被证明不会停止,团队需要决定如何最佳地将这些结果组合成一个完整的证明。

与此同时,部分团队成员已经开始研究下一个忙碌海狸。

然而就在四天前,mxdys和另一位名为Racheline的贡献者发现了BB(6)的一个似乎无法逾越的障碍:一个六规则图灵机,其停机问题类似于一个著名的数学难题——Collatz猜想。

图灵机与Collatz猜想之间的联系,可以追溯到1993年数学家Pascal Michel的一篇论文。

但新发现的图灵机,被称为「Antihydra」,是迄今为止最小的一个,似乎在没有数学上的概念性突破的情况下无法解决。

论文地址:https://link.springer.com/article/10.1007/BF01409968

显然,可以想象的到,BB(5)将是我们所知道的最后一个忙碌海狸的数字。

忙碌海狸问题有许多不同的变种,一些忙碌海狸挑战的参与者计划继续研究这些变种。但并不是所有人都打算继续这项工作。

他们各自因为不同的原因参与到这个项目中,现在他们的研究道路开始分道扬镳。

Stérin希望开发软件工具,以促进其他数学领域的在线协作。

他表示,「忙碌海狸挑战带给我的是一种非常深刻的信念,它是一种非常有效的研究方式」。

参考资料:

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

https://mathstodon.xyz/@TaliaRinger/112719444060361451