FIT BUT research on quantum computation verification selected among the most interesting works in the field of computer science

The article entitled An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits, to which Ondřej Lengál from the VeriFIT group made a significant contribution, was selected as a research highlight for the journal Communications of the ACM. The research highlights section usually selects several of the most interesting results from tens of thousands of articles submitted annually to ACM conferences across all areas of computer science. This is the first time that an article with a Czech affiliation has received this honor. It should be added that the full version of the text was first published in 2023 at the leading PLDI'23 (CORE A*) conference, where it received the Distinguished Paper award.

Developments in the field of quantum computing are advancing inexorably, both in terms of technology (better hardware) and algorithms (better error correction techniques). Quantum computing promises to solve problems that we are currently unable to deal with effectively using conventional techniques, such as factoring large numbers, searching unstructured databases, or problems in the fields of materials engineering, pharmacology, or the simulation of physical systems. However, writing programs for quantum computers is much more demanding than for classical computers—one reason being that quantum programs are probabilistic in nature and the key technique by which they achieve their efficiency is the use of superposition and constructive interference. This can be simplified by imagining that a program runs in several states at the same time, each with a certain probability, and these probabilities can interact with each other: they can amplify or weaken each other. In order to limit the possibility of errors when programming quantum computers, we need tools that can search for errors in quantum programs. However, analyzing quantum programs is a challenging problem even for computers themselves, because a quantum program can be in a superposition of an exponential number of states at any given moment, all of which must be taken into account during analysis.

The article introduces a new approach to the automatic verification of quantum computations using automata theory and builds a bridge between these two research areas (quantum computing and automata). Automata (specifically finite tree automata, which are an extension of standard finite automata representing regular languages) are used here for the compact representation of complex sets of quantum states. Follow-up work introduces variants of these automata that allow the representation of sets of quantum states with several dimensions of infinity (such as the number of qubits or potential amplitude values) and the verification of parametric quantum programs (e.g., that the algorithm works correctly for any number of qubits).

The article was written in collaboration with researchers from Academia Sinica in Taiwan (Republic of China), with whom the VeriFIT group has been actively collaborating for more than 15 years. The text of the article is available HERE.

A recording of Ondřej Lengál's public habilitation lecture on the topic is also available.