SAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum Circuits

• URL: http://arxiv.org/abs/2507.13635v1
• Date: Fri, 18 Jul 2025 03:48:36 GMT
• Title: SAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum Circuits
• Abstract summary: Reasoning about quantum programs remains a fundamental challenge, regardless of the programming model or computational paradigm.<n>This paper presents a logic for reasoning in such settings, called SAQR-QC.<n>It 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, all reasoning steps are local--i.e., they each involve just a small number of qubits.
• Score: 13.511470455769482
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• 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 Scalable but Approximate Quantitative Reasoning about Quantum Circuits, 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, all reasoning steps are local--i.e., they each involve 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.

Related papers

• Verifiable quantum advantage in extremely low depth [52.51019642214249]
  We give a problem that is solvable by shallow quantum circuits, hard for computation in time under lattice-based assumptions.<n>We prove that shallow quantum circuits have sufficient structure to solve certain classically hard tasks whose solutions can be verified efficiently.
  arXiv  Detail & Related papers  (2026-09-01T15:54:34Z)
• Compilation-informed probabilistic quantum error cancellation [2.079863206645103]
  We introduce a quantum error mitigation (QEM) scheme against both compilation errors and logical-gate noise that is circuit-, QEC code-, and compiler-agnostic.<n>It features maximal circuit size and QEC code-distance both independent of the target precision, in contrast to strategies based on QEC alone.<n>Our method significantly reduces quantum resource requirements for high-precision estimations, offering a practical route towards fault-tolerant quantum computation with precision-independent overheads.
  arXiv  Detail & Related papers  (2025-08-27T18:00:10Z)
• Advancing Quantum State Preparation Using Decision Diagram with Local Invertible Maps [5.328178128965817]
  We propose a family of efficient Quantum State Preparation (QSP) algorithms tailored to different numbers of available ancilla qubits.<n>Our approach exploits the power of Local Invertible Map Decision Diagrams (LimTDDs) to reduce quantum circuit complexity.
  arXiv  Detail & Related papers  (2025-07-23T03:34:44Z)
• VQC-MLPNet: An Unconventional Hybrid Quantum-Classical Architecture for Scalable and Robust Quantum Machine Learning [60.996803677584424]
  Variational Quantum Circuits (VQCs) offer a novel pathway for quantum machine learning.<n>Their practical application is hindered by inherent limitations such as constrained linear expressivity, optimization challenges, and acute sensitivity to quantum hardware noise.<n>This work introduces VQC-MLPNet, a scalable and robust hybrid quantum-classical architecture designed to overcome these obstacles.
  arXiv  Detail & Related papers  (2025-06-12T01:38:15Z)
• QCircuitBench: A Large-Scale Dataset for Benchmarking Quantum Algorithm Design [63.02824918725805]
  Quantum computing is recognized for the significant speedup it offers over classical computing through quantum algorithms.<n>QCircuitBench is the first benchmark dataset designed to evaluate AI's capability in designing and implementing quantum algorithms.
  arXiv  Detail & Related papers  (2024-10-10T14:24:30Z)
• SuperEncoder: Towards Universal Neural Approximate Quantum State Preparation [12.591173729459427]
  We show that it is possible to leverage a pre-trained neural network to directly generate the QSP circuit for arbitrary quantum state. Our study makes a steady step towards a universal neural designer for approximate QSP.
  arXiv  Detail & Related papers  (2024-08-10T04:39:05Z)
• Reductive Quantum Phase Estimation [0.0]
  We show a circuit that distinguishes an arbitrary set of phases with a fewer number of qubits and unitary applications. We show a trade-off between measurement precision and phase distinguishability, which allows one to tune the circuit to be optimal for a specific application.
  arXiv  Detail & Related papers  (2024-02-06T23:38:36Z)
• QuantumSEA: In-Time Sparse Exploration for Noise Adaptive Quantum Circuits [82.50620782471485]
  QuantumSEA is an in-time sparse exploration for noise-adaptive quantum circuits. It aims to achieve two key objectives: (1) implicit circuits capacity during training and (2) noise robustness. Our method establishes state-of-the-art results with only half the number of quantum gates and 2x time saving of circuit executions.
  arXiv  Detail & Related papers  (2024-01-10T22:33:00Z)
• QuBEC: Boosting Equivalence Checking for Quantum Circuits with QEC Embedding [4.15692939468851]
  We propose a Decision Diagram-based quantum equivalence checking approach, QuBEC, that requires less latency compared to existing techniques. Our proposed methodology reduces verification time on certain benchmark circuits by up to $271.49 times$.
  arXiv  Detail & Related papers  (2023-09-19T16:12:37Z)
• GSQAS: Graph Self-supervised Quantum Architecture Search [0.18899300124593643]
  Existing Quantum Architecture Search (QAS) algorithms require to evaluate a large number of quantum circuits during the search process. We propose GSQAS, a graph self-supervised QAS, which trains a predictor based on self-supervised learning. GSQAS outperforms the state-of-the-art predictor-based QAS, achieving better performance with fewer labeled circuits.
  arXiv  Detail & Related papers  (2023-03-22T08:35:28Z)
• End-to-end resource analysis for quantum interior point methods and portfolio optimization [63.4863637315163]
  We provide a complete quantum circuit-level description of the algorithm from problem input to problem output. We report the number of logical qubits and the quantity/depth of non-Clifford T-gates needed to run the algorithm.
  arXiv  Detail & Related papers  (2022-11-22T18:54:48Z)
• Quantum Davidson Algorithm for Excited States [42.666709382892265]
  We introduce the quantum Krylov subspace (QKS) method to address both ground and excited states. By using the residues of eigenstates to expand the Krylov subspace, we formulate a compact subspace that aligns closely with the exact solutions. Using quantum simulators, we employ the novel QDavidson algorithm to delve into the excited state properties of various systems.
  arXiv  Detail & Related papers  (2022-04-22T15:03:03Z)
• Quantum circuit debugging and sensitivity analysis via local inversions [62.997667081978825]
  We present a technique that pinpoints the sections of a quantum circuit that affect the circuit output the most. We demonstrate the practicality and efficacy of the proposed technique by applying it to example algorithmic circuits implemented on IBM quantum machines.
  arXiv  Detail & Related papers  (2022-04-12T19:39:31Z)
• Circuit Symmetry Verification Mitigates Quantum-Domain Impairments [69.33243249411113]
  We propose circuit-oriented symmetry verification that are capable of verifying the commutativity of quantum circuits without the knowledge of the quantum state. In particular, we propose the Fourier-temporal stabilizer (STS) technique, which generalizes the conventional quantum-domain formalism to circuit-oriented stabilizers.
  arXiv  Detail & Related papers  (2021-12-27T21:15:35Z)
• QUANTIFY: A framework for resource analysis and design verification of quantum circuits [69.43216268165402]
  QUANTIFY is an open-source framework for the quantitative analysis of quantum circuits. It is based on Google Cirq and is developed with Clifford+T circuits in mind. For benchmarking purposes QUANTIFY includes quantum memory and quantum arithmetic circuits.
  arXiv  Detail & Related papers  (2020-07-21T15:36:25Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.