Doctorant – Raisonnement graphique et tolérant aux fautes en informatique quantique

Type de contrat : CDD Contexte et atouts du poste 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. Après une phase d'étude des NISQ (Noisy intermediate scale quantum devices), les efforts de la communauté scientifique se portent aujourd'hui naturellement vers l'étude du calcul quantique tolérant aux fautes, avec comme ligne de mire des premières machines capables de correction d'erreurs dans un futur proche. Il s'agit d'une étape essentielle dans le développement d'un ordinateur quantique à grande échelle. Dans ce contexte, le développement de la pile quantique, et plus généralement du logiciel quantique, est crucial. Les représentations les plus couramment utilisées en informatique quantique sont les circuits quantiques. En effet, ils 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. Mission confiée Plusieurs tâches liées aux logiciels quantiques, telles que l'optimisation du code 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 ont été prouvées complètes, c'est-à-dire qu'elles capturent l'équivalence des circuits quantiques [4, 3, 2, 8]. Diverses variantes et raffinements des circuits quantiques, tels que les calculs ZX [5, 12, 11, 13, 14], et ZH [1], ont été introduits et se sont révélés être des cadres utiles pour le raisonnement et l'optimisation des circuits [9, 16, 19]. L'équipe Mocqua a activement contribué à ces développements. L'objectif de cette thèse est de développer ces techniques de raisonnement graphique dans le cadre du calcul tolérant aux fautes. De premiers travaux ont montré que certaines règles du ZX-calcul préservent les propriétés de tolérance aux fautes [17, 18], d'autres travaux montrent que le ZX-calcul est un langage permettant la description de codes correcteurs d'erreurs [10, 7, 6, 15]. Références [1] Miriam Backens and Aleks Kissinger. Zh: A complete graphical calculus for quantum computations involving classical non-linearity. https:// arxiv.org/abs/1805.02175, 2018. arXiv preprint arXiv:1805.02175. [2] Alexandre Clément, Noé Delorme, and Simon Perdrix. Minimal equational theories for quantum circuits. In Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’24, New York, NY, USA, 2024. Association for Computing Machinery. [3] Alexandre Clément, Noé Delorme, Simon Perdrix, and Renaud Vilmart. Quantum circuit completeness: Extensions and simplifications. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 2024. [4] Alexandre Clément, Nicolas Heurtel, Shane Mansfield, Simon Perdrix, and Benoit Valiron. A complete equational theory for quantum circuits. In 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–13. IEEE, 2023. [5] Bob Coecke and Ross Duncan. Categorical algebra and diagrammatics. 13(4):043016, apr 2011. Interacting quantum observables: New Journal of Physics, [6] Niel de Beaudrap, Ross Duncan, Dominic Horsman, and Simon Perdrix. Pauli fusion: a computational model to realise quantum transformations from zx terms. arXiv preprint arXiv:1904.12817, 2019. [7] Niel de Beaudrap and Dominic Horsman. The zx-calculus is a language for surface code lattice surgery. Quantum, 4:218, 2020. [8] Noé Delorme and Simon Perdrix. Diagrammatic reasoning with control as a constructor, applications to quantum circuits, 2026. [9] Ross Duncan, Aleks Kissinger, Simon Perdrix, and John Van De Wetering. Graph-theoretic simplification of quantum circuits with the ZX- calculus. Quantum, 4:279, 2020. [10] Ross Duncan and Maxime Lucas. Verifying the Steane code with quantomatic. arXiv preprint arXiv:1306.4532, 2013. [11] Amar Hadzihasanovic, Kang Feng Ng, and Quanlong Wang. Two complete axiomatisations of pure-state qubit quantum computing. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, pages 502–511, New York, NY, USA, 2018. ACM. [12] Emmanuel Jeandel, Simon Perdrix, and Renaud Vilmart. A complete axiomatisation of the ZX-calculus for Clifford+T quantum mechanics. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science LICS, 2018. [13] Emmanuel Jeandel, Simon Perdrix, and Renaud Vilmart. Diagrammatic reasoning beyond Slifford+t quantum mec