Linear and non-linear relational analyses for Quantum Program Optimization

TL;DR

The paper tackles the high T-count challenge in Clifford+$T$ quantum circuits by generalizing phase folding from circuits to complete quantum programs with classical control. It reframes phase folding as an affine-relations analysis (ARA) and then extends it to non-linear relations by introducing polynomial-ideal (Gröbner-basis) domains, including a path-integral based method to extract precise classical transitions. The authors present two concrete domains, KS for affine relations and Pol for polynomial relations, and develop forward-analysis and summarization techniques to scale to large programs; they also introduce sum-over-paths to increase precision and a Strengthen procedure to exploit interference for further optimization. Experimental results on program and circuit benchmarks demonstrate non-trivial loop invariants and competitive T-count reductions, including cases previously achievable only by hand, illustrating the practical potential of applying classical relational analysis to quantum programming. Overall, this work bridges classical program analysis with quantum compilation, enabling more powerful, scalable optimizations across hybrid quantum-classical programs and opening avenues for deeper invariant-driven quantum optimizations.

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.

Figures (13)

• Figure 1: The relational approach to phase folding. If every classical state $\ket{\vec{x}'}$ in the support of $U\ket{\vec{x}}$ satisfies $x_j'=x_i$, a phase gate on $\ket{x_i}$ can be commuted through $U$. More generally, a phase conditional on some function $f:\mathbb{F}_2^n\rightarrow \mathbb{F}_2$ commutes with $U$ if and only if $f(\vec{x}) = g(\vec{x}')$ for all $\vec{x}'$ in the support of $U\ket{\vec{x}}$.
• Figure 2: Repeat-Until-Success circuits. The box denotes a loop which terminates exactly when the measurement result $xy$ of the first two qubits is $00$.
• Figure 3: A circuit with eliminable $\textsc{t}$ gates. The strongest affine loop invariant on the classical support is the relation $x'\oplus y' = x\oplus y$, which implies that the total phase contribution of both $\textsc{t}$ gates is $1$.
• Figure 4: An example of a quantum circuit, implementing the Toffoli gate $\textsc{tof}:\ket{x_1,x_2,x_3} \mapsto \ket{x_1,x_2,x_3\oplus x_1x_2}$
• Figure 5: Standard gates and their circuit notation.

Theorems & Definitions (28)

• Example 1
• Example 2
• Example 3
• Example 4
• Example 5
• Definition 6: sound & precise
• Proposition 7
• proof
• Remark 8
• Proposition 9