Equivalence Checking of Parameterized Quantum Circuits Verifying the Compilation of Variational Quantum Algorithms Tom Peham

2025-05-06 0 0 663.26KB 7 页 10玖币

侵权投诉

Equivalence Checking of Parameterized antum Circuits

Verifying the Compilation of Variational antum Algorithms

Tom Peham

Chair for Design Automation,

Technical University of Munich,

Germany

tom.peham@tum.de

Lukas Burgholzer

Institute for Integrated Circuits,

Johannes Kepler University Linz,

Austria

lukas.burgolzer@jku.at

Robert Wille

Chair for Design Automation,

Technical University of Munich,

Germany

Software Competence Center

Hagenberg GmbH, Austria

robert.wille@tum.de

ABSTRACT

Variational quantum algorithms have been introduced as a

promising class of quantum-classical hybrid algorithms that can

already be used with the noisy quantum computing hardware

available today by employing parameterized quantum circuits.

Considering the

non-trivial

nature of quantum circuit compilation

and the subtleties of quantum computing, it is essential to verify

that these parameterized circuits have been compiled correctly.

Established equivalence checking procedures that handle

parameter-free

circuits already exist. However, no methodology

capable of handling circuits with parameters has been proposed

yet. This work lls this gap by showing that verifying the

equivalence of parameterized circuits can be achieved in a purely

symbolic fashion using an equivalence checking approach based

on the

ZX-calculus

. At the same time, proofs of inequality can be

eciently obtained with conventional methods by taking

advantage of the degrees of freedom inherent to parameterized

circuits. We implemented the corresponding methods and proved

that the resulting methodology is complete. Experimental

evaluations (using the entire parametric ansatz circuit library

provided by Qiskit as benchmarks) demonstrate the ecacy of the

proposed approach. The implementation is open source and

publicly available as part of the equivalence checking tool

QCEC (

https://github.com/cda-tum/qcec

) which is part of the

Munich Quantum Toolkit (MQT).

1 INTRODUCTION

Quantum computers promise a computational advantage over

classical computers for certain problems [1]–[3]. Far-term

quantum algorithms such as Shor’s algorithm for integer

factorization [4] and Grover search [5] require robust, large-scale

error correction schemes to retrieve a meaningful result from their

execution [6]. Noisy Intermediate Scale Quantum (NISQ)

computers [7], the ones that are available today, are not able to

implement this error correction yet. Due to the high gate error

rates and short coherence times of NISQ devices, the depth of any

quantum circuit to be run on them is inherently limited.

Variational Quantum Algorithms [8] have been proposed to

achieve a computational advantage despite these limitations.

These algorithms use quantum programs as subroutines in a

classical optimization routine. The optimization loop iteratively

improves the parameters of a quantum circuit ansatz, which, in

turn, is used to estimate some desired quantity, such as the

expectation value of some observable. This general variational

framework has been applied to solve problems in chemistry [9],

nance [10], discrete optimization [11], and more.

But, before running an ansatz on a target device, a compilation

step has to be performed where the circuit is translated into a

natively supported gate-set and routed such that it conforms to the

device’s topological constraints—a costly and non-trivial

procedure [12]–[15]. To avoid the necessity of recompiling a

quantum circuit in each iteration step of a variational algorithm,

the circuit is usually compiled once in parameterized form in

which the parameters tuned by the classical optimization routine

are not bound to specic values. This compiled parameterized

circuit can then be used in the optimization loop without having to

perform all compilation steps over and over again.

The increasing use of parameterized circuits in the development

of quantum algorithms has also brought along the need for

verifying that these circuits have been compiled correctly.

Established equivalence checking methods such as proposed

in [16]–[20] are able to prove that a compiled circuit still adheres

to its specication after compilation. However, these approaches

cannot handle parameterized circuits. The only way to verify the

compilation of variational quantum algorithms with these

methods is to check the equivalence of the original and the

instantiated compiled ansatz in each iteration. Since equivalence

checking is a hard problem for even one instance—it is, in fact, a

QMA-complete problem [21]—solving it over and over again is

