Formal Verification of Continuous-Variable Quantum Programs

• URL: http://arxiv.org/abs/2607.17714v1
• Date: Mon, 20 Jul 2026 09:09:20 GMT
• Title: Formal Verification of Continuous-Variable Quantum Programs
• Abstract summary: We provide a formal framework for Continuous-Variable Quantum Computing (CQC)<n>While CQC is supported by photonic quantum hardware, we are not aware of a formal semantics for CQC.<n>We implement a symbolic weakest-precondition CQC based on our logic.
• Score: 6.925649240526206
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Reasoning about Continuous-Variable Quantum Systems [10.113921654362638]
  Continuous-variable quantum computing (CVQC) is a computing paradigm in which measurements yield values over a continuous domain.<n>CVQC is both a convenient omputational framework for modeling physical quantum systems, and a good abstraction for hardware platforms based on quantum optics.<n>We develop a formal semantics for a core CV quantum programming language, and sound verification methods for program correctness.
  arXiv  Detail & Related papers  (2026-07-25T10:36:34Z)
• AQER: a scalable and efficient data loader for digital quantum computers [62.40228216126285]
  We develop AQER, a scalable AQL method that constructs the loading circuit by systematically reducing entanglement in target states.<n>We conduct systematic experiments to evaluate the effectiveness of AQER, using synthetic datasets, classical image and language datasets, and a quantum many-body state datasets with up to 50 qubits.
  arXiv  Detail & Related papers  (2026-02-02T14:39:42Z)
• Continual Quantum Architecture Search with Tensor-Train Encoding: Theory and Applications to Signal Processing [68.35481158940401]
  CL-QAS is a continual quantum architecture search framework.<n>It mitigates challenges of costly encoding amplitude and forgetting in variational quantum circuits.<n>It achieves controllable robustness expressivity, sample-efficient generalization, and smooth convergence without barren plateaus.
  arXiv  Detail & Related papers  (2026-01-10T02:36:03Z)
• SAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum Circuits [13.511470455769482]
  Reasoning about quantum programs remains a fundamental challenge, regardless of the programming model or computational paradigm.<n>This paper presents a logic for reasoning in such settings, called SAQR-QC.<n>It has three characteristics: (i) some (deliberate) loss of precision is built into it; (ii) it has a mechanism to help the accumulated loss of precision during a sequence of reasoning steps remain small; and (iii) most importantly, to make reasoning scalable, all reasoning steps are local--i.e., they each involve just a small number of qubits.
  arXiv  Detail & Related papers  (2025-07-18T03:48:36Z)
• Formal Verification of Variational Quantum Circuits [44.06507276521908]
  Variational quantum circuits (VQCs) are a central component of many quantum machine learning algorithms.<n>We present the first in-depth theoretical and practical study of the formal verification problem for VQCs.
  arXiv  Detail & Related papers  (2025-07-14T12:28:32Z)
• VQC-MLPNet: An Unconventional Hybrid Quantum-Classical Architecture for Scalable and Robust Quantum Machine Learning [50.95799256262098]
  Variational quantum circuits (VQCs) hold promise for quantum machine learning but face challenges in expressivity, trainability, and noise resilience.<n>We propose VQC-MLPNet, a hybrid architecture where a VQC generates the first-layer weights of a classical multilayer perceptron during training, while inference is performed entirely classically.
  arXiv  Detail & Related papers  (2025-06-12T01:38:15Z)
• QbC: Quantum Correctness by Construction [4.068363933090715]
  We propose Quantum Correctness by Construction (QbC), an approach to constructing quantum programs from their specification in a way that ensures correctness.<n>We use pre- and postconditions to specify program properties, and propose sound and complete refinement rules for constructing programs in a quantum while language from their specification.<n>We find that the approach naturally suggests how to derive program details, highlighting key design choices along the way.
  arXiv  Detail & Related papers  (2023-07-28T16:00:57Z)
• Quantum process tomography of continuous-variable gates using coherent states [49.299443295581064]
  We demonstrate the use of coherent-state quantum process tomography (csQPT) for a bosonic-mode superconducting circuit. We show results for this method by characterizing a logical quantum gate constructed using displacement and SNAP operations on an encoded qubit.
  arXiv  Detail & Related papers  (2023-03-02T18:08:08Z)
• InQuIR: Intermediate Representation for Interconnected Quantum Computers [0.0]
  InQuIR is a representation that can express communication and computation on distributed quantum systems. We give examples written in InQuIR to illustrate the problems arising in distributed programs, such as deadlock. We also provide software tools for InQuIR and evaluate the computational costs of quantum circuits.
  arXiv  Detail & Related papers  (2023-02-01T06:19:23Z)
• TeD-Q: a tensor network enhanced distributed hybrid quantum machine learning framework [48.491303218786044]
  TeD-Q is an open-source software framework for quantum machine learning.<n>It seamlessly integrates classical machine learning libraries with quantum simulators.<n>It provides a graphical mode in which the quantum circuit and the training progress can be visualized in real-time.
  arXiv  Detail & Related papers  (2023-01-13T09:35:05Z)
• Tensor Network Quantum Virtual Machine for Simulating Quantum Circuits at Exascale [57.84751206630535]
  We present a modernized version of the Quantum Virtual Machine (TNQVM) which serves as a quantum circuit simulation backend in the e-scale ACCelerator (XACC) framework. The new version is based on the general purpose, scalable network processing library, ExaTN, and provides multiple quantum circuit simulators. By combining the portable XACC quantum processors and the scalable ExaTN backend we introduce an end-to-end virtual development environment which can scale from laptops to future exascale platforms.
  arXiv  Detail & Related papers  (2021-04-21T13:26:42Z)
• Using Quantum Metrological Bounds in Quantum Error Correction: A Simple Proof of the Approximate Eastin-Knill Theorem [77.34726150561087]
  We present a proof of the approximate Eastin-Knill theorem, which connects the quality of a quantum error-correcting code with its ability to achieve a universal set of logical gates. Our derivation employs powerful bounds on the quantum Fisher information in generic quantum metrological protocols.
  arXiv  Detail & Related papers  (2020-04-24T17:58:10Z)
• On the Principles of Differentiable Quantum Programming Languages [13.070557640180004]
  Variational Quantum Circuits (VQCs) are predicted to be one of the most important near-term quantum applications. We propose the first formalization of auto-differentiation techniques for quantum circuits.
  arXiv  Detail & Related papers  (2020-04-02T16:46:13Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.