This paper presents a novel approach for minimizing the number of teleportations in Distributed Quantum Computing (DQC) using formal methods. Quantum teleportation plays a major role in communicating quantum information. As such, it is desirable to perform as few teleportations as possible when distributing a quantum algorithm on a network of quantum machines. Contrary to most existing methods which rely on graph-theoretic or heuristic search techniques, we propose a drastically different approach for minimizing the number of teleportations through utilizing formal methods. Specifically, the contributions of this paper include: the formal specification of the teleportation minimization problem in Alloy, the generalizability of the proposed Alloy specifications to quantum circuits with $n$-ary gates, the reusability of the Alloy specifications for different quantum circuits and networks, the simplicity of specifying and solving other problems such as load balancing and heterogeneity, and the compositionality of the proposed approach. We also develop a software tool, called qcAlloy, that takes as input the textual description of a quantum circuit, generates the corresponding Alloy model, and finally solves the minimization problem using the Alloy analyzer. We have experimentally evaluated qcAlloy for some of the circuits in the RevLib benchmark with more than 100 qubits and 1200 layers, and have demonstrated that qcAlloy outperforms one of the most efficient existing methods for most benchmark circuits in terms of minimizing the number of teleportations.

翻译：本文提出了一种利用形式化方法最小化分布式量子计算（DQC）中量子隐形传态次数的新方法。量子隐形传态在量子信息通信中起着关键作用，因此在量子机器网络上分布量子算法时，尽可能减少隐形传态次数具有重要价值。与大多数依赖图论或启发式搜索技术的现有方法不同，我们提出了一种截然不同的形式化优化方法。具体而言，本文的贡献包括：在Alloy中形式化定义了隐形传态最小化问题；提出的Alloy规范可推广至含n元门的量子电路；该Alloy规范适用于不同量子电路与网络结构；能够简便地描述并求解负载均衡与异构性等其他问题；以及所提方法具有组合性。我们开发了名为qcAlloy的软件工具，该工具接收量子电路的文本描述，生成对应的Alloy模型，最终通过Alloy分析器求解最小化问题。针对RevLib基准测试中部分包含超过100个量子比特和1200层的电路，我们实验评估了qcAlloy的性能，结果表明，在最小化隐形传态次数方面，qcAlloy对大多数基准电路的优化效果优于效率最高的现有方法之一。