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

TL;DR

This paper introduces a scalable formal verification method for Quantum Phase Estimation circuits that efficiently handles circuits with over a thousand qubits by abstracting quantum phenomena into a bit-vector domain.

Contribution

The paper presents a novel symbolic qubit abstraction and verification approach that scales to large quantum circuits, enabling formal correctness proofs for circuits with thousands of qubits.

Findings

Verified QPE circuits with up to 6 precision qubits and 1024 phase qubits

Uses under 7.5 GB of memory for large-scale verification

Captures key quantum phenomena within a bit-vector abstraction

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 7.5~GB of memory.