Vérification pratique de transformations de circuits quantiques
Jeudi 4 juin 2026 à 14h00, heure de Paris
Salle 1Z61, École normale supérieure Paris-Saclay, 4 Av. des Sciences, 91190 Gif-sur-Yvette
Le lien de visioconférence et les informations pratiques seront disponibles sur la page de la soutenance : https://jricc.github.io/github.io
Résumé : Ma thèse porte sur la vérification formelle des transformations de circuits quantiques. Ces transformations sont essentielles en compilation, optimisation ou adaptation au matériel, mais elles peuvent modifier le comportement du circuit. Le travail se concentre sur les circuits quantiques unitaires et hybrides, incluant mesures, contrôle classique et fils auxiliaires comme les ancillas ou les discards. Les outils existants traitent surtout les circuits unitaires, ce qui limite leur capacité à vérifier des transformations hybrides plus générales. Deux approches sont étudiées. La première utilise la preuve formelle avec Qbricks pour certifier une passe de compilation d’un langage de haut niveau vers un langage de bas niveau. La seconde développe SQbricks, un outil de vérification d’équivalence de circuits hybrides avec discard, basé sur l’exécution symbolique et les sommes de chemins. Nous montrons qu’il est possible d’étendre des outils de vérification unitaires aux circuits hybrides via le principe de mesure différée. En ajoutant des mécanismes de séparation et de projection, SQbricks permet aussi de traiter des transformations plus complexes impliquant des fils auxiliaires.
Jury :
- Miriam Backens, LORIA
- Sylvie Boldo, Inria
- Christophe Chareton, CEA LIST, co-encadrant
- Aleks Kissinger, University of Oxford, rapporteur
- Alessandra Di Pierro, University of Verona, rapporteure
- Benoît Valiron, CentraleSupelec, co-encadrant