一句话：提出基于投影的等价性检查 PBEC，可在经典计算机上以对量子比特数线性时间/空间验证浅层量子电路等价性。
论文研究浅层量子电路的等价性检查：判定两个常深度量子电路是否计算相同。直接经典表示量子态需随量子比特数 n 指数增长。作者提出基于投影的等价性检查 PBEC，核心洞察是局部投影可作为约束完整刻画浅层电路的输出态，输出态是满足所有约束的唯一量子态。PBEC 为两类等价性问题给出判定过程，并可在固定深度下以关于 n 的线性时间与空间运行；还可将约束表示用于静态和运行时断言检查，对局部投影合取式断言既可靠又完备。实验在随机 100 量子比特电路上评估：depth 6 的 1D 电路约束表示需 129.64 s，depth 3 等价检查固定输入需 4.46 s，任意输入不超过 31.96 s。
This paper concerns the problem of checking if two shallow (i.e., constant-depth) quantum circuits perform equivalent computations. Equivalence checking is a fundamental correctness question—needed, e.g., for ensuring that transformations applied to a quantum circuit do not alter its behavior. For quantum circuits, the problem is challenging because a straightforward representation on a classical computer of each circuit’s quantum state can require time and space that are exponential in the number of qubits n . The paper presents Projection-Based Equivalence Checking (PBEC), which provides decision procedures for two variants of the equivalence-checking problem. Both can be carried out on a classical computer in time and space that, for any fixed depth, is linear in n . Our key insight is that local projections can serve as constraints that fully characterize the output state of a shallow quantum circuit. The output state is the unique quantum state that satisfies all the constraints. Beyond equivalence checking, we show how to use the constraint representation to check a class of assertions, both statically and at run time. Our assertion-checking methods are sound and complete for assertions expressed as conjunctions of local projections. Our experiments showed that computing the constraint representation of a random 100-qubit 1D circuit of depth 6 takes 129.64 seconds. Equivalence checking between two random 100-qubit 1D circuits of depth 3 requires 4.46 seconds for fixed input | 0 〉 ⊗ 100 , and no more than 31.96 seconds for arbitrary inputs. Computing the constraint description for a random 100-qubit circuit of depth 3 takes 6.99 seconds for a 2D structure, compared to 10.67 seconds for a circuit with arbitrary connectivity. At depth 2, equivalence checking takes 0.20 seconds for fixed input and 0.44 seconds for arbitrary input, with similar performance for both 2D and arbitrary-connectivity circuits.
@article{paperbot3012,
title = {Scalable Equivalence Checking and Verification of Shallow Quantum Circuits},
author = {Nengkun Yu and Xuan Du Trinh and Thomas Reps},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763153}
}