PaperlayerView exact revision on arXiv

Source-linked AI summary

Towards Large-scale Functional Verification of Universal Quantum Circuits

Matthew Amy

arXiv:1805.06908v2quant-phcs.LO

TL;DR

Quantum-circuit verification needs specifications that are clear and verifiable, as circuit and matrix presentations can be difficult for humans to write and understand. The paper uses path-sums and rewrite rules to specify and verify circuits, with polynomial-time equivalence checking for Clifford circuits and experiments on circuits and algorithms up to 200 qubits.

  • Problem

    Circuit and matrix presentations can be difficult for humans to write and understand, complicating functional verification against a specification.

    Source: §1 · p. 1

  • Method

    The paper represents unitary quantum circuits as path-sums and reduces those sums with rewrite rules for functional verification.

    Source: §1 · p. 2, §3.2 · p. 8

  • Results

    The reduction system gives a polynomial-time equivalence-checking algorithm for Clifford circuits and was used to verify optimized Clifford+T circuits and quantum algorithms up to 200 qubits.

    Source: §1 · p. 2

  • Takeaways & Limitations

    Path-sums provide symbolic polynomial representations that support efficient representation and functional verification of large quantum circuits against formal mathematical specifications.

    Source: §6 · p. 16

    At higher Clifford-hierarchy levels, phase-polynomial degree can become prohibitively large; even Clifford+T path-sums require space cubic in circuit volume, making some larger circuits difficult to verify.

    Source: §2.2 · p. 7

Abstract

from arXiv · show

We introduce a framework for the formal specification and verification of quantum circuits based on the Feynman path integral. Our formalism, built around exponential sums of polynomial functions, provides a structured and natural way of specifying quantum operations, particularly for quantum implementations of classical functions. Verification of circuits over all levels of the Clifford hierarchy with respect to either a specification or reference circuit is enabled by a novel rewrite system for exponential sums with free variables. Our algorithm is further shown to give a polynomial-time decision procedure for checking the equivalence of Clifford group circuits. We evaluate our methods by performing automated verification of optimized Clifford+T circuits with up to 100 qubits and thousands of T gates, as well as the functional verification of quantum algorithms using hundreds of qubits. Our experiments culminate in the automated verification of the Hidden Shift algorithm for a class of Boolean functions in a fraction of the time it has taken recent algorithms to simulate.

1 Introduction

The paper addresses the difficulty of specifying quantum programs clearly and scaling their verification, proposing path-sums as a formal specification and verification framework. Its rewrite system gives polynomial-time equivalence checking for Clifford circuits and supports experiments on circuits and algorithms up to 200 qubits.

1 Introduction

  • Verification must address human-readable specifications and scale; this matters because compiler-varying quantum resource analyses inform real security policies.Circuit, diagram, and matrix specifications can be difficult for people to write and understand, while some matrix presentations require exponential space or remain abstract.Source: §1 · p. 1
  • Path-sums represent quantum operators as exponential sums over Boolean path variables and let classical functions directly specify quantum operations.The framework uses a Feynman path-integral approach and is intended for unitary circuits over Clifford gates extended with Z-axis rotations from the Clifford hierarchy.Source: §1 · p. 2
  • Polynomial-time equivalence checking for Clifford circuits follows from a complete path-sum reduction system, which is also used to verify optimized Clifford+T circuits and quantum algorithms up to 200 qubits.The path-sum interpretation is efficiently computable and compact for Clifford+Rk circuits for any fixed k.Source: §1 · p. 2
  • The framework assumes a strictly unitary model without measurements, while allowing qubit initialization as partial isometries.It places the Pauli group, Clifford group, and Clifford+T in hierarchy levels C1, C2, and C3, respectively.Source: §1 · p. 2
  • The formalism represents pseudo-Boolean functions with polynomial forms, using dyadic fractions for Rk phases and to represent the quantum Fourier transform precisely.Source: §1 · p. 2

2 The path-sum framework

