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.

翻译：我们提出了一款名为AutoQ 2.0的量子程序验证器。量子程序通过引入经典控制流结构扩展了量子电路（AutoQ 1.0的领域），从而使用户能够以形式化且精确的方式描述高级量子算法。这一扩展具有高度非平凡性，因为我们需同时应对理论挑战（如测量处理、归一化问题，以及将含循环经典程序验证技术提升至量子世界的提升方法）和工程问题（如扩展输入格式以支持循环不变量的指定）。我们已成功使用AutoQ 2.0验证了两类无法仅用量子电路表达的高级量子程序：重复直至成功算法和基于弱测量的格罗弗搜索算法。AutoQ 2.0能高效验证所有基准测试：所有重复直至成功算法均实现即时验证，而对于基于弱测量的格罗弗搜索，我们能在约20分钟内处理100量子比特的案例。