We present sqire, a low-level language for quantum computing and verification. sqire uses a global register of quantum bits, allowing easy compilation to and from existing `quantum assembly' languages and simplifying the verification process. We demonstrate the power of sqire as an intermediate representation of quantum programs by verifying a number of useful optimizations, and we demonstrate sqire's use as a tool for general verification by proving several quantum programs correct.
We present sqire, a low-level language for quantum computing and verification. sqire uses a global register of quantum bits, allowing easy compilation to and from existing `quantum assembly' languages and simplifying the verification process. We demonstrate the power of sqire as an intermediate representation of quantum programs by verifying a number of useful optimizations, and we demonstrate sqire's use as a tool for general verification by proving several quantum programs correct.
We present VOQC, the first fully verified optimizer for quantum circuits, written using the Coq proof assistant. Quantum circuits are expressed as programs in a simple, low-level language called SQIR, a simple quantum intermediate representation, which is deeply embedded in Coq. Optimizations and other transformations are expressed as Coq functions, which are proved correct with respect to a semantics of SQIR programs. SQIR uses a semantics of matrices of complex numbers, which is the standard for quantum computation, but treats matrices symbolically in order to reason about programs that use an arbitrary number of quantum bits. SQIR's careful design and our provided automation make it possible to write and verify a broad range of optimizations in VOQC, including full-circuit transformations from cutting-edge optimizers.
We present voqc , the first verified optimizer for quantum circuits, written using the Coq proof assistant. Quantum circuits are expressed as programs in a simple, low-level language called sqir , a small quantum intermediate representation, which is deeply embedded in Coq. Optimizations and other transformations are expressed as Coq functions, which are proved correct with respect to a semantics of sqir programs. sqir programs denote complex-valued matrices, as is standard in quantum computation, but we treat matrices symbolically to reason about programs that use an arbitrary number of quantum bits. sqir ’s careful design and our provided automation make it possible to write and verify a broad range of optimizations in voqc , including full-circuit transformations from cutting-edge optimizers.
We demonstrate the utility of the Multi-Level Intermediate Representation (MLIR) for quantum computing. Specifically, we extend MLIR with a new quantum dialect that enables the expression and compilation of common quantum assembly languages. The true utility of this dialect is in its ability to be lowered to the LLVM intermediate representation (IR) in a manner that is adherent to the quantum intermediate representation (QIR) specification recently proposed by Microsoft. We leverage a qcor-enabled implementation of the QIR quantum runtime API to enable a retargetable (quantum hardware agnostic) compiler workflow mapping quantum languages to hybrid quantum-classical binary executables and object code. We evaluate and demonstrate this novel compiler workflow with quantum programs written in OpenQASM 2.0. We provide concrete examples detailing the generation of MLIR from OpenQASM source files, the lowering process from MLIR to LLVM IR, and ultimately the generation of executable binaries targeting available quantum processors.
Quantum Intermediate Representation (QIR) is a Microsoft-developed, LLVM-based intermediate representation for quantum program compilers. QIR aims to provide a general solution for quantum program compilers independent of front-end languages and back-end hardware, thus avoiding duplicate development of intermediate representations and compilers. Since it is still under development, QIR is described in natural language and lacks a formal definition, leading to ambiguity in its interpretation and a lack of rigor in implementing quantum functions. In this paper, we provide formal definitions for the data types and instruction sets of QIR, aiming to provide correctness and security guarantees for operations and intermediate code conversions in QIR. To validate our design, we show some samples of unsafe QIR code where errors can be detected by our formal approach.
In this survey, there is a systematic assessment of the existing plans of manufacturing Quantum.Their ability to make Intermediate Representations (QIRs) sell optimization solutions to problems, plasticity in the both hardware and verification.We survey the existent methodologies and identify them in four waves, i.e. language-derived paradigm, multi-level paradigm, classically-quantum and hybrid classicalquantum paradigm and hybrid formally verified and verify their performance in some major parameters, i.e., circuit depth reduction, compilation transversal and cross-operating system portability.We find that the optimal compromise of performance and reliability is realised on hybrid systems that combine classical Compiler with extensions supporting quantum, in which current tools (note that we are not exist and future designs, which implement quantum provide technology at the center of the research significant enhancement of optimization ability and black box testing of the verification suite.Nevertheless, essential there are problems within the development of the new quantum paradigms supporter, temporal optimization and error correction incorporation.An outlook is provided at the end of the paper on the creation of next generation QIR with a special emphasis on the need to have verifiable, quantifiable frameworks that maintain optimization at the various levels transparent.This paper can be used as are source on both the technical community designing quantum compilers in addition to a roadmap that researchers should pursue in this various area of QIR.
We present a multilevel quantum–classical intermediate representation (IR) that enables an optimizing, retargetable compiler for available quantum languages. Our work builds upon the multilevel intermediate representation (MLIR) framework and leverages its unique progressive lowering capabilities to map quantum languages to the low-level virtual machine (LLVM) machine-level IR. We provide both quantum and classical optimizations via the MLIR pattern rewriting subsystem and standard LLVM optimization passes, and demonstrate the programmability, compilation, and execution of our approach via standard benchmarks and test cases. In comparison to other standalone language and compiler efforts available today, our work results in compile times that are 1,000× faster than standard Pythonic approaches, and 5–10× faster than comparative standalone quantum language compilers. Our compiler provides quantum resource optimizations via standard programming patterns that result in a 10× reduction in entangling operations, a common source of program noise. We see this work as a vehicle for rapid quantum compiler prototyping.