An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits

Explore a groundbreaking paradigm for analyzing and detecting bugs in quantum circuits through this 18-minute conference talk from PLDI 2023. Discover how researchers utilize tree automata to represent quantum states compactly and develop transformers for implementing quantum gate semantics. Learn about the innovative approach that employs algebraic representations of quantum states, avoiding floating-point number inaccuracies. Examine the performance of this technique against various benchmarks, including its ability to verify a large circuit with 40 qubits and 141,527 gates, and detect bugs in a circuit with 320 qubits and 1,758 gates. Gain insights into the connection between quantum program verification and automata theory, opening new possibilities for leveraging automata-based verification in quantum computing.