A Logic for Approximate Quantitative Reasoning about Quantum Circuits

TL;DR

The paper tackles the challenge of scalable verification for quantum circuits by introducing SAQR-QC, a logic that blends quantitative reasoning with scalable, local predicates derived from quantum abstract interpretation. It combines QAI-style qualitative predicates with QHL-inspired quantitative observables to enable proofs whose size grows polynomially with system size, and demonstrates effectiveness on GHZ circuits with non-Clifford gates and on Quantum Phase Estimation, including an exact, lossless QFT analysis via QAI. The main contributions are the formal SAQR-QC framework, its soundness, and two detailed case studies showing precise, scalable reasoning about both correctness and probabilistic performance in key quantum algorithms. The work positions SAQR-QC as a foundational step toward automated, scalable verification of quantum circuits on classical hardware, with clear paths for automation and extensions to broader quantum programming paradigms and noise models.

Abstract

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.

Figures (5)

• Figure 1: CNOT circuit $\mathbf{C}$.
• Figure 2: Inference rules for program constructs in SAQR-QC. We can use the proof rules for both forward reasoning or backward reasoning.
• Figure 3: GHZ circuit with unitaries $U_i$.
• Figure 4: Quantum Fourier Transform: swap gates that reverse the qubit order at the circuit’s end are omitted.
• Figure 5: Quantum Phase Estimation: $U\ket{\psi}=e^{i\theta}\ket{\psi}$. We only consider the circuit without the measurements.

Theorems & Definitions (26)

• definition 1: Syntax
• Lemma 2.1
• Lemma 2.2
• Lemma 2.3
• Lemma 2.4
• Lemma 2.5
• Definition 2.1: YP21
• Definition 2.2: YP21
• Theorem 2.1: YP21
• Theorem 2.2: YP21