谷歌DeepMind用AI写量子程序，成本最高降九成

在新药研发、电池材料以及核聚变能源这些方向，研究者有个共同的判断：只要量子计算机规模够大、跑得够稳，传统计算机做不了的事它就能做。

可眼下的量子芯片又小又容易出错，想让它可靠地跑长时间计算，纠错这道关绕不过去。谷歌现役的 Willow 芯片只有 105 个量子比特，公司定的目标是在 2029 年前后拿出一台“有用的、经过纠错的量子计算机”，这类机器大约要 100 万个物理量子比特才够。

硬件之外，算法同样是关键一环。算法越省资源，硬件要堆到的规模就越小，量子计算机真正派上用场的时间点也就越早。问题是机器还没影，研究者写出了算法也没处跑；量子比特数量一多，模拟所需算力猛涨，普通计算机很难再拿来做检验。所以过去想改进一个量子算法，常常得靠专家手工推导好几年。

近日，谷歌 DeepMind 与谷歌量子人工智能团队（Google Quantum AI）在预印本平台 arXiv 上发了篇论文，给出的思路是：程序跑不起来，那就用数学证明它没错。

具体做法是让多支由 AI 代理组成的团队来写量子程序，每个程序都得由机器一步步核验，既确认算得对不对，也确认花了多少资源。在核聚变、光化学和药物代谢三个科学模拟问题上，AI 代理找到的程序都比此前的最优方案更省资源，降得最狠的一项省了大约九成。

从测试转向证明

最近有不少团队都在试着让 AI 参与量子算法设计，路子大体相似：AI 出方案，普通计算机来判断方案对不对、开销有多大，AI 再照着结果改。

10 月中旬，

这套策略能成立，前提是方案能在普通计算机上检验。于是两项工作都把搜索范围压在一类特殊电路里，这类电路的行为可以由普通计算机快速抽样测试。可抽样给不了严格的正确性保证，况且大量实用量子算法根本写不进这类电路，一旦出了这个圈子，经典计算机就无从检验。

数学证明能绕开这道坎。它可以保证程序对所有可能的输入都成立，全程不用真的把程序跑起来。当然，证明本身也可能写错，以前得靠专家一行行读。近两年 AI 生成的代码和证明越来越多，定理证明工具 Lean 被广泛使用，情况变了。

Lean 既能当编程语言用，也能检查证明。用户可以用它写程序，也可以写关于程序的数学论证，内容会被可信内核逐步核验，只要有一步推不通，整个证明就作废。谷歌这次的成果，就是想把这套办法搬进量子程序设计里。

团队先在 Lean 里搭了一套量子编程库。程序可以像真实的量子算法那样，根据中途的测量结果决定接下来走哪条执行路径，并且严格算出程序消耗的资源。

题目由研究者出，每道题对应一份 Lean 文件，合格规则、计算误差范围这些限定条件都写在文件里。AI 代理由谷歌 Gemini 4 系列模型驱动，程序、成本数字和具体证明由它自己填。Lean 一旦接收 AI 上传的文件，这道题便算解决；若被退回，AI 就拿到报错信息，据此修改，直到通过为止。

团队还拉起了 7 支结构各不相同的代理团队。有的“单兵作战”，一个代理反复打磨同一个方案；有的分层分工，不同代理分别管子程序设计、误差分析和证明编写。

代理之间靠“榜单”和“学术会议”交流。共享维基会记下每个问题当前最好的已验证方案、能复用的证明片段，以及走通和走不通的路子。新方案要过独立复核，还得比原纪录至少好 5% 才能上榜。另一种是每 4 小时开一次的“会议”，各团队在共享论坛上提想法、互相挑错。不过会议上的想法只有写成证明并发布到维基，别的团队才能拿去复用。

