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.

翻译：我们提出了一种用于分析和发现量子电路中缺陷的新范式。在该方法中，问题由三元组 $\{P\}\,C\,\{Q\}$ 表述，即给定电路 $C$ 输入上的一组量子态 $P$，输出上的量子态集合是否等于（或包含于）集合 $Q$。虽然此范式不适用于指定量子电路的功能正确性等场景，但足以检测量子电路中的众多缺陷。我们提出了一种基于树自动机的技术，以紧凑方式表示量子态集合，并开发了转换器来实现量子门在该表示上的语义。该技术采用量子态的代数形式进行计算，避免了浮点数运算带来的不精确性。我们将此方法实现为原型工具，并基于文献中的多种基准对其性能进行了评估。评估表明该方法具有良好的可扩展性：例如，我们成功验证了包含40个量子比特和141,527个门的大规模电路，或检测到注入到含320个量子比特和1,758个门的电路中的缺陷（所有对比工具均未成功）。此外，本工作建立了量子程序验证与自动机之间的关联，为在量子计算世界中利用自动机理论的丰富内涵及基于自动机的验证方法开辟了新可能。