Manjushri: A Tool for Equivalence Checking of Quantum Circuits

TL;DR

The paper tackles scalable verification of quantum-circuit equivalence by introducing Manjushri, a Projection-Based Equivalence Checking framework that encodes local projections with Weighted Binary Decision Diagrams via the Quasimodo symbolic backend. It provides a rigorous empirical comparison to ECMC on large-scale random 1D Clifford+$T$ circuits across up to 128 qubits and depths up to 50, demonstrating substantial speedups for shallower circuits and a practical depth bound around $\approx38$ before performance degrades. The work critically analyzes the trade-offs between PBEC-based methods and model-count-based approaches, showing that Manjushri is a practical and scalable solution for large-scale quantum-circuit verification and would be preferred for circuit fragments up to moderate depth. The results have direct implications for quantum circuit optimization workflows, enabling faster verification of rewritten subcircuits and potentially guiding the design of optimizers that operate within the depth window where Manjushri remains reliable.

Abstract

Verifying whether two quantum circuits are equivalent is a central challenge in the compilation and optimization of quantum programs. We introduce \textsc{Manjushri}, a new automated framework for scalable quantum-circuit equivalence checking. \textsc{Manjushri} uses local projections as discriminative circuit fingerprints, implemented with weighted binary decision diagrams (WBDDs), yielding a compact and efficient symbolic representation of quantum behavior. We present an extensive experimental evaluation that, for random 1D Clifford+$T$ circuits, explores the trade-off between \textsc{Manjushri} and \textsc{ECMC}, a tool for equivalence checking based on a much different approach. \textsc{Manjushri} is much faster up to depth 30 (with the crossover point varying from 39--49, depending on the number of qubits and whether the input circuits are equivalent or inequivalent): when inputs are equivalent, \textsc{Manjushri} is about 10$\times$ faster (or more); when inputs are inequivalent, \textsc{Manjushri} is about 8$\times$ faster (or more). For both kinds of equivalence-checking outcomes, \textsc{ECMC}'s success rate out to depth 50 is impressive on 32- and 64-qubit circuits: on such circuits, \textsc{ECMC} is almost uniformly successful. However, \textsc{ECMC} struggled on 128-qubit circuits for some depths. \textsc{Manjushri} is almost uniformly successful out to about depth 38, before tailing off to about 75\% at depth 50 (falling to 0\% at depth 48 for 128-qubit circuits that are equivalent). These results establish that \textsc{Manjushri} is a practical and scalable solution for large-scale quantum-circuit verification, and would be the preferred choice unless clients need to check equivalence of circuits of depth $>$38.

Figures (3)

• Figure 1: Results for 32-qubit random-circuit benchmarks.
• Figure 2: Results for 64-qubit random-circuit benchmarks.
• Figure 3: Results for 128-qubit random-circuit benchmarks.

Theorems & Definitions (1)

• definition thmcounterdefinition: Circuit equivalence