一句话：提出 SAQR-QC 逻辑，通过可控精度损失和局部推理，实现对大规模量子电路的可扩展近似定量验证。
量子程序与量子电路的验证仍是基础性难题；现有形式化方法在表示和操作断言与判断时往往需要指数级时间和空间，难以处理多量子比特电路。本文提出 SAQR-QC，一种面向量子电路的可扩展近似定量推理逻辑。其核心设计包含三点：有意引入精度损失；提供机制使一系列推理步骤中累积的精度损失保持较小；每个推理步骤都是局部的，只涉及少量量子比特，从而提升可扩展性。作者通过两个案例研究评估该逻辑：验证包含非 Clifford 门的 GHZ 电路，以及分析 Shor 因数分解算法中的核心子程序——量子相位估计，展示了 SAQR-QC 的有效性。
Reasoning about quantum programs remains a fundamental challenge, regardless of the programming model or computational paradigm. 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 SAQR-QC, a logic for Scalable but Approximate Quantitative Reasoning about Quantum Circuits. 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) every reasoning step is local -- involving just a small number of qubits -- making reasoning scalable. 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.
@article{paperbot3766,
title = {SAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum Circuits},
author = {Nengkun Yu and Jens Palsberg and Thomas Reps},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808284}
}