Anthropic 内部模型三天证明量子计算18年悬赏猜想

Anthropic一个非公开模型近日证明了量子计算领域悬而未决18年的Aaronson-Ambainis猜想。据新智元报道，以该内部模型为核心的Harness系统搭建完成后，三天即完成首个证明，随后被送入Lean证明助手接受检验。

该猜想由Scott Aaronson与Andris Ambainis于2008年提出，涉及量子计算机相对经典计算机的加速边界。网友推测，此次出手的内部模型即非公开版Claude Model 4。

猜想从何而来

这一猜想的源头可追溯到1994年。当年Peter Shor提出肖尔算法，可在多项式时间内分解大整数，而经典计算机完成同一任务需要指数级时间，现代加密体系的基石由此受到动摇。此后量子霸权一词在全球科技界与资本市场流行，一种认知也随之扩散：只要掌握量子叠加与纠缠，量子计算机似乎就能对大多数难题实现指数级加速。

但研究者很快指出，肖尔算法的指数级优势来自整数分解背后强烈的周期性结构，而量子计算机擅长捕捉这类重复规律。若输入数据完全随机、没有任何结构，量子计算机是否仍能指数级超越经典计算机，成为悬而未决的问题。

他们把计算机读取输入的过程比作观察：经典计算机每读一位得到确定的0或1，量子计算机则借叠加态把一次观察分散到海量状态上。两人发现，量子计算机经过T次观察后输出是的概率，可被严格刻画为一个有界低阶多项式。若能证明该多项式在翻转某个变量时必然出现足够大的变化，即存在影响力显著的变量，就可证明经典计算机只需多项式级别的额外代价便能模拟量子计算机的行为。

三天完成证明

这一模型并非公开版本，网友推测其就是非公开版Claude Model 4。

报道称，此次证明并非简单检索文献后复述，而是以一种相当奇妙的方式汇聚了布尔函数分析、概率组合等多个研究方向的内容。参与相关工作的研究者一直在阅读新的证明，其中包括此前解决该猜想经典模拟推论一个特例的麻省理工学院Guy Blanc、Jordan Docter、Carmen Strassle与斯坦福大学Li-Yang Tan。他们认为这是一个大结果，解决了一个数十年之久的猜想，对哪些问题能够实现量子加速这一本质具有重要启示。

报道还提到，这并非该方向上的首次出手：上个月相关系统已解决量子信息论中五个长期悬而未决的问题。至于人类多领域专家合作是否最终也能证明该猜想，报道未给出结论，只强调AI的速度人所难及。

Lean形式化检验

报道称，定理和推论均已完成Lean形式化。这意味着证明不仅以自然语言呈现，也经过了机器可检验的形式化环节。

形式化检验的意义在于把证明的每一步落到可核验的逻辑基础上。报道没有披露检验过程的具体耗时与细节，只说明证明在完成后进入这一环节并完成形式化。

从流程上看，Harness系统承担了从提出问题到产出证明的角色，Lean则承担验证角色，两者构成了此次结果公布时被强调的技术路径。

指数反复压缩

证明并未止步于首个版本。报道称，当模型实例被要求借助这些中间结果去攻克悬而未决的难题时，它们反过来打磨了这些中间结果，将指数从22压到11，再到7，不断下降。

这一过程被描述为发现过程本身的缩影：证明不是一蹴而就的灵光，而是在中间结果的反复打磨中一步步逼近最优边界。指数的连续压缩，说明系统在得到可行证明后仍继续优化相关界。

报道未说明指数最终停留在哪个数值，也未给出每一轮压缩的具体方法，只呈现了22、11、7这一递减序列。

学界如何评价

对于这一结果，报道援引相关研究者的看法称，它解决了一个数十年之久的猜想，对于哪些问题能够实现量子加速这一本质具有重要启示。这一评价来自长期阅读新证明的学者群体，而非单一来源。

报道同时强调，量子霸权并没有消失，该定理终结的是量子计算的盲目迷信，明确了量子优势的合法领地。换言之，量子计算在特定结构问题上仍具优势，但并非对所有随机输入都能无条件实现指数级超越。

用Aaronson与Ambainis的话说，量子计算仍有许多未解之谜，但现在又少了一个。报道的结语则称，在探索理性疆域的队伍中，如今不再只有人类自己。

要点

• 猜想由Aaronson与Ambainis于2008年提出
• Harness系统搭建完成后三天完成首个证明
• 证明已送入Lean证明助手接受检验
• 模型反复打磨中间结果，将指数从22压到11再到7
• 网友推测所用模型为非公开的Claude Model 4