谷歌AI自主攻克量子算法优化难题，成本砍掉九成，还能自证无误
在新药研发、电池材料和核聚变能源等领域，研究者普遍认为，规模足够大、运行足够可靠的量子计算机有望做到传统计算机做不到的事。
但现实是，目前的量子芯片规模小、错误率高，必须经过纠错才能可靠地完成长时间的计算。谷歌目前的 Willow 芯片只有 105 个量子比特，而公司的目标是在 2029 年前后造出一台“有用的、经过纠错的量子计算机”，这样一台机器大约需要 100 万个物理量子比特。
硬件之外，算法的进展同样关键，算法越省资源，硬件需要达到的规模就越小，量子计算机派上用场的那一天也就来得越早。可机器还没造出来，研究者即便写出了量子算法，也没有机器可以运行；量子比特一多，模拟所需的计算量急剧膨胀，很难再用普通计算机模拟检验。因此过去，一个量子算法的改进往往要靠专家花上多年时间手工推导。
近日，谷歌 DeepMind 联合谷歌量子人工智能团队（Google Quantum AI）在预印本平台 arXiv 发表论文，介绍了一种新的做法：程序没法运行，那就用数学证明它是对的。
他们让多支由 AI 代理组成的团队编写量子程序，每个程序都必须由机器逐步核验，既要证明是否算对，也要证明消耗了多少资源。 在核聚变、光化学和药物代谢三个科学模拟问题的验证中，AI 代理找到的程序都比此前的最优方案更省资源，降幅最大的一项省下了约九成。
图 | 研究者编写题目后，AI 代理团队提交程序并根据 Lean 的报错反复修改，通过独立复核的结果发布到共享维基，各团队还会定期开会交流。（来源： arXiv ）
从测试到证明
近期不少团队都在尝试让 AI 帮忙设计量子算法，思路大多很直观：AI 提出方案，由普通计算机检验方案对不对、开销多大，AI 再据此改进。
10 月中旬，哈佛大学（Harvard University）、Anthropic 和量子计算公司 QuEra 的研究者发布预印本论文，用 Claude Mythos 5 模型在 8 个电路设计任务中的 7 个上降低了所需的量子比特和运算量。10 月 21 日，谷歌量子人工智能团队在数据科学竞赛平台 Kaggle 上发起了奖金池 15 万美元的竞赛，邀请外界用 AI 压缩核聚变、组合优化和化学模拟中的关键电路。
这种策略成立的前提，是设计方案能在普通计算机上检验。因此，两项工作都把搜索限制在一类特殊电路中，电路的行为可以由普通计算机快速抽样测试，但抽样无法严格保证正确，而且，大量实用的量子算法写不进这类电路，一旦超出范围，经典计算机也无从检验。
但数学证明可以绕开这道限制，它能确保程序对所有可能的输入都成立，而且全程不需要真的运行程序。不过，证明同样可能出错，过去要靠专家逐行审读，近两年，随着 AI 生成的代码和证明越来越多，定理证明工具 Lean 的广泛使用改变了这一点。
Lean 兼具编程语言和证明检查的功能，用户可以用它写程序，也可以写关于程序的数学论证，内容会受到可信内核的逐步核验，任何一步推不通，整个证明就不成立。谷歌的最新成果，正试图将这套方法搬进量子程序设计。
团队先在 Lean 中搭建了一套量子编程库，程序可以像真实的量子算法一样，根据中途的测量结果选择接下来的执行路径，并严格算出一个程序消耗的资源。
在这套库里，研究者负责出题，每个问题被写成一份 Lean 文件，其中包括合格规则、计算误差范围等限定条件，由谷歌 Gemini 4 系列模型驱动的 AI 代理自主填写程序、成本数字和具体证明。如果 Lean 接受了 AI 上传的文件，题目就算解决；如果不被接受，AI 会收到报错信息，继续修改直到通过为止。
团队还组建了 7 支结构各不相同的代理团队， 有的“单兵作战”，由一个代理反复修改同一个方案；有的分层分工，不同代理分别负责设计子程序、分析误差和编写证明。
AI 代理之间可以通过“榜单”和“学术会议”开展交流。共享维基会记录每个问题当前最好的已验证方案、可以复用的证明片段，以及走通和走不通的思路，新方案要经过独立复核，且比原纪录至少好 5% 才能上榜；另一种是每 4 小时举行一次的“会议”，各团队在共享论坛上提出想法、互相挑错。不过，会议产生的想法只有写成证明并发布到维基，其他团队才可以拿来复用。
这种协作同样依赖证明运转：每个结果都经过机器核验，一支团队可以直接在另一支团队的程序上继续工作，不必反复花时间验证。例如，在光化学模拟问题上，不同团队先后提出了多种领先方案，单次最大改进削减了 34% 的成本，它最初是一支团队在会议上提出的设想，由另一支团队完善并完成证明。团队统计，在论文展示的三个科学问题中，平均约四成改进都来自团队之间的交流。
让 AI 自己写证明，还得防着它在题目上动手脚、钻空子。能改写文件的代理有时会悄悄放宽定理的表述，或者加一条会让 Lean 无条件接受的公理（axiom），假装已经解决了题目。
研究团队为此在外部设置了独立的核验程序，确认题目与最初冻结的版本一致、证明没有借助额外的假设。不过，由于证明只能保证程序满足题目的要求，题目写得不对，证明也无能为力。 论文提到，曾有代理钻了成本计数规则的空子，电路没有实质改进，成本数字却变低了，最后只能改写题目。
压 缩后的程 序离硬件还有多远？
论文显示，AI 代理在一个基础运算上取得了降幅最大的成果：在量子叠加态中计算反正弦函数是把数值载入量子态的常用步骤，而 AI 代理给出的方案是目前已发表最优方案成本的 1/290。
相比之下，在论文中演示的三个科学模拟问题，所需程序都要用到数百乃至数千个逻辑量子比特（logical qubit，经过纠错保护的量子比特），无法用经典计算机检验，只能借助证明确认其正确性。