Formal Verification of Quantum Algorithms Using Quantum Hoare Logic
Formal Verification of Quantum Algorithms Using Quantum Hoare Logic
Liu and colleagues connect quantum Hoare logic, interactive theorem proving, and verification of quantum algorithms.
Paper information (2019, CAV, LNCS, pp. 187–207) — Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, and Naijun Zhan. DOI
Work
The paper formalizes quantum Hoare logic in Isabelle/HOL, including program syntax, semantics, and a partial-correctness proof system. It mechanizes soundness and completeness of that system and connects quantum assertions and algorithm specifications to checked proof scripts.
Contributions
- An Isabelle/HOL formalization of QHL program syntax and semantics.
- Mechanized soundness and completeness proofs for the partial-correctness system.
- Formal verification of nontrivial quantum algorithms using this framework.
- A connection between the metatheory of program logic and proofs of algorithm specifications.
Limits
The conclusions concern the formalized specifications, input preconditions, and program model. Parameterized proofs can cover all inputs in their quantified domain, but do not automatically cover other implementations or hardware. Proof construction and loop invariants still require human reasoning. This work should not be conflated with the 2016 prototype that used an external Python oracle.
Connections
The paper advances Floyd–Hoare Logic for Quantum Programs to metatheory and algorithm verification in Isabelle/HOL. It contrasts with the paired-program reasoning in Quantum Relational Hoare Logic. Verification Methods and Tools explains how specifications, proofs, and implementations differ in the guarantees they provide.
Original paper
Junyi Liu, Bohua Zhan, Shuling Wang, Shenggang Ying, Tao Liu, Yangjia Li, Mingsheng Ying, and Naijun Zhan, Formal Verification of Quantum Algorithms Using Quantum Hoare Logic, in CAV 2019, LNCS, 187–207, DOI: 10.1007/978-3-030-25543-5_12.