Výzkum z FITu zabývající se verifikací kvantových výpočtů byl vybrán mezi nejzajímavější práce na poli informatiky

Článek s názvem An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits, na němž se významně podílel Ondřej Lengál z výzkumné skupiny VeriFIT, byl vybrán jako research highlight do časopisu „Communications of the ACM“. Do rubriky research highlights bývá přitom voleno několik nejzajímavějších výsledků z řádově desítek tisíc článků zaslaných ročně na ACM konference napříč všemi oblastmi informatiky. Je to vůbec poprvé, co se článku s českou afiliací dostalo této výsady. 

Citovaný článek zavádí nový přístup k automatické verifikaci kvantových výpočtů pomocí teorie automatů, a vytváří tak most mezi těmito dvěma výzkumnými oblastmi (kvantové počítání a automaty). Automaty jsou zde využity pro kompaktní reprezentaci složitých množin kvantových stavů. Návazné práce zavádějí varianty těchto automatů, které umožňují reprezentovat množiny kvantových stavů s několika dimenzemi nekonečnosti (jako jsou např. počet qubitů či potenciální hodnoty amplitud) a verifikovat parametrické kvantové programy (např. to, že algoritmus funguje správně pro libovolný počet qubitů).

Článek vznikl ve spolupráci s výzkumníky z Academia Sinica na Tchaj-wanu (Čínská republika), s nimiž skupina VeriFIT aktivně spolupracuje již déle než 15 let.
Více k tématu výzkumu Ondřeje Lengála a k výzvám souvisejícím s kvantovým počítáním najdete zde.