PaperlayerView exact revision on arXiv

Source-linked AI summary

Advanced Equivalence Checking for Quantum Circuits

Lukas Burgholzer, Robert Wille

arXiv:2004.08420v2quant-phcs.ET

TL;DR

Quantum design flows substantially change circuit descriptions, creating a need to check whether intended functionality is preserved; existing approaches extend classical methods and remain unsatisfactory in many cases. The paper combines reversibility-based checking with simulation, and experiments report dramatically faster equivalence checking, often with just one simulation run.

  • Problem

    Quantum design flows change circuit descriptions, while existing quantum equivalence methods extend classical approaches and remain unsatisfactory in many cases.

    Source: §I · p. 1

  • Method

    The flow uses reversibility to keep G · G′−1 close to identity and simulations on arbitrary states to seek counterexamples or indicate possible equivalence.

    Source: §I · p. 2, B. Discussion · p. 10

  • Results

    Experiments report dramatically faster equivalence checking, often using simulation alone or just a single simulation run.

    Source: §I · p. 2, §IX · p. 12

  • Takeaways & Limitations

    Even if proof completion is blocked by resource limits, simulations can already provide a counterexample or an indication that the circuits might be equivalent.

    Source: B. Discussion · p. 10, A. Resulting Flow · p. 10

    Some simulation runs can themselves be too resource-consuming, especially when simulation fails because of immense complexity.

    Source: B. Discussion · p. 10

Abstract

from arXiv · show

Quantum computing will change the way we tackle certain problems. It promises to dramatically speed-up many chemical, financial, and machine-learning applications. However, to capitalize on those promises, complex design flows composed of steps such as compilation, decomposition, or mapping need to be employed before being able to execute a conceptual quantum algorithm on an actual device. This results in descriptions at various levels of abstraction which may significantly differ from each other. The complexity of the underlying design problems necessitates to not only provide efficient solutions for the single steps, but also to verify that the originally intended functionality is preserved throughout all levels of abstraction. This motivates methods for equivalence checking of quantum circuits. However, most existing methods are inspired by the classical realm and have merely been extended to support quantum circuits (i.e., circuits which do not only rely on 0's and 1's, but also employ superposition and entanglement). In this work, we propose an advanced methodology which takes the different paradigms of quantum circuits not only as a burden, but as an opportunity. In fact, the proposed methodology explicitly utilizes characteristics unique to quantum computing in order to overcome the shortcomings of existing approaches. We show that, by exploiting the reversibility of quantum circuits, complexity can be kept feasible in many cases. Moreover, we show that, in contrast to the classical realm, simulation is very powerful in verifying quantum circuits. Experimental evaluations confirm that the resulting methodology allows one to conduct equivalence checking dramatically faster than ever before--in many cases just a single simulation run is sufficient. An implementation of the proposed methodology is publicly available at https://iic.jku.at/eda/research/quantum_verification/.

I. INTRODUCTION

Quantum design flows transform algorithms across abstraction levels, so equivalence checking is needed to verify that these changes preserve intended functionality. The paper proposes exploiting reversibility and simulation, reporting much faster checking and often only one simulation run.

I. INTRODUCTION

  • Design steps such as decomposition, mapping, and optimization change circuit descriptions, making equivalence checking necessary to verify that intended functionality is preserved.The circuits being compared are the original algorithm and the result of the design process.Source: §I · p. 1
  • Prior quantum equivalence methods extend classical rewriting, SAT, and decision-diagram approaches, but remain unsatisfactory in many cases.The paper proposes treating quantum-specific characteristics as an opportunity rather than a burden.Source: §I · p. 1
  • Reversibility lets equivalent circuits G and G′ be compared through G · G′−1 = I, with gate ordering chosen to keep representations near the compact identity.The identity has a linear-size decision-diagram representation in the stated example class.Source: §I · p. 2
  • A few simulations on arbitrary input states often reveal non-equivalence, while matching simulation results indicate possible—but do not prove—equivalence.The proposed flow uses simulation first and can accelerate a subsequent proof by keeping G · G′−1 close to identity.Source: §I · p. 2
  • Experiments report dramatically faster equivalence checking, often with just a single simulation run.The paper also highlights simulation’s potential for quantum-circuit verification.Source: §I · p. 2

A. Quantum Computing

  • Unlike classical bits, qubits can be in superpositions, and some system states are entangled so their individual qubit states cannot be separated.Circuit simulation applies gate matrices to an input state; for a computational basis input, the output is the corresponding system-matrix column.Source: A. Quantum Computing · pp. 2–3

B. Decision Diagrams for Quantum Computing

Decision diagrams represent quantum functionality by recursively decomposing matrices and sharing repeated structure. Edge weights and redundancy can make representations compact, although worst-case size remains exponential.

