在新药研发、电池材料和核聚变能源等领域，研究者普遍认为，规模足够大、运行足够可靠的量子计算机有望做到传统计算机做不到的事。
但现实是，目前的量子芯片规模小、错误率高，必须经过纠错才能可靠地完成长时间的计算。谷歌目前的 Willow 芯片只有 105 个量子比特，而公司的目标是在 2029 年前后造出一台“有用的、经过纠错的量子计算机”，这样一台机器大约需要 100 万个物理量子比特。
硬件之外，算法的进展同样关键，算法越省资源，硬件需要达到的规模就越小，量子计算机派上用场的那一天也就来得越早。可机器还没造出来，研究者即便写出了量子算法，也没有机器可以运行；量子比特一多，模拟所需的计算量急剧膨胀，很难再用普通计算机模拟检验。因此过去，一个量子算法的改进往往要靠专家花上多年时间手工推导。
近日，谷歌 DeepMind 联合谷歌量子人工智能团队（Google Quantum AI）在预印本平台 arXiv 发表论文，介绍了一种新的做法：程序没法运行，那就用数学证明它是对的。
他们让多支由 AI 代理组成的团队编写量子程序，每个程序都必须由机器逐步核验，既要证明是否算对，也要证明消耗了多少资源。在核聚变、光化学和药物代谢三个科学模拟问题的验证中，AI 代理找到的程序都比此前的最优方案更省资源，降幅最大的一项省下了约九成。
（来源：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，经过纠错保护的量子比特），无法用经典计算机检验，只能借助证明确认其正确性。
（来源：arXiv）
其中，核聚变问题研究的是惯性约束聚变（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 辅助生成
