Parameterized Verification of Quantum Circuits (Technical Report)
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866908686211874816 |
|---|---|
| author | Abdulla, Parosh Aziz Chen, Yu-Fang Hečko, Michal Holík, Lukáš Lengál, Ondřej Lin, Jyun-Ao Thinniyam, Ramanathan S. |
| author_facet | Abdulla, Parosh Aziz Chen, Yu-Fang Hečko, Michal Holík, Lukáš Lengál, Ondřej Lin, Jyun-Ao Thinniyam, Ramanathan S. |
| contents | We present the first fully automatic framework for verifying relational properties of parameterized quantum programs, i.e., a program that, given an input size, generates a corresponding quantum circuit. We focus on verifying input-output correctness as well as equivalence. At the core of our approach is a new automata model, synchronized weighted tree automata (SWTAs), which compactly and precisely captures the infinite families of quantum states produced by parameterized programs. We introduce a class of transducers to model quantum gate semantics and develop composition algorithms for constructing transducers of parameterized circuits. Verification is reduced to functional inclusion or equivalence checking between SWTAs, for which we provide decision procedures. Our implementation demonstrates both the expressiveness and practical efficiency of the framework by verifying a diverse set of representative parameterized quantum programs with verification times ranging from milliseconds to seconds. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2511_19897 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Parameterized Verification of Quantum Circuits (Technical Report) Abdulla, Parosh Aziz Chen, Yu-Fang Hečko, Michal Holík, Lukáš Lengál, Ondřej Lin, Jyun-Ao Thinniyam, Ramanathan S. Logic in Computer Science Formal Languages and Automata Theory We present the first fully automatic framework for verifying relational properties of parameterized quantum programs, i.e., a program that, given an input size, generates a corresponding quantum circuit. We focus on verifying input-output correctness as well as equivalence. At the core of our approach is a new automata model, synchronized weighted tree automata (SWTAs), which compactly and precisely captures the infinite families of quantum states produced by parameterized programs. We introduce a class of transducers to model quantum gate semantics and develop composition algorithms for constructing transducers of parameterized circuits. Verification is reduced to functional inclusion or equivalence checking between SWTAs, for which we provide decision procedures. Our implementation demonstrates both the expressiveness and practical efficiency of the framework by verifying a diverse set of representative parameterized quantum programs with verification times ranging from milliseconds to seconds. |
| title | Parameterized Verification of Quantum Circuits (Technical Report) |
| topic | Logic in Computer Science Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2511.19897 |