Compilation and Verification of Quantum Software in the Noisy and Approximate Regime

Like classical computers, quantum computers need compilers, which are tools that translate code written by a human into something the machine can run. Unlike classical computers, today's quantum computers have extremely limited computational resources and are highly susceptible from noise from the environment. Furthermore, it is often impractical or impossible to implement a computation exactly, meaning quantum compilers need to make certain approximations, which can yield further errors. 

In this project, we will develop the next generation of quantum compilers which are able to understand, and tame, these many sources of errors, and produce efficient software with independently checkable guarantees of reliable performance. 

The proposed work addresses two objectives: 

• Verifiable quantum circuit optimisation 
• Verifiable compilation of Hamiltonians for quantum simulation 

Both of these objectives aim to produce better quantum compilers, and ultimately extend the capabilities of existing and near-future quantum hardware, by taking into account sophisticated hardware error models of specific platforms as well as hardware constraints such as qubit connectivity and native gatesets. In addition to accounting for hardware sources of error, these techniques will account for deliberate sources of error, i.e. approximations, introduced by the compilation process itself, and the project will explore ways to trade off hardware vs software errors. 

By adopting a methodology based on rigorous, composable transformations of quantum computations, such compilers can produce scalable, trustworthy software to drive quantum computers.