This work provides a comprehensive framework for noise-aware quantum program analysis, ranging from logical foundations to model checking and automated synthesis. While most research on quantum programming considers an idealized, noise-free semantics for quantum programs, we reason about quantum programs that are executed on real, noisy hardware. We use the error models published by quantum-hardware vendors to give a hardware-dependent semantics to quantum programs. We then present a noise-aware quantum Hoare logic with a relatively complete proof system. We finally use state-space exploration techniques for the hardware-aware verification and synthesis of loop-free quantum programs. In this way, we synthesize optimal, hardware-dependent solutions for parity bit-flip, GHZ state preparation, and other problems that commonly occur as subroutines in larger quantum algorithms. We evaluate our method on all 55 hardware specifications provided by the IBM Qiskit toolkit. Finally, we also show that classical probabilistic branching is needed for optimality in quantum programming.

翻译：暂无翻译