OpenAI 公布了 ETH 的反证，从学数学的人的角度看，这是最让人坐不住的一条 AI 研究消息 当然 Ryan Williams 和 ETH 的提出者正在组织独立核查，结果还没有获得最终确认。 但它碰到了我一直很在意的一个问题：我们遇到的那些“算不动”，有多少是问题本身就难，又有多少只是还没找到好办法。 ETH ，全称是 Exponential Time Hypothesis，一般叫指数时间假说。假设我们用逐个尝试的办法处理一堆“是或否”的选项。每多一个选项，要试的组合就翻一倍。10 个选项是一千多种组合，30 个是十亿多种，50 个就超过了 1000 万亿种。 一台每秒能试十亿种组合的机器，把这 50 个选项的全部组合试完，大概要跑 13 天，差不多两周。 现在花一大笔钱，把机器换成快一百万倍的。同样两周，它就大概能处理 70 个。很奇怪的是，快了一百万倍，实际只多处理了大约 20 个选项。原因很简单，每多 20 个选项，组合数就要再乘上一百万左右，我们在硬件上的投入所带来的提速正好被这个组合增加的窗口吃掉。 所以在这个情况下，再买点 GPU、再等几代芯片，当然能解决一些眼前的问题。但碰到这种增长方式，问题规模稍微变大，硬件带来的收益就可能被抵消。要改变长期的增长趋势，就得在算法上找到新的办法。 当然组合多，不代表一定要把所有组合试完。一个足够聪明的算法，可能跳过大量没必要的尝试。有没有办法从根本上降低计算量，才是数学家关心的问题。研究这个问题，需要一个定义清楚、方便分析的对象。ETH 针对的对象叫 3-SAT，可以把它理解成“很多条简单规则，能不能同时满足”。 比如有一堆只能选“是”或“否”的变量，每条规则最多涉及三个条件，至少满足其中一个，而所有规则又必须同时成立。单看每条都很简单，放在一起却可能互相冲突。ETH 给出的判断是：至少在某个基础问题上，通用算法面对最坏情况时，无法摆脱指数时间。 玩过数独的人，应该熟悉这种感觉：每个格子填什么都受规则限制，单看每条规则都很简单，缠在一起就麻烦了，这里填对了，那边又冲突。 现有算法已经比一个个硬试快很多。ETH 认为，再怎么改，碰到最坏情况也逃不出指数增长。现实里很多具体的题，求解器早就能解；ETH 讨论的是，通用算法面对最难的那批题时，至少要付出多少计算代价。 Impagliazzo 和 Paturi 关于 ETH 的经典期刊论文发表于 2001 年，会议版本更早出现在 1999 年。此后二十多年，大量复杂性研究都以它为前提，推导其他问题的计算难度。原始论文、作者论文目录 这次公开材料里的主张，比“找到一种满足条件的选法”更进一步。按照形式化范围说明，对于每条规则宽度固定的这类逻辑公式，一个确定性算法可以在亚指数时间、多项式空间内，精确算出满足条件的选法一共有多少种。它不用把解一个个列出来，只给出总数。这个数是不是零，就回答了有没有解。形式化范围说明 如果这个结论站住，ETH 就被推翻了。 这类逻辑求解已经进入了不少真实系统。三个例子，分别关系到钱、芯片和工厂交期。 第一个是一场 198 亿美元的拍卖。 2016 到 2017 年，美国 FCC 要把一部分电视广播频段腾出来给移动通信使用。留下来的电视台得重新分频道，同时满足干扰限制。A 台换到某个频道，B 台能去的地方就少了，C 台又被 B 台牵连。拍卖过程中，系统要反复回答同一个问题：剩下这些台还能不能全部安排进去？ 回答这个问题的，是一个叫 SATFC 的求解器。项目论文里有个细节很值得注意：每次求解都有时间上限，到点没算完，系统就按“塞不进去”处理。方案也许存在，只是没来得及找到，腾出频谱的成本就可能因此变高。实际项目论文算得慢，在这里直接变成了钱。 那场拍卖用的是多年打磨的专用求解器，没有用到今天这篇论文里的算法。但这类工具已经在真金白银的系统里跑着，新的算法思想如果能改善它们，影响就有机会进入实际决策。 第二个例子在芯片设计里。 工程师为了省电或者改善时序，经常要改电路。改完必须确认，新的电路实现仍然符合原来的逻辑设计。麻烦在于，有些错误只在极少见的输入组合或状态下才冒出来，普通测试可能一直碰不到。 Intel 的工程论文介绍过他们的做法：把电路实现、参考设计和环境条件一起编码成逻辑问题，让 SAT 求解器去找一个能让两边表现不同的反例。找到了，工程师就拿到一条具体的调试线索；证明不存在这样的反例，才能在这个模型和假设下确认两者等价。Intel 工程论文 这一步会影响一个改动能不能被接受。更快的求解器，有机会支持更大的验证模型，让工程师在同样时间里检查更多候选设计。以前因为验证代价太高而搁下的优化，也可能值得重新拿出来。模型本身有没有漏条件，仍然需要检查，求解提速不会自动补上这些遗漏。 第三个例子是工厂里的急单。 一张急单临时插进来，几道工序有严格先后，关键设备已经排满。生产负责人得决定接不接。把某道工序往前挪，可能占了另一张单要用的机器；把机器腾出来，上一道工序又赶不上。每一步单看都合理，拼在一起可能根本排不下去。 这类排程已经有成熟工具。Google 的 OR-Tools 提供了用 CP-SAT 处理车间排程的官方示例，把工序先后、一台机器同一时间只能干一件活这些限制写进模型。Google 官方排程示例 如果哪天求解器因为新思路变快了，负责人在拍板之前就可能多比较几套完整方案。有时能找到一张之前没来得及找到的排程，有时能确认，在现有设备和交期下这单确实接不了。接不了就早点谈交期，接得了就拿一份查过的方案出来，少一些先答应、再靠加班和催货硬扛的情况。 我们所期待的实际变化，大概就是这种。企业在有限的时间里，能把相互牵制的条件考虑得更完整一点，不用因为算不下去，就过早定死某些选择。 不过，每个例子和这篇论文之间，都隔着很长的工程距离。 亚指数时间仍然可能慢得没法用，理论算法里藏着的常数也可能大得吓人。现实问题翻译成 SAT，规模还可能膨胀。能写成 SAT，不等于能拿到同样幅度的加速。ETH 被反证也推不出 P=NP，更不能据此宣布现在的密码失效了。 数学上的影响会来得更早。 我不知道这个反证最后能带来多大的工程收益，也不打算预测哪款软件会突然快多少倍。 但如果它站住，我们对计算难度的一条长期判断就得改。那些早就习惯了的代价，多花的钱、多等的时间，里面有多少其实能被一个更好的方法省下来，现在有理由重新问一遍了。 对一个学数学的人来说，这够我兴奋很久。