Formally Verifying Quantum Phase Estimation Circuits with 1,000+ Qubits
This addresses the challenge of ensuring functional correctness in large-scale quantum computing for researchers and engineers, though it appears incremental as it builds on existing formal verification approaches.
The researchers tackled the problem of formally verifying quantum phase estimation circuits, achieving verification of circuits with up to 1,024 phase qubits using under 7.5 GB of memory.
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.