Hybrid Path-Sums for Hybrid Quantum Programs

TL;DR

This paper introduces Hybrid Path-Sums, a symbolic framework for the formal verification of hybrid quantum programs with classical and quantum control, enabling automated reasoning and validation.

Contribution

It presents a novel symbolic representation, rewriting rules, and assertion language for hybrid quantum programs, along with a symbolic execution engine and case-study evaluations.

Findings

Efficient verification of hybrid quantum/classical programs demonstrated.

The framework correctly proves properties and equivalences of hybrid quantum programs.

Showcases advantages over existing solutions in case-study evaluations.

Abstract

As quantum computing becomes an emerging reality, designing efficient quantum programming capabilities is becoming more and more important. Particularly, the debugging and validation of quantum programs is of paramount importance, as these programs are by definition hard to test. Static analysis and formal verification methods for quantum programs started to emerge a few years now, yet they often miss hybrid quantum/classical reasoning facilities with, e.g., generic quantum control, classical control and classical computation instructions. In this paper, we lay out the foundations of a framework for the automated formal verification of (full) hybrid quantum programs featuring both classical and quantum control, measurement and hybrid data structures. In particular, we propose: (1) a novel symbolic representation for describing and manipulating sets of hybrid quantum/classical states called Hybrid Path-Sums (HPS); (2) a set of rewriting rules providing a rich mechanism for simplifying and reasoning on these symbolic hybrid states, and (3) a core assertion language to specify equivalence of hybrid quantum programs, the satisfaction of properties on (parts of) hybrid states, and the extraction of probabilistic statements about the program behavior. We prove the correctness of the novel symbolic representation, of its rewriting system and of the specification system. Finally, we propose a full implementation of this framework as a dedicated symbolic execution engine for hybrid programs. We present an evaluation of a set of representative hybrid case-studies from the literature, showcasing the advantage of our approach and its efficiency compared to state-of-the-art solutions.