An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits
Yu‐Fang Chen, Kai-Min Chung, Ondřej Lengál, Jyun-Ao Lin, Wei-Lun Tsai, Di-De Yen
Abstract
As quantum computing hardware advances, the demand for scalable, precise, and fully automated verification techniques for quantum circuits grows. This paper introduces a novel automata-based framework tailored for the verification of quantum circuits. In our approach, the problem is framed as a triple <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:mrow> <mml:mo>{</mml:mo> <mml:mi>P</mml:mi> <mml:mo>}</mml:mo> <mml:mspace width="0.166667em"/> <mml:mi>C</mml:mi> <mml:mspace width="0.166667em"/> <mml:mo>{</mml:mo> <mml:mi>S</mml:mi> <mml:mo>}</mml:mo> </mml:mrow> </mml:math> and the question is whether, given a set <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:mi>P</mml:mi> </mml:math> of quantum states on the input of a circuit <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:mi>C</mml:mi> </mml:math> , the set of quantum states on the output is equal to (or included in) a set <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML" display="inline"> <mml:mi>S</mml:mi> </mml:math> . Our framework leverages tree automata to compactly represent sets of quantum states and we develop transformers to implement the semantics of quantum gates over this representation. We implemented the proposed approach in a prototype tool and evaluated its performance against various benchmarks from the literature. The evaluation shows that our approach is quite scalable, for example, we managed to verify a large circuit with 40 qubits and 141,527 gates, or catch bugs injected into a circuit with 320 qubits and 1,758 gates, where all tools we compared with failed. Additionally, our work bridges quantum program verification and automata, opening new possibilities to exploit the richness of automata theory in quantum computing.