Towards Large-scale Functional Verification of Universal Quantum Circuits
arXiv:1805.06908 · doi:10.4204/EPTCS.287.1
Abstract
We introduce a framework for the formal specification and verification of quantum circuits based on the Feynman path integral. Our formalism, built around exponential sums of polynomial functions, provides a structured and natural way of specifying quantum operations, particularly for quantum implementations of classical functions. Verification of circuits over all levels of the Clifford hierarchy with respect to either a specification or reference circuit is enabled by a novel rewrite system for exponential sums with free variables. Our algorithm is further shown to give a polynomial-time decision procedure for checking the equivalence of Clifford group circuits. We evaluate our methods by performing automated verification of optimized Clifford+T circuits with up to 100 qubits and thousands of T gates, as well as the functional verification of quantum algorithms using hundreds of qubits. Our experiments culminate in the automated verification of the Hidden Shift algorithm for a class of Boolean functions in a fraction of the time it has taken recent algorithms to simulate.
arXiv commentIn Proceedings QPL 2018, arXiv:1901.09476
References in corpus (15)
- Quantum Teleportation is a Universal Computational Primitive
- Improved classical simulation of quantum circuits dominated by Clifford gates
- Polynomial-time T-depth Optimization of Clifford+T circuits via Matroid Partitioning
- On the advantages of using relative phase Toffolis with an application to multiple control Toffoli optimization
- QWIRE Practice: Formal Verification of Quantum Circuits in Coq
- On the CNOT-complexity of CNOT-PHASE circuits
- Verified compilation of space-efficient reversible circuits
- Verifying the Steane code with Quantomatic
- Quantum circuits and low-degree polynomials over F_2
- A quantum primality test with order finding
- Efficient rate-adaptive reconciliation for continuous-variable quantum key distribution
- Robustness of QMA against witness noise
- Rewriting modulo symmetric monoidal structure
- Verifying the Smallest Interesting Colour Code with Quantomatic
- Computing quopit Clifford circuit amplitudes by the sum-over-paths technique
Cited by in corpus (48)
- Reducing T-count with the ZX-calculus
- A Verified Optimizer for Quantum Circuits
- staq -- A full-stack quantum processing toolkit
- A Deductive Verification Framework for Circuit-building Quantum Programs
- Equivalence Checking of Quantum Circuits with the ZX-Calculus
- Formal Verification of Quantum Programs: Theory, Tools and Challenges
- Synthesizing Quantum-Circuit Optimizers
- symQV: Automated Symbolic Verification of Quantum Programs
- ZX-calculus for the working quantum computer scientist
- Fast Stabiliser Simulation with Quadratic Form Expansions
- Techniques to Reduce -Parity-Phase Circuits, Motivated by the ZX Calculus
- Equivalence Checking of Parameterized Quantum Circuits: Verifying the Compilation of Variational Quantum Algorithms
- Equivalence Checking of Sequential Quantum Circuits
- Benchmarking the performance of quantum computing software
- Proving Quantum Programs Correct
- Hypergraph Simplification: Linking the Path-sum Approach to the ZH-calculus
- Relating Measurement Patterns to Circuits via Pauli Flow
- Classical simulation of quantum circuits by half Gauss sums
- Partial Equivalence Checking of Quantum Circuits
- Efficient Formal Verification of Quantum Error Correcting Programs
- Rotational Abstractions for Verification of Quantum Fourier Transform Circuits
- On the need for effective tools for debugging quantum programs
- A Case for Synthesis of Recursive Quantum Unitary Programs
- CertiQ: A Mostly-automated Verification of a Realistic Quantum Compiler
- The Basis of Design Tools for Quantum Computing: Arrays, Decision Diagrams, Tensor Networks, and ZX-Calculus
- Symbolic Reasoning about Quantum Circuits in Coq
- Linear and non-linear relational analyses for Quantum Program Optimization
- AND-gates in ZX-calculus: Spider Nest Identities and QBC-completeness
- Abstraqt: Analysis of Quantum Circuits via Abstract Stabilizer Simulation
- FeynmanDD: Quantum Circuit Analysis with Classical Decision Diagrams
- Formal Methods for Quantum Programs: A Survey
- Complete Equational Theories for the Sum-Over-Paths with Unbalanced Amplitudes
- Completeness of the ZH-calculus
- Building Qutrit Diagonal Gates from Phase Gadgets
- Symbolic Synthesis of Clifford Circuits and Beyond
- Scaling W state circuits in the qudit Clifford hierarchy
- Relaxed Peephole Optimization: A Novel Compiler Optimization for Quantum Circuits
- Automating Equational Proofs in Dirac Notation
- Optimal compilation of parametrised quantum circuits
- Multi-controlled Phase Gate Synthesis with ZX-calculus applied to Neutral Atom Hardware
- Generators and Relations for the Group On(Z[1/2])
- Rewriting and Completeness of Sum-Over-Paths in Dyadic Fragments of Quantum Computing
- Quantum Hoare Type Theory: Extended Abstract
- Type-Based Verification of Connectivity Constraints in Lattice Surgery
- Quantum Theory from Principles, Quantum Software from Diagrams
- Hybrid Path-Sums for Hybrid Quantum Programs
- Polynomial-Time Classical Simulation of Hidden Shift Circuits via Confluent Rewriting of Symbolic Sums
- Bit-Vector Abstractions to Formally Verify Quantum Error Detection & Entanglement