Search papers, labs, and topics across Lattice.
This paper introduces Hybrid Path-Sums (HPS), a novel symbolic representation for formal verification of hybrid quantum programs that integrates both quantum and classical control. They define rewriting rules for simplifying and reasoning about these HPS representations and develop an assertion language for specifying program equivalence and properties. The authors implement a symbolic execution engine based on HPS and demonstrate its effectiveness on hybrid quantum programs, showing advantages over existing methods.
Hybrid Path-Sums offer a new way to formally verify complex quantum programs, potentially catching bugs that are notoriously difficult to find through testing.
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.
