11 月 6 日，美国 AI 物理实验室 PSI（Physical Superintelligence）宣布，其内部研发的研究系统运行未公开的 Anthropic 模型，找到了 Aaronson–Ambainis 猜想的证明。这个由 Scott Aaronson 与 Andris Ambainis 在 2008 年提出的量子复杂性理论核心问题，悬了整整 18 年。按 PSI 的说法，系统在运行的第 3 天就拿出了完整证明，Lean 证明助手逐行验算通过；随后系统又在相关问题上把结果改进了两次，Lean 每次都通过。60 页论文与 Lean 4 形式化证明已公开在 GitHub 上。
这个猜想问的是：量子计算机到底在什么时候能比经典计算机指数级更快？结论是，对没有结构的随机输入，量子计算机做不到指数级加速——经典计算机只需要多项式次数的查询就能模拟它的回答。换句话说，Shor 算法那种指数级加速，需要输入本身带有结构。最终的界是：某个输入位对结果的影响力至少约为 0.0025·Var(f)5/2/d6，指数从最初的 22 一路优化到 11、最终 7。证明沿用了 Shachar Lovett 与 Jiapeng Zhang 的路线，关键一步是用行列式配对构造的新不等式，替代了他们留下的未解不等式。
验证链条目前是这样的：形式化证明包含 648 个机器验证的定理，没有占位符、没有额外公理，代码按 Apache 2.0 开源；今年 8 月证明了该猜想特例的斯坦福团队（Guy Blanc、Jordan Docter、Carmen Strassle、Li-Yang Tan）正在审读证明，并为专家写简版，据报道称之为“重大成果”。但保留意见也不少：论文尚未经过同行评审；Lean 只保证形式化陈述本身成立，形式化定义是否与原猜想完全一致，仍需数学家人工确认；人类可读的论文正文不在机器验证范围内；所用模型未公开、系统不对外，别人无法复现这次三天运行。Aaronson 与 Ambainis 截至 11 月 7 日尚未公开表态。
如果证明最终站得住脚，这将是 AI 攻下的最重量级的开放数学问题之一——不是解一道现成习题，而是给出一个被机器逐行验证的完整证明。Anthropic 模型本身的研发速度也在加速，METR 最近的评估称其能力提升速度比一年前翻了一倍（AI 一年干了两年的活）；而 DeepMind 上周也用 AI 智能体找出了 1024 位 RSA 的两处弱点（DeepMind 用 AI 智能体找出 1024 位 RSA 两处弱点）。AI 正在从“帮人算”走向“帮人证”，数学证明这条路，可能比多数人预想的走得更快。
来源：PSI，原文
没有回复内容