The path-sum framework represents quantum operators through discrete paths, polynomial phases, and output functions. Its compositions provide a circuit semantics that supports equivalence reasoning, with efficiency and representation limits depending on the circuit and phase form.

2 The path-sum framework

  • A path-sum represents an operator with an input signature, phase polynomial, Boolean output signature, and internal path variables.The amplitude is summed over possible paths; path-sums can also specify quantum implementations of classical functions.Source: §2 · p. 3
  • Well-formed path-sums denote partial isometries, but checking well-formedness remains open and matters in practice for directly written specifications.The verification methods also work when a path-sum is not guaranteed to be well-formed.Source: §2 · p. 4

2.1 Compositions of path-sums

  • Sequential composition substitutes one path-sum’s outputs into the next inputs; compatible signatures are required to avoid unintended post-selection.For partial-isometry cases, a variable output composed with a constant input can effectively post-select on that variable’s value.Source: §2.1 · pp. 4–5
  • Path-sums make structurally equivalent circuits strictly equal without explicit structural-law management and capture semantic equivalences such as long-distance phase-gate cancellation.The framework also provides an intermediary representation between circuit diagrams and matrix representations.Source: §2.1 · pp. 5–6

2.2 Path-sums as a circuit semantics

  • Clifford+Rk path-sums have phase-polynomial degree at most k, and their circuit interpretations are computable in polynomial time with size polynomial in circuit volume.The interpretation preserves the circuit operator.Source: §2.2 · pp. 6–7
  • At higher hierarchy levels, phase-polynomial degree can become prohibitively large; Fourier expansion uses linear space for any k but complicates verification because it may not be unique modulo integers.For standard Clifford+T circuits, the path-sum requires space cubic in circuit volume, making some larger circuits difficult to verify.Source: §2.2 · p. 7

3 A calculus for path-sums

The path-sum calculus checks circuit equivalence by reducing path variables in a miter to a normal form. Its rewrite rules encode recognizable interference patterns and verify functional specifications through examples.

3.1 Overview

  • For the identity circuit HH, the two branches of an internal path interfere constructively or destructively according to the input and output bits.The reductions apply when the internal variable appears with Boolean-subgroup coefficients, and are used when the restricted sum can be reified by solving a Boolean equation.Source: §3.1 · p. 8
  • The rules target recognizable interference patterns; [HH] suffices for the vast majority of path-sum reductions.The rule set also includes [ω] and [Case]; [Elim] simplifies [HH] and appears in some verification contexts.Source: §3.2 · pp. 8–9, §3.1 · p. 8

3.2 Reduction rules

  • Each rewrite reduces path variables, yielding an irreducible path-sum in polynomial time.The rewrite sequence is linear in the number of path variables.Source: §3 · p. 7, §3.2 · p. 9

3.3 Examples

  • The calculus verifies the Toffoli implementation against its functional specification and confirms that a controlled-T implementation leaves its ancilla clean.The Toffoli specification maps |x1x2x3⟩ to |x1x2(x3 ⊕ x1x2)⟩.Source: §3.3 · pp. 9–10

4 Completeness

The completeness results combine path-sum restrictions and non-equivalence tests with reductions, establishing polynomial-time equivalence checking for Clifford circuits while acknowledging that the general rewrite system is incomplete.

4 Completeness

  • The rewrite system is incomplete because normal forms need not be unique; explicit expansion can complete verification, but is generally unnecessary in practice.Together with additional observations, the reductions prove equivalence or non-equivalence for most circuits.Source: §4 · pp. 10–11

4.1 Isometry restrictions

  • For well-formed, isometric path-sums, restricting to outputs f(x,y)=x preserves identity testing; reifiable substitutions can remove up to n path variables.Restrictions that cannot be reified are ignored.Source: §4.1 · p. 11

4.2 Non-equivalence

  • A nonzero integer-valued phase polynomial Q with no path variables certifies that the path-sum is not the identity.The criterion supports a variant of [HH] for proving non-equivalence.Source: §4.2 · pp. 11–12

