Linear and non-linear relational analyses for Quantum Program Optimization

TL;DR

This paper introduces a novel relational analysis framework for quantum circuit optimization that extends phase folding to complex quantum programs with classical control flow, incorporating non-linear relations for improved optimization.

Contribution

It reformulates phase folding as an affine relation analysis, enabling optimization of complex quantum programs with classical control and introduces non-linear relation analysis using sum-over-paths for better circuit simplification.

Findings

Enabled optimization of quantum programs with nested loops and procedures.

Achieved circuit reductions previously only possible manually.

Demonstrated the effectiveness of non-linear relation analysis in quantum circuit optimization.

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+$T$ -- 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.