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

Saved in:

Bibliographic Details
Title:	An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits.
Authors:	Chen, Yu-Fang¹ (AUTHOR) yfc@iis.sinica.edu.tw, Chung, Kai-Min¹ (AUTHOR) kmchung@iis.sinica.edu.tw, Lengál, Ondřej² (AUTHOR) lengal@fit.vut.cz, Lin, Jyun-Ao³ (AUTHOR) jyalin@gmail.com, Tsai, Wei-Lun^1,4 (AUTHOR) alan23273850@gmail.com, Yen, Di-De⁵ (AUTHOR) bottlebottle13@gmail.com
Source:	Communications of the ACM. Jun2025, Vol. 68 Issue 6, p85-93. 9p.
Subjects:	Quantum computing, Machine theory, Scalability, Qubits, Quantum gates
Abstract:	As quantum computing progresses, scalable and precise verification of quantum circuits becomes essential. This work introduces an automata-based framework that uses tree automata to represent quantum state sets and applies transformers to model gate semantics. A prototype tool based on this framework successfully verified circuits with up to 320 qubits, outperforming existing tools. The approach also connects quantum verification with automata theory, suggesting new directions for applying formal methods in quantum computing.
Database:	Engineering Source

Description
Abstract:	As quantum computing progresses, scalable and precise verification of quantum circuits becomes essential. This work introduces an automata-based framework that uses tree automata to represent quantum state sets and applies transformers to model gate semantics. A prototype tool based on this framework successfully verified circuits with up to 320 qubits, outperforming existing tools. The approach also connects quantum verification with automata theory, suggesting new directions for applying formal methods in quantum computing.
ISSN:	00010782
DOI:	10.1145/3725728