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

Quantum computing holds the potential to solve complex problems that classical computers struggle to address. Since its inception, quantum algorithms have showcased capabilities beyond classical limits, exemplified by Shor's factoring algorithm and Grover's search algorithm--both of which can solve important computational problems provably faster than classical methods.16,20 For many years, the lack of hardware posed a barrier to implementing these algorithms, but recent advancements--including Google's 2019 demonstration of a quantum computational advantage on a programmable superconducting processor--have marked significant milestones, though their results remain the subject of ongoing debate.3 As quantum computing moves toward practical applications, programming languages and systems for quantum computers are under active development to meet growing demands. Efficient algorithms have begun to emerge in fields such as optimization, machine learning (ML), and quantum chemistry, creating a pressing need for reliable verification methods to ensure circuit correctness in these applications.19