Detail výsledku

AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs

LENGÁL, O.; CHEN, Y.; LIN, J.; TSAI, W.; HSIEH, M.; HUANG, W.; CHUNG, K. AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs. In Proceedings of TACAS'25. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2025. no. 15698, p. 87-108. ISSN: 0302-9743.
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Lengál Ondřej, doc. Ing., Ph.D., UITS (FIT)
Chen Yu-Fang
LIN, J.
TSAI, W.
HSIEH, M.
HUANG, W.
CHUNG, K.
Abstrakt

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 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 20
minutes.

Klíčová slova

quantum programs tree automata measurement verification

Rok
2025
Strany
87–108
Časopis
Lecture Notes in Computer Science, č. 15698, ISSN 0302-9743
Sborník
Proceedings of TACAS'25
Konference
31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems --- TACAS'25
Vydavatel
Springer Verlag
Místo
Heidelberg
DOI
10.1007/978-3-031-90660-2_5
EID Scopus
2-s2.0-105004795048
BibTeX 
@inproceedings{BUT196845,
  author="LENGÁL, O. and CHEN, Y. and LIN, J. and TSAI, W. and HSIEH, M. and HUANG, W. and CHUNG, K.",
  title="AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs",
  booktitle="Proceedings of TACAS'25",
  year="2025",
  journal="Lecture Notes in Computer Science",
  number="15698",
  pages="87--108",
  publisher="Springer Verlag",
  address="Heidelberg",
  doi="10.1007/978-3-031-90660-2\{_}5",
  issn="0302-9743"
}
Projekty
Efektivní konečné automaty pro automatické usuzování, MŠMT, ERC CZ, LL1908, zahájení: 2020-01-01, ukončení: 2024-12-31, ukončen
QUAK: Analýza kvantových programů pomocí automatů, GAČR, Standardní projekty, 25-18318S, zahájení: 2025-01-01, ukončení: 2027-12-31, řešení
Reliable, Secure, and Intelligent Computer Systems, VUT, Vnitřní projekty VUT, FIT-S-23-8151, zahájení: 2023-03-01, ukončení: 2026-02-28, řešení
Výzkumné skupiny
Automata@FIT (VZ Automata@FIT)
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)
Pracoviště
Ústav inteligentních systémů (UITS)
Nahoru