Formal Verification of Continuous-Variable Quantum Programs
2026-07-20 • Logic in Computer Science
Logic in Computer Science
AI summaryⓘ
The authors created a formal way to understand and verify programs for Continuous-Variable Quantum Computing (CQC), which deals with quantum systems that have infinitely many states. This is hard because CQC involves infinite-dimensional spaces and measurements that can produce unlimited values. They developed a formal language and logic to prove properties about CQC programs and implemented a tool to assist with verification and error calculation. Their work helps ensure correctness of CQC algorithms and assists in determining resource needs for simulating these programs.
Continuous-Variable Quantum ComputingHilbert SpaceHoare LogicQuantum ProgramsCanonical ObservablesWeakest-PreconditionGate DecompositionPhoton-Number States
Authors
Stefanie Muroya, Thomas A. Henzinger
Abstract
We provide a formal framework for Continuous-Variable Quantum Computing (CQC). While CQC is supported by photonic quantum hardware, we are not aware of a formal semantics for continuous-variable quantum programs nor of a unary Hoare logic for their verification. There are several technical obstacles to extending to CQC any of the formal frameworks available for Discrete-Variable Quantum Computing (DQC). Most importantly, continuous-variable quantum programs act on {\em infinite-dimensional} Hilbert spaces; their measurement outcomes are often {\em unbounded} and have expected values that are defined by an improper integral (or an infinite series), which may not converge. We overcome these challenges to give a formal semantics to a universal programming language for CQC and to provide the first Hoare logic for CQC. The assertions of our logic are built from polynomials over canonical observables. Besides proving relative completeness, we implement a symbolic weakest-precondition calculator for CQC based on our logic. Our tool has successfully verified CQC algorithms from textbooks and calculated their approximation errors for physically realizable implementations, proved the correctness (i.e., equivalence) of gate decompositions for CQC hardware, and computed the resource requirements (i.e., number of photon-number states) for achieving a desired accuracy in the classical simulation of continuous-variable quantum programs.