B. Decision Diagrams for Quantum Computing

  • Decision diagrams can compactly represent quantum functionality in many cases, but remain exponential in the worst case.State vectors can be handled as a special case of matrices.Source: B. Decision Diagrams for Quantum… · p. 3
  • Each matrix split on the topmost qubit creates four submatrices and a corresponding decision-diagram node with four successors.Recursively splitting until scalar entries remain allows identical submatrices to share a node.Source: B. Decision Diagrams for Quantum… · p. 3
  • The identity matrix’s decision diagram has exactly n nodes; for three qubits, the figure shows that compact structure.Its diagonal submatrices recur identically, while off-diagonal submatrices contain only zeros.Source: B. Decision Diagrams for Quantum… · p. 3, Figure 3 · p. 3
  • Edge weights unify submatrices differing by a common factor, while matrix multiplication recursively combines corresponding subexpressions.For the illustrated matrix U, seven nodes capture the whole functionality by exploiting edge weights and redundancy.Source: B. Decision Diagrams for Quantum… · p. 4

III. MOTIVATION

Quantum algorithms pass through design steps that alter their circuit descriptions, motivating checks that the resulting circuits retain the desired functionality.

III. MOTIVATION

  • Decomposition, mapping, and optimization are among the steps used to realize a quantum algorithm on a device, and the resulting functionality must remain unchanged.Equivalence checking is motivated by the need to verify this preservation.Source: §III · p. 4
  • Canonicity of the described decision-diagram representation assumes a fixed variable order and a suitable normalization scheme.One example normalization divides by the leftmost non-zero edge weight.Source: §III · p. 4
  • Figure 5 identifies G′ as an alternative circuit realization.Source: Figure 5 · p. 4

A. The Quantum Circuit Equivalence Checking Problem

The equivalence-checking problem asks whether two quantum circuits implement the same function, allowing a global phase difference. Constructing complete system matrices makes the comparison computationally demanding.

A. The Quantum Circuit Equivalence Checking Problem

  • Circuit equivalence means that two circuits implement the same function, or that a counterexample can demonstrate their non-equivalence.The circuits’ system matrices may differ by a global phase and still count as equivalent.Source: A. The Quantum Circuit Equivalence… · p. 4
  • A computational basis state |i⟩ is a counterexample when the corresponding system-matrix columns differ by more than a global phase.The example identifies |4⟩ as a counterexample for circuits whose matrices differ in column four.Source: A. The Quantum Circuit Equivalence… · pp. 4–5
  • Constructing and comparing full system matrices requires matrix multiplication over exponentially sized objects, and circuit equivalence checking is QMA-complete.The matrices are built from the individual gate descriptions.Source: A. The Quantum Circuit Equivalence… · p. 5

B. Related Work

Decision diagrams remain the state of the art for quantum-circuit equivalence checking, but full representations, intermediate growth, and counterexample extraction can make the approach costly.

B. Related Work

  • Decision-diagram approaches remain the state of the art because they compactly represent and efficiently manipulate circuit functionality, with equivalence checked by comparing canonical root edges.When circuits differ only by a global phase, the associated weights are also compared.Source: B. Related Work · p. 5
  • Earlier approaches based on rewriting can be incomplete or require exponential enumeration, while SAT approaches must encode infinitely many quantum states.The cited SAT encoding addressed this only partially and did not support entanglement.Source: B. Related Work · p. 5
  • Full circuit representations may be exponential, and intermediate diagrams can grow substantially beyond the final representation.The example’s final diagram has seven nodes, while construction requires up to nine; realistic circuits can have differences of several orders of magnitude.Source: B. Related Work · p. 5
  • Counterexample extraction from non-equivalent diagrams requires determining their difference through inversion and multiplication, potentially expensive operations on large representations.A path containing a node that does not resemble the identity can provide a counterexample, as illustrated by Figure 7.Source: B. Related Work · p. 5, Figure 7 · p. 6

IV. GENERAL IDEAS

The paper treats quantum-specific properties as opportunities for faster equivalence checking, rather than merely as complications to support.

IV. GENERAL IDEAS

  • The proposed ideas use characteristics unique to quantum computing to address shortcomings in existing equivalence-checking approaches.The section sketches these ideas before later sections present dedicated schemes and flows.Source: §IV · p. 6
  • The authors frame superposition and entanglement as properties that can offer verification potential, despite making quantum circuits seem harder to verify.Source: §IV · p. 6
  • The paper reports that equivalence checking can be dramatically faster, in many cases using just one simulation run.Source: §IV · p. 6

A. Exploiting Reversibility

Reversibility lets equivalence checking build toward the identity by interleaving gates from a circuit and inverse gates from its counterpart. This can keep intermediate decision diagrams small and make counterexamples easier to obtain.

