AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs (Technical Report)
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866909018356711424 |
|---|---|
| author | Chen, Yu-Fang Chung, Kai-Min Hsieh, Min-Hsiu Huang, Wei-Jia Lengál, Ondřej Lin, Jyun-Ao Tsai, Wei-Lun |
| author_facet | Chen, Yu-Fang Chung, Kai-Min Hsieh, Min-Hsiu Huang, Wei-Jia Lengál, Ondřej Lin, Jyun-Ao Tsai, Wei-Lun |
| contents | We present a verifier of quantum programs called AutoQ 2.0. Quantum programs extend quantum circuits (the domain of AutoQ 1.0) by classical control flow constructs, which enable users to describe advanced quantum algorithms in a formal and precise manner. The extension is highly non-trivial, as we needed to tackle both theoretical challenges (such as the treatment of measurement, the normalization problem, and lifting techniques for verification of classical programs with loops to the quantum world), and engineering issues (such as extending the input format with a~support for specifying loop invariants). We have successfully used AutoQ 2.0 to verify two types of advanced quantum programs that cannot be expressed using only quantum circuits: the \emph{repeat-until-success} (RUS) algorithm and the weak-measurement-based version of Grover's search algorithm. AutoQ 2.0 can efficiently verify all our benchmarks: all RUS algorithms were verified instantly and, for the weak-measurement-based version of Grover's search, we were able to handle the case of 100 qubits in $\sim$20 minutes. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2411_09121 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs (Technical Report) Chen, Yu-Fang Chung, Kai-Min Hsieh, Min-Hsiu Huang, Wei-Jia Lengál, Ondřej Lin, Jyun-Ao Tsai, Wei-Lun Logic in Computer Science Formal Languages and Automata Theory We present a verifier of quantum programs called AutoQ 2.0. Quantum programs extend quantum circuits (the domain of AutoQ 1.0) by classical control flow constructs, which enable users to describe advanced quantum algorithms in a formal and precise manner. The extension is highly non-trivial, as we needed to tackle both theoretical challenges (such as the treatment of measurement, the normalization problem, and lifting techniques for verification of classical programs with loops to the quantum world), and engineering issues (such as extending the input format with a~support for specifying loop invariants). We have successfully used AutoQ 2.0 to verify two types of advanced quantum programs that cannot be expressed using only quantum circuits: the \emph{repeat-until-success} (RUS) algorithm and the weak-measurement-based version of Grover's search algorithm. AutoQ 2.0 can efficiently verify all our benchmarks: all RUS algorithms were verified instantly and, for the weak-measurement-based version of Grover's search, we were able to handle the case of 100 qubits in $\sim$20 minutes. |
| title | AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs (Technical Report) |
| topic | Logic in Computer Science Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2411.09121 |