This project started as the benchmark implementation for my Bachelor’s thesis, Automated Equivalence Checking of Stabilizer Codes, and was later extended into a replication package for the paper Methods for Automated Equivalence Checking of Quantum Error-Correction Codes. The result is both a collection of algorithmic prototypes and a framework for empirically evaluating their runtime and memory performance. The final hybrid algorithms were also contributed to MQT QECC, where they provide the user-facing equivalence checks.

The motivating research question for equivalence checking is the following:

Given two descriptions of quantum error-correction codes, do they represent genuinely different codes, or are they the same up to an admissible transformation?

This matters when comparing code constructions, removing duplicate entries from code databases, or reusing an expensively constructed encoding circuit for an equivalent code. The difficulty is that the same mathematical code can have very different computational descriptions, while two physically different code spaces may still be equivalent under the relation of interest.

Take the Steane code, drawn below as a with its characteristic triangle of seven qubits with three colored plaquettes. The base construction sits in the center. On the left, the same code appears with its qubits relabeled, so every stabilizer acts on different qubit indices. On the right, local Clifford gates ($H$ or $HS$) are instead applied to individual qubits of the original, which changes the Pauli operators the stabilizers consist of. Written down as matrices, the three look nothing alike, yet they are equivalent under the respective transformations.

Two Degrees of Freedom

I represent a general $\llbracket n,k,d\rrbracket$ stabilizer code as the binary symplectic tableau of its stabilizer group, which characterizes its code space,

whose rows encode independent stabilizer generators, and a CSS code as its separated check matrices

This representation of an abstract mathematical object (the stabilizer group of a stabilizer code) as a concrete matrix exposes two independent sources of freedom, which have to be accounted for in my equivalence checking algorithms.

Representation Freedom

The chosen generators are not unique. Reordering generators or multiplying them produces a different matrix but preserves the stabilizer group, and therefore the code space. In the tableau or check-matrix representation this is an invertible row transformation

Consequently, comparing two tableaus or check matrixes $S$ and $S'$ entry by entry would be incorrect. What matters is their row space.

Physical Freedom

The second freedom comes from the definition of equivalence. Meaning, two codes that can be transformed into each other using the physical transformations, are considered equivalent. I primarily looked at two transformations which only concern the code space:

• a permutation, which relabels the physical qubits;
• a local Clifford operation, which independently changes the Pauli basis of every qubit without introducing entanglement.

Example

Both freedoms are summarized in the figure below. In the mathematical domain on the left, the abstract Steane code and a relabeled copy are related by a qubit permutation $\pi$—a physical transformation. Representing those abstract codes as data objects in the computational domain on the right, there are many different matrices representing one and the same abstract code—such as its standard self-dual check matrices $H_X$ and $H_Z$, but also a combined symplectic tableau using a different generator basis. These different representations are essentially related by row operations $R$—the representation freedom. An equivalence checker only ever sees such matrices as its input, but has to decide whether any two of them describe equivalent codes—aka it as to recognize the red dashed connections, which compose the two possible types of transformation.

Together, both freedoms give the central equation of the project:

Here, $R$ absorbs the arbitrary choice of stabilizer generators and $T$ is the admissible physical transformation. The different checking problems arise by changing the structure permitted for $T$, or the concrete representation $S$ and $S'$.

Equivalence Problems

In my thesis I formulated and considered four different equivalence problems. The last one is omitted in the paper, which focuses on pairwise equivalence problems. All of these checks use the phase-free symplectic representation. Thus, stabilizer phases are ignored and permutation equivalence is understood up to a possible physical Pauli correction.

Pairwise Permutation Equivalence of Stabilizer Codes

Are two general stabilizer codes the same up to relabeling their physical qubits? A qubit permutation has to move the corresponding $X$ and $Z$ columns together.

Pairwise Permutation Equivalence of CSS Codes

The same question for CSS codes, where the generator bases of the two check matrices may change independently, but the qubit permutation must again be shared.

Pairwise Local-Clifford Equivalence of Stabilizer Codes

