算法与理论计算机2025arxiv.org编辑精选
第五个 Busy Beaver 值的确定
Determination of the fifth Busy Beaver value
专业 · 约 75 分钟读完前置知识:图灵机与可计算性基础、Busy Beaver 问题定义、半判定器/抽象解释
导读
这篇论文宣布确定了第五个 Busy Beaver 值 BB(5):即 5 状态图灵机中停机前运行步数最多的机器(Champion)在 47,176,870 步后停机。团队通过穷举约 1.81 亿台 5 状态图灵机,并结合多种(半)判定器证明其余机器永不停机,从而完成了 BB(5) 问题的求解。
HN 关注点:Busy Beaver 是可计算性理论中著名的开放问题,HN 读者关注其被攻克的过程与技术细节,以及这种大规模协作式数学/计算项目的可行性。
HN 评论精选
这几条评论里:支持 1 质疑 2 亲历 1
亲历作者之一详解求解流程:穷举 + 有限步运行 + 多个(半)判定器分类剩余机器
给程序员的高层次概述:约 1.81 亿台本质不同的 5 状态图灵机被穷举,每台先运行约 1 亿步,约 25% 在此期间停机(包括运行 47,176,870 步后停机的 Champion)。剩下约 1.4 亿台长期运行,问题是它们究竟永不停机还是只是没跑够。由于不存在对所有图灵机都有效的通用算法,项目构建了一系列(半)判定器,基于已证明的启发式将机器分类为“确定永不停机”或“可能停机”。共用了四个判定器:Loops(若重新进入已见过的构型则必然死循环,覆盖约 90%);NGram CPS(抽象模拟,跟踪纸带两侧可能出现的二进制 n-gram 集合,计算可达状态的超近似,若抽象状态都不触发停机转移则原机器不能停机,覆盖约 600 万台中的大部分)……
nathanrf查看英文原文
Here's a high level overview for a programmer audience (I'm listed as an author but my contributions were fairly minor): [See specifics of the pipeline in Table 3 of the linked paper] * There are 181 million ish essentially different Turing Machines with 5 states, first these were enumerated exhaustively * Then, each machine was run for about 100 million steps. Of the 181 million, about 25% of them halt within this memany step, including the Champion, which ran for 47,176,870 steps before halting. * This leaves 140 million machines which run for a long time. So the question is: do those TMs run FOREVER, or have we just not run them long enough? The goal of the BB challenge project was to answer this question. There is no universal algorithm that works on all TMs, so instead a series of (semi-)deciders were built. Each decider takes a TM, and (based on some proven heuristic) classifies it as either "definitely runs forever" or "maybe halts". Four deciders ended up being used: * Loops: run the TM for a while, and if it re-enters a previously-seen configuration, it definitely has to loop forever. Around 90% of machines do this or halt, so covers most. 6.01 million TMs remain. * NGram CPS: abstractly simulates each TM, tracking a set of binary "n-grams" that are allowed to appear on each side. Computes an over-approximation of reachable states. If none of those abstract states enter the halting transition, then the original machine cannot halt either. Covers 6.005 million TMs. Around 7000 TMs remain. * RepWL: Attempts to derive counting rules that describe TM configurations. The NGram model can't "count", so this catches many machines whose patterns depend on parity. Covers 6557 TMs. There are only a few hundred TMs left. * FAR: Attempt to describe each TM's state as a regex/FSM. * WFAR: like FAR but adds weighted edges, which allows some non-regular languages (like matching parentheses) to be described * Sporadics: around 13 machines had complicated behavior that none of the previous deciders worked for. So hand-written proofs (later translated into Rocq) were written for these machines. All of the deciders were eventually written in Rocq, which means that they are coupled with a formally-verified proof that they actually work as intended ("if this function returns True, then the corresponding mathematical TM must actually halt"). Hence, all 5-states TMs have been formally classified as halting or non-halting. The longest running halter is therefore the champion- it was already suspected to be the champion, but this proves that there wasn't any longer-running 5-state TM.
支持赞赏在线协作式科研模式,期待其平台化普及
这项研究最让我感兴趣的是它是在线协作完成的。我想知道还有多少类似项目,这种模式能否更普及,甚至做成一个平台。
fedeb95查看英文原文
what's most interesting to me about this research is that it is an online collaborative one. I wonder how many more project such as this there are, and if it could be more widespread, maybe as a platform.
质疑询问该成果是否有实际应用价值
作为对该领域不熟悉的人,这个成果有什么实际好处,还是纯学术性质?
DarkNova6查看英文原文
As somebody not familiar with this field, is there any tangible benefit to this solution or is it purely academic?
相关资源
从这篇论文所有 HN 讨论帖的全部评论里整理出来的链接。
历次讨论
- 2025Hacker News 讨论帖288 分 · 116 评
同领域还值得读
哲学家为何应关注计算复杂性
Why Philosophers Should Care About Computational Complexity (2011)
Scott Aaronson 的这篇长文论证计算复杂性理论(如 P vs NP、停机问题的复杂度视角)对哲学问题(如知识的本质、中文房间、水槽论证等)具有实质意义,而不仅是技术细…
算法与理论计算机2015 · 552 分 · 120 评进阶 · 约 90 分钟编辑精选通信的数学理论
A Mathematical Theory of Communication
是香农1948年的《通信的数学理论》,为通信建立数学框架:把信息量定义为不确定性或自由度(信息熵),并讨论信源编码、信道容量与可靠传输。
算法与理论计算机2020 · 495 分 · 91 评进阶 · 约 120 分钟编辑精选物理、拓扑、逻辑与计算:罗塞塔石碑
Physics, Topology, Logic and Computation: A Rosetta Stone (2009)
用范畴论充当“罗塞塔石碑”,试图在量子物理、拓扑、逻辑与计算四个领域之间建立统一的结构性类比:物理中的量子过程、拓扑中的配边、逻辑中的证明和计算中的程序,都可被视为某类范畴中的态…
算法与理论计算机2009 · 390 分 · 55 评 · 引用 13专业 · 约 180 分钟编辑精选一种快速、极小内存的一致性哈希算法
A Fast, Minimal Memory, Consistent Hash Algorithm
论文给出一种快速、省内存的一致哈希方案,目标是在桶数量变化时保持较小的键迁移成本,同时降低计算和内存开销。
算法与理论计算机2014 · 327 分 · 57 评 · 引用 4进阶 · 约 25 分钟编辑精选近线性时间内的最大流与最小费用流
Maximum Flow and Minimum-Cost Flow in Almost-Linear Time
给出了最大流与最小费用流的近线性时间精确算法,是理论计算机科学的重要突破。
算法与理论计算机2022 · 230 分 · 40 评 · 引用 8专业 · 约 120 分钟编辑精选