Raisonner et Optimiser des Circuits Quantiques

Mots clés

Informatique quantique, Circuits quantiques

Détail de l'offre

Les récentes avancées dans le domaine de l'informatique quantique nous permettent d'espérer que les avantages informatiques majeurs promis par l'informatique quantique seront mis en œuvre à moyen terme. Dans ce contexte, le développement de la pile quantique et plus généralement du software quantique est crucial. Les représentations les plus couramment utilisées de l'informatique quantique sont les circuits quantiques. En effet, les circuits quantiques sont fondamentaux pour l'informatique quantique, car ils fournissent une représentation de bas niveau des programmes quantiques et constituent le principal moyen de représenter les algorithmes quantiques. La plupart des langages de programmation quantique sont essentiellement des langages de description de circuits quantiques.
Plusieurs tâches liées aux logiciels quantiques, telles que l'optimisation du code, l'adaptation des algorithmes à des contraintes spécifiques (comme la disposition des qubits dans la mémoire d'un ordinateur quantique) ou la vérification des algorithmes, sont nécessaires au développement d'un ordinateur quantique. Ces tâches ne sont rien d'autre que des transformations de circuits qui peuvent être formalisées par une théorie équationnelle décrivant comment les circuits peuvent être transformés en circuits équivalents.
Plusieurs théories équationnelles ont été développées récemment pour les circuits quantiques, et il a été prouvé qu'elles étaient complètes, c'est-à-dire qu'elles capturaient l'équivalence des circuits quantiques. Diverses variantes et raffinements des circuits quantiques, tels que les calculs ZX, ZW et ZH, ont été introduits et se sont révélés être des cadres utiles pour le raisonnement et l'optimisation des circuits. L'équipe Mocqua a activement contribué à ces développements.
Alors qu'il a été prouvé que les circuits quantiques sont complets pour les circuits quantiques agissant sur des qubits, l'existence d'une théorie équationnelle complète pour un cadre plus général comme les qudits, ou des fragments intéressants, comme les Cliffors+T, reste ouverte.
Le premier objectif de la thèse est de développer une telle théorie équationnelle pour les systèmes qudits. Après l'introduction d'une théorie équationnelle solide, le candidat se concentrera sur une preuve de complétude. Le candidat envisagera ensuite le développement de techniques d'optimisation basées sur de telles théories équationnelles.
Au cours de la première année, le candidat se familiarisera avec le formalisme des circuits quantiques, les langages graphiques et l'approche catégorielle de l'informatique quantique. Le candidat développera également des théories équationnelles provisoires pour les systèmes quantiques et travaillera sur leur preuve de complétude. A partir de la deuxième année, des extensions et des applications à l'optimisation de circuits et/ou à la satisfaction de contraintes de cartographie seront explorées. Le candidat validera également ses résultats par des preuves et des concepts et contribuera au développement d'outils académiques et de logiciels pour le raisonnement et l'optimisation de circuits quantiques.
Le doctorant rejoindra l'équipe Mocqua, située au Centre Inria de l'Université de Lorraine, et collaborera directement avec ses directeurs de thèse Miriam Backens et Simon Perdrix.