Are two stabilizer codes the same up to a local Clifford operation the physical qubits? Modulo Pauli operations and global phases, a single-qubit Clifford has six possible actions on the Pauli axes.

Existence of a local-Clifford-equivalent of CSS Codes

The thesis additionally asks whether a given stabilizer code is local-Clifford equivalent to any CSS code.

Algorithmic Toolbox

I implemented and evaluated several complementary strategy families rather than assuming that a single method would dominate. For each equivalence problem, 5 concrete prototypes were implemented. In their structure, the implementations seem rather random, and for the thesis they mostly were to be honest. For the paper, I categorized and structured them a bit more intentionally, like it is explained below.

Invariants and Signatures

An invariant is a property preserved by the selected equivalence relation. Examples include the code parameters, ranks of tableau submatrices, zero- and duplicate-column counts, low-order linear dependencies, stabilizer weight enumerators, and low-degree local invariants.

For example, the stabilizer weight enumerator

is preserved by both permutations and local Clifford operations. A mismatch proves inequivalence immediately; a match is only a necessary condition and cannot prove equivalence.

For permutation problems I also adapted coordinate signatures from classical coding theory, namely from Sendrier’s Support Splitting Algorithm. Each qubit receives a fingerprint derived from the weight enumerator of a punctured code’s hull. Qubits with different signatures can never be mapped to one another, as indicated below, so the signatures partition the candidate permutation space into classes. They can both reject an instance globally and make a later exact check smaller.

Group-Action Search

These methods explicitly traverse the physical transformation group and resolve representation freedom at every step, which is abstractly shown below. The baseline is brute force, while more involved variants avoid redundant or unpromising paths through automorphism groups, canonicalization (implementing the KLS normal form really drove me crazy), or orbit traversal when representing a stabilizer code as a graph state.

The graph-state variant relies on the fact that a local Clifford operation on a graph state corresponds to a local complementation of the underlying graph. In the example below, complementing at node $0$ toggles every edge within its neighborhood (light lilac). The orbit traversal explores all graphs reachable by such steps, discarding those it has already visited.

These methods are very efficient when the physical transformation space stays small, otherwise the traversal takes too much time. Even the graph-state orbit can grow exponentially in the number of qubits.

Isomorphisms

Another strategy removes the arbitrary generator basis by construction and encodes the remaining physical freedom into a colored graph. Thus, we mapped both the representation transformations and the physical transformations to the same kind of freedom, namely, a color-preserving relabeling of the graph-vertices, such that

For general stabilizer codes, graph vertices can represent every stabilizer-group element and its incidences with qubits and Pauli labels. In the example below, this full stabilizer-group construction is applied to two exemplary codes which indeed are permutation equivalent, as indicated by the existing graph isomorphism. The freedom of the graph isomorphism then simultaneously handles the permitted reordering and the basis-independent structure.

The same idea adapts to local-Clifford equivalence, only the graph construction is a bit different to allow for an independent Pauli-basis change of each qubit, while keeping their order intact. Below is one such constructed graph for the paper’s running example of a code with stabilizer group $\langle IXXX, ZZIZ\rangle$.

Both constructions grow with the full stabilizer group, i.e. with $2^r$. For CSS codes, a slightly different construction instead uses the circuits (not quantum or hardware circuits) of the binary matroids induced by $H_X$ and $H_Z$, as shown using the same running example below. This shifts the exponential cost from the number of generators $r$ to the number of qubits $n$.

These methods can be extremely effective while the graph stays small. Their main failure mode is not the isomorphism test itself, but the time and memory needed to construct an exponentially growing graph.

Constraint Solving

Encodings of the equivalence problems into constraint systems or linear systems of equations handle both freedoms simultaneously, and can be solved by delegating the system to a specialized solver.

For SAT, boolean variables describe a row transformation $R$ and either a permutation or local Clifford witness. An auxiliary tableau $A$ can then be constrained from both sides, as sketched below: it must result from physically transforming one input $S$ by $P$ or $Q$, and from changing the generator basis of the other input $S'$ by $R$. The formula is satisfiable exactly if both paths can meet, and a satisfying assignment directly yields the witness.

