Automated Expected Cost Analysis for Quantum Programs

Abstract

In recent years, quantum computing has gained a substantial amount of momentum, and the capabilities of quantum devices are continually expanding and improving. Nevertheless, writing a quantum program from scratch remains tedious and error-prone work, showcasing the clear demand for automated tool support. We present Qet, a fully automated static program analysis tool that yields a precise expected cost analysis of mixed classical-quantum programs. Qet supports programs with advanced features like mid-circuit measurements and classical control flow. The methodology of our prototype implementation is based on a recently proposed quantum expectation transformer framework, generalising Dijkstra's predicate transformer and Hoare logic. The prototype implementation Qet is evaluated on a number of case studies taken from the literature and online references. Qet is able to fully automatically infer precise upper bounds on the expected costs that previously could only be derived by tedious manual calculations.

Figures (17)

• Figure 1: The $-X$ program.
• Figure 2: Overview of the expected cost analysis tool .
• Figure 3: The quantum circuit for the $RUS$ program.
• Figure 4: The quantum expectation transformer $\wpt{\cdot}{\cdot}$.
• Figure 5: Universal laws derivable for the quantum expectation transformer.

Theorems & Definitions (5)

• proposition 1
• theorem 1: Soundness Theorem
• lemma 1
• theorem 2: Soundness Theorem
• proof