An automated deductive verification framework for circuit-building quantum programs
From MaRDI portal
Publication:2233453
Abstract: While recent progress in quantum hardware open the door for significant speedup in certain key areas, quantum algorithms are still hard to implement right, and the validation of such quantum programs is a challenge. Early attempts either suffer from the lack of automation or parametrized reasoning, or target high-level abstract algorithm description languages far from the current de facto consensus of circuit-building quantum programming languages. As a consequence, no significant quantum algorithm implementation has been currently verified in a scale-invariant manner. We propose Qbricks, the first formal verification environment for circuit-building quantum programs, featuring clear separation between code and proof, parametric specifications and proofs, high degree of proof automation and allowing to encode quantum programs in a natural way, i.e. close to textbook style. Qbricks builds on best practice of formal verification for the classical case and tailor them to the quantum case: we bring a new domain-specific circuit-building language for quantum programs, namely Qbricks-DSL, together with a new logical specification language Qbricks-Spec and a dedicated Hoare-style deductive verification rule named Hybrid Quantum Hoare Logic. Especially, we introduce and intensively build upon HOPS, a higher-order extension of the recent path-sum symbolic representation, used for both specification and automation. To illustrate the opportunity of Qbricks, we implement the first verified parametric implementations of several famous and non-trivial quantum algorithms, including the quantum part of Shor integer factoring (Order Finding - Shor-OF), quantum phase estimation (QPE) - a basic building block of many quantum algorithms, and Grover search. These breakthroughs were amply facilitated by the specification and automated deduction principles introduced within Qbricks.
Recommendations
Cites work
- \textit{Re}\(\mathcal{Q}\)\textsc{wire}: reasoning about reversible quantum circuits
- A lambda calculus for quantum computation with classical control
- A quantum adiabatic evolution algorithm applied to random instances of an NP-complete problem
- An automated deductive verification framework for circuit-building quantum programs
- An introduction to quantum programming in Quipper
- Formalization \textit{of} quantum protocols using Coq
- How to Verify a Quantum Computation
- scientific article; zbMATH DE number 1579275 (Why is no real title available?)
- scientific article; zbMATH DE number 5899272 (Why is no real title available?)
- scientific article; zbMATH DE number 5320229 (Why is no real title available?)
- scientific article; zbMATH DE number 1256737 (Why is no real title available?)
- Invariants of quantum programs: characterisations and generation
- Model-checking linear-time properties of quantum systems
- Optimising Clifford circuits with quantomatic
- Picturing quantum processes. A first course in quantum theory and diagrammatic reasoning
- QPCF: higher-order languages and quantum circuits
- Quantomatic: a proof assistant for diagrammatic reasoning
- Quantum algorithms revisited
- Quantum implicit computational complexity
- QWIRE: a core language for quantum circuits
- REVS: a tool for space-optimized reversible circuit synthesis
- The spirit of ghost code
- Toward automatic verification of quantum programs
- Towards large-scale functional verification of universal quantum circuits
- Verification of quantum computation: an overview of existing approaches
- Verified compilation of space-efficient reversible circuits
- Why3 -- where programs meet provers
Cited in
(17)- The structure of sum-over-paths, its consequences, and completeness for Clifford
- An automated deductive verification framework for circuit-building quantum programs
- A modeling and verification framework for optical quantum circuits
- Towards quantum programs verification: from Quipper circuits to QPMC
- Towards large-scale functional verification of universal quantum circuits
- Automatically Translating Quantum Programs from a Subset of Common Gates to an Adiabatic Representation
- A strict constrained superposition calculus for graphs
- \textsf{symQV}: automated symbolic verification of quantum programs
- A formalization of the CHSH inequality and Tsirelson's upper-bound in Isabelle/HOL
- Verification of quantum systems using barrier certificates
- Rewriting and completeness of sum-over-paths in dyadic fragments of quantum computing
- Formal reasoning about Bernstein-Vazirani algorithm
- Typed compositional quantum computation with lenses
- The many-worlds calculus
- A rewriting theory for quantum -calculus
- Satisfiability modulo theories for verifying MILP certificates
- Typed compositional quantum computation with lenses
This page was built for publication: An automated deductive verification framework for circuit-building quantum programs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2233453)
