⚛️ quantum physics

AlchemQ: Proof-Carrying Quantum Circuit Optimization with Per-Result Equivalence Certificates

本文介绍了 AlchemQ v0.5，这是一个概念验证系统，它通过将不可信的优化器与一个可由机器检查的认证层相结合，为每一次输出生成自包含且防篡改的等效性证书，从而确保量子电路优化的可靠性，并保证所有优化后的电路都经过了正确性和非退化性的验证。

原作者： Adam Laabs

发布于 2026-09-18

📖 1 分钟阅读🧠 深度阅读

CC BY 4.0

原作者： Adam Laabs

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

在量子计算那静谧且受控的世界里，科学家们构建出复杂的指令序列，用以操纵物质最小的单元。这些被称为“电路”的指令，旨在解决普通计算机无法处理的问题。然而，从理论构想到实现工作的量子程序，其路径充满了危险。为了让这些电路高效运行，软件工具必须不断地重写并简化它们，剔除不必要的步骤。问题在于，这些工具并不完美。它们是由人类编写的复杂程序，和任何软件一样，都包含隐藏的错误。当一个工具在不知不觉中以破坏逻辑的方式改变了电路时，其结果就是一次失败的实验，白白浪费了昂贵的时间和资源，而这些硬件是无法轻易重置的。科学界长期以来一直需要一种方法，来保证一个简化的电路确实与原始电路等效，而不仅仅是一个看起来正确的猜测。

一个名为 AlchemQ 的新系统为这个问题提供了不同的处理方式。研究人员并没有试图证明软件工具本身是完美的，而是构建了一个将每一个输出都视为“嫌疑人”，直到被证明“清白”的系统。他们创建了一个流程：由优化器建议一个简化版的量子电路，然后一个独立的、单独的检查器立即验证新版本是否与旧版本执行的操作完全一致。如果检查器发现哪怕极其微小的差异，该建议就会被丢弃。如果通过了验证，系统会颁发一份数字证书——一份自包含的文档，证明两个电路是恒等的。这份证书旨在让任何人、在任何地方都能阅读，而无需信任创建它的原始软件。这是一种“证明携带型优化”（proof-carrying optimization）的方法，证据随结果一同传递。

研究人员在一组包含一百个不同量子电路的大型集合上测试了该系统，这些电路涵盖了从标准基准测试到复杂的随机生成示例。他们运行优化器以寻找这些电路的更佳版本，随后对每一个结果都进行了严格的验证过程。该系统运行得毫无差错。四百次优化尝试全部顺利完成，没有出现错误，并且返回的每一个电路都附带了一份有效的证书，证明其与原始电路等效。该系统还捕捉到了一个广泛使用的库中存在的细微漏洞，研究人员在进行验证时使用了该库。在一种特定情况下，该库用于比较两个电路的标准方法放大了微小的数值噪声，导致它错误地拒绝了一个完美的优化结果。AlchemQ 系统检测到了这一失效，识别出了错误的来源，并对其进行了修正，这证明了验证层能够发现那些优化工具本身可能会遗漏的问题。

除了捕捉错误外，该系统还证明了它能够找到真正的改进。平均而言，优化后的电路比原始版本明显更短，且使用的复杂门数量更少。在一次针对 IBM 真实量子硬件的具体测试中，经该系统优化的电路比未优化的版本浅了 78%，且使用的双比特门减少了 6 de 65%。当研究人员在物理机器上运行原始电路和优化后的电路时，结果几乎完全相同，这表明剧烈的简化并未损害输出质量。虽然由于实验次数有限，性能差异在统计学上尚未达到显著水平，但趋势清晰地指向优化后的电路表现更好。

研究人员还探索了不同的数学规则如何影响决策过程中的“最优”结果。他们测试了三种不同的方法，用于权衡各种改进指标，例如减少门数量与减少电路深度之间的权衡。令人惊讶的是，对于他们测试的标准电路集，所有三种方法都产生了完全相同的结果。只有在他们测试一组专门设计的、具有对抗性的困难电路集时，这种规则差异才会显现出来——在这些罕见的情况下，不同的规则会导致不同的选择。但系统通过确保无论使用哪种规则，最终电路在任何单一类别上都不会比原始电路表现更差，从而处理了这一问题。

