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电路验证，以及量子相位估计——Shor因式分解算法中的核心子程序——的分析。