Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Local Reasoning about Probabilistic Behaviour for Classical-Quantum Programs

Huiling Wu, Yuxin Deng, Ming Xu

TL;DR

The paper tackles the challenge of verifying classical--quantum programs that exhibit probabilistic behavior due to quantum measurements and unbounded loops. It introduces a local, separation-logic-inspired quantum Hoare logic that uses distribution formulas $\oplus_{i\in I} p_i\cdot F_i$ and $\oplus_{i\in I} F_i$ to specify probabilistic properties and supports frame-style local reasoning via a QFrame rule. The authors establish soundness with respect to a denotational semantics, verify non-trivial quantum algorithms (HHL and Shor) within the system, and implement the framework inside the Coq proof assistant as CoqQLR for semi-automated reasoning. This work provides a modular, machine-checkable approach to reasoning about real-world classical--quantum programs, enabling formal verification of probabilistic quantum behavior. It also lays the groundwork for future extensions toward completeness analysis and alternative probabilistic logics.

Abstract

Verifying the functional correctness of programs with both classical and quantum constructs is a challenging task. The presence of probabilistic behaviour entailed by quantum measurements and unbounded while loops complicate the verification task greatly. We propose a new quantum Hoare logic for local reasoning about probabilistic behaviour by introducing distribution formulas to specify probabilistic properties. We show that the proof rules in the logic are sound with respect to a denotational semantics. To demonstrate the effectiveness of the logic, we formally verify the correctness of non-trivial quantum algorithms including the HHL and Shor's algorithms. Moreover, we embed our logic into the proof assistant Coq. The resulting logical framework, called CoqQLR, can facilitate semi-automated reasoning about classical--quantum programs.

Local Reasoning about Probabilistic Behaviour for Classical-Quantum Programs

TL;DR

The paper tackles the challenge of verifying classical--quantum programs that exhibit probabilistic behavior due to quantum measurements and unbounded loops. It introduces a local, separation-logic-inspired quantum Hoare logic that uses distribution formulas and to specify probabilistic properties and supports frame-style local reasoning via a QFrame rule. The authors establish soundness with respect to a denotational semantics, verify non-trivial quantum algorithms (HHL and Shor) within the system, and implement the framework inside the Coq proof assistant as CoqQLR for semi-automated reasoning. This work provides a modular, machine-checkable approach to reasoning about real-world classical--quantum programs, enabling formal verification of probabilistic quantum behavior. It also lays the groundwork for future extensions toward completeness analysis and alternative probabilistic logics.

Abstract

Verifying the functional correctness of programs with both classical and quantum constructs is a challenging task. The presence of probabilistic behaviour entailed by quantum measurements and unbounded while loops complicate the verification task greatly. We propose a new quantum Hoare logic for local reasoning about probabilistic behaviour by introducing distribution formulas to specify probabilistic properties. We show that the proof rules in the logic are sound with respect to a denotational semantics. To demonstrate the effectiveness of the logic, we formally verify the correctness of non-trivial quantum algorithms including the HHL and Shor's algorithms. Moreover, we embed our logic into the proof assistant Coq. The resulting logical framework, called CoqQLR, can facilitate semi-automated reasoning about classical--quantum programs.
Paper Structure (15 sections, 13 theorems, 46 equations, 1 figure, 18 tables)

This paper contains 15 sections, 13 theorems, 46 equations, 1 figure, 18 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. A Classical--Quantum Language
  4. Syntax
  5. Denotational Semantics
  6. Proof System
  7. Assertion Language
  8. Proof System
  9. Case Analysis
  10. HHL Algorithm
  11. Shor's Algorithm
  12. Coq Formalization
  13. Conclusion and Future Work
  14. Proof of Proposition \ref{['prop:closed']}
  15. Proof outlines for functional correctness of programs

Key Result

lemma 1

Let $\mu$ be a distribution and $F$ an assertion. For any $V \subseteq \mathbf{QVar}$ such that $\mathrm{qfree}(F) \subseteq V \subseteq \mathrm{dom}(\mu)$, we have that $\mu \models F \Leftrightarrow \mu|_{V} \models F$.

Figures (1)

  • Figure 1: Relationship between different files

Theorems & Definitions (15)

  • definition 1
  • lemma 1
  • lemma 2
  • lemma 3
  • lemma 4
  • lemma 5
  • proposition 1
  • definition 2
  • theorem 1: Soundness
  • lemma 6
  • ...and 5 more