SAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum Circuits
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.
Wed 17 JunDisplayed time zone: Mountain Time (US & Canada) change
11:00 - 12:40 | |||
11:00 20mTalk | Verification of Recursively Defined Quantum CircuitsDistinguished Paper PLDI Research Papers DOI | ||
11:20 20mTalk | SAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum Circuits PLDI Research Papers Nengkun Yu Stony Brook University, Jens Palsberg University of California at Los Angeles, Thomas Reps University of Wisconsin-Madison DOI | ||
11:40 20mTalk | Hybrid Path-Sums for Hybrid Quantum Programs PLDI Research Papers Christopĥe Chareton CEA List - Université Paris-Saclay, Sébastien Bardin CEA List - Université Paris-Saclay, Jad Issa CEA List - Université Paris-Saclay, Mathieu Nguyen CEA List - Université Paris-Saclay, Nicolas Blanco CEA List - Université Paris-Saclay DOI | ||
12:00 20mTalk | [TOPLAS] VyZX: Formal Verification of a Graphical Quantum Language PLDI Research Papers Adrian Lehmann University of Chicago, Ben Caldwell University of Chicago, A: Bhakti Shah , William Spencer , Robert Rand University of Chicago | ||
12:20 20mTalk | Cobble: Compiling Block Encodings for Quantum Computational Linear AlgebraDistinguished Paper PLDI Research Papers Charles Yuan University of Wisconsin-Madison DOI | ||