Reasoning about quantum programs remains a fundamental challenge, regardless of the programming model or computational paradigm. Despite extensive research, existing verification techniques are insufficient -- even for quantum circuits, a deliberately restricted model that lacks classical control, but still underpins many current quantum algorithms. Many existing formal methods require exponential time and space to represent and manipulate (representations of) assertions and judgments, making them impractical for quantum circuits with many qubits. This paper presents a logic for reasoning in such settings, called SAQR-QC. The logic supports {S}calable but {A}pproximate {Q}uantitative {R}easoning about {Q}uantum {C}ircuits, whence the name. SAQR-QC has three characteristics: (i) some (deliberate) loss of precision is built into it; (ii) it has a mechanism to help the accumulated loss of precision during a sequence of reasoning steps remain small; and (iii) most importantly, to make reasoning scalable, every reasoning step is local -- i.e., it involves just a small number of qubits. We demonstrate the effectiveness of SAQR-QC via two case studies: the verification of GHZ circuits involving non-Clifford gates, and the analysis of quantum phase estimation -- a core subroutine in Shor's factoring algorithm.

翻译：无论采用何种编程模型或计算范式，对量子程序的推理仍是一项根本性挑战。尽管已有大量研究，现有验证技术仍显不足——即使对于量子电路这一刻意受限的模型（缺乏经典控制，但仍支撑着当前许多量子算法）亦是如此。许多现有形式化方法需要指数级时间和空间来表示与操作断言和判断的（表示形式），导致其无法适用于多量子比特的量子电路。本文提出一种适用于此类场景的推理逻辑，称为SAQR-QC。该逻辑支持对量子电路进行可扩展但近似定量的推理，其名称即源于此。SAQR-QC具有三个特征：（i）内置了（刻意设计的）精度损失；（ii）具备一种机制，使推理步骤序列中累积的精度损失保持较小；（iii）最重要的是，为实现可扩展推理，每个推理步骤都是局部的——即仅涉及少量量子比特。我们通过两个案例研究证明SAQR-QC的有效性：涉及非克利福德门的GHZ电路验证，以及量子相位估计（肖尔因数分解算法的核心子程序）的分析。