A Deductive Verification Framework for Circuit-building Quantum Programs
arXiv:2003.05841 · doi:10.1007/978-3-030-72019-3_6
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.
References in corpus (31)
- Supplementary information for "Quantum supremacy using a programmable superconducting processor"
- Quantum Machine Learning
- Quantum algorithm for solving linear systems of equations
- Quantum Simulation
- A Quantum Adiabatic Evolution Algorithm Applied to Random Instances of an NP-Complete Problem
- A Quantum Approximate Optimization Algorithm
- Quantum Algorithms Revisited
- Quantum measurements and the Abelian Stabilizer Problem
- ProjectQ: An Open Source Software Framework for Quantum Computing
- An approximate Fourier transform useful in quantum factoring
- Q#: Enabling scalable quantum computing and development with a high-level domain-specific language
- Verification of quantum computation: An overview of existing approaches
- A formal proof of the four color theorem
- LIQUi|>: A Software Design Architecture and Domain-Specific Language for Quantum Computing
- Quipper: A Scalable Quantum Programming Language
- Statistical Assertions for Validating Patterns and Finding Bugs in Quantum Programs
- Towards Large-scale Functional Verification of Universal Quantum Circuits
- A Verified Optimizer for Quantum Circuits
- QWIRE Practice: Formal Verification of Quantum Circuits in Coq
- How to Verify a Quantum Computation
- Verified compilation of space-efficient reversible circuits
- ReQWIRE: Reasoning about Reversible Quantum Circuits
- Quantomatic: A Proof Assistant for Diagrammatic Reasoning
- Optimising Clifford Circuits with Quantomatic
- Formalization of Quantum Protocols using Coq
- Toward Automatic Verification of Quantum Programs
- QDB: From Quantum Algorithms Towards Correct Quantum Programs
- Formal Verification of Quantum Protocols
- A Theorem Prover for Quantum Hoare Logic and Its Applications
- Pauli Fusion: a Computational Model to Realise Quantum Transformations from ZX Terms
- Enabling Accuracy-Aware Quantum Compilers using Symbolic Resource Estimation
Cited by in corpus (20)
- Formal Verification of Quantum Programs: Theory, Tools and Challenges
- Synthesizing Quantum-Circuit Optimizers
- symQV: Automated Symbolic Verification of Quantum Programs
- Symbolic Execution for Quantum Error Correction Programs
- Efficient Formal Verification of Quantum Error Correcting Programs
- On the need for effective tools for debugging quantum programs
- Symbolic Reasoning about Quantum Circuits in Coq
- A Case for Synthesis of Recursive Quantum Unitary Programs
- Abstraqt: Analysis of Quantum Circuits via Abstract Stabilizer Simulation
- Formal Methods for Quantum Programs: A Survey
- FeynmanDD: Quantum Circuit Analysis with Classical Decision Diagrams
- Verification of Quantum Systems using Barrier Certificates
- Automated Verification of Silq Quantum Programs using SMT Solvers
- Automating Equational Proofs in Dirac Notation
- Rewriting and Completeness of Sum-Over-Paths in Dyadic Fragments of Quantum Computing
- Equivalence Checking of Quantum Circuits via Path-Sum and Weighted Model Counting
- A Practical Quantum Hoare Logic with Classical Variables, I
- Polynomial-Time Classical Simulation of Hidden Shift Circuits via Confluent Rewriting of Symbolic Sums
- Hoare meets Heisenberg: A Lightweight Logic for Quantum Programs
- Hybrid Path-Sums for Hybrid Quantum Programs