Linear and non-linear relational analyses for Quantum Program Optimization
arXiv:2410.23493 · doi:10.1145/3704873
Abstract
The phase folding optimization is a circuit optimization used in many quantum compilers as a fast and effective way of reducing the number of high-cost gates in a quantum circuit. However, existing formulations of the optimization rely on an exact, linear algebraic representation of the circuit, restricting the optimization to being performed on straightline quantum circuits or basic blocks in a larger quantum program. We show that the phase folding optimization can be re-cast as an \emph{affine relation analysis}, which allows the direct application of classical techniques for affine relations to extend phase folding to quantum \emph{programs} with arbitrarily complicated classical control flow including nested loops and procedure calls. Through the lens of relational analysis, we show that the optimization can be powered-up by substituting other classical relational domains, particularly ones for \emph{non-linear} relations which are useful in analyzing circuits involving classical arithmetic. To increase the precision of our analysis and infer non-linear relations from gate sets involving only linear operations -- such as Clifford+ -- we show that the \emph{sum-over-paths} technique can be used to extract precise symbolic transition relations for straightline circuits. Our experiments show that our methods are able to generate and use non-trivial loop invariants for quantum program optimization, as well as achieve some optimizations of common circuits which were previously attainable only by hand.
30 pages, 13 figures, comments welcome!
References in corpus (20)
- Elementary gates for quantum computation
- Surface codes: Towards practical large-scale quantum computation
- Quantum Teleportation is a Universal Computational Primitive
- Improved Simulation of Stabilizer Circuits
- Restrictions on Transversal Encoded Quantum Gate Sets
- A Game of Surface Codes: Large-Scale Quantum Computing with Lattice Surgery
- Polynomial-time T-depth Optimization of Clifford+T circuits via Matroid Partitioning
- Automated optimization of large quantum circuits with continuous parameters
- On the advantages of using relative phase Toffolis with an application to multiple control Toffoli optimization
- Reducing T-count with the ZX-calculus
- Towards Large-scale Functional Verification of Universal Quantum Circuits
- PyZX: Large Scale Automated Diagrammatic Reasoning
- A Verified Optimizer for Quantum Circuits
- Quantum entanglement analysis based on abstract interpretation
- T-count optimization and Reed-Muller codes
- Synthesizing Quantum-Circuit Optimizers
- Enabling Dataflow Optimization for Quantum Programs
- Assertion-Based Optimization of Quantum Programs
- Quantifier Elimination over Finite Fields Using Gröbner Bases
- Abstraqt: Analysis of Quantum Circuits via Abstract Stabilizer Simulation