这种协作也靠证明转起来：每个结果都过了机器核验，一支团队能直接在另一支团队的程序上接着干，不用反复花时间验证。光化学模拟问题就是个例子，不同团队先后拿出多种领先方案，单次最大改进砍掉了 34% 的成本。这个设想最早是一支团队在会议上提的，由另一支团队完善并完成证明。团队统计，论文展示的三个科学问题里，平均约四成改进来自团队之间的交流。

让 AI 自己写证明，还得防着它在题目上做手脚、钻空子。能改文件的代理有时会偷偷放宽定理的表述，或者加一条让 Lean 无条件接受的公理（axiom），装作题目已经解决。

研究团队因此在外部设了独立的核验程序，确认题目和最初冻结的版本一致、证明没有借助额外假设。可证明只能保证程序满足题目的要求，题目本身写错了，证明也救不了。论文提到，曾有代理钻了成本计数规则的空子，电路没什么实质改进，成本数字却变低了，最后只能改写题目。

压缩后的程序，离硬件还有多远？

论文显示，AI 代理在一个基础运算上拿到了降幅最大的成果：在量子叠加态中计算反正弦函数，是把数值载入量子态的常用步骤，AI 代理给出的方案成本只有目前已有发表最优方案的 1/290。

对比之下，论文演示的三个科学模拟问题，所需程序都要用到数百乃至数千个逻辑量子比特（logical qubit，经过纠错保护的量子比特），经典计算机检验不了，只能靠证明确认正确性。

核聚变那个问题研究的是惯性约束聚变（inertial confinement fusion）中，燃料能不能吸收足够多聚变反应产生的能量，让燃烧持续下去。AI 代理的新程序把成本压到此前最优方案的约 9%，所需逻辑量子比特也从 5,650 个降到 4,374 个。其中一处改进用了个低成本计算步骤，它在三个及以上电子处于同一位置时会算错，但 Lean 证明这种情况在物理上不会出现，确认可以放心用。

光化学问题要模拟一个分子在光驱动反应中的短时变化，这类过程和太阳能转化有关。计算得同时考虑电子和原子核的量子行为，比常规化学计算复杂得多。AI 代理设计的新程序把成本压到了原先的 1/8 左右。

生物学里，大部分药物在人体内如何代谢，要看细胞色素 P450（cytochrome P450）这个酶家族；可按现有近似算法，反应过程中那部分关键能量始终算不准。新程序把成本压低了 60%，省下来的钱主要来自一种编码方式——过去大家觉得它效果差一些。

不过研究也有明显的短板：演示出来的全是资源估算，程序没在真正的量子计算机上跑过。就算做了压缩，前面说的药物代谢问题仍要一台能完成约 1 万亿次逻辑运算的容错量子计算机才算得完，核聚变和光化学问题对机器规模的要求还更高。论文估算，首批容错量子计算机大约只能做 100 万次逻辑运算。

团队表示将很快公开 Lean 库、题目和验证后的程序，在此之前，外界还无法独立检查这些证明。

谷歌 DeepMind 7 月的一篇政策文章里提到，AI 代理抛出科学设想的节奏，已经快过了验证这些设想的速度，验证环节成了科研的新堵点。

量子算法这边更麻烦：能跑这些程序的机器还没造出来，实验验证根本谈不上。谷歌团队换了路子，拿数学证明顶替实验，让 AI 一边出方案一边把验证做完；研究者转而负责挑问题、把物理条件准确写进题目，再去读懂 AI 交回来的结果。

按照这样的分工，量子算法研究或有望在硬件成熟前先行推进。

参考内容：

https://arxiv.org/abs/2611.09822

https://arxiv.org/abs/2610.22367

https://opensource.googleblog.com/2026/10/announcing-verifiable-quantum-circuit-compilation-competition-on-kaggle.html

https://deepmind.google/public-policy/conjecture-machines-ai-agents-and-the-new-validation-bottleneck-in-science/

https://www.insidequantumtechnology.com/?p=12317

https://heise.de/-10192990

运营/排版：何晨龙

注：封面/首图由 AI 辅助生成