Formalization of Quantum Intermediate Representations for Code Safety

TL;DR

This paper formalizes the definitions of Quantum Intermediate Representation (QIR) to improve correctness and security in quantum program compilation, addressing ambiguities in its natural language description.

Contribution

It provides the first formal definitions of QIR's data types and instructions, enhancing rigor and enabling error detection in quantum code.

Findings

Formal definitions enable detection of unsafe QIR code

Improves correctness and security guarantees for quantum compilation

Addresses ambiguity in natural language specifications

Abstract

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.