For local-Clifford equivalence I also implemented the graph-state algorithm of Van den Nest, Dehaene, and De Moor. It reduces the problem to a linear system over $\mathbb{F}_2$ with $4n$ unknowns, followed by constraints ensuring that every local block is symplectic. Within its valid domain it is polynomial and particularly fast.

Limitation of the Graph-State Reduction

Representing a stabilizer code as a graph state, which itself can be represented by a simple undirected graph, enables algorithms such as orbit traversal or the aforementioned polynomial-time algorithm to solve local-Clifford equivalence. However, the use of these algorithms first requires the transformation of a stabilizer code into a stabilizer state, and then a graph state—and here I noticed a slight issue, which made my life a lot harder.

Turning a stabilizer code into a stabilizer state introduces $k$ reference qubits through a Choi-Jamiolkowski-style purification. This requires choosing logical $X$ and $Z$ operators, or equivalently a concrete logical encoding of the code space. That choice is not intrinsic to the code space, so consequently, needs to be accounted for as an additional representation freedom within my checks. As sketched below, an encoding map $V$ and its precomposition $V \circ U$ with a logical Clifford $U$ have the same image $\mathcal{C}$, so they describe the same code, but fix different logical frameworks.

Two descriptions of the same code may use logical frameworks related by an arbitrary $k$-qubit Clifford. For $k\geq2$, that Clifford may entangle the reference qubits, while the graph-state equivalence algorithm only permits local operations there, as is visualized below. As a result, a graph-state method that is complete for stabilizer states does not automatically remain complete for general stabilizer codes.

The implemented graph-state algorithms can therefore only be used (without additional restrictions) when $k<2$: there is no logical freedom when $k=0$, and for $k=1$ every logical Clifford is still a single-qubit operation. Identifying this boundary was one of the most interesting theoretical outcomes of the thesis.

Refute - Refine - Decide

The experiment verified my expectations and showed that no single backend is best for every code class, equivalence notion, and parameter range. I therefore combined the methods into an input-dependent hybrid architecture:

1. Refute: Compare cheap invariants for every input and more expensive invariants only where their measured benefit justifies their cost.
2. Refine: For permutation equivalence, partition qubits by their signatures so that later methods only consider mappings within compatible classes.
3. Decide: Select a sound and complete backend based on the code family and dimensions: group-action search for very small search spaces, graph or matroid isomorphism while their representations remain manageable, the graph-state linear system within its valid domain, and SAT as the broad fallback.

The flowchart below shows this architecture. Invariants refute (pink) the instance potentially which leads to an early exit, and signatures refine (cyan) the permutation search space before the dispatcher chooses a fitting strategy to decide the instance (lilac), routing each instance along one of the dashed edges to the strategy that suits it: group-action search for a small physical transformation space, isomorphisms for small representation freedom, and constraint solving as the reliable fallback.

This ordering creates an intentional runtime asymmetry. An inequivalent pair may be rejected by the first inexpensive mismatch, whereas an equivalent pair generally has to reach a complete decision procedure.

The library-facing checks return witnesses when possible:

from mqt.qecc import (
    are_local_clifford_equivalent,
    are_permutation_equivalent,
)

permutation = are_permutation_equivalent(code_a, code_b)
local_cliffords = are_local_clifford_equivalent(code_a, code_b)

# None means that no such equivalence exists. Otherwise, the result
# explicitly describes the transformation mapping code_a to code_b.

As a note, the hybrids constructed in the thesis differ from those considered in the paper, as I constructed the latter one with a bit more data from the empirical evaluation.

Evaluation

Problem Instances

I evaluated the implementations in two complementary regimes. The randomized suite covered a grid of code parameters up to $n=47$, with up to ten equivalent and ten inequivalent pairs for each $(n,k)$ setting and algorithm. A second suite used 18 named, structured codes ranging from the small 3-qubit repetition, 5-qubit perfect, and Hamming codes to Golay, color, rotated-surface, and bivariate bicycle codes with up to $144$ physical qubits. This combination was important: dense, random instances expose broad scaling behavior, while structured codes reveal whether the resulting hybrid still works on the kinds of constructions one might actually want to compare.

