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 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 critical insight is that local projections are precise enough to completely characterize the output state of a shallow quantum circuit. Instead of explicitly computing the output state of a circuit, we generate a set of local projections that serve as constraints on the output state. Moreover, the circuit's 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 show that on a server equipped with 2 x Intel\textsuperscript{\textregistered} Xeon\textsuperscript{\textregistered} Gold 6338 CPUs (128 threads total) and 1.0~TiB of RAM, running Ubuntu 20.04.6 LTS, the constraint representation of a random 100-qubit circuit of depth 6 can be computed in 19.8 seconds. For fixed inputs $\ket{0}^{\otimes 100}$, equivalence checking of {random} 100-qubit circuits of depth 3 takes 4.46 seconds; for arbitrary inputs, it takes no more than 31.96 seconds.

翻译：本文研究如何检验两个浅层（即恒定深度）量子电路是否执行等价计算的问题。等价性检验是一个基本的正确性问题——例如，确保应用于量子电路的变换不会改变其行为。对于量子电路而言，该问题具有挑战性，因为在经典计算机上直接表示每个电路的量子态可能需要时间和空间随量子比特数$n$呈指数增长。本文针对等价性检验问题的两种变体提出了判定流程。对于任意固定深度，两者均可在经典计算机上以时间和空间与$n$呈线性关系的方式执行。我们的核心洞见在于：局部投影足以精确刻画浅层量子电路的输出态。我们并非显式计算电路的输出态，而是生成一组作为输出态约束的局部投影。此外，电路的输出态是满足所有约束的唯一量子态。除等价性检验外，我们还展示了如何利用约束表示在静态和运行时检查一类断言。对于以局部投影合取式表达的断言，我们的断言检查方法具有可靠性和完备性。实验表明，在配备2×Intel® Xeon® Gold 6338 CPU（共128线程）和1.0 TiB内存、运行Ubuntu 20.04.6 LTS的服务器上，深度为6的随机100量子比特电路的约束表示可在19.8秒内完成计算。对于固定输入$\ket{0}^{\otimes 100}$，深度为3的随机100量子比特电路的等价性检验耗时4.46秒；对于任意输入，检验耗时不超过31.96秒。