Automata-Based Approach for Quantum Circuit and Program Verification

Explore an innovative paradigm for analyzing and detecting bugs in quantum circuits through this 44-minute lecture. Delve into a new approach that represents the problem as a triple {P}C{Q}, questioning whether a set P of quantum states on the input of a circuit C results in an output equal to or included in a set C. Learn about a tree automata-based technique for compact representation of quantum states and the development of transformers to implement quantum gate semantics. Discover how this method computes with an algebraic representation of quantum states, avoiding inaccuracies associated with floating-point numbers. Examine the performance of a prototype tool implementing this approach against various benchmarks, showcasing its scalability in verifying large circuits and detecting bugs. Gain insights into the connection between quantum program verification and automata theory, opening up new possibilities for leveraging automata-based verification in quantum computing.