hardly a feasible approach.

In this work, we propose, for the rst time, a methodology to

solve the equivalence checking problem for parameterized quantum

circuits. The proposed, multi-stage method starts out by using an

approach based on the

ZX-calculus

[22], [23] to try and prove the

equivalence of both parameterized circuits. If this does not succeed,

parameters of the circuits are instantiated, and a conventional,

complete equivalence checker is employed. In order to make this

check as easy as possible, we derive an instantiation scheme that

allows simplifying most of the parameterized gates from the circuits.

Furthermore, we prove this yields a complete equivalence checking

procedure for parameterized quantum circuits.

The resulting methodology has been evaluated on the entire

Qiskit [24] parameterized circuit library, which shows that the

proposed approach can decide the equivalence of variational ansatz

circuits for a high number of qubits and larger circuit depth than

is even practically executable today. The instantiation scheme, in

particular, allows for checking instances that would be infeasible

to handle otherwise—reducing the equivalence checking runtime

arXiv:2210.12166v1 [quant-ph] 21 Oct 2022

Tom Peham, Lukas Burgholzer, and Robert Wille

𝑍𝑍 (𝜃)

𝑍𝑍 (𝜃)𝑍 𝑍 (𝜃)

𝑞2:𝐻𝑅𝑋(𝛾)

𝑞1:𝐻𝑅𝑋(𝛾)

𝑞0:𝐻𝑅𝑋(𝛾)

(a) Parametric quantum circuit

𝑄0

𝑄1

𝑄2

𝑄3

𝑄4

𝑞2↦→

𝑞1↦→

𝑞0↦→

Architecture

𝐻𝑅𝑍(𝜃)𝐻𝑅𝑍(𝛾)𝐻

𝐻𝑅𝑍(𝜃)𝑅𝑍(𝜃)𝐻𝑅𝑍(𝛾)𝐻

𝐻 𝐻 𝑅𝑍(𝛾)𝐻

(b) Compiled circuit

Figure 1: Compiling a parametric circuit to a device

by orders of magnitude in many cases. While this method has

been developed with variational algorithms in mind, the approach

is much more general and works for any application that uses

parameterized quantum circuits. The implementation is open source

and publicly available at https://github.com/cda-tum/qcec.

The remainder of this paper is structured as follows. To keep

this work self-contained, Section 2 establishes the necessary

background on quantum computing and variational quantum

algorithms. Section 3 motivates the problem of equivalence

checking of parameterized quantum circuits, discussing the

shortcomings of existing equivalence checking approaches in the

parameterized case and proposes a complete equivalence checking

ow for parameterized circuits. After elaborating the details of the

proposed methods in Section 4, results obtained from the

experimental evaluations are provided in Section 5. Finally,

Section 6 concludes this paper.

2 BACKGROUND

This section briey covers the necessary background to keep this

work self-contained as well as the relevant related work from the

literature. For an in-depth introduction, see [25].

2.1 Quantum Computing

In quantum computing, information is represented in the form of

quantum bits (short qubits) which, contrary to the classical world,

cannot only be in the basis states

|0⟩=1

0

and

|1⟩=0

1

, but also

in a superposition

𝛼0|0⟩+𝛼1|1⟩with 𝛼0, 𝛼1∈Cand |𝛼0|2+ |𝛼1|2=1.

Multi-qubit systems are then described as superpositions of basis

states in the product Hilbert space

(C2)⊗𝑛

. All transformations of

qubits have to be unitary transformations, i.e., linear

transformations

𝑈

C2𝑛→C2𝑛

such that

𝑈 𝑈 †=𝐼

, where

𝑈†

the conjugate transpose of

𝑈

and

𝐼

is the identity transformation.

Quantum computations are typically described as quantum circuits

which are diagrams composed of wires (representing qubits) as

well as boxes and interconnections on these wires called gates

(representing transformations of qubits). If the gate set is

expressive enough, any quantum computation can be written as a

quantum circuit using only gates from this set.

Example 1. The Hadamard gate

𝐻=1

√21 1

1−1

is one of the

fundamental single-qubit quantum gates because it puts a qubit in

