March 18, 2026 by Japan Advanced Institute of Science and Technology
Collected at: https://phys.org/news/2026-03-future-quantum.html
Quantum computers could solve certain problems that would take traditional classical computers an impractically long time to solve. At the Japan Advanced Institute of Science and Technology (JAIST), researchers are now working to make these systems reliable and trustworthy.
Unlike classical computers that process information in binary digits (bits) as either 0 or 1, quantum computers use quantum bits or “qubits” that can represent both 0 and 1 simultaneously, enabling dramatic speedups in computations for specific problems.
The potential applications of quantum computing are wide-ranging. These include factoring large numbers that could break today’s encryption, optimizing complex industrial processes, accelerating drug discovery, and supporting advances in artificial intelligence (AI).
The computing science research group
At the Laboratory on Formal Methods for Quantum Computing at JAIST, Professor Kazuhiro Ogata and Senior Lecturer Canh Minh Do are working to make quantum systems dependable.
Prof. Ogata, who heads the laboratory, began his career with a background in computer science. As a student, he explored AI and fuzzy logic before moving into system programming, including work on operating systems and programming language processors. He eventually joined the team of former professor Kokichi Futatsugi at JAIST and later became involved in formal methods research.
Senior Lecturer Do arrived in Japan about seven to eight years ago to pursue graduate studies at JAIST, where he completed both his master’s and Ph.D. in Information Science. His early research focused on testing for concurrent and distributed systems.
Over time, his work expanded into verification techniques, such as model checking and theorem proving for large-scale systems. Today, his research centers on formal methods designed specifically for quantum computing.
Prof. Ogata explains the potential advantage of quantum computers with a simple comparison, “If a problem has a size comparable to 264 possibilities, a classical computer will need an enormous number of bits to handle it. In contrast, a quantum computer could represent such complexity with just 64 qubits, showing how dramatically the scale of computation can change.”
Together, their laboratory focuses on formal methods for quantum computing. They develop ways to formally specify and verify quantum circuits, programs, and protocols before they are deployed in real-world systems.
Making quantum systems reliable
The team’s work focuses on using formal methods to ensure that quantum systems behave as intended. “Traditional testing techniques are significantly less effective for quantum software due to the nondeterminism and probabilistic nature of quantum measurement. For example, each time you measure a quantum state, it collapses, and you may obtain a different result. This makes testing unreliable, so formal methods become essential,” says Dr. Do.
“Formal methods consist of two parts: formal specification and formal verification. One describes how the system behaves and defines desired properties, and the other checks whether the system satisfies the desired properties,” explains Prof. Ogata.
Researchers first model a system’s behavior and expected requirements and then verify them using techniques such as model checking and theorem proving. Prof. Ogata compares this process to that of analyzing a vending machine, where inserting coins or selecting a drink changes the system’s state. By modeling these transitions, researchers can verify whether certain rules, such as conserving the total amount of money, always hold.
Applying these ideas to quantum computing, however, is significantly more complex. This is because, unlike the classical bits, qubits can exist in “quantum superposition” and may become “entangled,” in which the quantum states of multiple qubits remain correlated irrespective of their physical separation.
Because measuring a quantum system changes its state, traditional software testing methods often fall short. As a result, mathematically grounded verification techniques are becoming increasingly important for building reliable quantum technologies.
One of the lab’s recent breakthroughs involves verifying quantum protocols in the presence of concurrency and communication among participants.
“In quantum protocols, multiple participants operate at the same time while exchanging information. While earlier approaches could describe the quantum behavior, such as unitary transformations and quantum measurement, they did not capture concurrency and communication between participants,” explains Dr. Do.
To address this gap, the team developed a framework called Concurrent Dynamic Quantum Logic (CDQL) that can formally describe quantum protocols, such as quantum teleportation, and automatically verify whether the system is behaving correctly.
The group also developed a support tool incorporating an optimization technique called the lazy rewriting strategy to manage the large number of interleavings arising from concurrency and communication, thereby enabling the automatic and effective verification of CDQL models.
“Our goal is to create methods and tools that allow researchers to rigorously verify quantum programs and protocols before they are deployed,” says Prof. Ogata.
International research connections
The research team collaborates with international scientists working in dependable and secure computing, including researchers at the Technical University of Valencia and the Complutense University of Madrid. The team’s work has caught the attention of researchers worldwide, with some visiting JAIST’s campus to explore potential collaborations.
Training the next generation of researchers
Prof. Ogata has a reassuring message for prospective students: they do not need to be a quantum physicist to start working in the field.
“Students do not need to learn everything. If they are good at programming, that is enough to begin. When I was a student, I took quantum mechanics and did not fully understand it,” says Prof. Ogata. The only essential prerequisite is linear algebra, a subject most science and engineering students are familiar with.
From there, students can gradually learn the mathematical and theoretical foundations of quantum computing while contributing to ongoing research projects.
The broader impact of research at JAIST: A ‘Sen Tan’ vision for the future
Quantum computing has the potential to reshape cybersecurity, optimization, AI and large-scale simulations. For instance, quantum algorithms like Shor’s algorithm could one day break widely used encryption systems.
This possibility has already prompted the development of post-quantum cryptography, with organizations such as the National Institute of Standards and Technology (NIST) encouraging the transition to quantum-resistant security methods.
“We should start using post-quantum transport layer security (TLS) as soon as possible. Today’s encrypted data might be stored now and decrypted later when quantum computers exist,” says Prof. Ogata.
Formal verification will likely play a crucial role in ensuring the safety, security, and reliability of future quantum systems. Beyond cryptography, quantum computing may also transform AI.
“Quantum AI aims to accelerate certain machine learning tasks by leveraging quantum computing. Because quantum systems can exist in superposition, they can represent complex information in high-dimensional spaces. In principle, this may allow researchers to encode data into quantum states, embed AI models into quantum circuits, and potentially train them more efficiently. However, several challenges remain, including efficient data encoding and the limitations of current quantum hardware,” elaborates Dr. Do.
Through these “Sen Tan” (cutting-edge) aspects of their work at JAIST, Professor Ogata, Senior Lecturer Do, and their students are helping lay the theoretical and practical foundations for the next generation of computing. By ensuring that quantum systems can be rigorously designed and verified, the laboratory is paving the way for technologies that may come to define the coming decades.
Leave a Reply