Detail projektu
QUAK: Quantum Program Analysis using Automata Toolkit
Období řešení: 1.1.2025 — 31.12.2027
Zdroje financování
Grantová agentura České republiky - Standardní projekty
O projektu
Quantum computing promises solving problems deemed infeasible for classical computers. While certain problems (e.g. factoring) are known to have fast quantum algorithms, development of quantum algorithms for other problems is extremely challenging due to the complexity of understanding quantum programs and reasoning over them. Existing approaches for their verification, analysis, and simulation are limited in their expressivity, precision, scalability, or require significant manual effort. In the project, we will address these limitations by a) developing new formal models capable of compactly encoding structured (sets of) quantum states that occur in quantum programs, building on ideas from automata theory; b) designing languages for describing pre-/post-conditions in quantum programs that will be easy to use and algorithms for their translation into the formal models; and c) proposing new efficient algorithms for automated reasoning over quantum programs that will, together with the two previous goals, push the capabilities of reasoning over quantum programs to a new level.
Popis česky
Kvantové počítače slibují řešení problémů, které nelze efektivně řešit klasickými
počítači. Zatímco některé problémy (např. faktorizace) jde řešit rychleji
kvantovými algoritmy, vývoj kvantových programů pro jiné problémy je extrémně
náročný z důvodu složitosti pochopení kvantových programů a usuzování nad nimi.
Existující přístupy pro jejich verifikaci, analýzu a simulaci mají omezenou
expresivitu, přesnost, škálovatelnost, nebo vyžadují značné manuální úsilí.
V tomto projektu se zaměříme na tato omezení prostřednictvím a) vývoje nových
formálních modelů schopných kompaktní reprezentace strukturovaných (množin)
kvantových stavů vyskytujících se v kvantových programech, založených na teorii
automatů; b) návrhu jazyků pro popis vstupních a výstupních podmínek v kvantových
programech, které budou jednoduché na použití, a algoritmů pro překlad do
formálních modelů a c) vytvoření nových efektivních algoritmů pro automatické
usuzování nad kvantovými programy, které, spolu s dvěmi předchozími cíly, posune
možnosti usuzování nad kvantovými programy na novou úroveň.
Klíčová slova
quantum algorithms;specification languages;formal models;decision diagrams;tree
automata;verification;simulation;analysis;logic
Klíčová slova česky
kvantové algoritmy;specifikační jazyky;formální modely;rozhodovací
diagramy;stromové automaty;verifikace;simulace;analýza;logika
Označení
25-18318S
Originální jazyk
angličtina
Řešitelé
Lengál Ondřej, Ing., Ph.D. - hlavní řešitel
Havlena Vojtěch, Ing., Ph.D. - spoluřešitel
Hečko Michal, Ing. - spoluřešitel
Hudák David, Ing. - spoluřešitel
Rogalewicz Adam, doc. Mgr., Ph.D. - spoluřešitel
Síč Juraj, Mgr. - spoluřešitel
Útvary
Ústav inteligentních systémů
- odpovědné pracoviště (27.3.2024 - nezadáno)
Ústav inteligentních systémů
- příjemce (27.3.2024 - 31.12.2027)
Odpovědnost: Lengál Ondřej, Ing., Ph.D.