Automated Expected Cost Analysis for Quantum Programs

TL;DR

Qet is an automated static analysis tool that accurately estimates the expected costs of mixed classical-quantum programs, supporting advanced features like mid-circuit measurements.

Contribution

The paper introduces Qet, a novel tool that automates expected cost analysis for complex quantum programs using a quantum expectation transformer framework.

Findings

Qet automatically infers precise upper bounds on expected costs.

Qet supports programs with mid-circuit measurements and classical control flow.

Qet outperforms manual calculations in accuracy and automation.

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.