电路等价性验证｜中性原子量子计算知识库

编译器对电路动辄改头换面——重排、路由、优化——验证”编译结果仍然实现原功能”本质上是判定 $G^{†} G^{'} = 1$ ，这是一个 QMA-完全问题；ZX 演算用”把组合电路化简到恒等”的做法在大量真实实例上秒级通过，成为编译流正确性的实用防线。

问题背景

算法描述（高级门集）到硬件执行（低级门集 + 架构约束）之间的所有变换——综合、映射、路由（SWAP 插入）、优化——都可能引入错误。电路等价性验证（equivalence checking）问的是：电路 $G$ 与编译产物 $G^{'}$ 是否实现同一幺正？概念上简单：比较两个 $2^{n} \times 2^{n}$ 矩阵 $U, U^{'}$ ；实际上矩阵指数大，直接比较不可行——哪怕只是”跑一遍看输出”，最坏情形也等价于全态模拟——且该问题已被证明是 QMA-完全的（QMA 之于量子计算如 NP 之于经典计算） Burgholzer 2020 Peham 2022。

三大主流范式各有地盘 Peham 2022：

决策图（decision diagrams, DD）：矩阵的紧致规范型表示，等价判定是平凡的（规范型唯一）；
路径和（path sums）：电路的代数（多项式/求和）表示；
ZX 演算：图形重写（本条重点），实现于 PyZX（PyZX 与图论化简）与 Munich Quantum Toolkit 的开源工具 QCEC Peham 2022。

对中性原子这类”编译链长、重构频繁”的平台——布局映射（OLSQ-DPQA）、分治搬运（DasAtom 分治搬运）、分区调度（分区架构）层层变换——编译结果的等价检查不是锦上添花，而是整条编译流可信的前提。

理论模型

判定条件与 ZX 方法

等价的代数判据是

G \equiv G^{'} ⟺ U_{G^{†} G^{'}} = U_{G^{'}}^{†} U_{G} = 1 (可能相差输出端置换) .

ZX 方法把 $G^{†}$ 与 $G^{'}$ 拼成一张 ZX 图（输出弯回输入），然后用化简规则削减：同色蜘蛛融合、恒等消去、局域补图与支点变换。若图被化简到空图（恒等），等价得证。两个关键理论事实 Peham 2022：

可靠但不完备：化简到恒等 $\Rightarrow$ 等价；化不干净不能下结论。不完备性在带 ancilla 的电路（辅助比特仅中途使用）上尤其突出——NA113 通过把 ancilla 显式纳入 ZX 框架部分缓解，但一般不可判定性仍在。一个理论上的例外是纯 Clifford 电路：由于演算对 Clifford 类完备 van de Wetering 2020，此时”化简失败”即可反证不等价，判定重新变得完备；
资源有界：等价检查中蜘蛛数严格单调下降，故 ZX 方法的内存上界由原电路规模决定，最坏情形运行时间约 $O (n^{3})$ ——适合与其它方法并行运行、互不挤占资源。

与之对照，DD 是规范型： $G^{†} G^{'}$ 的系统矩阵若为恒等，其决策图必为恒等图，故 DD 方法天然完备（可证等价亦可证不等价），但表示尺寸随 qubit 数指数波动，且对含任意旋转角的算法存在浮点精度敏感性——数值误差累积后”几乎恒等”的中间图可能爆掉 Peham 2022。ZX 图对数值误差不敏感，这正是它作为补充的价值。

编译流知识与置换处理

真实编译流的两个坑：初始布局/末态置换（编译后的逻辑-物理 qubit 映射与输入不同）与 SWAP 路由。NA108 在验证 Qiskit 编译流时确立的处理原则 Burgholzer 2020：

用 qubit 映射 $m (\cdot)$ 显式追踪布局变化，输出端按置换补偿后再比较；
编译器常把 SWAP 展开成 3 个 CNOT——连续的特定 CNOT 序列要逆向重构成 SWAP 再对消，否则大量真实优化无法通过验证；
利用”编译流知识”决定 $G$ 与 $G^{'}$ 门的施加次序，使中间表示始终贴近恒等，把经常性指数复杂度压到线性或近线性。

不等价判定与互补调度

验证不只回答”等价”，还要快速否定”不等价”。对不等价电路，化简到恒等几乎注定失败，但此时判定应当尽快终止：DD 方法可用随机输入模拟，少数次模拟即高概率暴露差异；ZX 侧则表现为化简迅速停滞。NA113 的实践是让多范式在 QCEC 中按”交替/引擎”策略协同：先用便宜的方法筛查，再交给最可能成功的方法深算 Peham 2022。对数值敏感电路（含任意旋转角的变分线路等），DD 中间表示的浮点误差会使”几乎恒等”的图无法收缩甚至爆炸，ZX 重写对这类数值噪声稳健，恰好补位 Peham 2022。

评测协议与失效模式

NA113 的对比实验给出了可复用的评测协议 Peham 2022：把高级电路编译到 65-qubit IBM Manhattan 架构（任意单比特旋转 + CNOT）验证编译结果；再把原电路与其 O1/O2 优化版对照（O1 平均仅优化掉 $0.9%$ 的门、O2 为 $6.1%$ ——这说明”优化幅度小”的编译产物同样需要验证，错误往往藏在重排与置换里）。随机基准由 CNOT + 各 $20%$ 概率的 Hadamard 与 T 门构成，按比特数/门数扫描运行时间；可逆基准覆盖加法器、oracle 与 Toffoli 链。失效模式也值得记录：DD 的失败通常表现为 1 小时超时前的内存耗尽，ZX 的失败表现为化简停滞——蜘蛛数不再下降但不能归零；对带 ancilla 的电路（如多控 Toffoli 的含 ancilla 分解），ZX 方法的不完备性最易显形 Peham 2022。

方法与实现

QCEC 工具链：NA113 将 ZX 方法与路径和、DD 集成进 QCEC（MQT 组件，C++），支持编译结果验证与优化前后等价两种用例；评测把电路编译到 65-qubit IBM Manhattan 架构，并以 O1/O2 优化级做等价对照（O1 平均优化掉 $0.9%$ 的门，O2 为 $6.1%$ ） Peham 2022。
实用判据：可逆电路（加法器、oracle 等 Clifford+T 类）上，ZX 与路径和缩放相近，但 ZX 平均快数个数量级；含大块可逆逻辑的电路（Grover、QWL 等）DD 更占优；两两互补、宜并联使用 Peham 2022。
大规模编译验证：NA108 的流感知 DD 方案在数万门规模的电路上秒级完成验证，而既有通用技术在 1 小时超时内频繁失败；该方案与编译器无关，可移植到任何编译流 Burgholzer 2020。
不等价的快速筛查：对确实不等价的电路，DD 可用随机输入模拟快速暴露差异（少数次模拟即高概率发现）；ZX 化简路径则表现为”化不干净”，二者结合可快速分流 Peham 2022。
开源工具：ZX 等价检查的参考实现随 QCEC 发布（github.com/cda-tum/qcec，MQT 组件）；NA108 的 Qiskit 流验证器亦开源（github.com/iic-jku/qcec），二者均可直接接入 CI 对编译结果做回归验证 Peham 2022 Burgholzer 2020。
正确性的分层观：超优化器（Quartz 超优化）在替换生成期用定理证明器逐条把关，编译末端再用整电路等价检查兜底——两层验证缺一不可，因为优化与映射、置换的组合效应无法在单条替换层面预见。
验证的抽象层级：等价检查在门/线路层工作，不覆盖脉冲波形与噪声误差——门目标在局域等价意义下的定义见门相位与局域等价，物理层误差的建模见误差预算与真实建模。
与中性原子工具链的衔接：原子搬运、重排与并行门调度类编译器输出的是”门 + 移动”混合序列，验证前需按末端原子位置还原纯电路；等价检查应作为编译器公平评测与可视化中正确性一票否决项，与中性原子基准测试的保真度指标互补。

结果对比

范式/指标	结论/数值	来源
问题复杂度	QMA-完全（含置换/ancilla 变体）	Peham 2022
可逆电路（等价例）	ZX vs 路径和：92% 实例运行时差 < 10 s，ZX 平均快数个量级	Peham 2022
大块可逆逻辑电路	DD 显著占优（Grover、QWL、adder/oracle）	Peham 2022
ZX 内存/时间	蜘蛛数严格下降：内存有界，最坏约 $O (n^{3})$	Peham 2022
DD 完备性	规范型 → 等价/不等价皆可判定；对任意旋转角数值敏感	Peham 2022
流感知验证规模	数万门电路秒级（基线 1 h 超时频发）	Burgholzer 2020
评测编译目标	65-qubit IBM Manhattan；O1/O2 优化 0.9%/6.1% 门	Peham 2022
随机基准构成	CNOT + 各 20% 概率 H/T，按 qubit/门数扫描	Peham 2022

与其他概念的关系

判定用的化简引擎就是ZX 演算的重写系统，工程实现在PyZX 与图论化简（verify_equality）。
验证的对象覆盖综合类词条：Quartz 超优化的替换类靠定理证明器保证，而整电路优化结果仍需等价检查兜底；T 计数与非 Clifford 约简同理。
中性原子编译流（OLSQ-DPQA、FPQA 计算模型、DasAtom 分治搬运）重构剧烈，等价检查是其正确性验证的核心环节，评测框架见编译器公平评测与可视化。
等价性（局域等价意义下的门定义）在门层面也有对应物：见门相位与局域等价。
若把验证延伸到含测量的动态电路，流条件（电路提取与 Pauli Flow）与中电路测量与非破坏读出的语义须一并处理。

参考文献

T. Peham, L. Burgholzer, R. Wille, “Equivalence Checking of Quantum Circuits With the ZX-Calculus”, IEEE J. Emerging and Selected Topics in Circuits and Systems (2022). NA113 · DOI 10.1109/JETCAS.2022.3202204 · arXiv:2208.12820
L. Burgholzer, R. Raymond, R. Wille, “Verifying Results of the IBM Qiskit Quantum Circuit Compilation Flow”, IEEE QCE (2020). NA108 · DOI 10.1109/QCE49297.2020.00051 · arXiv:2009.02376
A. Kissinger, J. van de Wetering, “PyZX: Large Scale Automated Diagrammatic Reasoning”, EPTCS 318, 229 (2020). NA104 · DOI 10.4204/EPTCS.318.14
R. Duncan, A. Kissinger, S. Perdrix, J. van de Wetering, “Graph-theoretic Simplification of Quantum Circuits with the ZX-calculus”, Quantum 4, 279 (2020). NA102 · DOI 10.22331/q-2020-06-04-279

中性原子百科

探索

电路等价性验证