Approximate Equivalence Checking

Approximate and exact equivalence

Two quantum circuits are exactly equivalent if their unitary matrix representations, \(U\) and \(V\), are identical up to the equivalence relation of interest. For full unitary equivalence up to global phase, this can be checked by determining whether \(UV^\dagger\) is the identity up to global phase.

In approximate synthesis and optimization, it is often useful to accept a circuit that is sufficiently close to the original. MQT QCEC quantifies this using the projective Hilbert–Schmidt distance:

\[D_\mathrm{HS}(U, V) = \sqrt{1 - \left|\frac{\operatorname{Tr}(UV^\dagger)}{2^n}\right|^2},\]

where \(n\) is the number of qubits. The distance is invariant under global phase and ranges from zero to one for unitary matrices. MQT QCEC considers two circuits approximately equivalent when their distance is at most the configured threshold \(\epsilon\).

Supported checkers

Set check_approximate_equivalence to True to enable approximate checking. The approximate_checking_threshold option controls the accepted distance and defaults to 1e-8. It must be finite and lie in the closed interval [0, 1].

The construction and alternating checkers compute the normalized trace using decision diagrams. At least one of these two checkers or the HSF checker described below must be enabled. The simulation checker compares individual output states, so its fidelity threshold does not represent the configured process distance; MQT QCEC disables it automatically in approximate mode. MQT QCEC also disables the ZX-calculus checker because it cannot establish approximate non-equivalence.

Approximate checking currently supports fixed, full-unitary circuits for which no ancillary or garbage qubits remain after preprocessing. Parameterized circuits and partial equivalence use different equivalence relations and are rejected when approximate checking is enabled.

The optional hybrid Schrödinger–Feynman (HSF) checker computes the same projective Hilbert–Schmidt distance by cutting each circuit into two horizontal slices. Cross-cut controlled gates are decomposed into sums of tensor products, allowing the slices and summands to be evaluated independently, as described in [7]. Enable it with run_hsf_checker=True in addition to check_approximate_equivalence=True.

HSF is a standalone alternative to the alternating and construction checkers. When it is enabled, MQT QCEC disables those checkers; the simulation and ZX-calculus checkers are already disabled by approximate mode. The parallel option controls HSF’s internal parallelism: when it is False, HSF uses one worker; when it is True, HSF uses up to nthreads workers. For \(k\) cross-cut gates, it evaluates \(2^k\) summands; although at most 63 decisions can be represented, the practical limit is typically much smaller. The checker is therefore intended for sufficiently shallow circuits with few cross-cut gates.

HSF uses trace_threshold as its numerical tolerance for the projective distance. Within that tolerance, the trace phase distinguishes equivalent from equivalent_up_to_global_phase. Outside it, only approximate_checking_threshold determines acceptance. Phase proximity alone never establishes equivalence. As with any floating-point trace calculation, distances near zero are limited by rounding error.

Normal circuit optimization and layout processing still run before HSF. MQT QCEC normalizes initial layouts and cancels common output permutations. Only the relative output permutation is materialized: SWAPs within a slice remain SWAPs, while those crossing the cut become three CNOTs each and count toward the decision limit. Incomplete mappings are rejected. A nontrivial HSF check requires at least two qubits after idle-qubit removal and does not support gates with targets on both sides of the cut or multiple controls on the control side of a cross-cut gate. These are implementation limitations; unsupported circuits are rejected instead of falling back to another checker.

Example

Consider a three-qubit Toffoli gate and the identity circuit.

from qiskit import QuantumCircuit

qc_lhs = QuantumCircuit(3)
qc_lhs.mcx([0, 1], 2)

qc_rhs = QuantumCircuit(3)
qc_rhs.id(range(3))

qc_lhs.draw(output="mpl", style="iqp")

The normalized trace magnitude of the Toffoli matrix is \(0.75\), so its projective Hilbert–Schmidt distance from the identity is \(\sqrt{1 - 0.75^2} = \sqrt{7}/4 \approx 0.6614\). A threshold of \(0.7\) therefore accepts the pair:

from mqt.qcec import verify
from mqt.qcec.pyqcec import Configuration

config = Configuration()
config.functionality.check_approximate_equivalence = True
config.functionality.approximate_checking_threshold = 0.7
config.execution.run_hsf_checker = True

verify(qc_lhs, qc_rhs, configuration=config)

[QCEC] Warning: the simulation checker does not implement the unitary process distance used for approximate equivalence checking and will be disabled.
[QCEC] Warning: the ZX checker cannot establish approximate non-equivalence and will be disabled.
[QCEC] Warning: the HSF checker is an exclusive approximate checker; the alternating checker will be disabled.

<EquivalenceCheckingManager.Results: equivalent>

A threshold below \(\sqrt{7}/4\) rejects the same pair:

config.functionality.approximate_checking_threshold = 0.6
verify(qc_lhs, qc_rhs, configuration=config)

[QCEC] Warning: the simulation checker does not implement the unitary process distance used for approximate equivalence checking and will be disabled.
[QCEC] Warning: the ZX checker cannot establish approximate non-equivalence and will be disabled.
[QCEC] Warning: the HSF checker is an exclusive approximate checker; the alternating checker will be disabled.

<EquivalenceCheckingManager.Results: not_equivalent>

This is the unitary distance used by BQSKit. The approach is also inspired by work on approximate equivalence checking and approximate quantum-circuit synthesis.