谷歌DeepMind用Lean证明把关：AI设计量子算法，最高省九成成本

在新药研发、电池材料、核聚变能源这些方向上，研究者有一个普遍判断：只要量子计算机的规模够大、运行够可靠，它就有望完成传统计算机做不到的任务。

可眼下的量子芯片规模偏小、错误率高，得先过纠错这一关，才能撑起长时间运算。谷歌现有的 Willow 芯片仅有 105 个量子比特；公司打算在 2029 年前后造出一台“有用的、经过纠错的量子计算机”，而这样一台机器大约要 100 万个物理量子比特。

算法同样关键。算法越省资源，硬件所需的规模就越小，量子计算机真正派上用场的时间点也会提前。问题是机器尚未造出，研究者写出了算法也无处运行；量子比特一多，模拟所需计算量急剧膨胀，普通计算机很难再承担检验任务。所以过去，量子算法的每一次改进，常常要专家手工推导多年。

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

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

从测试转向证明

近来不少团队都在尝试用 AI 设计量子算法，做法大多很直接：AI 出方案，普通计算机检查方案是否正确、开销多大，AI 再据此调整。

10 月中旬，哈佛大学（Harvard University）、Anthropic 和量子计算公司 QuEra 的研究者发布预印本论文，用 Claude Mythos 5 模型在 8 个电路设计任务中的 7 个上降低了所需的量子比特和运算量。10 月 21 日，谷歌量子人工智能团队在数据科学竞赛平台 Kaggle 上发起竞赛，奖金池 15 万美元，邀请外界用 AI 压缩核聚变、组合优化和化学模拟中的关键电路。

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

数学证明能绕开这道坎：它可以确保程序对所有可能的输入都成立，全程不必真正运行程序。当然，证明本身也可能出错，过去靠专家逐行审读。近两年，AI 生成的代码和证明越来越多，定理证明工具 Lean 的广泛使用改变了这一局面。

Lean 既是编程语言，也是证明检查器。用户可以用它写程序，也可以写关于程序的数学论证，内容会由可信内核逐步核验，只要有一步推不通，整个证明就不成立。谷歌这项新成果，正试着把这套方法引入量子程序设计。

团队先是在 Lean 中搭起一套量子编程库。程序能像真实的量子算法那样，依据中途测量结果决定后续执行路径，并严格算出自身消耗的资源。

这套库里的出题环节由研究者包办：一份 Lean 文件对应一道题，合格规则、计算误差范围这些限制条件都写在文件里。AI 代理由谷歌 Gemini 4 系列模型驱动，程序、成本数字和具体证明都由它自己填。AI 把文件传上去，Lean 点头，题就算过了；Lean 不认，报错信息会退回来，代理就接着改，一遍遍改到通过。

此外，7 支代理团队也搭了起来，彼此结构并不一样。有的让一个代理单干，对着同一套方案反复打磨；有的走分层分工的路子，设计子程序、分析误差、编写证明分别交给不同代理。

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

这种协作同样靠证明运转：每个结果都经过机器核验，一支团队能直接在另一支团队的程序上继续做，不必反复花时间验证。比如在光化学模拟问题上，不同团队先后提出多种领先方案，单次最大改进削减了 34% 的成本——它最初是一支团队在会议上提出的设想，由另一支团队完善并完成证明。团队统计，论文展示的三个科学问题中，平均约四成改进来自团队之间的交流。

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

所以研究团队在外面另设了独立核验程序，查两件事：题目跟最初冻结的版本是否一致，证明有没有借额外假设。但证明能管的只是程序符不符合题目要求，题目本身要是写错了，证明也救不回来。论文里提到，有代理钻过成本计数规则的空子——电路没实质改进，成本数字反倒降了，最后只好回头改题目。

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

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

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

核聚变这一题，盯的是惯性约束聚变里燃料能不能吃进足够多聚变反应放出的能量，让燃烧自己维持下去。AI代理给出的新程序把成本压到此前最优方案的约9%，逻辑量子比特需求从5,650个降到4,374个。改动里有一处用了个便宜的计算步骤，三个及以上电子挤在同一位置时它会算错，不过Lean证明了这种情况在物理上不会发生，所以能放心用。光化学那题要模拟分子在光驱动反应中的短时变化，这类过程和太阳能转化有关，算的时候电子与原子核的量子行为得一起考虑，比普通化学计算复杂不少。AI代理设计的新程序把成本压到原来的1/8上下。

生物学那边，人体代谢大多数药物靠的是一个叫细胞色素P450（cytochrome P450）的酶家族，现有近似算法很难算准它在反应中的关键能量。新程序省下60%的成本，省下来的部分主要来自一种过去被认为效果稍差的编码方式。

研究也有明显的短板：演示出来的都是资源估算，程序没在真实量子计算机上跑过。就算压缩过，药物代谢这题仍要一台能做约1万亿次逻辑运算的容错量子计算机才算得完，核聚变和光化学所需的机器还要更大。论文估计，最早那批容错量子计算机大概只能做100万次逻辑运算。

团队说Lean库、题目和验证过的程序很快就会公开。在这之前，外面的人还没法独立核查这些证明。

谷歌DeepMind在7月的一篇政策文章里提到，AI代理抛出的科学设想已经比验证它们的速度快，验证正变成科研的新卡点。量子算法这块更棘手——能跑这些程序的机器还没造出来，实验验证根本谈不上。谷歌团队的办法是拿数学证明顶替实验，让AI一边给方案一边把验证做完；研究者的活则变成挑问题、写能准确反映物理条件的题目、读懂AI吐出来的结果。照这个分工，量子算法研究有可能赶在硬件成熟之前先往前走。

运营/排版：何晨龙

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