一句话：首个全自动验证参数化量子程序关系性质的框架，以同步加权树自动机刻画无限族量子态并给出判定过程。
参数化量子程序指给定输入规模即生成相应量子电路的程序，其关系性质（输入-输出正确性与等价性）此前缺乏全自动验证手段。本文提出首个全自动框架：核心是新的自动机模型——同步加权树自动机（SWTA），它能紧凑而精确地刻画参数化程序产生的无限族量子态；作者引入一类换能器来建模量子门语义，并给出组合算法以构造参数化电路的换能器。验证问题被归约为 SWTA 之间的函数包含与等价检查，文中提供了相应判定过程。原型实现通过对一组具有代表性的参数化量子程序进行验证，展现出框架的表达能力与实用效率，验证时间从毫秒级到秒级不等。
We present the first fully automatic framework for verifying relational properties of parameterized quantum programs , i.e., a program that, given an input size, generates a corresponding quantum circuit. We focus on verifying input-output correctness as well as equivalence. At the core of our approach is a new automata model, synchronized weighted tree automata (SWTAs), which compactly and precisely captures the infinite families of quantum states produced by parameterized programs. We introduce a class of transducers to model quantum gate semantics and develop composition algorithms for constructing transducers of parameterized circuits. Verification is reduced to functional inclusion or equivalence checking between SWTAs, for which we provide decision procedures. Our implementation demonstrates both the expressiveness and practical efficiency of the framework by verifying a diverse set of representative parameterized quantum programs with verification times ranging from milliseconds to seconds.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2511-19897,
title = {Parameterized Verification of Quantum Circuits},
author = {Parosh Aziz Abdulla and Yu-Fang Chen and Michal Hečko and Lukáš Holík and Ondřej Lengál and Jyun-Ao Lin and Ramanathan S. Thinniyam},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776712}
}