The benchmark pairs were generated deliberately. Positive instances start from one code and apply a known random qubit permutation or local Clifford, followed by a random change of stabilizer-generator basis. For negative instances, simply sampling two independent codes would make many comparisons unrealistically easy. I instead applied a short two-gate Clifford or CNOT perturbation and retained the pair only after an exact SAT or matroid backend certified inequivalence where feasible. Larger CSS cases use a separate permutation-invariant certificate. All randomized experiments derive from a master seed of $42$, and input generation and certification happen before the timed call.

Resource Restriction

Every algorithm call was isolated in its own supervised worker and received a wall-clock budget of $5400$ seconds and a memory budget of $13$ GiB. The supervisor combined an address-space limit with periodic monitoring of the worker’s complete process group, so memory allocated by child processes was counted as well. On a timeout or memory violation it terminated the whole group, while recording timeouts, memory failures, execution errors, wrong answers, and input-generation failures separately. The successful-call timer surrounds only the algorithm itself; worker startup and result transfer are excluded.

I also collected diagnostics beyond elapsed time, for example solver decisions when comparing SAT implementations, or deciding stage when measuring hybrids.

Insights

Invariants and Signatures

Cheap invariants, like the code parameters or matrix ranks, are always applied. The question was whether the more expensive ones are worth it. Preliminary experiments narrowed the candidates down to linear column dependencies and signatures for permutation equivalence, and a low-degree local invariant for local-Clifford equivalence.

Their job is to reject as many inequivalent instances as possible, and they do so remarkably well, especially on CSS codes, as the mean rejection rates on the randomized inequivalent instances show:

However, a high rejection rate alone does not make an invariant useful. It also has to be cheaper than the decision work it tries to avoid—it doesn’t make sense to compute an invariant for minutes that can only hopefully reject the instance, when a full decision algorithm would have decided it within seconds. The parameter maps below therefore compare each invariant’s runtime with that of the fastest decision method for the same parameters: blue cells favor the invariant, red ones the decision method, and the pink outlines mark where I consider the invariant worthwhile. Linear column dependencies only pay off for larger codes, signatures on general stabilizer codes only for small ones (they scale badly with the number of generators $r$), and the local invariant only for small $n$, where it actually is the most discriminant anyways. The specialized signature implementation for CSS codes, is the exception and beneficial throughout the whole parameter space. Thus is probably an implementation artifact, because for the CSS case I could make use of heavily optimized $\mathbb{F}_2$ libraries, whereas I needed to handroll a lot of $\mathbb{F}_4$ arithmetic myself in Python for the adaptation to general stabilizer codes.

Signatures have a second job: refining the permutation search space by partitioning the qubits into classes. The maps below show the fraction $\bar{q}$ of qubit pairs they tell apart, from $0$ (no refinement) to $1$ (every qubit distinguished). On average, two random distinct qubits are distinguished with a probability of $86\,\%$ for general stabilizer codes and $69\,\%$ for CSS codes. The refinement saturates as $r$ grows, while the computation time keeps growing, as the timed-out cells in the upper right of the left map show.

So invariants and signatures are beneficial, but only in parts of the parameter space, and the hybrid has to apply them depending on the input parameters.

Decision Methods

The most important result was not a universal winner strategy, but a map of where each paradigm performs best, shown below. Apart from general selection guidelines, these maps also provided the exact parameter thresholds for the dispatcher of the hybrids.

Group-action search is only competitive while the physical search space is small. The exhaustive search over permutations, combined with the rank-based row-space check, wins for CSS codes with few qubits in the lower left of the middle map. Traversing the LC-orbit while canonicalizing into KLS form at each step is fastest for a few isolated settings, but shows no consistent trend.