4.3 Clifford completeness

  • Clifford-circuit equivalence to the identity is decidable in time polynomial in circuit space-time volume.The proof uses linearity of the output function and reductions that preserve phase-polynomial order at most 2.Source: §4.3 · p. 12

5 Case studies

The case studies evaluate path-sum verification on optimized circuits and formally specified quantum algorithms. They report large verified instances, including hidden-shift circuits checked faster than recent simulation methods.

5 Case studies

  • The framework was implemented in the open-source FEYNMAN Haskell library, with experiments run on a quad-core Intel Core i7 system with 8 GB RAM.The verification benchmarks could be run from the command line.Source: §5 · p. 13

5.1 Translation validation

  • All but 3 optimized benchmarks were verified; the largest completed, GF(2^32) with 96 bits and over 25,000 gates, finished in under 10 minutes.The remaining 3 ran out of memory under a 6 GB limit.Source: §5.1 · p. 13, Table 1 · p. 14
  • After randomly removing one gate, all but 3 benchmarks were proven non-equivalent, with negative checks taking about as long as positive checks.The three exceptions were among the benchmarks that ran out of memory.Source: §5.1 · p. 13

5.2 Verifying quantum algorithms

  • The algorithm case studies checked implementations, including versions with errors, directly against path-sum specifications; Table 2 reports the results.The experiments also included reversible-function implementations such as generalized Toffoli and addition.Source: §5.2 · p. 13, Table 2 · p. 15
  • Both generalized Toffoli implementations were verified up to 100 bits in seconds, including the standard and Maslov decompositions.The decompositions use different ancilla counts and gate constructions.Source: §5.2 · p. 13
  • The ripple-carry adder specification was verified for sizes up to 16 bits within a minute, while its bitwise expansion made 32-bit cases difficult.The circuit uses 5n − 1 bits of space and 4(n − 1) Toffoli gates.Source: §5.2 · p. 15
  • The QFT implementation was verified up to 31 bits in 16 seconds; larger instances exceeded the implementation’s dyadic-arithmetic handling.The authors identify integer overflow as the limit encountered at 31 bits.Source: §5.2 · p. 15
  • Seconds versus hours: after finding a bug in its first implementation, the framework verified both hidden-shift versions beyond the sizes simulated in [10].One version uses a concrete shift and the other supplies the shift symbolically in a quantum register.Source: §5.2 · p. 16

6 Conclusion

The conclusion presents path-sums as a symbolic framework for representing quantum operations and verifying circuits. It characterizes the work as preliminary and identifies broader program support and stronger verification tools as future directions.

6 Conclusion

  • Path-sums represent partial isometries as discrete path sums, with symbolic polynomial representations for Clifford+Rk circuits.These representations support efficient computation of a circuit’s action on an arbitrary basis state.Source: §6 · p. 16
  • Rewrite rules reduce path-sums for functional verification, and the experiments demonstrate the framework on large circuits and formal specifications of quantum algorithms.Source: §6 · p. 16
  • The authors call the work preliminary and propose broader quantum-program support, concrete syntax for verified libraries, more efficient path-sum methods, and interactive proof-assistant support.They also identify decision diagrams and other tools as possible ways to complete verification when reductions stop.Source: §6 · pp. 16–17

A Correctness of rewrite rules

The appendix establishes correctness of the rewrite rules by direct calculation, including case analyses based on a Boolean polynomial’s parity.

A Correctness of rewrite rules

B Reduction examples

The appendix illustrates rewrite-rule reductions on circuit identities, including an SH-based example and a one-bit full adder.

B Reduction examples

  • The reduction rules are illustrated through further examples of proofs of circuit identities.Source: B Reduction examples · p. 20
  • The example using the [ω] rule reduces the circuit (SH)^3 to the ω constant.Source: B Reduction examples · p. 20
  • The one-bit full adder is specified as a reversible path-sum, and its Clifford+T implementation uses Reed–Muller decoding to reduce T gates versus a standard two-Toffoli implementation.The appendix then shows how to verify that circuit against the specification.Source: B Reduction examples · p. 21
Loading 1805.06908v2…