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 ze skupiny VeriFIT, byl vybrán jako research highlight do časopisu „Communications of the ACM“. Do rubriky research highlights bývá přitom vybráno 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 pocty. Doplňme, že plná verze textu byla poprvé publikována v roce 2023 na špičkové konferenci PLDI’23 (CORE A*), kde získala ocenění „Distinguished paper“.

Vývoj v oblasti kvantového počítání významně postupuje, a to jak na poli technologickém (lepší hardware), tak i algoritmickém (lepší techniky opravy chyb). Kvantové počítání slibuje řešení problémů, s nimiž si nejsme aktuálně schopni efektivně poradit konvenčními technikami, jako jsou např. faktorizace velkých čísel, hledání v nestrukturované databázi či problémy v oblasti materiálového inženýrství, farmakologie nebo simulace fyzikálních systémů. Psaní programů pro kvantové počítače je však mnohem náročnější než pro počítače klasické – důvodem je i fakt, že kvantové programy mají pravděpodobnostní povahu a klíčovou technikou, kterou dosahují své efektivity, je využití tzv. superpozice a konstruktivní interference. Zjednodušeně si to lze představit následovně: Program je při svém běhu v několika stavech zároveň, v každém s určitou pravděpodobností, a tyto pravděpodobnosti spolu mohou interagovat – zesilovat se či zeslabovat. Abychom omezili možnosti vzniku chyb při programování kvantových počítačů, je potřeba mít nástroje, které umí v kvantových programech chyby hledat. Analýza kvantových programů je však náročný problém i pro samotné počítače z důvodu toho, že kvantový program může být v jeden okamžik v superpozici exponenciálně mnoha stavů, které je všechny třeba při analýze brát do úvahy.

Č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 (konkrétně konečné stromové automaty, což je rozšíření standardních konečných automatů reprezentujících regulární jazyky) 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. Text článku je dostupný ZDE.

K dispozici je také záznam veřejné habilitační přednášky Ondřeje Lengála na dané téma.