Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Arun Govindankutty, Sudarshan K. Srinivasan

TL;DR

The proposed methodology maps quantum circuit functional behaviour from Hilbert space to a bit-vector domain, and develops formal properties aligned with this abstraction to ensure functional correctness of QPE circuits.

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.

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

TL;DR

The proposed methodology maps quantum circuit functional behaviour from Hilbert space to a bit-vector domain, and develops formal properties aligned with this abstraction to ensure functional correctness of QPE circuits.

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 (8 sections, 15 equations, 1 figure, 1 table)

This paper contains 8 sections, 15 equations, 1 figure, 1 table.

Table of Contents

  1. Introduction
  2. Background
  3. Existing Approaches
  4. Abstraction Framework
  5. Correctness Properties
  6. Verification Methodology
  7. Experimental Results
  8. Conclusion and Future Works

Figures (1)

  • Figure 1: (a) Quantum phase estimation circuit. (b)3-qubit inverse quantum Fourier transform circuit iqft_arun. (c) Quantum phase estimation circuit with 3 precision qubits and 1 phase qubit implemented in IBM-Qiskit.

Theorems & Definitions (7)

  • proof
  • proof
  • proof
  • proof
  • proof
  • proof
  • proof