论文标题
用ZX-Calculus对量子电路进行等效检查
Equivalence Checking of Quantum Circuits with the ZX-Calculus
论文作者
论文摘要
由于最先进的量子计算机能够运行越来越复杂的算法，因此需要自动化方法设计和测试潜在应用程序的需求上升。量子电路的等效检查是量子软件堆栈开发的重要但几乎没有自动化的任务。最近，已经提出了新的方法，可以从广泛不同的角度解决这个问题。其中之一是基于ZX-Calculus，这是一种用于量子计算的图形重写系统。但是，几乎没有探索这种等价检查方法的功率和能力。这项工作的目的是评估ZX-Calculus作为等效检查量子电路的工具。为此，可以展示如何扩展基于ZX-calculus的等效检查方法，以验证编译流的结果和对量子电路的优化。还表明，基于ZX-Calculus的方法不是完成$ \ unicode {x2014} $，尤其是对于具有辅助量子的量子电路。为了正确评估所提出的方法，我们通过将其与其他两种等效检查的最先进的方法进行比较，进行了详细的案例研究：一种基于路径 - 和基于决策图的方法。所提出的方法已集成到公开可用的QCEC工具（https://github.com/cda-tum/qcec）中，该方法是慕尼黑量子工具包（MQT）的一部分。
As state-of-the-art quantum computers are capable of running increasingly complex algorithms, the need for automated methods to design and test potential applications rises. Equivalence checking of quantum circuits is an important, yet hardly automated, task in the development of the quantum software stack. Recently, new methods have been proposed that tackle this problem from widely different perspectives. One of them is based on the ZX-calculus, a graphical rewriting system for quantum computing. However, the power and capability of this equivalence checking method has barely been explored. The aim of this work is to evaluate the ZX-calculus as a tool for equivalence checking of quantum circuits. To this end, it is demonstrated how the ZX-calculus based approach for equivalence checking can be expanded in order to verify the results of compilation flows and optimizations on quantum circuits. It is also shown that the ZX-calculus based method is not complete$\unicode{x2014}$especially for quantum circuits with ancillary qubits. In order to properly evaluate the proposed method, we conduct a detailed case study by comparing it to two other state-of-the-art methods for equivalence checking: one based on path-sums and another based on decision diagrams. The proposed methods have been integrated into the publicly available QCEC tool (https://github.com/cda-tum/qcec) which is part of the Munich Quantum Toolkit (MQT).
