Offre de thèse
Langage de programmation quantique garantissant la polynomialité des circuits
Date limite de candidature
07-05-2024
Date de début de contrat
01-10-2024
Directeur de thèse
PECHOUX Romain
Encadrement
Réunions hebdomadaires entre les directeurs et le doctorant.
Type de contrat
école doctorale
équipe
MOCQUAcontexte
Les algorithmes quantiques sont habituellement représentés par des circuits quantiques [Deu89]. Cette représentation ne permet pas d'utiliser des constructions de programmation de haut-niveau telles que les types de données ou les structures de contrôle. C'est pourquoi des langages de programmation quantiques ont été proposés [Sel04]. Parmi les développements récents, [CSV23] propose un langage qui permet de programmer des programmes réversibles et linéaires. Ce langage présente des constructions pour encoder les opérations unitaires. Ces constructions permettent d'effectuer du pattern matching réversible et, de ce fait, peuvent être vues comme des formes spécifiques systèmes de réécriture de termes. Les systèmes de réécriture de termes définissent un programme via un ensemble de règles de réécriture. De nombreux travaux ont permis de certifier la terminaison et des résultats de complexité sur ces systèmes [BMM11 ; MP09]. Ces travaux utilisent des outils, appelés interprétation (quasi-interprétations, sup-interprétations) qui, combinées avec des techniques de terminaison (Recursive Path Ordering, Multiset Path Ordering), permettent de caractériser la classe des fonctions calculables en temps polynomial et celle des fonctions calculables en espace polynomial. En informatique quantique, la complexité est définie en premier lieu à l'aide de machine de Turing quantiques (QTM) ou de famille de circuits quantiques. La classe de complexité naturelle est FBQP (Bounded-error Quantum Polynomial time) qui considère les fonctions qui s'exécutent en temps polynomial sur une QTM et donnent le bon résultat dans au moins 2/3 des cas. Cette notion de complexité correspond également aux fonctions qui peuvent être réalisées par une famille uniforme de circuits quantiques dont la taille augmente polynomialement avec le nombre de qubits. Plusieurs travaux récents [Yam20 ; HPS23] ont proposé des caractérisations de FBQP basées sur des algèbres de fonctions et des langages de programmation.spécialité
Informatiquelaboratoire
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Mots clés
Informatique quantique, Complexité
Détail de l'offre
Nous chercherons à développer des analyses statiques permettant de caractériser des classes de complexité quantique comme FBQP ainsi que de déterminer les ressources (temps, nombre de qubits, ...) utilisées par un programme quantique.
Une première étape consistera à définir un langage de programmation et des contraintes sur ses programmes pour garantir que les fonctions calculées respectent les lois de la mécanique quantique : l'impossibilité de dupliquer un qubit, la réversibilité, l'unitarité des programmes.
Dans une deuxième étape, nous développerons les techniques permettant de garantir la complexité des programmes. Par exemple, en étendant les méthodes basées sur des techniques d'interprétations de programmes au cadre quantique.
Un dernier objectif consistera à certifier des propriétés de complexité des circuits quantiques obtenus par compilation des programmes. Par exemple en garantissant la polynomialité du nombre de portes quantiques utilisées par le circuit.
Keywords
Quantum Computing, Complexity
Subject details
Our aim is to develop static analyses to characterize quantum complexity classes such as FBQP, and to determine the resources (time, number of qubits, etc.) used by a quantum program. A first step will be to define a programming language and constraints on its programs to ensure that the functions computed respect the laws of quantum mechanics: the impossibility of duplicating a qubit, reversibility, program unitarity. In a second stage, we will develop techniques for guaranteeing program complexity. For example, by extending methods based on program interpretation techniques to the quantum framework. A final objective will be to certify the complexity properties of quantum circuits obtained by compiling programs. For example, by guaranteeing the polynomiality of the number of quantum gates used by the circuit.
Profil du candidat
M2 Informatique ou équivalent, compétences en informatique quantique et en méthodes formelles
Candidate profile
Quantum Computing and Formal Methods
Référence biblio
[BMM11] Guillaume Bonfante, Jean-Yves Marion et Jean-Yves Moyen. « Quasi-interpretations a way to control resources ». In : Theoretical Computer Science 412.25 (juin 2011), p. 2776-2796. issn : 0304-3975. doi : 10.1016/j.tcs.2011.02.007.
[CSV23] Kostia Chardonnet, Alexis Saurin et Benoît Valiron. « A Curry-Howard Correspondence for Linear, Reversible Computation ». In : 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). T. 252. 2023, 13:1-13:18. doi : 10.4230/LIPIcs.CSL.2023.13.
[Deu89] David Elieser Deutsch. « Quantum computational networks ». In : Proceedings of the Royal Society of London. A. Mathematical and Physical Sciences 425.1868 (1989), p. 73-90. url : https://www.jstor.org/stable/2398494.
[HPS23] Emmanuel Hainry, Romain Péchoux et Mário Silva. « A programming language characterizing quantum polynomial time ». In : Foundations of Software Science and Computation Structures (FoSSaCS 23). Paris, France, avr. 2023. doi : 10.1007/978-3-031-30829-1_8.
[MP09] Jean-Yves Marion et Romain Péchoux. « Sup-interpretations, a semantic method for static analysis of program resources ». In : ACM Transactions on Computational Logic 10.4 (août 2009), p. 1-31. issn : 1557-945X. doi : 10.1145/1555746.1555751.
[Sel04] Peter Selinger. « Towards a quantum programming language ». In : Mathematical Structures in Computer Science 14.4 (2004), p. 527-586. doi : 10.1017/S0960129504004256.
[Yam20] Tomoyuki Yamakami. « A schematic definition of quantum polynomial time computability ». In : Journal of Symbolic Logic 85.4 (2020), p. 1546-1587. doi : 10.1017/jsl.2020.45.