Detail publikace

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.

Originální název

Typ

článek ve sborníku ve WoS nebo Scopus

Jazyk

angličtina

Originální 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

Autoři

LENGÁL, O.; CHEN, Y.; LIN, J.; TSAI, W.; HSIEH, M.; HUANG, W.; CHUNG, K.

Vydáno

3. 5. 2025

Nakladatel

Springer Verlag

Místo

Heidelberg

ISSN

0302-9743

Periodikum

Lecture Notes in Computer Science

Číslo

15698

Stát

Spolková republika Německo

Strany od

Strany do

108

Strany počet

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"
}