一道卡了 25 年的题，被 AI 一周拿下

无线通信里有个经典难题叫 MIMO 检测：发送端把 N 个比特塞进 N×N 信道发出去，信号在途中被搅乱、叠上噪声，接收端要一字不差地把原始比特还原回来。

理论上有笨办法——穷举所有 2^N 种比特组合，找最匹配的那个。但 N 稍大就算到天荒地老。1989 年有人证明这问题在最坏情况下是 NP-hard 的。

学界真正想知道的是另一件事：现实信道是随机的，不是刻意构造的最难情况。只要信噪比达到 2logN，统计上原始比特就能被恢复。那能不能设计一个跑得快的算法，精确命中这条阈值？

25 年来，球形译码、半正定松弛、比特翻转、AMP、统计物理方法轮番上阵，最好成绩也只能停在理论门槛的两倍处。统计上「能恢复」和用快算法「能恢复」之间，隔着一条没人能跨过的鸿沟。

上周，微软研究院首席研究员 Dimitris Papailiopoulos 用 GPT-5.6 和 Fable 5 把这条鸿沟填平了——一个只有两步的算法，多项式时间，O(N³) 运算就能精确命中 2logN 阈值。

两个模型怎么分工

Dimitris 让两个模型分别试这道题。GPT-5.6 走的是 AMP（近似消息传递）路径，这是 Dimitris 自己一直没吃透的分析工具；Fable 5 给了另一条路——「符号 LMMSE 加贪心逐位翻转」，一个业内实际在用、却从没被严格证明过的老算法。

两条路都各自给出了完整证明。Dimitris 选了 Fable 的方案，让 GPT 接手检查和修补漏洞。修好之后的证明是一堵「符号墙」——变量指着变量，塞满他看不懂的矩阵分析工具。

接下来几天，他反复让两个模型互相简化对方给出的论证，唯一底线是保住 2logN 这个门槛，其余怎么改都行。他甚至拒绝了 Lean 形式化验证——原因很直接：他不懂 Lean，没法检查翻译对不对。

折腾一周后，终于拿到一份可以逐行手算核对的证明。

算法拆解：两步就够了

第一步：LMMSE 取整。 LMMSE（线性最小均方误差估计）给出一个连续取值的粗略猜测，再把每个坐标按正负号取整成 +1 或 -1。这步不需要精确猜中每一位，证明保证取整后结果与真实比特的汉明距离只有 o(N)——猜错的占比随 N 增大趋近于零。

第二步：贪心逐位翻转。 从第一步的猜测出发，每轮检查所有比特，翻转能让代价函数下降最多的那一位，重复直到找不到能改进的翻转为止。

关键在于证明贪心搜索不会卡死：在猜测起点周围，每一个还没猜对的点都至少存在一位翻转能让代价严格下降，且下降幅度有不趋于零的下限。同时代价函数本身随汉明距离增大而增大，形成天然护栏——搜索路径没法翻越护栏跑到猜测范围之外。

复杂度算出来是 O(NlogN) 步，加上第一步的 O(N³)，整体多项式时间。

真正值得注意的事

比这道题本身更值得关注的是它意味着什么。

第一，AI 在数学证明里的角色已经从「辅助计算」升级到「提出证明路径」。GPT-5.6 和 Fable 5 各自给出不同的证明思路，Fable 的路径是业内用了多年却从未被严格证明的算法——这意味着 AI 能把工程实践中的「经验有效」提升为「数学必然」。

第二，人机协作的模式变了。Dimitris 不懂 AMP、不懂 Lean、不懂矩阵分析工具，但他知道结果对不对、底线在哪。他做的是审稿人和仲裁者，不是证明者。 两个模型互相简化对方的论证，他负责判断「这个我看得懂，保住门槛就行」。这种「AI 证明 + 人类仲裁」的分工，可能是未来硬核科研的常态。

第三，Dimitris 2009 年读博时用 MCMC 试过这道题，没成功。17 年后用 AI 把它解开了。学术生涯里卡住的题，现在多了一条解法路径。

这对普通人意味着什么

MIMO 检测是 5G/6G、Wi-Fi 7/8 的底层技术。更高效的检测算法意味着接收端芯片可以用更少算力还原信号——直接红利是更低功耗、更高吞吐的通信基带芯片。

但更深远的影响在 AI 这侧：当大模型能啃下硬核数学证明，它就不是「更聪明的搜索」了，而是开始参与人类知识的生成环节。写代码、改 bug、做设计——这些是应用层。数学证明是基础层。应用层被 AI 渗透是这两年的事，基础层被打开，可能才是接下来五年的真正叙事。

LynxHot · 跟踪 AI 工具、模型与产业变化