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因子分解算法的核心子程序）的分析。