Isomorphisms win where their encoded object stays small: the full-group encoding for few stabilizer generators (low $r$), the matroid-circuit encoding for few qubits (low $n$). Isolating their runtime, as in the maps below, shows how steeply the cost rises with the graph size, until memory becomes the actual limiting factor (crosses). Surprisingly, the permutation construction runs out of memory before the local-Clifford one, despite having fewer nodes in our examples. This is actual an implementation artifact: the graph-isomorphism backend does not support colored edges, so the permutation encoding represents them by auxiliary nodes (aka blowing up the graph size even more).

SAT is the strongest general baseline. It covers the widest parameter range for both permutation and local-Clifford equivalence of stabilizer codes, and never ran out of memory, an important property for a fallback solution for big codes. The one surprise was permutation equivalence of CSS codes: as the comparison below shows, there are some parameter ranges where the CSS codes are slower by a magnitude compared to same-size general stabilizer codes. This is not caused by the concrete representation, as CSS codes given as full tableaus behave the same, and choosing a different generator basis to make a CSS code look non-CSS also does not help. Instead, the separated $X/Z$ structure couples the constraints less, so a wrong partial permutation is refuted much later by the solver (but I go into way more detail about that in the paper). Ironically, the same structure is what makes other things like signatures so effective on CSS codes.

The graph-state linear system has a noticeable conversion overhead for small codes, but within its restricted domain $k<2$, it is the fastest local-Clifford method.

Hybrid Checkers

Finally, I evaluated the complete implemented hybrids with conservative thresholds derived from the experiments above, on randomized variants of the structured codes. In the table below, the color of each cell encodes the mean runtime for equivalent ($+$) and inequivalent ($-$) instances, and its label names the stage that terminated most runs: CI/EI cheap/expensive invariants, S signatures, BF exhaustive (“brute force”) search, MI/GI matroid/graph isomorphism, SAT, and LSE for the graph-state linear system.

The most visible effect is an asymmetry between equivalent and inequivalent inputs. An equivalent pair can never be rejected early and always has to reach a complete decision procedure, whereas cheap invariants terminate many inequivalent permutation instances, and signatures become decisive for larger CSS codes.

In numbers, most cases with at most $37$ physical qubits had mean hybrid runtimes below $10$ seconds. Even at $n=144$, inequivalent CSS permutation instances were decided in about $310$ seconds on average, while inequivalent local-Clifford instances remained below $16$ seconds on average. For equivalent local-Clifford instances, every evaluated $n=72$ case completed with a mean of $49$ seconds, while larger cases increasingly reached the timeout. These numbers are empirical feasibility results under the paper’s resource budget, not worst-case guarantees.

Replication Package

The repository preserves the research prototypes, tests, structured code instances, thesis benchmarks, and the complete experimental pipeline used for the paper, which is structured as follows:

paper/
  benchmarks/       long-running data collection
  experiments/      deterministic extraction and aggregation
  visualizations/   generation of the paper's figures

The paper pipeline deliberately separates three phases for each figure that is used in the paper, as shown below. Only the first phase generates codes, runs algorithms, and consumes meaningful compute time, on a benchmark server. Its raw measurements in data/collected/ are the only thing transferred to the local machine, where a deterministic extraction step turns them into figure-ready tables, which the visualization step then draws. This makes it possible to inspect the exact measurements and aggregation rules, regenerate the figures without rerunning days of benchmarks, or reproduce the entire experiment from the original seeded inputs.

As a note, I committed the actually used data from the paper in the repo as well.

Acknowledgements

I really really enjoyed working on this project as a thesis, and am super happy about my (unofficial) advisor Tom, who introduced me to that topic and really helped me a lot getting started—even months before I actually started the thesis officially. And he helped me get a job as a student assistant at the CDA, for which I am super thankful. Obviously I am also super grateful for mu official advisor and co-author Ludwig who I finished the thesis with in the end, and who was super supportive when I threw the idea of a potential publication into the room. And last but definitely not least, my supervisor, co-author, and employer, Robert, whose guidance, motivation, and approachability I cannot appreciate and cherish enough :)