iQbricks: integration of a fully-featured quantum language in the framework Qbricks

Abstract

Quantum Computing has noticeably grown over the last two decades, making it a revolu tionary field of investigation in the current era of technological research. Such a growth has been leading to an increasing demand in research by several big enter prises such as IBM, Google and Microsoft, paving the way for a richer ecosystem and untold benefits among the Quantum Computing community. Verification is a crucial aspect of software development, as it ensures that a program per forms as intended and reduces the risk of introducing errors. This is especially important in the field of Quantum Computing, where the complexity of programs is high and the behavior of quantum systems is often counterintuitive. Verification of quantum programs can help detect errors that may lead to incorrect results, which is of utmost importance when dealing with quantum algorithms and quantum simulations. As a result, having a formal verification framework for quantum programs can greatly benefit the development of reliable and accurate quantum software. Qbricks is a verification framework for building quantum programs, and corresponds to the framework on which this project has been integrated. During the course of this thesis, iQbricks – an intuitive and user-friendly language to build and formally verify quantum programs – was developed, along with a framework to translate and generate verifiable Qbricks programs from iQbricks. This project’s main achievements were: (1) the design and implementation of a high-level programming language for describing quantum circuits in an intuitive and user-friendly way and (2) the implementation of a translator, embedded in Qbricks’ framework, that converts iQbricks programs to Qbricks ones. The developed framework was evaluated against two different quantum algorithms: the Quantum Fourier Transform and Grover’s algorithm. This project was accompanied by an internship at the Commissariat à l’énergie atomique et aux énergies alternatives (CEA) - LSL, where this implementation was developed in direct involvement with Qbricks’ team of investigators.

A Computação Quântica cresceu de forma notável nas últimas duas décadas, tornando-se um campo revolucionário de investigação na atual era da investigação tecnológica. Tal crescimento tem levado a uma crescente procura na investigação por parte de várias grandes empresas como a IBM, Google e Microsoft, abrindo caminho para um ecossistema mais rico e benefícios inéditos entre a comunidade da Computação Quântica. A verificação é um aspecto crucial no desenvolvimento de software, pois garante que um programa execute conforme o previsto e reduz o risco de introduzir erros. Isso é especialmente importante no campo da computação quântica, onde a complexidade dos programas é alta e o comportamento dos sistemas quânticos é frequentemente contra-intuitivo. A verificação de programas quânticos pode ajudar a detectar erros que possam levar a resultados incorretos, o que é de extrema importância ao lidar com algoritmos quânticos e simulações quânticas. Como resultado, ter um framework de verificação formal para programas quânticos pode beneficiar grandemente o desenvolvimento de software quântico confiável e preciso. Qbricks é uma estrutura de verificação para a construção de programas quânticos, e corresponde à estrutura sobre a qual este projecto foi integrado. Durante o curso desta tese, foi desenvolvida iQbricks - uma linguagem intuitiva e de fácil utilização para construir e verificar formalmente programas quânticos - juntamente com uma ferramenta para traduzir e gerar programas Qbricks verificáveis a partir de iQbricks. As principais concretizações deste projecto foram: (1) a concepção e implementação de uma linguagem de programação de alto nível para descrição de circuitos quânticos de uma forma intuitiva e de fácil utilização e (2) a implementação de um tradutor, embutido em Qbricks, que converte programas iQbricks para Qbricks. A ferramenta desenvolvida foi testada utilizando dois algoritmos quânticos diferentes: o Transformada de Fourier Quântica (QFT) e algoritmo de Grover. Este projecto foi acompanhado por um estágio no Commissariat à l’énergie atomique et aux énergies alternatives (CEA) - LSL, onde esta implementação foi desenvolvida em colaboração direta com a equipa de investigadores de Qbricks.