Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Arun Govindankutty

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.

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

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.
Paper Structure (12 sections, 11 equations, 1 figure, 3 tables)

This paper contains 12 sections, 11 equations, 1 figure, 3 tables.

Table of Contents

  1. Introduction
  2. Theoretical Background
  3. Quantum Entanglement
  4. Quantum Errors and Error Correcting Codes
  5. Formal Verification
  6. Existing Approaches
  7. Verification Framework
  8. Abstractions
  9. Properties
  10. Verification Methodology
  11. Experimental Results
  12. Conclusion and Future Directions

Figures (1)

  • Figure 1: Figure shows quantum circuits for the following: (a) 3-qubit code with error detection. (b) Bell state ($\frac{1}{\sqrt{2}}(\ket{0}+\ket{1})$). (c) GHZ-state with 4-qubits ($\frac{1}{\sqrt{2}}(\ket{0000}+\ket{1111})$). (d) 9-qubit Shor code with error detection. H indicates Hadamard gate and M indicates measurement operation on qubits.