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