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

Ishikawa, Japan -- 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. Looking ahead, 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.

###

Reference

About Japan Advanced Institute of Science and Technology, Japan

Founded in 1990 in Ishikawa prefecture, the Japan Advanced Institute of Science and Technology (JAIST) was the first independent national graduate school in Japan. Now, after 30 years of steady progress, JAIST has become one of Japan’s top-ranking universities. JAIST counts with multiple satellite campuses and strives to foster capable leaders with a state-of-the-art education system where diversity is key; about 40% of its alumni are international students. The university has a unique style of graduate education based on a carefully designed coursework-oriented curriculum to ensure that its students have a solid foundation on which to carry out cutting-edge research. JAIST also works closely both with local and overseas communities by promoting industry–academia collaborative research.  

About Assistant Professor Canh Minh Do from Japan Advanced Institute of Science and Technology, Japan

Canh Minh Do is currently an Assistant Professor at the School of Information Science at Japan Advanced Institute of Science and Technology (JAIST). He obtained his Ph.D. and M.S. degrees in Information Science from JAIST, under the guidance of Professor Kazuhiro Ogata. His primary research interests are in the areas of formal methods, such as formal specification, interactive theorem proving and model checking, and tools supporting formal methods. His research focuses on formal specification and verification of concurrent/distributed systems for both conventional and emerging technologies.

Funding information: This work was supported by JST SICORP Grant Number JPMJSC20C2, Japan and JSPS KAKENHI Grant Numbers JP23H03370, JP23K19959, JP24K20757.