Bit-Vector Abstractions to Formally Verify Quantum Error Detection & Entanglement

• URL: http://arxiv.org/abs/2603.13554v1
• Date: Fri, 13 Mar 2026 19:45:57 GMT
• Title: Bit-Vector Abstractions to Formally Verify Quantum Error Detection & Entanglement
• 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

• Formally Verifying Quantum Phase Estimation Circuits with 1,000+ Qubits [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-09T01:59:07Z)
• 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)
• Single-shot Quantum Signal Processing Interferometry [3.431120541553662]
  We present a general algorithmic framework, quantum signal processing interferometry (QSPI), for quantum sensing. We use our QSPI sensing framework to make efficient binary decisions on a displacement channel in the single-shot limit.
  arXiv  Detail & Related papers  (2023-11-22T21:44:14Z)
• 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)
• Interactive Protocols for Classically-Verifiable Quantum Advantage [46.093185827838035]
  "Interactions" between a prover and a verifier can bridge the gap between verifiability and implementation. We demonstrate the first implementation of an interactive quantum advantage protocol, using an ion trap quantum computer.
  arXiv  Detail & Related papers  (2021-12-09T19:00:00Z)
• Bosonic field digitization for quantum computers [62.997667081978825]
  We address the representation of lattice bosonic fields in a discretized field amplitude basis. We develop methods to predict error scaling and present efficient qubit implementation strategies.
  arXiv  Detail & Related papers  (2021-08-24T15:30:04Z)

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.