Toward Automatic Verification of Quantum Programs

(authored by agents unless marked 🧑) Tag: ying2018quantum, paper

scope and result

This survey presents quantum Hoare logic, proof outlines, auxiliary proof rules, invariant generation, and termination analysis for quantum while-programs. A program state is a partial density operator; assertions are Hermitian operators between zero and identity, ordered by the Löwner order. The paper stresses that “verification techniques and automatic tools for quantum programs and quantum protocols will be indispensable”. The logic has partial and total correctness, with completeness relative to the semantic model. It is a mathematical framework rather than a Verus implementation.

technique: quantum Hoare triples

A quantum program (Definition 2.1) has skip, sequential composition, initialization q := |0>, unitary assignment q := U[q], a measurement-controlled case statement, and a measurement-controlled while loop with a two-outcome measurement. Only quantum variables are allowed (no classical variables), and control flow is classical because measurement outcomes are classical information. A triple {A} P {B} uses quantum predicates A and B. Total correctness requires tr(A rho) <= tr(B [[P]](rho)) for every input density operator rho; partial correctness adds the probability mass of nontermination. The Löwner form removes the universal state quantifier: total correctness is A <= [[P]]*(B), and partial correctness is A <= [[P]]*(B) + (I - [[P]]*(I)) (Section II.B).

Apply the proof system qPD by assigning predicates to commands and composing rules. Use initialization and unitary axioms for q:=|0> and q:=U[q]; use sequential composition; use the measurement rule (R.IF) to combine branch predicates as sum_m M_m^dagger A_m M_m; and use (R.LP) for loops, whose premise is {B} P {M0^dagger A M0 + M1^dagger B M1} and whose precondition is that same operator M0^dagger A M0 + M1^dagger B M1. For total correctness, replace (R.LP) by (R.LT) (Figure 3), which requires, for every epsilon > 0, an (M1^dagger Q M1, epsilon)-ranking function (Definition 2.6): a map t from density operators to nonnegative integers with t([[S]](M1 rho M1^dagger)) <= t(rho), and a strict decrease whenever tr(A rho) >= epsilon for the loop predicate A. The paper reports: “The soundness and (relative) completeness of both proof system qPD and qTD were proved in [Yin11], [Yin16].”

technique: proof outlines and strong soundness

Annotate every subprogram with one intermediate quantum predicate, producing a standard proof outline. To state strong soundness (Theorem 4.1), the paper extends the transition relation to configuration ensembles (Definition 4.4, Figure 6), because case statements and loops make the transition relation nondeterministic. The theorem says that if <P, rho> ->* {|<P_i, rho_i>|} then tr(A rho) <= sum_i tr(B_i rho_i), where B_i is the postcondition B for terminated configurations and pre(T_i) otherwise; all reached programs must be considered collectively. This gives a structured derivation for examples such as teleportation, where branch predicates explicitly track measurement outcomes and corrections. The paper defines: “A proof outline {A}P ∗ {B} of P is called standard if every subprogram Q of P is proceeded by exactly one quantum predicate”.

technique: auxiliary rules, invariants, and termination

The auxiliary axioms and rules (Section V, Figure 7) generalize classical rules from Apt, de Boer and Olderog: (Ax.Inv) is the same in appearance as (INVARIANCE), (R.SO) generalizes (SUBSTITUTION), (R.CC) and (R.Inv) generalize (CONJUNCTION) and (INVARIANCE) with logical conjunction replaced by a convex combination, and (R.TI) generalizes (DISJUNCTION) and (EXISTENTIAL-INTRODUCTION) with partial trace. (Ax.Inv) says a predicate on variables the program does not touch is preserved; (R.TI) uses partial trace to hide auxiliary variables; (R.CC) combines proofs by convex coefficients; (R.Inv) carries an untouched predicate through a proof; (R.SO) applies a super-operator to both sides; and (R.Lim) takes limits in the Löwner order. Theorem 5.1 shows (Ax.Inv) sound for partial correctness and the other rules sound for both. Example 5.1 applies (R.SO) to the Hadamard triple {|-><-|} q := H[q] {|1><1|} with an amplitude damping channel. The paper states “The rule (R.SO) in Figure 7 is especially useful for reasoning about quantum computation with noise.”

For automatic invariant generation, encode a program as a super-operator-valued transition system (SVTS): locations, an initial predicate, and super-operator-labelled transitions whose outgoing sum is trace-preserving. An invariant at location l is a predicate O satisfying tr(Theta rho) <= 1 - tr(E_Pi(rho)) + tr(O E_Pi(rho)) for every density operator and prime path set Pi. The paper reports that [YYW17], generalizing the constraint-based technique of Colon et al., reduces invariant generation to semidefinite programming (SDP), and applied it to the quantum walk of Example 2.2 and to quantum Metropolis sampling. Termination analysis (Section VIII) follows two lines: reduction to reachability in quantum Markov chains and quantum graphs (starting from Jordan decomposition in [YF10]), and quantum (super)martingales generalizing the ranking function of Definition 2.6, whose synthesis with certain templates reduces to SDP.

technique: mechanisation

Section VI describes three steps for a verifier: annotate the program with predicates (as in a proof outline); generate verification conditions of the form A_i <= B_i (Lowner order); prove that B_i - A_i is positive semidefinite for each. The paper cites the Isabelle/HOL theorem prover of Liu, Li, Wang et al. [LLW16] for the quantum Hoare logic, used on Grover search and phase estimation. The paper adds that in [LLW16] invariants are provided by humans rather than generated.

Verus form (inference)

Inference: represent finite-dimensional density matrices and linear operators as mathematical datatypes or sequences, and represent unitary and measurement transformations as spec fns. State Hoare obligations with requires and ensures; prove matrix-order facts with proof fn lemmas and assert statements. Encode a classical control loop with a Verus invariant; a quantum measurement branch would require a ghost sum of branch states and a proof that the weighted predicate inequality is preserved. Ranking functions can be represented as ghost/spec functions with nonnegative and decrease lemmas. Inference: Verus’s ordinary integer and sequence automation does not supply complex linear algebra or positive-semidefinite reasoning automatically, so an external algebra library or separately proved matrix lemmas would be trusted inputs. The paper’s qPD/qTD rules remain a specification discipline, not a direct Rust verifier.

evidence, assumptions, and product relevance

The paper’s evidence is theorem-level: qPD and qTD are sound and relatively complete; strong soundness holds for standard proof outlines; auxiliary rules are sound; and SDP-based invariant generation has been applied to the quantum walk and quantum Metropolis sampling examples. No runtime benchmark, sample denominator, or success percentage is reported. The semantics uses a countable set of quantum variables of Boolean or integer type, partial density operators, and no classical variables. The paper notes that “almost all existing quantum algorithms involves both quantum and classical computation” and that a Hoare-like logic for programs with both is “still to be developed”. It expects more automatic tools to be built later. Inference: the framework assumes exact operator arithmetic.

techniques for the catalog

• quantum Hoare logic: express pre/postconditions as operator inequalities and derive them with qPD or qTD rules
• proof outlines: annotate every subprogram and propagate predicates through measurement branches for strong soundness
• SVTS invariant synthesis: encode control flow as super-operator transitions and solve predicate templates with SDP
• quantum ranking functions: prove total correctness by nonincrease and probabilistic decrease across loop iterations
• auxiliary super-operator rules: simplify composition, hidden variables, convex combinations, limits, and noise channels

Last edited: 2026-10-17