Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Efficient equivalence checking of Clifford-U circuits with shared single-qubit unitaries

Daisuke Sakamoto, Soshun Naito, Yusei Mori, Kosuke Mitarai

Abstract

Quantum circuit equivalence checking asks whether two circuits implement the same unitary. It guarantees compiler correctness and safe optimization, yet most existing approaches scale exponentially with the number of qubits or the circuit depth, or are restricted to specific circuit structures. In this work, we present an equivalence-checking method for circuits formed by arbitrary single-qubit layers interleaved with Clifford layers. This pattern is common in variational quantum algorithms and Hamiltonian simulation via Trotter decomposition. It can also represent any unitary with sufficient depth. We prove the existence of an efficient classical algorithm that determines whether a pair of circuits with shared single-qubit layers are equivalent for every possible choice of the shared single-qubit unitaries. The same algorithm can also certify their non-equivalence for fixed assignments of single-qubit unitaries. Our framework supports the validation of emerging quantum compilers and facilitate the discovery of novel circuit optimization passes.

Efficient equivalence checking of Clifford-U circuits with shared single-qubit unitaries

Abstract

Quantum circuit equivalence checking asks whether two circuits implement the same unitary. It guarantees compiler correctness and safe optimization, yet most existing approaches scale exponentially with the number of qubits or the circuit depth, or are restricted to specific circuit structures. In this work, we present an equivalence-checking method for circuits formed by arbitrary single-qubit layers interleaved with Clifford layers. This pattern is common in variational quantum algorithms and Hamiltonian simulation via Trotter decomposition. It can also represent any unitary with sufficient depth. We prove the existence of an efficient classical algorithm that determines whether a pair of circuits with shared single-qubit layers are equivalent for every possible choice of the shared single-qubit unitaries. The same algorithm can also certify their non-equivalence for fixed assignments of single-qubit unitaries. Our framework supports the validation of emerging quantum compilers and facilitate the discovery of novel circuit optimization passes.
Paper Structure (18 sections, 13 theorems, 81 equations, 3 figures, 1 table)

This paper contains 18 sections, 13 theorems, 81 equations, 3 figures, 1 table.

Table of Contents

  1. Introduction
  2. Problem Setting and Main Result
  3. Proof Sketch
  4. Discussion
  5. Applicability
  6. Limitations Imposed by NQP- and QMA-Hardness Results
  7. Advantages over Heuristic and Local Verification Methods
  8. numerical experiment
  9. Setup
  10. Experimental procedure
  11. Results of numerical experiments
  12. Runtime comparison between the proposed method and QCEC (Experiment 1)
  13. Observing the runtime of the proposed method (Experiment 2)
  14. Discussion of the experimental results
  15. Conclusion
  16. ...and 3 more sections

Key Result

Theorem 1

Under definition def:F,Fprime, def:V, and def:B,Bprime, $F(\vec{U})$ and $F'(\vec{U})$ are equivalent for any $\vec{U}$, if and only if these two equations simultaneously hold.

Figures (3)

  • Figure 1: Circuit diagrams of the quantum circuits $F$ and $F'$ targeted for equivalence checking in this paper.
  • Figure 2: Relationship between the number of layers $m$ of the circuit pair and the runtime of the proposed method and QCEC (logarithmic scale on the vertical axis). We evaluate the runtime of these methods for pairs of equivalent circuits in (a) and non-equivalent circuits in (b) and (c). In (b), $F_\text{err}$ was generated by inserting an Pauli error into $F$. In (c), $F$ and $G$ are generated independently.
  • Figure 3: Relationship between the number of layers $m$ of the equivalent circuit pair $F,F'$ and the runtime of the proposed method (log-log plot). We evaluate the runtime of the proposed method on circuit pairs. In (a), we measure the runtime as a function of the number of qubits $n$. In (b), we measure the runtime as a function of the number of layers $m$.

Theorems & Definitions (35)

  • Definition 1
  • Definition 2
  • Definition 3: Decision matrix
  • Theorem 1
  • Definition 4: Cumulative Adjoint Products
  • Lemma 1
  • proof
  • Lemma 2
  • proof
  • Lemma 3
  • ...and 25 more