Formally Verifying Quantum Phase Estimation Circuits with 1,000+ Qubits
Fuente:
arXiv
Salvato in:
| Autori principali: | , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2026
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866917352193392640 |
|---|---|
| author | Govindankutty, Arun Srinivasan, Sudarshan K. |
| author_facet | Govindankutty, Arun Srinivasan, Sudarshan K. |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_08762 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Formally Verifying Quantum Phase Estimation Circuits with 1,000+ Qubits Govindankutty, Arun Srinivasan, Sudarshan K. Quantum Physics Logic in Computer Science 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. |
| title | Formally Verifying Quantum Phase Estimation Circuits with 1,000+ Qubits |
| topic | Quantum Physics Logic in Computer Science |
| url | https://arxiv.org/abs/2603.08762 |