[Thèse] Langage diagrammatique pour l’ordinateur quantique

Langage diagrammatique pour  l’ordinateur quantique

Encadrement : Simon Perdrix (simon.perdrix@loria.fr), Emmanuel Jeandel (emmanuel.jeandel@loria.fr)

Lieu : Loria (équipe Mocqua), Nancy

description du sujet [pdf]

Contexte

L’informatique quantique est un sujet de recherche en plein essor. Un traitement quantique de l’information permet en théorie de résoudre certains problèmes informatiques hors de portée des ordinateurs classiques. Les annonces de Google, le flagship européen sur les technologies quantique, les programmes britannique (NQIT) et néerlandais (QuTech) ainsi que la commercialisation de nouvelles machines quantiques par la société D-Wave, démontrent que l’informatique quantique est en train d’entrer dans une nouvelle ère. L’émergence de machines quantiques est très prometteuse, mais ouvre aussi des nouvelles problématiques concrètes comme la programmation et la vérification quantique de ces machines. En effet, les machines quantiques commercialisées aujourd’hui sont-elles véritablement quantiques ? Peut-on les simuler efficacement avec un ordinateur classique ? L’émergence de l’ordinateur quantique doit aussi être accompagnée de langages de programmation adaptés. Le développement d’outils et de méthodes formelles permettant la vérification et l’utilisation de machines quantiques est donc essentiel dans le développement de l’ordinateur quantique.

Le ZX-calculus est un puissant langage graphique pour l’informatique quantique. Le ZX-calculus a de multiples applications en théorie de l’information quantique : codes correcteurs d’erreurs quantiques, calcul par mesures, mais aussi questions fondamentales de mécanique quantique.

Objectifs

Le ZX-calculus est un langage de diagrammes, muni d’une puissante théorie équationnelle qui permet de décider si deux diagrammes représentent la même évolution quantique. Cependant décider si deux diagrammes sont équivalents peut nécessiter un grand nombre d’étapes de calcul.

  •  Le premier objectif sera de développer des techniques permettant de donner des conditions nécessaires à l’équivalence de diagrammes, basées par exemples sur des invariants, ou des évaluations aléatoires des diagrammes.
  • Le deuxième objectif sera de développer des algorithmes permettant d’éva\-luer et de simuler efficacement des diagrammes du ZX-calculus et aussi d’identifier des familles de diagrammes pour lesquels le calcul de la sémantique peut être efficace, par exemple en utilisant des propriétés structurelles comme la largeur arborescente.
  • Enfin, les points précédents seront également aborder dans le cas où les diagrammes sont paramétrés par des variables: à quelle condition peut on peut-on réduire le problème au cas sans variables ?

Les résultats théoriques de ces trois points seront implémentés et intégrés à l’outil Quantomatic, un assistant de preuve diagrammatique.

En ce moment

Colloquium Loria 2018

Exposés précédents

Logo du CNRS
Logo Inria
Logo Université de Lorraine