JUNE 21, 2024 by Japan Advanced Institute of Science and Technology
Collected at: https://techxplore.com/news/2024-06-error-free-quantum-approach-circuits.html
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.
More information: Canh Minh Do et al, Symbolic model checking quantum circuits in Maude, PeerJ Computer Science (2024). DOI: 10.7717/peerj-cs.2098
Leave a Reply