研究机构PSI宣布：AI系统三天证明困扰18年的量子猜想
研究机构 PSI（Physical Superintelligence）11 月 6 日宣布，其内部研究系统证明了 Aaronson-Ambainis 猜想。这个量子复杂性理论的猜想由计算机科学家斯科特·阿伦森与安德里斯·安巴尼斯于 2008 年提出，关系到量子计算机何时能比经典计算机快指数级，18 年来一直未获解决。
PSI 表示，这套由其技术人员戴维·图图雷安主导开发的研究系统，运行的是 Anthropic 尚未公开的模型实例，在运行的第三天得出了完整证明；此后系统又两次改进结果。证明的形式化版本由 Lean 证明助手逐项机检通过：公开的代码库包含 648 条机器验证的定理，没有留空待证的占位、也没有添加额外公理，并经两种独立的 Lean 内核实现复核。论文与 Lean 代码已一并公开。
需要说明的是，这项成果目前没有经过同行评审，论文为预印本；阿伦森与安巴尼斯本人尚未公开表态。PSI 的代码库也留了一项工作给读者：形式化陈述是否与猜想原文完全等价，需要专家自行确认；供人阅读的论文文本本身不在机检范围内。今年 8 月，斯坦福大学团队曾证明该猜想的一个特例（固定并行轮次的情形）；PSI 称其证明覆盖一般情形，最终结论仍待学界检验。
（来源：PSI）
Startup PSI Says Its AI System Proved an 18-Year-Old Quantum Conjecture in Three Days
Research startup PSI (Physical Superintelligence) announced on November 6 that its internal research system has proved the Aaronson-Ambainis conjecture. Stated by computer scientists Scott Aaronson and Andris Ambainis in 2008, the quantum complexity conjecture bears on when quantum computers can be exponentially faster than classical machines, and had resisted proof for 18 years.
PSI says the research system — built and run by member of technical staff David Turturean — runs instances of a non-public Anthropic model, and produced a complete proof on the third day of its run; the system then improved the result twice. The formal version was machine-checked step by step by the Lean proof assistant: the public repository holds 648 machine-checked theorems, with no unproved placeholders and no added axioms, re-verified by two independent Lean kernel implementations. The paper and the Lean code were released together.
The result has not been peer-reviewed and the paper is a preprint; neither Aaronson nor Ambainis has publicly weighed in. PSI's repository also leaves one task to readers: confirming that the formal statement matches the conjecture as originally printed, since the human-readable paper itself is not machine-checked. In August, a Stanford team proved a special case of the conjecture, for algorithms using a fixed number of parallel query rounds; PSI says its proof covers the general case. Whether it holds under sustained expert scrutiny remains the open question.
(Source: PSI)
来源：PSI
发布：GSM·美国（发布链接）
图片来源：图：IBM 量子计算机装置。An IBM quantum computing installation. (Wikimedia Commons, CC BY 2.0)
GSM Global · 本篇英文版 English edition of this story
