The Road to Error-Free Quantum Computing

In a study published in PeerJ Computer Science, Professor Kazuhiro Ogata and Assistant Professor Canh Minh Do of the Japan Advanced Institute of Science and Technology (JAIST) suggested using symbolic model checking to validate quantum circuits.

Quantum computing is a fast-developing technology that utilizes the principles of quantum physics to tackle complicated computational problems that are extremely difficult for classical computing.

To take advantage of quantum computing, researchers worldwide have created a large number of quantum algorithms that show notable gains over classical algorithms.

Creating these algorithms requires the use of quantum circuits, which are models of quantum processing. Before they are actually deployed on quantum hardware, they are utilized to design and implement quantum algorithms.

Quantum circuits consist of a series of quantum gates, measurements, and qubit initializations, among other events. Quantum gates execute quantum computations by working on qubits, the quantum equivalents of conventional bits (0s and 1s), and manipulating the system's quantum states.

Quantum states are the output of quantum circuits that can be monitored to provide classical outcomes with probabilities from which additional actions can be taken. Since quantum computing is frequently counterintuitive and substantially distinct from classical computing, the likelihood of mistakes is significantly larger. As a result, it is critical to ensure that quantum circuits have the correct features and perform as planned.

This can be accomplished using model checking, a formal verification approach used to ensure that systems meet desirable attributes. Although certain model checkers are specialized to quantum programs, there is a distinction between model-checking quantum programs and quantum circuits due to differences in representation and the absence of iterations in quantum circuits.

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.

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

Maude is a high-level specification/programming language based on rewriting logic that enables the formal definition and verification of complicated systems. It comes with a Linear Temporal Logic (LTL) model checker that determines if systems meet the necessary features. Maude also enables the development of exact mathematical models of systems.

Using the Dirac notation and the rules of quantum physics, the researchers formally defined quantum circuits in Maude as a set of quantum gates and measurement applications. They provided the system’s intended attributes and its initial state 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. The researchers then automatically checked whether quantum circuits satisfied the required characteristics using the integrated Maude LTL model checker.

Using this method, several early quantum communication protocols, each with increasing complexity, were checked: Superdense Coding, Quantum Teleportation, Quantum Secret Sharing, Entanglement Swapping, Quantum Gate Teleportation, Two Mirror-image Teleportation, and Quantum Network Coding.

They discovered that the initial iteration did not meet the desired property of Quantum Gate Teleportation. By employing this method, the researchers suggested an updated version and verified that it was accurate.

These findings highlight the significance of the suggested novel technique for the verification of quantum circuits. However, the researchers highlight certain drawbacks of their strategy that need more investigation.

Dr. Do added, “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 expected functionality of quantum circuits will be extremely useful in the approaching era of quantum computing. In this context, the current technique is the first step toward a broader framework for verifying and specifying quantum circuits, opening the way for error-free quantum computing.

The study was supported by JST SICORP Grant Number JPMJSC20C2, Japan, and JSPS KAKENHI Grant Numbers JP23H03370, JP23K19959, and JP24K20757.

Journal Reference:

Do, C. M., et al. (2024) Symbolic model checking quantum circuits in Maude. PeerJ Computer Science. doi:10.7717/peerj-cs.2098