又见忙碌海狸

唐家山

海狸这种可爱的小东西是第三次出圈了。不过我说的不是真实世界的海狸，而是理论计算机科学中的某一类有趣的问题。
图灵很早就证明了停机问题是不可判定的。忙碌的海狸（Busy Beaver）是停机问题的一种弱化问题，由Tibor Radó在1962年提出。维基上的介绍是：
“在计算机科学中，忙碌的海狸（Busy Beaver）是一个在给定参数后，寻找可能产生的最大输出的可终止程序。忙碌的海狸游戏包括设计一个可终止的，只输出0或1的图灵机，让其在一条纸带上尽可能多的输出1。”
说人话就是：限定图灵机的某个参数，去寻找在该参数下能够停机并且在停机时能输出最多1的某个（类）图灵机。
这个参数就是图灵机的状态。限定在4个状态图灵机的忙碌海狸问题或者函数就记为BB(4)。在该规模下输出1的个数就是忙碌海狸数。前4个数分别是1、6、21、107。
忙碌海狸第一次出圈就是科学家们在2024年形式证明了BB(5)=47,176,870。记住，我说的是证明。也就是说凡是5状态的图灵机，如果是输出多于47,176,870个1，一定是不停机（陷入某种循环）的。这个证明听起来就很麻烦，实际上也是如此。Coq证明代码跑起来就需要10多个小时。
前一段时间，对于BB(6)有两个不大不小的新闻。一个是某台6状态图灵机有可能等价于考拉兹猜想（Collatz conjecture）或者是角谷定则。另一个是BB(6)的上界已经无法用常规数学符号表示。
最近看到的一则新闻是瑞士一个团队的论文。论文通过参数化生成不同复杂度的忙碌海狸图灵机，从简单的64个机器（N=1）到极其复杂的42亿个机器（N=4）。通过调整参数，可以生成各种可调节难度的证明挑战，用于评估大模型的逻辑推理和定理证明能力。
我在两年前曾提过一嘴，说如果大模型能够独立解决类似于停机问题之类的具有否定性结果的问题，那就说明大模型是真正理解了问题的本质，能够做真正的抽象和推理。没想到现在人类可以用弱化的停机问题去评估大模型的定理证明能力，看来人类的创造性还是独一无二的。