Verified Pauli-Product Measurement Compilation for Fault-Tolerant Quantum Computation

量子计算机有望解决目前即使是最强大的超级计算机也无法完成的问题，从破解复杂的密码到模拟新材料。然而，这些机器极其脆弱。来自热量或振动的哪怕最轻微的干扰都可能导致其计算崩溃。为了生存，科学家们正在构建容错量子计算机，它们使用特殊的纠错码来保护信息。这些系统并非将数据存储在单个脆弱的粒子上，而是将信息分散在许多粒子中，不断检查并修复错误。挑战在于翻译：如何将高层算法转换为这些纠错机器实际能够执行的具体底层操作？

许多这类未来机器的标准方法涉及一种称为晶格手术（lattice surgery）的技术。想象一张代表计算机内存的大型织物。要执行计算，你不仅仅是拨动一个开关；而是以精确的模式将这些织物的碎片缝合在一起并将其拉开。这些缝线并非物理上的线，而是对成组粒子的联合测量。计算机测量这些组之间的关系，将结果记录为简单的位数据，然后利用该数据决定下一步的操作。这个过程被称为泡利乘积测量（Pauli-product measurement），是这些未来机器的基础语言。问题在于，用于将人类设计的算法翻译成这种语言的软件工具一直未经验证。如果编译器在翻译过程中出错，整个计算都可能失败，并且由于过程如此复杂，很难知道错误发生在何处。

加州大学洛杉矶分校的一个研究小组通过创建一个能够从数学上证明翻译正确性的系统，填补了这一空白。他们开发了一种专门针对这类基于测量的程序的语言，并构建了一个能将标准量子电路转换为这种语言的编译器。至关重要的是，他们不仅编写了代码，还使用了一种名为 Lean 的形式化验证工具，构建了一个严密的数学证明，证明他们的编译器保留了原始算法的行为。这意味着对于编译器的每一步操作，都有一个证书保证输出结果完全符合输入所期望的结果，甚至精确到了结果的具体概率。

研究人员专注于两个主要任务：降级（lowering）和优化。降级是将一个标准的量子门（如旋转门或逻辑门）分解为晶格手术硬件所需的测量与修正序列的过程。优化则涉及重新排列这些测量，使过程更快、更高效。在他们的工作中，他们证明了编译器可以将一个电路翻译成测量指令，然后应用规则来融合和重排这些指令，而不会改变最终结果。他们验证了编译器能够正确处理“魔术态”（magic states）——即执行某些类型计算所需的特殊资源，并确保在保持公共结果可访问的同时，将私有测量结果对外界隐藏。

当他们在 35 个小型量子电路套件上测试该系统时，结果是具体且可衡量的。经过验证的编译器成功翻译了每一个有效的输入，并生成了一个确认翻译正确的证书。在性能方面，他们验证的优化技术将运行这些电路所需的逻辑测量轮数平均减少了 17.9%。对于某些特定电路，这种减少甚至更高，达到了近 29%。这种减少非常显著，因为在这些容错系统中，每一轮测量都需要时间和资源；减少轮数直接意味着计算机运行得更快、效率更高。

该团队还展示了如何处理近似计算，这在无法构建精确的完美数学旋转时是必要的。他们创建了一种方法来限制这些近似所引入的误差，确保最终结果保持在用户定义的限度内。他们展示了系统如何从候选列表中选择出最佳版本的电路，即选择那个既符合误差限度又使用最少资源的电路。这一选择过程也经过了验证，这意味着计算机不会意外地选择一个过于不准确或过于缓慢的电路。

这项工作代表了一种转变：从“希望编译器有效”转向“确定编译器有效”。通过为整个编译流水线构建机器检查证明，研究人员消除了通往大规模量子计算路径中的一个主要不确定性来源。他们证明了可以将复杂的算法翻译成纠错硬件的特定语言，并针对速度进行优化，同时保持逻辑完整性的数学保证。该系统成功处理了多达 433 个量子比特的电路，证明了这种级别的验证可以扩展到实质性的问题。虽然运行这些电路的物理硬件仍在开发中，但这一软件基础确保了当机器到来时，发送给它们的指令是值得信赖的。