这项工作并非旨在取代驱动优化的复杂软件，而是将其定位为叠加在优化软件之上的安全网。研究人员明确指出，他们的优化器是一个简单的实验性工具，而真正的力量在于那份证书。通过将正确性的证明作为输出的标准组成部分，他们允许任何人独立验证工作成果。该系统设计具有透明性；证书包含了所有必要的数据，例如所使用的软件确切版本以及应用的特定数学容差，因此证明过程可以在任何计算机上进行复现。研究人员已向公众发布了证书格式和验证软件，邀请他人检查他们的工作并将其用于自己的实验。

这项研究的终极目标是建立对量子软件流水线的信任。通过确保每一个优化的电路都附带一份机器可检查的正确性保证，该系统消除了发生隐性失效的风险。它承认用于构建量子软件的工具总会存在漏洞，但它提供了一种在这些漏洞造成实际损害之前将其捕捉到的方法。该系统并不声称自己是量子优化的终极方案，也不承诺解决所有问题。相反，它提供了一个务实且可验证的进步，证明了构建一个“结果始终伴随其自身真理证明”的系统是完全可能的。

技术摘要：AlchemQ v0.5

问题陈述

量子线路优化是一种对正确性至关重要的变换，因为优化后的线路将替换原始线路，且通常是在单次错误就会导致昂贵实验失效的硬件上运行。目前的工具链依赖于启发式或学习型重写过程（例如模板匹配、ZX-演算简化、强化学习），这些过程提供的正确性证据非常微弱。生产级编译器应用长序列的重写，却缺乏针对单个结果的保证；而广泛使用的编译器（如 Qiskit）中出现的历史性漏洞曾导致电路被静默损坏。形式化验证整个编译器极其耗费资源，且往往滞后于启发式的先进技术，而现有的等效性检查器通常仅作为流水线中的断言，而非为单个结果生成独立的、机器可检查的证据。核心问题在于缺乏一种机制，能够为每一个优化的电路制品附加自包含、防篡改且可独立验证的等效性证明。

方法论

AlchemQ v0.5 提出了一种**携带证明的优化器（proof-carrying optimizer）**架构，将不受信任的优化引擎与受信任的认证层解耦。该系统的运作原则是：优化器是不可信的，但契约（即证书）是唯一受信任的组件。

系统架构

系统由七个模块组成，包括一个束搜索（beam-search）优化器、一个使用模糊 t-范数（fuzzy t-norms）的评分引擎以及一个双层认证协议。

优化器： 一个固定种子的束搜索代理，探索重写建议（门合并、交换、逆操作抵消以及基于 PyZX 的提取）。在结构上，它无法返回未经认证的电路。
认证硬门槛（Certification Hard Gate）： 每个候选电路在进入束搜索之前必须通过认证检查。认证器通过两条路径证明其在全局相位下的等效性：
- ZX 路径： 将电路转换为 ZX 图并应用 full_reduce 和 normalize。如果结果是严格的恒等图，则精确证明等效性，并通过图标量（graph scalar）得出全局相位。
- 数值回退路径： 对于 ZX 路径无法得出结论的 $\le 6$ 量子比特电路，系统计算稠密张量并估计相对相位（通过最优希尔伯特-施密特重叠 $\phi^* = \arg\langle t_0, t_1 \rangle$ ）。它使用归一化残差度量而非单一枢轴元素，以避免噪声放大。
安全性保证： 自 v0.4 版本起，代理强制执行分量级非退化（componentwise non-regression）。如果候选电路相对于原始电路而非基准电路恶化了任何目标函数（T-count、双比特门计数或深度），则会被拒绝。
聚合： 代理使用三种模糊 t-范数（Gödel、Product、Łukasiewicz）来聚合各目标的得分。

认证协议

