Das Kapitel geht der entscheidenden Rolle der Quantenschaltkreissimulation und -verifikation bei der Entwicklung von Quantenalgorithmen nach. Er hebt die Mängel aktueller Simulationswerkzeuge hervor, die entweder umfassende Zustandsinformationen liefern, die zu Skalierungsproblemen führen, oder sich auf Stichproben stützen, was zu Präzisionsverlusten führt. Das Kapitel stellt eine erweiterte Version des SliQSim-Simulators vor, der boolesche Datenstrukturen nutzt, um exakte und effiziente Abfragen von Wahrscheinlichkeiten und Erwartungswerten für anpassbare Quantenzustände zu ermöglichen. Diese Weiterentwicklung ermöglicht es den Anwendern, Simulationsergebnisse aus verschiedenen Perspektiven zu betrachten und die Funktionalität von Quantenalgorithmen mit beispielloser Genauigkeit zu überprüfen. Die Architektur des Tools wird gründlich erklärt und zeigt, wie es Gate-Anwendungen und Immobilienabfragen effizient handhabt. Das Kapitel stellt außerdem mehrere Beispiele und Fallstudien vor, darunter Anwendungen in Grovers und Simons Algorithmen und das N-I-Äquivalenz-Boolesche Matching-Problem. Diese Demonstrationen unterstreichen die Fähigkeit des Werkzeugs, subtile Fehler zu erkennen und präzise Ergebnisse zu liefern, was es zu einem wertvollen Vorteil für die Analyse und Verifizierung von Quantenschaltungen macht.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
SliQSim, originally developed as the first exact quantum circuit simulator, is extended in this paper to provide capabilities for the analysis and verification of quantum states. It provides an interface for users to specify interested quantum states for querying the exact probability or expectation value of a user-defined property. Case studies on three quantum algorithms show the unique capability of SliQSim benefiting exact quantum circuit analysis and verification, beyond the support by other tools.
1 Introduction
Quantum computation shows promise in its advantage of solving certain important problems, which are classically hard. Simulation and verification of quantum circuits play a crucial role in quantum program compilation, ensuring quantum algorithms are correctly executed. To date, many classical simulators have been proposed to efficiently simulate given quantum circuits, such as decision-diagram-based SliQSim [19], DDSim [25], Quasimodo [17], and MEDUSA [5], ZX-calculus-based QuiZX [12], tensor-network-based TensorCircuit [24], and model-counting-based [14] methods. To the best of our knowledge, none of the existing simulators allow users to query the probability for a customizable set of quantum states.
Current simulation tools mainly provide two kinds of interfaces for returning measurement outcomes. The first one is providing the whole quantum state information, i.e., the full spectrum of probability distribution. In this case, to know the probability corresponding to the set of states satisfying certain properties, the user has to iterate over and sum up the probabilities of all states under the computational basis that satisfies the properties. However, this brute-force method is barely scalable due to the exponential quantum state blow-up in the qubit number. The second one is providing random sampling results of a specified number of shots. However, the Monte-Carlo-based methods are far from exact and may lead to incorrect conclusions when one requires a precise answer.
Anzeige
For example, given a Grover’s circuit with a certain search criterion, to verify the formula of amplitude amplification in Grover’s algorithm, we may be interested in the probability that the measurement result satisfies the specified search criterion after certain iterations. Although current simulation tools may finish simulating the circuit fast, there is no way to quickly extract such probability from the simulation result. With the first interface, one may need to enumerate through an exponential number of quantum states for proper computation of the interested probability or expectation value. On the other hand, with the second interface, the precision of the estimated probability is sensitive to the shot number and can be far from exact. As to be demonstrated later in Example 1, the precision loss can severely affect the property checking results. Therefore, an exact and efficient property query interface is necessary.
In this work, we extend the state-of-the-art quantum circuit simulator SliQSim [19], which achieves exact complex number representation without numerical precision loss via algebraic methods and high computation efficiency by partitioned BDD representation and manipulation for implicit matrix-vector multiplication, to further support effective and exact queries about probabilities or expectation values of user-specified properties. Utilizing the Boolean-based data structure, SliQSim can easily mask out the computational components that do not satisfy a property, and the probabilities of the remaining parts are then summed over and reported. Our tool allows users to specify any set of quantum states for exact probability and expectation value queries of customizable properties. The provided query functions allow users to inspect the simulation results from different perspectives and verify the functionality of quantum algorithms.
We note that there are prior efforts on quantum circuit verification. However, they target different goals from ours. For instance, some verifiers focus on checking the equivalence or similarity between two quantum circuits or their output states [1, 4, 7, 20], Hoare-logic style reasoning over program execution [8], quantum abstract interpretation [23], first-order specifications of quantum programs [2], model-checking quantum automata or quantum Markov chains [22], etc. These verification tools do not handle our considered tasks.
2 Tool Architecture
SliQSim [19] exploits an algebraic representation to exactly specify an n-qubit quantum state \( \left| \psi \right\rangle = [\alpha _0, \alpha _1, \ldots , \alpha _{2^n-1}]^\text {T}\) without any numerical precision loss as follows. Each probability amplitude, a complex number \(\alpha _i\), in the state vector is represented by \(\alpha _i = \frac{1}{\sqrt{2}^k}(a_i\omega ^3 + b_i\omega ^2 + c_i\omega + d_i)\), where \(\omega = e^{i\pi /4}\), k is an integer shared by all \(\alpha _i\)’s, and \(a_i, b_i, c_i\), and \(d_i\) are each an r-bit integer. Then \( \left| \psi \right\rangle \) can be represented by 4rn-variable Boolean functions, and each Boolean function can be represented by a standard reduced ordered binary decision diagram (ROBDD) [3]. We denote these 4r BDDs by \({F^a}_{\!\!j}, {F^b}_{\!\!j}, {F^c}_{\!\!j}\), and \({F^d}_{\!\!j}\) for \(j = 1, 2, \ldots , r\). The functionality of the 4r ROBDDs is defined by letting the truth value of \({F^x}_{\!\!j}\) under binary assignments of the index t be equal to the \(j^\text {th}\) bit of \(x_t\), \(x \in \{a, b, c, d\}\). Therefore, the value of \(\alpha _t\) can be recovered from the 4r ROBDDs by substituting the n-qubit variables with the binary values of index \(t \in \{0, 1, \ldots , 2^n-1\}\). In such a data structure, gate applications can be done by Boolean operations on the BDDs.
Fig. 1.
Tool architecture of SliQSim.
Anzeige
We extend SliQSim as shown in Figure 1. First, a circuit file for simulation or analysis is taken (
). SliQSim will calculate the output state of the circuit and, depending on users’ requirements, do random samplings or return the output state vector (
), which are the functions of the original SliQSim. After that, the newly equipped verifier core will read the list of user-defined properties (
). In the verifier core, each property will be translated into a Boolean function \(F^p\), where \(F^p = 1\) indicates that the property is satisfied. This property function \(F^p\) is sent to the Boolean function handler (
), which will conduct the conjunction of \(F^p\) and the Boolean functions that represent the output state (i.e., \({F^x}{\!\!_j}\)’s). In other words, we will obtain a “pseudo-state” copied from the output state, but for the computation bases that do not satisfy the property, their probability amplitudes are equivalently set to 0. After the pseudo-state is obtained and returned, the verifier will send the pseudo-state to the probability calculator (
), which will calculate the total probability of the state. Finally, the probability or truth value of each property will be returned, depending on the types of properties (
).
To understand why SliQSim can easily include the probability query function, we note that SliQSim takes advantage of representing quantum states as Boolean formulas. This allows it to filter out components that do not meet the required properties by a simple conjunction with the property’s function. Therefore, our framework can be easily adapted for simulators that use decision diagrams or Boolean functions as their underlying data structures, such as DDSim [25], Quasimodo [17], and MEDUSA [5].
We note that a similar idea is mentioned in Quasimodo [17], which claims to have the potential capability of probability query. However, it does not implement an interface that accepts user-defined functions, while SliQSim provides various kinds of query functions and can automatically transform them into corresponding Boolean formulas. More importantly, even if Quasimodo implements the probability query function, it suffers from the numerical precision loss problem and cannot achieve exact analysis as SliQSim does.
3 Features and Demo
SliQSim supports various types of queries for user-defined properties. The users can use the expressions listed below to specify their desired properties.
1.
bf {formula}: Returns the probability that the measurement result satisfies the specified Boolean formula formula. We notice that any state set can be generally characterized by a Boolean formula, so solely the bf function is complete for arbitrary state-set specification. Moreover, we provide some common state-set expressions below (Expressions 2 and 3) for users’ convenience.
2.
hweq/hwneq/hwgt/hwlt {qubits} {num}: Returns the probability that the Hamming weight of the measured bit-string of the specified qubits qubits is equal to, nonequal to, greater than, lower than the specified number num.
3.
inteq/intneq/intgt/intlt {qubits} {num}: Returns the probability that the binary integer represented by the specified qubits qubits is equal to, non-equal to, greater than, lower than the specified number num.
4.
expt {qubits} {Pauli(-value)_string}: Returns the expectation value of the observable defined by the specified Pauli string with optionally specified measured-values (0 or 1) for each individual Pauli operator over the specified qubits qubits, commonly used in variational quantum circuits [10, 11, 21] and wire-cut circuits [15, 18]. Specifically, the returned value is calculated by the product of the probability of obtaining the specified measured values and the expectation value of the Pauli operators without measured values with respect to the post-measurement state.
5.
weightedsum{weight_1}{expression_1}... {weight_k}{expression_k}endweighteedsum, for some \(k\ge 1\): Returns the weighted sum of the query results of the specified expressions. This query statement is commonly used in variational quantum circuits [10, 11, 21]. Each weight weight and its corresponding expression expression are stated in an independent line, and the lines are clipped by keywords weightedsum and endweightedsum. The expression can be bf, hweq, hwneq, hwgt, hwlt, inteq, intneq, intgt, intlt, or expt.
6.
assign {var_name} {expression}: Does not return values, but rather stores the specified expression expression in the specified variable name var_name, which can be further utilized in the bf expression. The expression can be bf, hweq, hwneq, hwgt, hwlt, inteq, intneq, intgt, or intlt.
7.
between/outof/leq/geq {range or threshold}: Is specified before the expressions: bf, hweq, hwneq, hwgt, hwlt, inteq, intneq, intgt, intlt, expt, weightedsum. The predicate returns true or false according to whether or not the probability returned by its subsequent expression function is between, out of, less than or equal to, or greater than or equal to the specified range or threshold.
8.
amp {compt_basis}: Returns the probability amplitude (as a complex number) of the specified computational basis compt_basis.
9.
dist {qubits}: Returns the exact spectrum of the probability distribution upon measuring the specified qubits qubits.
We notice that expt is a special case since it is not a “property” that directly corresponds to truth values. To get the expectation value of a Pauli string over some qubits, we first convert the Pauli string to computation basis (i.e., I and Z) by updating the quantum state according to the equalities \(Y = (SH)Z(HS^\dagger )\) and \(X = HZH\). Then we define the property \(P_a\) to be the XNOR operation over negations of all qubits whose Pauli string correspondence is the expectation value of Z, and the property \(P_b\) to be the AND operation over qubits (resp. negations of qubits) whose Pauli string correspondence is obtaining 1 (resp. 0) on Z basis. Then the expectation value of the original string is \(\textsc {Prob}{P_b \wedge P_a} - \textsc {Prob}{P_b \wedge \lnot P_a}\), where \(\textsc {Prob}{P}\) is the probability of P.
To demonstrate the usage and application of our tool, we give three examples as follows.
Example 1
Consider an m-bit oracle that returns true if and only if there are w non-zero bits among the m input bits. We may use Grover’s algorithm [9] to search for satisfying assignments of the oracle. Let p be the probability of obtaining a satisfying assignment after one Grover iteration. Then p should follow the relation \( p = \sin ^2{(3 \cdot \arcsin {\sqrt{t/{2^m}}})}, \) where t is the number of satisfying assignments. We can use a simulator to verify this point. For example, let \(m = 10, w = 2\). Then, we construct a Grover’s algorithm circuit with one Grover iteration and specify the desired property as
Then SliQSim helps us to calculate the probability \(p = 0.350517\). (Note that the real-number output of SliQSim is represented in an (inexact) floating-point number converted from the exact algebraic representation in the last step.) Accordingly, we can infer that there are \(t = 2^m * \sin ^2{((\arcsin {\sqrt{p}}) / 3)} = 45\) satisfying assignments, which equals the expected result \(10 \atopwithdelims ()2\).
We notice that the exact value of the probability is important in this example application. For instance, if there is a \(2\%\)-error to mistake p as 0.345, then the inferred t would become 44, which is incorrect.
Example 2
Suppose an oracle \(U_f: \left| x \right\rangle \left| 0 \right\rangle \mapsto \left| x \right\rangle \left| f(x) \right\rangle \) is designed for Simon’s algorithm [16]. To be able to apply Simon’s algorithm, f should be a two-to-one function satisfying \(f(x) = f(y)\) if and only if \(x = y\) or \(x = y \oplus s\), where s is a secret key. Let t be the measurement outcome of Simon’s algorithm circuit. Then it is promised that
$$\begin{aligned} t \cdot s \!\!\!\!\mod 2 = 0 \end{aligned}$$
(1)
We can use a simulator to verify this point. For example, let \(m=5\) be the variable number of f and \(s = 11001\). Then we construct a Simon’s algorithm circuit and specify the desired property as
Then SliQSim can help us to calculate the probability p that \(t \cdot s \!\!\mod 2 \ne 0\), which should equal 0.
However, if due to a compilation error, the oracle does not satisfy the two-to-one constraint for two input assignments, then Eq. (1) will not always hold. To be precise, the probability p would be \(p = 1/2^m\). In this case, SliQSim can still detect the small probability \(p = 0.03125\) for \(m = 5\) in the above example.
Fig. 2.
The circuit of N-I equivalence checking with delayed initialization.
In this example, the error in the oracle is so small that the random sampling method can hardly detect the small probability. Averagely, \(1/p=2^m\) number of samplings are expected to detect such error, which is too large to be practical as m grows. In contrast, SliQSim provides an efficient way to obtain the exact value of p.
Example 3
The N-I equivalence Boolean matching problem [6], which asks whether two given reversible circuits can be equivalent under some input negation conditions, has recently been shown tractable by quantum computation, but intractable by classical computation [6]. The reader is referred to [6] for the detailed algorithm on finding the input negation condition that makes two oracle circuits \(C_1\) and \(C_2\) equivalent. Figure 2 shows the quantum circuit for deciding the N-I equivalence between \(C_1\) and \(C_2\). The circuit is equipped with the ancilla-assisted initialization technique [13] (shown in the dashed boxes with ancilla qubits q[4 : 6] and q[10 : 12]), so that the initialization of q[i] to \(|0\rangle \) (resp. \(|+\rangle \)) is delayed and transformed into letting \(q[i+3]\) collapse to \(|1\rangle \) on Z-basis (resp. \(|-\rangle \) on X-basis), for \(i \in \{1,2,3,7,8,9\}\). (This will introduce a probability factor of constant 0.5 for each i as side effects.)
For m-bit oracles (\(m=3\) here), it needs to iterate through m types of measurements on q[0], q[4 : 6], q[10 : 12]. For the \(i^\text {th}\) iteration, we compute the probability of obtaining \(|0\rangle \) on q[0], \(|1\rangle \) on q[i] and \(q[6+i]\), and \(|-\rangle \) on other qubits in q[4 : 6] and q[10 : 12]. This can be specified as checking properties as follows.
If the \(i^\text {th}\) qubits of oracles are matched without a negation, the \(i^\text {th}\) resulting probability should be \(1/2^{2m}\). Otherwise, the \(i^\text {th}\) resulting probability should be \(1/2^{2m+1}\).
We notice that the above example conducts multiple property queries on a single circuit, and it requires the capability of X-basis measurements, which can be easily handled by SliQSim. Otherwise, one may need to execute the circuit many times and manually modify the circuit to translate X-basis measurements to computational bases for each execution. Moreover, the exactness of SliQSim helps distinguish the subtle difference between \(1/2^{2m}\) and \(1/2^{2m+1}\).
4 Case Studies
We performed empirical case studies on the examples mentioned in Section 3 for demonstration. All experiments were conducted on a server with Intel Core i7-8700 CPU at 3.20GHz and 32 GB RAM. The timeout (TO) limit is set to 600 seconds. Note that, because there are no other tools that can handle our considered verification tasks, only the results of SliQSim were reported.
4.1 Grover’s Algorithm
Table 1.
Results on Grover’s circuits.
Dummy
We generated Grover’s algorithm circuits with different numbers of qubits. The bit number m of the oracle ranges from \(\{20, 40, 60\}\), and the search criterion is set to have m/10 non-zero bits among the m input bits. The qubit number of the circuit is set to \(n = m + \lceil {\log _2{m}}\rceil + 1\). We intend to simulate the circuit to get the probability of obtaining a satisfying assignment after one Grover iteration, which is utilized to infer the number of satisfying assignments of the oracle.
Table 1 shows the results. In the first column, “m” denotes the bit number of the oracle. In the second column, “cnt” denotes the number of satisfying assignments. The following columns show the result from different methods: using SliQSim for exact query, using SliQSim with \(10^5\) random samplings for estimation, or using SliQSim to report the whole state vector. For each method, the “cnt” column shows the number of satisfying assignments inferred from the calculated exact or estimated approximate probability. The runtime in seconds is also reported.
As one can see in Table 1, SliQSim is precise enough to always infer the correct number of satisfying assignments. In contrast, the results estimated from random samplings suffer from precision loss and have longer runtime. This situation becomes more significant as the circuit size grows. For \(m = 40\) and 60, random sampling with \(10^5\) shots cannot even detect the small probability, and the runtime is much longer than SliQSim. As for the interface that provides the whole quantum state information, it fails to finish any circuit because there are tens of qubits, leading to millions of entries in the state vector.
4.2 Simon’s Algorithm
Table 2.
Results on Simon’s circuits.
Dummy
We design Simon’s algorithm circuits with different numbers of qubits. The variable number m of the oracle function ranges from \(\{10, 15, 20\}\), and the erroneous oracle has exactly two input assignments that do not satisfy the two-to-one constraint. The qubit number of the circuit is \(n = 2m\). We then simulate the circuit to check if the simulator can find the probability of violating Eq. (1).
Table 2 shows the results. In the first column, “m” denotes the variable number of the oracle, and the following columns show the results from different methods. For each method, the “prob” column shows the calculated exact or estimated approximate probability of violating Eq. (1), and the “time” column reports the runtime in seconds.
As one can see in Table 2, SliQSim can always detect the error of the oracle by reporting the small probability of violating Eq. (1). In contrast, a lot of sampling shots are required to detect the small probability, and the runtime is also longer. For \(m = 20\), \(10^5\) shots are not even enough while taking a much longer runtime. As for the interface that provides the whole quantum state information, although it can report the exact probability, it is not scalable enough to finish \(m \ge 15\) in the time limit, showing the infeasibility of brute-force methods.
4.3 N-I Equivalence Boolean Matching
Table 3.
Results on N-I equivalence checking circuits.
Dummy
We generate N-I equivalence-checking circuits with different numbers of qubits. The input number of the oracle function m ranges from 3 to 7, and the qubit number of the whole circuit is \(n = 4m+1\). We generate the first oracle as a random logic circuit with 5m gates, and the second oracle is produced by adding random negation gates at the input. We then simulate the circuit to find the input negation gates required to make the oracles equivalent.
The experiment results are shown in Table 3. In the first column, “m” denotes the variable number of the oracle, and in the second column, “n” denotes the qubit number of the whole circuit. The third column reports the runtime of SliQSim querying the m properties, while the fourth column reports the runtime of SliQSim obtaining one random sampling result in seconds for reference. Here, we omit to compare with the interface that provides the whole quantum state information because X-basis measurement is required in this algorithm, so summing up probability amplitudes in a state vector does not work.
Although SliQSim seems to take much longer time than the one-shot simulation, we notice that more than \(2^m\) shots are required to achieve enough precision to decide whether a negation gate exists, and a total of m different circuits are required to be sampled. Therefore, SliQSim is still much more efficient than sampling-based methods.
Acknowledgments
This work was supported in part by the National Science and Technology Council of Taiwan under grants 113-2119-M-002-024, the NTU Center of Data Intelligence: Technologies, Applications, and Systems under grant NTU-113L900903, and the NTU Core Consortium Project NTU-CC114L895002. The authors thank IBM Q Hub at NTU and Quantum Technology Cloud Computing Center at NCKU for supporting access to quantum devices.
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
). 
), which are the functions of the original 
). In the verifier core, each property will be translated into a Boolean function \(F^p\), where \(F^p = 1\) indicates that the property is satisfied. This property function \(F^p\) is sent to the Boolean function handler (
), which will conduct the conjunction of \(F^p\) and the Boolean functions that represent the output state (i.e., \({F^x}{\!\!_j}\)’s). In other words, we will obtain a “pseudo-state” copied from the output state, but for the computation bases that do not satisfy the property, their probability amplitudes are equivalently set to 0. After the pseudo-state is obtained and returned, the verifier will send the pseudo-state to the probability calculator (
), which will calculate the total probability of the state. Finally, the probability or truth value of each property will be returned, depending on the types of properties (
).
