Towards Large-Scale Functional Verification of Universal Quantum Circuits
Towards Large-Scale Functional Verification of Universal Quantum Circuits
Amy uses Feynman path integrals and exponential-sum rewriting to verify large universal quantum circuits functionally.
Paper information (formal version: 2019, EPTCS 287, pp. 1–21; preprint: 2018) — Matthew Amy. DOI; arXiv:1805.06908
Work
The paper introduces a formal specification and verification framework for quantum circuits based on the Feynman path integral. Quantum operations are represented by exponential sums of polynomial functions, which gives a structured account of quantum implementations of classical functions. A rewrite system with free variables supports comparison with a specification or reference circuit. The framework covers the Clifford hierarchy and experiments verify circuits and algorithms with hundreds of qubits and thousands of T gates.
Contributions
- A structured functional semantics for circuits using exponential sums and polynomial functions.
- A rewrite system with free variables for specification, reference-circuit, and equivalence checking.
- A polynomial-time decision procedure for equivalence of Clifford-group circuits.
- Automated verification experiments on large Clifford+T circuits and quantum algorithms.
Limits
Efficiency and scale depend on the circuit fragment, rewrite system, and specification representation; the experiments do not imply equal performance for every universal circuit. The method proves functional properties of ideal circuits and does not automatically cover noise, compiler implementation, hardware calibration, or resource optimality. Other gate sets and more complex control structures may require extensions.
Connections
The paper advances the circuit-equivalence direction in Verification Methods and Tools toward large-scale functional verification. It can be compared with A Complete Axiomatisation of the ZX-Calculus for Clifford+T Quantum Mechanics: this work centers exponential sums and algorithmic verification, while the other centers diagrammatic equational completeness. It forms a path from circuit formats such as OpenQASM and Quipper to verification.
Original paper
Matthew Amy, Towards Large-Scale Functional Verification of Universal Quantum Circuits, EPTCS 287, 1–21 (2019), DOI: 10.4204/EPTCS.287.1. arXiv:1805.06908