High-level descriptions of quantum algorithms do not take the restrictions of physical hardware into account. Therefore actually executing an algorithm in the form of a quantum circuit on a quantum computer requires compiling it for the desired target architecture first. The compilation of quantum circuits depends on efficient methods to be feasible for all but the trivial instances. To this end, different compiling methods have been introduced in the past, but room for improvement still exists. Moreover, just an efficient compilation process itself is not sufficient-the resulting circuits must be correct as well. In this summary paper, we review how existing compilation approaches can be optimized by utilizing heuristic search algorithms or exact reasoning engines. Furthermore, we review how the correctness of the obtained results can be verified afterwards by clever data structures such as decision diagrams. This illustrates core steps of a compilation flow which can generate minimal or close-to-minimal results for many instances and, additionally, guarantees correctness throughout the process.
High-level descriptions of quantum algorithms do not take the restrictions of physical hardware into account. Therefore actually executing an algorithm in the form of a quantum circuit on a quantum computer requires compiling it for the desired target architecture first. The compilation of quantum circuits depends on efficient methods to be feasible for all but the trivial instances. To this end, different compiling methods have been introduced in the past, but room for improvement still exists. Moreover, just an efficient compilation process itself is not sufficient-the resulting circuits must be correct as well. In this summary paper, we review how existing compilation approaches can be optimized by utilizing heuristic search algorithms or exact reasoning engines. Furthermore, we review how the correctness of the obtained results can be verified afterwards by clever data structures such as decision diagrams. This illustrates core steps of a compilation flow which can generate minimal or close-to-minimal results for many instances and, additionally, guarantees correctness throughout the process.
Realizing a conceptual quantum algorithm on an actual physical device necessitates the algorithm's quantum circuit description to undergo certain transformations in order to adhere to all constraints imposed by the hardware. In this regard, the individual high-level circuit components are first synthesized to the supported low-level gate-set of the quantum computer, before being mapped to the target's architecture-utilizing several optimizations in order to improve the compilation result. Specialized tools for this complex task exist, e.g., IBM's Qiskit, Google's Cirq, Microsoft's QDK, or Rigetti's Forest. However, to date, the circuits resulting from these tools are hardly verified, which is mainly due to the immense complexity of checking if two quantum circuits indeed realize the same functionality. In this paper, we propose an efficient scheme for quantum circuit equivalence checking-specialized for verifying results of the IBM Qiskit quantum circuit compilation flow. To this end, we combine characteristics unique to quantum computing, e.g., its inherent reversibility, and certain knowledge about the compilation flow into a dedicated equivalence checking strategy. Experimental evaluations confirm that the proposed scheme allows to verify even large circuit instances with tens of thousands of operations within seconds or even less, whereas state-of-the-art techniques frequently time-out or require substantially more runtime. A corresponding open source implementation of the proposed method is publicly available at https://github.com/iic-jku/qcec.
Quantum circuit compilation is a crucial step in translating high-level quantum algorithms into executable quantum circuits on specific hardware. The complexity and potential for errors within this process necessitate rigorous verification methods. This paper proposes a novel approach leveraging symbolic execution to formally verify quantum circuit compilation. We represent quantum circuits and compilation steps as a symbolic program, enabling the exploration of all possible compilation paths. By incorporating quantum gate fidelities and noise models into the symbolic execution engine, we can identify potential errors in the compilation logic, providing a robust and systematic way to ensure the correctness of the compilation process. The core claim is that symbolic execution can be extended to formally verify the correctness of quantum circuit compilation processes. This work addresses a critical need in quantum computing, offering a new technique for building trust and reliability into quantum software.
Quantum circuit compilation is a crucial step in the realization of quantum computation, transforming high-level quantum algorithms into gate-level operations executable on specific quantum hardware. However, this process is inherently complex and susceptible to errors, including gate decomposition errors, qubit mapping errors, and resource allocation errors. These errors can significantly degrade the fidelity of the final computation. This paper proposes and investigates the application of formal verification techniques to guarantee the correctness of quantum circuit compilation. We demonstrate how model checking and formal methods can be applied to rigorously verify that the compilation algorithm adheres to predefined constraints, such as preserving quantum properties like unitary evolution and qubit orthogonality. The core claim is that formal verification offers a robust solution to the challenges of detecting and preventing errors in quantum compilation. The proposed approach significantly advances the reliability and trustworthiness of quantum computing by providing a rigorous method for ensuring compilation accuracy. We outline a framework for applying these techniques, focusing on key constraints and illustrating their application through a simplified compilation scenario.
Quantum computing capabilities have developed rapidly in the last years, both in terms of experimental control of quantum systems and theoretical knowledge of quantum algorithms. During this time, the field has progressed from few-qubit prototypes to small computers that can do non-trivial calculations. In a few cases, these calculations approach the current limits of what classical computers can achieve. At this point in time, it is critical to get the maximal performance out of the available quantum hardware, which requires practical applications, smart algorithms, error mitigation and powerful decoding strategies. One near-term application of these quantum devices is quantum optimization, which utilizes quantum computers to solve combinatorial optimization problems. The way these problems are encoded on the quantum device is crucial and often requires both hardware-independent as well as hardware-specific ideas. A core part of this process is compilation, which translates the high-level quantum algorithm to instructions that can be executed on the physical quantum computer. In this thesis we focus on a specific kind of compilation, which originates from the Lechner-Hauke-Zoller model. We present the parity architecture, which is a hardware-independent way to compile arbitrary combinatorial optimization problems to quantum systems. With the parity architecture, analog and digital quantum algorithms can be executed using only local interactions, at the cost of a qubit overhead. First, we introduce a mathematical framework for the parity compiler using linear algebra and give some practical examples. This framework also allows the encoding of higher-order interactions directly, without the need to convert them to quadratic terms. We then benchmark the resource requirements of the parity architecture for digital algorithms, comparing against standard methods that use qubit routing. After that, we show how to compile for digital quantum devices with arbitrary connectivity. Here, we relax the condition that the interactions in the parity architecture are all completely local, resulting in a more flexible compilation approach. Finally, we show that parity compilation can be done constructively for any optimization problem at the cost of a qubit overhead. This qubit overhead can then be minimized by performing a search through different configurations.
Executing quantum circuits on currently available quantum computers requires compiling them to a representation that conforms to all restrictions imposed by the targeted architecture. Due to the limited connectivity of the devices' physical qubits, an important step in the compilation process is to map the circuit in such a way that all its gates are executable on the hardware. Existing solutions delivering optimal solutions to this task are severely challenged by the exponential complexity of the problem. In this paper, we show that the search space of the mapping problem can be limited drastically while still preserving optimality. The proposed strategies are generic, architecture-independent, and can be adapted to various mapping methodologies. The findings are backed by both, theoretical considerations and experimental evaluations. Results confirm that, by limiting the search space, optimal solutions can be determined for instances that timeouted before or speed-ups of up to three orders of magnitude can be achieved.
Quantum circuit compilation is a crucial step in the process of executing quantum algorithms on near-term quantum hardware. The challenge lies in translating high-level quantum algorithms, often expressed using universal gate sets, into efficient, gate-level circuits that minimize gate count and circuit depth, thereby reducing error rates and improving execution times. Traditional compilation methods often rely on hand-crafted heuristics or limited search algorithms, failing to fully explore the exponentially large search space of possible circuit transformations. This work proposes an adaptive quantum circuit compilation framework leveraging Bayesian optimization. The system dynamically explores the space of potential circuit transformations, learning to identify optimal compilation strategies through a probabilistic modeling approach. The core claim is that Bayesian optimization can effectively adaptively compile quantum circuits, optimizing for performance and minimizing gate count. The system incorporates a compiler that utilizes Bayesian optimization to explore the vast space of possible quantum circuit transformations, learning to identify the most efficient compilation strategies. The results demonstrate the potential of this approach to significantly reduce the complexity of quantum circuits while maintaining algorithm fidelity.