a basis state

|0⟩

|1⟩

into an equal superposition of these basis

states. The two-qubit controlled not (

CNOT

) gate (which is natively

supported on many quantum computers) ips the second qubit if the

rst qubit is in the |1⟩state and leaves it unchanged otherwise.

Although quantum algorithms are commonly described via

quantum circuits across dierent abstraction levels, their initial

description usually contains high-level gates and concepts that are

not directly supported by actual quantum computers. In fact,

existing quantum computers only support a limited gate library

and frequently have limited connectivity between the qubits which

means that not every pair of qubits on a quantum hardware can

interact in a two-qubit gate. Hence, in order to run a quantum

algorithm on an actual device, a compilation step has to be

performed which consists of synthesizing the gates of a quantum

circuit to the supported gate set, mapping logical to physical

qubits, inserting

SWAP

gates such that all two-qubit gates can be

properly executed, and applying optimizations to reduce the size

of the circuit [12]–[15].

Example 2. Assume the circuit in Fig. 1a shall be compiled to

an architecture which supports a gate library consisting of

CNOT

𝑅𝑍

, and

𝐻

gates, and has limited two-qubit interactions as shown on

the left-hand side of Fig. 1b. Then, Fig. 1b shows a possible way of

compiling this circuit. Because the

gate (which is synthesized to

two

CNOT

gates and an

𝑅𝑍

gate) between physical qubit

𝑄2

and

𝑄0

cannot be executed directly, a

SWAP

gate has to be introduced into the

circuit. As shown above the circuit, this

SWAP

gate is synthesized as a

sequence of three

CNOT

gates. One of these

CNOT

s can be cancelled

with the

CNOT

of the synthesized

gate, simplifying the circuit in

the process.

2.2 Variational Quantum Algorithms

Even with sophisticated compilation schemes, the noisy nature of

state-of-the-art quantum computing devices makes it impossible to

run far-term quantum algorithms such as Shor’s algorithm [4],

which require a substantial amount of gates. As every gate

potentially introduces an error into the system and, due to the

short coherence times of qubits, the maximal depth of quantum

circuits is limited on NISQ devices [7].

Variational Quantum Algorithms have been proposed to allow

for expressing more functionality even with low-depth circuits.

The quantum computations in variational algorithms are

expressed via ansatz circuits. These are shallow parameterized

quantum circuits

𝐺(𝜃)

with a parameter vector

𝜃=(𝜃0,··· , 𝜃𝑝−1)

Each assignment

𝜎

{𝜃𝑖|

≤𝑖<𝑛} → (−𝜋, 𝜋 ]𝑛

yields an

instantiated circuit

𝐺(𝜎(𝜃))

. The goal of a variational algorithm is

to successively adapt the circuit parameters using a classical

optimization routine (e.g., gradient descent) so that the resulting

circuit can be used to estimate some desired quantity, i.e, the

ground state of a molecule. By using classical computing,

variational ansatz circuits can be deliberately kept shallow.

However, shallow circuits are generally less expressive then more

文档加载中……请稍候！
如果长时间未打开，您也可以点击刷新试试。

下载文档到电脑，查找使用更方便

10 玖币 0人已下载

立即下载

摘要：

EquivalenceCheckingofParameterizedQuantumCircuitsVerifyingtheCompilationofVariationalQuantumAlgorithmsTomPehamChairforDesignAutomation,TechnicalUniversityofMunich,Germanytom.peham@tum.deLukasBurgholzerInstituteforIntegratedCircuits,JohannesKeplerUniversityLinz,Austrialukas.burgolzer@jku.atRobertWill...

展开>> 收起<<

Equivalence Checking of Parameterized Quantum Circuits Verifying the Compilation of Variational Quantum Algorithms Tom Peham.pdf

共7页,预览2页

还剩页未读，继续阅读

声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！

Equivalence Checking of Parameterized Quantum Circuits Verifying the Compilation of Variational Quantum Algorithms Tom Peham

相关推荐

开通VIP享超值会员特权

作者详情

相关内容

热门标签

举报选择: