Verifying Quantum Circuits with Level-Synchronized Tree Automata
summary
Introduces level-synchronized tree automata that label transitions with joint choices to synchronize different tree branches, enabling a symbolic encoding of sets of quantum states; improves handling of the Hadamard operation so Hadamard gate complexity from exponential to quadratic; provides decidable emptiness and inclusion (inclusion PSPACE-hard, in EXPspace); ships as a C++ tool solves circuits orders of magnitude larger, outperforms three symbolic verifiers and two simulators, and verifies Grover iterations up to 200 qubits in ~18 seconds.
AI-written summary · about