一句话：提出层级同步树自动机（LSTA）表示量子态集，实现可扩展且支持参数化的量子电路验证。
本文提出基于层级同步树自动机（LSTA）的量子电路符号化验证方法。LSTA 在经典树自动机的迁移上附加选择集，用以同步被接受树的子树，从而符号化表示量子态集合；其表达能力与经典树自动机不可比，但保持并、交封闭及语言空性与包含可判定。作者实现全自动验证算法，支持门操作复杂度至多二次，显著优于早期树自动机方法的指数最坏复杂度，并能进行参数化验证，即验证任意量子比特数下同结构电路族。C++ 工具在基准上与三个符号量子电路验证器和两个模拟器比较，可求解规模远大于现有技术的实例。
We present a new method for the verification of quantum circuits based on a novel symbolic representation of sets of quantum states using level-synchronized tree automata (LSTAs). LSTAs extend classical tree automata by labeling each transition with a set of choices , which are then used to synchronize subtrees of an accepted tree. Compared to the traditional tree automata, LSTAs have an incomparable expressive power while maintaining important properties, such as closure under union and intersection, and decidable language emptiness and inclusion. We have developed an efficient and fully automated symbolic verification algorithm for quantum circuits based on LSTAs. The complexity of supported gate operations is at most quadratic, dramatically improving the exponential worst-case complexity of an earlier tree automata-based approach. Furthermore, we show that LSTAs are a promising model for parameterized verification , i.e., verifying the correctness of families of circuits with the same structure for any number of qubits involved, which principally lies beyond the capabilities of previous automated approaches.We implemented this method as a C++ tool and compared it with three symbolic quantum circuit verifiers and two simulators on several benchmark examples. The results show that our approach can solve problems with sizes orders of magnitude larger than the state of the art.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2410-18540,
title = {Verifying Quantum Circuits with Level-Synchronized Tree Automata},
author = {Parosh Aziz Abdulla and Yo-Ga Chen and Yu-Fang Chen and Lukáš Holík and Ondřej Lengál and Jyun-Ao Lin and Fang-Yi Lo and Wei-Lun Tsai},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {POPL},
year = {2025},
doi = {10.1145/3704868}
}