AlchemQ 引入了两种认证协议：

协议 0.1.1： 用于搜索循环内部的遗留格式。
协议 0.2.0： 发布格式，旨在用于离线的第三方验证。其特点包括：
- 带有规范哈希（gate-canon-v1）的自包含 JSON 制品，用于篡改检测。
- 三态判定： certified（已认证）、rejected（已拒绝）或 inconclusive（无法确定），避免了沉默的布尔舍入。
- 版本化 Schema，用于相位说明和规范化器，以确保跨平台的复现性。
- 结构化的验证结果及原因代码。

核心贡献

开放认证协议： 一种版本化的、防篡改的制品格式（协议 0.2.0），允许第三方仅凭嵌入的电路即可重新验证等效性。它包含从遗留版本迁移的严格路径。
参考认证器与验证器： 实现了一个通过 ZX-演算全还原结合数值张量回退来证明至全局相位等效性的系统。它明确记录了如何确定全局相位（通过测量、通过见证者或未追踪）。
结构化安全搜索代理： 一个玩具级的代理，保证不会返回未经认证的电路，永远不会低于基于 PyZX 的基准线得分，且绝不会在分量级上相对于原始电路发生任何目标退化。
缺陷的经验验证： 系统成功识别并诊断了两个关键缺陷：
- 一个广泛使用的上游库（PyZX 的 compare_tensors）中的假阴性问题，其中枢轴归一化将数值噪声放大了约 $2 \times 10^8$ ，导致正确的优化被拒绝。
- 八个仅在 macOS 上失败的证书，原因是 BLAS 相关的原始浮点数渲染影响了相位说明，这通过版本化的相位说明 Schema 得到了解决。

结果

系统在包含 100 个电路（QASMBench、Feynman 以及生成的 Clifford+T 实例）的基准测试上进行了评估，共产生了 400 次优化。

正确性与鲁棒性： 所有 400 次优化均在未出现错误或超时的情况下终止。每个返回的电路都被证明是等效的。2998 项测试套件在 Linux (Python 3.12) 和 macOS (Python 3.14) 上均通过。
性能对比基准： 对于具有非零 T-count 的电路，PyZX 基准线平均减少了 21.4% 的 T-count。在当前的评分语义下，代理从未差于基准线，并在 100 个电路中的 9 个上表现优于基准线（在 Gödel 和 Product 范数下）。
T-范数分析： 在标准的 100 电路基准测试中，所有三种 t-范数都返回了相同的最终电路。仅在 4/38 个对抗性消融实验实例中出现了分歧，这些实例中帕累托前沿（Pareto fronts）在不同目标之间提供了真实的权衡。
硬件实验： 在 IBM Heron r2 (ibm_kingston）上的初步实验显示，经认证优化后的电路比原始电路浅 78%，且双比特门减少了 65%。虽然点估计值在所有质量指标（总变差距离、Hellinger 保真度、Simon 约束率）上都倾向于优化后的电路，但由于 1024 次采样产生的噪声，这些差异在统计学上并不显著。

意义与主张

本文将 AlchemQ 定位为一个携带证明的优化器，这与经过形式化验证的编译器不同。

以制品为中心的信任： 不同于验证编译器（如 VOQC, CertiQ）证明编译器代码本身正确，AlchemQ 为单个结果附加了机器可检查的证据。这使得任何优化器（即使是未经验证或基于学习的）都可以置于相同的信任契约之下。
故障检测： 该系统的主要价值不仅体现在优化增益上，还在于其能够发现底层工具链（PyZX）中的缺陷以及标准基准测试可能忽略的跨平台复现性问题（BLAS 依赖）。
范围适中： 作者明确指出，AlchemQ 并非工业级优化过程的竞争性替代品，也不是一个学习型优化器。它是一个试点研究，旨在展示一个小型、不受信任的优化器配合一个严谨的认证层，可以产生可独立验证、字节级可复现且保证非退化的输出。该系统的设计理念是“对优化器本身保持对抗性”，将证书视为唯一的信任接口。