一句话：提出基于树自动机的量子电路验证与缺陷发现框架，可验证大型电路并捕获注入缺陷。
论文研究量子电路验证与缺陷发现：给定形如 {P} C {Q} 的三元组，判断电路 C 将输入量子态集合 P 映射后的输出集合是否等于或包含于 Q。作者提出基于树自动机的表示方法，紧凑编码量子态集合，并为量子门构造语义变换器；采用代数表示避免浮点误差。实现原型工具并在文献基准上评估，能验证 40 量子比特、141,527 个门的大电路，或发现注入 320 量子比特、1,758 个门电路中的缺陷，而对比工具均失败。该工作建立了量子程序验证与自动机理论的联系。
We introduce a new paradigm for analysing and finding bugs in quantum circuits. In our approach, the problem is given by a triple { P } C { Q } and the question is whether, given a set P of quantum states on the input of a circuit C , the set of quantum states on the output is equal to (or included in) a set Q . While this is not suitable to specify, e.g., functional correctness of a quantum circuit, it is sufficient to detect many bugs in quantum circuits. We propose a technique based on tree automata to compactly represent sets of quantum states and develop transformers to implement the semantics of quantum gates over this representation. Our technique computes with an algebraic representation of quantum states, avoiding the inaccuracy of working with floating-point numbers. 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, e.g., 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. In addition, our work establishes a connection between quantum program verification and automata, opening new possibilities to exploit the richness of automata theory and automata-based verification in the world of quantum computing.
@article{paperbot1961,
title = {An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits},
author = {Yu-Fang Chen and Kai-Min Chung and Ondřej Lengál and Jyun-Ao Lin and Wei-Lun Tsai and Di-De Yen},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {PLDI},
year = {2023},
doi = {10.1145/3591270}
}