Minimizing the Number of Teleportations in Distributed Quantum Computing Using Alloy

TL;DR

Minimizing teleportations in Distributed Quantum Computing is essential due to decoherence and resource costs. The authors propose a formal Alloy-based framework and the qcAlloy tool to specify and solve the Teleportation Minimization Problem (TMP), generalizing to circuits with $n$-ary gates and enabling reusable, compositional problem solving. qcAlloy translates machine-readable circuit descriptions into Alloy models, applies SAT-based verification, and can partition large circuits into subproblems to manage complexity. Experimental results on RevLib benchmarks show qcAlloy often reduces teleportations by up to 50% compared with a leading heuristic, while highlighting challenges for certain circuit structures like QFT. The work emphasizes reuse, extensibility to heterogeneous networks, and a path toward a public repository of formal specs for DQC compilation and optimization.

Abstract

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.

Figures (8)

• Figure 1: A vision for the mapping of QAs to quantum networks.
• Figure 2: Abstracting circuit (a) as the circuit graph (b).
• Figure 3: Circuit 1 with binary gates and depth 10.
• Figure 4: Three consecutive layers of a solution generated by Alloy. Arrows represent the binary relations.
• Figure 5: Circuit 2 with 4-ary gates and depth 22.