A. Exploiting Reversibility

  • Quantum operations are reversible: a circuit’s inverse is formed by reversing gate order and taking each operation’s conjugate transpose.For equivalent circuits, composing one with the inverse of the other yields the identity.Source: A. Exploiting Reversibility · p. 6
  • The identity has a linear-size decision diagram, but naively concatenating circuits still constructs one circuit’s full diagram first.In Example 12, the first four operations effectively construct G’s diagram before the concatenation reaches the identity.Source: A. Exploiting Reversibility · p. 6
  • Associativity allows gates from G and inverted gates from G′ to be applied from opposite sides of the identity, with a suitable order frequently returning intermediate diagrams toward the identity.This strategy is intended to keep intermediate decision diagrams small.Source: A. Exploiting Reversibility · p. 6
  • When circuits are not equivalent, the resulting difference diagram can represent their difference and provide counterexamples without separate inversion and multiplication.The authors describe counterexamples as obtainable almost “for free” compared with the state-of-the-art procedure.Source: A. Exploiting Reversibility · p. 6
  • Choosing when to apply gates from each circuit is not obvious, so the paper presents and evaluates strategies for that choice.Source: A. Exploiting Reversibility · p. 7

B. The Power of Simulation

Reversibility makes simulation a useful way to find differences between quantum circuits: individual columns can reveal non-equivalence without constructing full system matrices. The proposed flow screens with simulations first, then proves likely equivalence if no counterexample is found.

B. The Power of Simulation

  • Random-input simulation is less effective for classical circuits because masking and information loss can hide differences, as when x ∧ 0 masks a difference in x.Classical verification therefore uses constraint-based stimulus generation and fuzzing.Source: B. The Power of Simulation · p. 7
  • Reversible quantum operations reduce masking, so a difference may affect system matrices and be found by comparing only a few columns rather than constructing both full matrices.If any compared columns differ, the circuits are non-equivalent.Source: B. The Power of Simulation · p. 7
  • Simulating a circuit on a computational-basis input produces one matrix column through matrix-vector multiplications, an exponentially easier task than constructing the full system matrix.Simulation complexity nevertheless remains exponential in the number of qubits.Source: B. The Power of Simulation · p. 7
  • The proposed flow first runs simulations to seek a counterexample, then proves the highly probable equivalence if none is found.A limited number of arbitrary basis-state simulations does not guarantee that a difference will be detected.Source: B. The Power of Simulation · p. 7

A. Naive Strategy

Three gate-ordering strategies aim to keep intermediate decision diagrams small. In the illustrated example, all outperform the state-of-the-art approach, while each strategy has distinct trade-offs.

A. Naive Strategy

  • Alternating corresponding gates and inverses works well for similar circuits, but structural or gate-count imbalance can leave many gates applied afterward.For Example 10, the naive strategy peaks at 7 nodes and averages 4.43, versus the state-of-the-art approach’s maximum of 9 and average of 5.95.Source: A. Naive Strategy · pp. 7–8

B. Proportional Strategy

  • The proportional strategy applies gates according to the circuits’ gate-count ratio, yielding a 4.33 average node count and near-optimal performance in Example 10.The example’s gate-count ratio is 4:16, or 1:4; the maximum intermediate diagram size is 7 nodes.Source: B. Proportional Strategy · p. 8

C. Look-ahead Strategy

  • Look-ahead chooses the gate application that yields the smaller intermediate diagram, potentially doubling multiplications; in Example 10 it averages 4.24 nodes and peaks at 7.It evaluates both alternatives before choosing a path.Source: C. Look-ahead Strategy · p. 8
  • All three strategies produce smaller maximum and average decision diagrams than the state-of-the-art approach in the illustrated example.Figure 9 shows the node counts for circuits G and G′ from Example 10.Source: C. Look-ahead Strategy · p. 8, Figure 9 · p. 8

VI. INVESTIGATING THE POWER OF SIMULATION

The analysis examines how differences between circuit matrices affect computational-basis-state simulations. It concludes that a few such simulations can often reveal non-equivalence, though this is not guaranteed.

Difference and basis-state simulation

  • The matrix difference D = U†U′ lets the authors test basis-state output fidelity; any Fi not approximately 1 establishes non-equivalence.For a basis state |i⟩, the comparison is between the outputs of both circuits from that input.Source: §VI · pp. 8–9

Single-qubit differences

  • A single-qubit operation in the difference circuit affects all columns, so any computational-basis-state simulation can detect the error in this case.This is the single-operation case considered in Example 19.Source: §VI · p. 9

Controlled-operation differences

  • A gate controlled by the remaining n − 1 qubits affects only the last two columns, so at most two basis states may reveal the difference.This is the worst-case counterexample coverage described for Example 20.Source: §VI · p. 9

Combined differences

  • With c controls, operations generally differ in 2^(n−c) columns; products usually retain the larger operand’s number of differing columns unless cancellations occur.In the two-qubit example, the Hadamard and CNOT differences combine to affect all columns.Source: §VI · p. 9

