Toward error-free quantum computing: A symbolic model checking approach to verify quantum circuits

Quantum computing is a rapidly growing technology that utilizes the laws of quantum physics to solve complex computational problems that are extremely difficult for classical computing. Researchers worldwide have developed many quantum algorithms to take advantage of quantum computing, demonstrating significant improvements over classical algorithms.

Quantum circuits, which are models of quantum computation, are crucial for developing these algorithms. They are used to design and implement quantum algorithms before actual deployment on quantum hardware.

Quantum circuits comprise a sequence of quantum gates, measurements, and initializations of qubits, among other actions. Quantum gates perform quantum computations by operating on qubits, which are the quantum counterparts of classical bits (0s and 1s), and by manipulating the quantum states of the system. Quantum states are the output of quantum circuits, which can be measured to obtain classical outcomes with probabilities, from which further actions can be done.

Since quantum computing is often counter-intuitive and dramatically different from classical computing, the probability of errors is much higher. Hence, it is necessary to verify that quantum circuits have the desired properties and function as intended. This can be done through model checking, a formal verification technique used to verify whether systems satisfy desired properties.

Although some model checkers are dedicated to quantum programs, there is a gap between model-checking quantum programs and quantum circuits due to different representations and no iterations in quantum circuits.

Addressing this gap, Assistant Professor Canh Minh Do and Professor Kazuhiro Ogata from Japan Advanced Institute of Science and Technology (JAIST) proposed a symbolic model checking approach.

Dr. Do explains, "Considering the success of model-checking methods for verification of classical circuits, model-checking of quantum circuits is a promising approach. We developed a symbolic approach for model checking of quantum circuits using laws of quantum mechanics and basic matrix operations using the Maude programming language."

Their approach is detailed in a study published in the journal PeerJ Computer Science.

Maude is a high-level specification/programming language based on rewriting logic, which supports the formal specification and verification of complex systems. It is equipped with a Linear Temporal Logic (LTL) model checker, which checks whether systems satisfy the specified properties.

Additionally, Maude allows the creation of precise mathematical models of systems. The researchers formally specified quantum circuits in Maude, as a series of quantum gates and measurement applications, represented as basic matrix operations using laws of quantum mechanics with the Dirac notation. They specified the initial state and the desired properties of the system in LTL.

By using a set of quantum physics laws and basic matrix operations formalized in our specifications, quantum computation can be reasoned in Maude. They then used the built-in Maude LTL model checker to automatically verify whether quantum circuits satisfy the desired properties.

They used this approach to check several early quantum communication protocols, including Superdense Coding, Quantum Teleportation, Quantum Secret Sharing, Entanglement Swapping, Quantum Gate Teleportation, Two Mirror-image Teleportation, and Quantum Network Coding, each with increasing complexity.

They found that the original version of Quantum Gate Teleportation did not satisfy its desired property. By using this approach, the researchers notably proposed a revised version and confirmed its correctness.

These findings signify the importance of the proposed innovative approach for the verification of quantum circuits. However, the researchers also point out some limitations of their method, requiring further research.

Dr. Do says, "In the future, we aim to extend our symbolic reasoning to handle more quantum gates and more complicated reasoning on complex number operations. We also would like to apply our symbolic approach to model-checking quantum programs and quantum cryptography protocols."

Verifying the intended operation of quantum circuits will be highly valuable in the upcoming era of quantum computing. In this context, the present approach marks the first step toward a general framework for the verification and specification of quantum circuits, paving the way for error-free quantum computing.