Formally Verifying Quantum Phase Estimation Circuits with 1,000+ Qubits

• URL: http://arxiv.org/abs/2603.08762v2
• Date: Wed, 11 Mar 2026 10:01:59 GMT
• Title: Formally Verifying Quantum Phase Estimation Circuits with 1,000+ Qubits
• Abstract summary: We present a scalable formal verification methodology for Quantum Phase Estimation (QPE) circuits.<n>Our approach uses a symbolic qubit abstraction based on quantifier-free bit-vector logic.<n>We develop formal properties aligned with this abstraction to ensure functional correctness of QPE circuits.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We present a scalable formal verification methodology for Quantum Phase Estimation (QPE) circuits. Our approach uses a symbolic qubit abstraction based on quantifier-free bit-vector logic, capturing key quantum phenomena, including superposition, rotation, and measurement. The proposed methodology maps quantum circuit functional behaviour from Hilbert space to a bit-vector domain. We develop formal properties aligned with this abstraction to ensure functional correctness of QPE circuits. The method scales efficiently, verifying QPE circuits with up to 6 precision qubits and 1,024 phase qubits using under 3.5~GB of memory.

Related papers

• Iterative quantum phase estimation with cQED encoding [0.0]
  Quantum phase estimation is a cornerstone algorithm for determining eigenvalues of unitary operators or Hamiltonians.<n>We propose a conceptually simple and experimentally feasible alternative that exploits the toolbox of circuit quantum electrodynamics.<n>A bosonic mode serves as an efficient quantum memory in which the binary digits of the phase are encoded into the direction of phase-space rotations.
  arXiv  Detail & Related papers  (2026-06-20T14:45:05Z)
• Bit-Vector Abstractions to Formally Verify Quantum Error Detection & Entanglement [0.0]
  We present a scalable formal verification methodology for Quantum Phase Estimation (QPE) circuits.<n>Our approach uses a symbolic qubit abstraction based on quantifier-free bit-vector logic.<n>We develop formal properties aligned with this abstraction to ensure functional correctness of QPE circuits.
  arXiv  Detail & Related papers  (2026-03-13T19:45:57Z)
• State Similarity in Modular Superconducting Quantum Processors with Classical Communications [41.94024259927014]
  We propose a cross-platform fidelity estimation algorithm tailored for modular architectures.<n>We experimentally implement the protocol on modular superconducting quantum processors with up to 6 qubits to verify the similarity of two 11-qubit GHZ states.<n>As a proof of concept, we apply it to a 5-qubit quantum phase learning task using six 3-qubit modules, successfully extracting phase information with just eight training samples.
  arXiv  Detail & Related papers  (2025-06-02T13:27:38Z)
• 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)
• Mapping quantum circuits to shallow-depth measurement patterns based on graph states [0.0]
  We create a hybrid simulation technique for measurement-based quantum computing. We show that groups of fully commuting operators can be implemented using fully-parallel, i.e., non-adaptive, measurements. We discuss how such circuits can be implemented in constant quantum depths by employing quantum teleportation.
  arXiv  Detail & Related papers  (2023-11-27T19:00:00Z)
• Quantum process tomography of continuous-variable gates using coherent states [49.299443295581064]
  We demonstrate the use of coherent-state quantum process tomography (csQPT) for a bosonic-mode superconducting circuit. We show results for this method by characterizing a logical quantum gate constructed using displacement and SNAP operations on an encoded qubit.
  arXiv  Detail & Related papers  (2023-03-02T18:08:08Z)
• Efficient estimation of trainability for variational quantum circuits [43.028111013960206]
  We find an efficient method to compute the cost function and its variance for a wide class of variational quantum circuits. This method can be used to certify trainability for variational quantum circuits and explore design strategies that can overcome the barren plateau problem.
  arXiv  Detail & Related papers  (2023-02-09T14:05:18Z)
• Rotational Abstractions for Verification of Quantum Fourier Transform Circuits [0.0]
  We propose a novel formal verification method that is targeted at Quantum Fourier Transform (QFT) circuits. QFT is a fundamental quantum algorithm that forms the basis of many quantum computing applications. Our method is able to scale up to the verification of QFT circuits with 10,000 qubits and 50 million quantum gates.
  arXiv  Detail & Related papers  (2023-01-02T16:13:39Z)
• 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.