Minimizing the Number of Teleportations in Distributed Quantum Computing Using Alloy

TL;DR

This paper introduces a formal methods-based approach using Alloy to minimize teleportations in Distributed Quantum Computing, offering a reusable, scalable solution that outperforms existing heuristics on large quantum circuits.

Contribution

It formalizes the teleportation minimization problem in Alloy, develops a versatile tool (qcAlloy), and demonstrates superior performance on large quantum circuits compared to existing methods.

Findings

qcAlloy reduces teleportations more effectively on benchmark circuits

The Alloy-based approach is generalizable to various quantum circuits and networks

The method outperforms existing heuristics in minimizing teleportations

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.