Practical scope and caveat

  • Typical single-qubit and CNOT or SWAP design errors can often be detected with few arbitrary computational-basis simulations, but this is not guaranteed.If a few simulations find no counterexample, the paper presents equivalence only as a highly probable estimate.Source: §VI · p. 9

VII. RESULTING ADVANCED EQUIVALENCE CHECKING FLOW

The flow first samples randomly chosen computational basis states, then uses a reversibility-based equivalence routine if sampling finds no difference. It can conclude non-equivalence or equivalence, or time out with an inconclusive indication.

A. Resulting Flow

  • The flow runs r ≪ 2^n random computational-basis simulations first; a differing output proves non-equivalence, while no difference triggers the equivalence routine.Figure 10 depicts the proposed flow.Source: A. Resulting Flow · p. 9, Figure 10 · p. 10
  • The routine can conclude non-equivalence or equivalence after simulation; the earlier runs add negligible overhead when it confirms equivalence.The full functionality is complexitywise equivalent to simulating all 2^n computational basis states, whereas r is much smaller.Source: A. Resulting Flow · p. 10
  • If simulations find no counterexample and the routine cannot finish within the resource limit, the flow times out without guaranteeing equivalence.The absence of a sampled counterexample is an indication that the circuits might be equivalent, not a proof.Source: A. Resulting Flow · p. 10

B. Discussion

The flow combines simulation with an identity-oriented circuit comparison, and experiments report faster equivalence checking with little simulation overhead. The discussion also describes when simulation may be costly and how the comparison strategies could be adapted or run alongside it.

B. Discussion

  • The flow simulates first and applies the G·I·G′ strategy if results are inconclusive, providing a likely-equivalence indication even when a complete proof exceeds available resources.Source: B. Discussion · p. 10
  • When state-vector simulation is too resource-intensive, the G·I·G′ scheme remains an alternative if a strategy keeps intermediate decision diagrams close to identity; designing circuit-origin-specific strategies remains future work.Source: B. Discussion · p. 10
  • Uniformly random computational basis states as simulation inputs promise high success rates for quantum-circuit checking, unlike classical simulation approaches that use constrained stimuli or fuzzing.Source: B. Discussion · p. 10
  • Valid circuit optimizations that lower gate count may improve performance, and simulation and equivalence checking can instead run in parallel when resources permit, stopping remaining work after a decisive result.Source: B. Discussion · p. 10

A. Setup

  • The evaluation uses benchmark pairs comprising high-level circuits and compiled or mapped versions, compares against the technique in, and imposes a 3,600-second timeout per run.Runs used a 4 GHz Amazon EC2 z1d instance with at least 32 GB per job.Source: A. Setup · p. 11

B. Showing Equivalence

  • In most equivalent-circuit cases, dedicated strategies cut checking time to half or a third of the state-of-the-art runtime; simulations add negligible overhead and can indicate equivalence in timeout cases.The proportional strategy sometimes achieves orders-of-magnitude improvement.Source: B. Showing Equivalence · p. 11

C. Showing Non-equivalence

For deliberately subtle non-equivalences, the proposed flow often detects differences through simulation alone, while repeated simulations show high success probabilities. The paper concludes that reversibility-based comparison and simulation can accelerate checking, with tailored strategies and their application to compilation flows remaining relevant directions.

C. Showing Non-equivalence

  • For all tested non-equivalent benchmarks, the proposed method finds the difference in seconds or less; simulation alone suffices in most cases, except mlp4_245 with one removed gate.That exception requires an equivalence-checking routine, which the G·I·G′ strategies complete in feasible runtime.Source: C. Showing Non-equivalence · p. 11
  • With three gates removed, no evaluated instance masked the difference from simulation; most were detected in one run and none required more than three.For one-gate removals, masking occurred only for mlp4_245.Source: C. Showing Non-equivalence · p. 11

D. The Power of Simulation

  • Across 100 generated instances per benchmark and up to 16 simulations, the average success probability was 85.2% for one-gate removals and close to 100% when three gates were removed.Source: D. The Power of Simulation · pp. 11–12

IX. CONCLUSIONS

  • For equivalent circuits, a complete proof can be dramatically accelerated when a strategy keeps G·I·G′ close to identity.Source: §IX · p. 12
  • The authors report checking equivalence or non-equivalence magnitudes faster than before, often using simulation alone, and say simulations can indicate equivalence even for minor differences.Source: §IX · p. 12
  • Information about how G was compiled into G′ may guide identity-preserving strategies; first studies have examined verification of IBM's Qiskit compilation flow in.The paper says this could eventually make verification of sophisticated design flows feasible in general.Source: §IX · p. 12
Loading 2004.08420v2…