Soutenance de thèse
Jérome Ricciardi
Titre : Vérification pratique de transformations de circuits quantiques
Date : jeudi 4 juin 2026
Heure : 14h00, heure de Paris (CEST)
Statut légal : soutenance publique
Langue : anglais
Format : 45 minutes de présentation, suivies des questions
Lieu : École normale supérieure Paris-Saclay, salle 1Z61
Adresse : 4 avenue des Sciences, 91190 Gif-sur-Yvette, France
Inscription
Pour des raisons d'organisation, l'ENS a besoin de connaître la liste des personnes présentes à la soutenance. L'inscription me permet aussi d'estimer le nombre de personnes présentes au pot.
Visio soutenance : TODO lien de visioconférence pour le public
Visio jury : TODO lien réservé aux membres du jury
Cadre institutionnel
- Établissement délivrant le diplôme : Université Paris-Saclay
- École doctorale : STIC - Sciences et Technologies de l'Information et de la Communication
- Unités de recherche : LMF et LSL
- Directeur de thèse : Benoît Valiron, LMF
- Encadrant CEA : Christophe Chareton, CEA-List
Résumé
L'informatique quantique, qui repose sur les principes de la physique quantique, promet des gains significatifs en termes de puissance de calcul. Cependant, elle introduit de nouveaux défis, notamment pour la vérification de programmes. En effet, les techniques de vérification classiques ne s'appliquent pas directement à l'informatique quantique. Cela s'explique principalement par l'utilisation de la mémoire quantique (unité d'information non standard) et de son opération de mesure, qui est le seul moyen de récupérer une information à partir d'un bit quantique et introduit un aspect probabiliste.
Dans cette thèse, nous nous concentrons sur le modèle de calcul quantique par circuits et sur un aspect pratique de ce modèle : les transformations de circuit. Un circuit quantique peut être purement quantique (circuit unitaire) ou inclure du contrôle classique et de la mesure (circuit hybride). Les transformations de circuits se produisent tout au long du processus de calcul quantique, qu'il s'agisse de compiler un circuit décrit dans un langage de haut niveau vers un langage de bas niveau, d'optimiser un circuit pour un matériel particulier (transpilation), de changer de modèle de calcul (one-way measurement), ou de transférer un état quantique (téléportation).
Chacune de ces transformations peut altérer le comportement du circuit ; nous avons donc besoin d'outils permettant de vérifier sa préservation. Mais la plupart des outils actuels sont limités au cas unitaire, donc limités à vérifier des transformations qui ne changent pas le type de circuit: un circuit unitaire est transformé en circuit unitaire. Et ceux qui s'aventurent dans le cas hybride sont limités à l'hybridation : un circuit unitaire est transformé en un circuit hybride. Alors que le vrai défi survient lors de l'introduction de fils auxiliaires, tels que les ancillas, ou les discards, car il faut s'assurer que ces fils auxiliaires n'affectent pas les autres.
Pour vérifier un circuit, plusieurs techniques existent (simulation, exécution symbolique, preuve), qui diffèrent par leur automatisation et leur scalabilité. La simulation, bien qu'automatisable, manque de scalabilité. L'exécution symbolique, automatisable, passe mieux à l'échelle. La preuve, insensible à l'échelle, est difficile à automatiser. Nous avons ainsi opté pour la preuve et pour l'exécution symbolique. Nous avons utilisé la preuve pour certifier une passe de compilation d'un langage de haut niveau vers un langage de bas niveau. Et l'exécution symbolique, en développant un outil de vérification d'équivalence de circuits hybrides avec discard.
Pour nous aider dans la preuve, nous avons utilisé l'outil de preuve semi-automatique Qbricks, capable de prouver des circuits unitaires paramétrés basés sur les sommes de chemins, un formalisme permettant une modélisation compacte et encodable des circuits.
En préalable au développement de notre outil de vérification de circuits hybrides avec discard, nous avons défini des relations d'équivalence partielles pour les circuits unitaires, ainsi qu'un mécanisme pour étendre les outils de vérification unitaires aux circuits hybrides. La combinaison de ces deux composants permet de traiter les circuits hybrides avec discard.
Pour évaluer notre approche, nous avons implémenté dans l'outil SQbricks nos relations d'équivalence ainsi que notre mécanisme d'extension des outils limités aux unitaires. Nous avons démontré que les outils unitaires étendus au cas hybride sans discard surpassent, pour la plupart, largement l'état de l'art. Et qu'avec l'ajout d'un test de séparation au niveau unitaire, nous pouvons traiter des classes beaucoup plus vastes.
Jury
- Miriam Backens - membre du jury, LORIA
- Sylvie Boldo - membre du jury, Inria
- Aleks Kissinger - rapporteur, University of Oxford
- Alessandra Di Pierro - rapporteure, University of Verona
Accès
La soutenance aura lieu à l'École normale supérieure Paris-Saclay, salle 1Z61, 4 avenue des Sciences, 91190 Gif-sur-Yvette.
Depuis Paris, prendre le RER B direction Saint-Rémy-lès-Chevreuse jusqu'au Guichet, puis le bus 9108 ou 4609 jusqu'à l'arrêt Moulon. Il est aussi possible de prendre le RER B ou le RER C jusqu'à Massy-Palaiseau, puis le bus 4606 ou 91.06B jusqu'à Moulon.
Après la soutenance
Un pot sera prévu après la soutenance dans la salle de billard du bâtiment 650. Ouvrir dans Google Maps
Plus tard dans la soirée, à partir de 19h-20h selon l'heure de fin de la soutenance, nous continuerons à Hall Of Beer : Ouvrir dans Google Maps