Les ordinateurs quantiques exploitent les principes de la physique quantique pour encoder et traiter l'information, avec le potentiel de surpasser les capacités des ordinateurs classiques dans certains domaines. Cette thèse explore l'une des technologies majeures du calcul quantique : l'optique linéaire, où les calculs sont effectués à l'aide de photons traversant des circuits d'optique linéaire.Si ces circuits sont bien compris et simulables à petite échelle, leur véritable intérêt apparaît à grande échelle lorsqu'ils atteignent des régimes hors de portée du calcul classique. Cette thèse s'intéresse à cette transition sous deux aspects : sur le plan calculatoire d'une part, en développant des modèles plus efficaces pour repousser les limites des simulations classiques, et sur le plan formel d'autre part, en modélisant à un niveau plus abstrait les circuits optiques et leurs interactions.En simulation, l'un des défis majeurs est le calcul efficace des probabilités de sortie des circuits. Nous présentons dans cette thèse de nouveaux algorithmes pour calculer plusieurs de ces probabilités, où l'utilisation de la mémoire est optimisée pour significativement réduire le temps de calcul. Ce travail mène au développement de Perceval, une plateforme logicielle open-source dédiée au calcul quantique photonique.Sur le plan théorique, nous introduisons un cadre formel et diagrammatique qui capture pleinement la structure des processus d'optique linéaire. Plus précisément, nous utilisons le formalisme des langages graphiques pour modéliser ces circuits. Nous établissons une théorie équationnelle complète, démontrant que deux circuits équivalents d'optique linéaire peuvent toujours être réécrits localement avec notre ensemble d'équations.Enfin, nous montrons comment nos contributions ont des applications à la fois en physique et en informatique quantique théorique. En particulier, nous étendons notre théorie équationnelle complète des circuits optiques à une théorie équationnelle complète pour les circuits quantiques, résolvant ainsi un problème ouvert des dernières décennies.
Les ordinateurs quantiques exploitent les principes de la physique quantique pour encoder et traiter l'information, avec le potentiel de surpasser les capacités des ordinateurs classiques dans certains domaines. Cette thèse explore l'une des technologies majeures du calcul quantique : l'optique linéaire, où les calculs sont effectués à l'aide de photons traversant des circuits d'optique linéaire.Si ces circuits sont bien compris et simulables à petite échelle, leur véritable intérêt apparaît à grande échelle lorsqu'ils atteignent des régimes hors de portée du calcul classique. Cette thèse s'intéresse à cette transition sous deux aspects : sur le plan calculatoire d'une part, en développant des modèles plus efficaces pour repousser les limites des simulations classiques, et sur le plan formel d'autre part, en modélisant à un niveau plus abstrait les circuits optiques et leurs interactions.En simulation, l'un des défis majeurs est le calcul efficace des probabilités de sortie des circuits. Nous présentons dans cette thèse de nouveaux algorithmes pour calculer plusieurs de ces probabilités, où l'utilisation de la mémoire est optimisée pour significativement réduire le temps de calcul. Ce travail mène au développement de Perceval, une plateforme logicielle open-source dédiée au calcul quantique photonique.Sur le plan théorique, nous introduisons un cadre formel et diagrammatique qui capture pleinement la structure des processus d'optique linéaire. Plus précisément, nous utilisons le formalisme des langages graphiques pour modéliser ces circuits. Nous établissons une théorie équationnelle complète, démontrant que deux circuits équivalents d'optique linéaire peuvent toujours être réécrits localement avec notre ensemble d'équations.Enfin, nous montrons comment nos contributions ont des applications à la fois en physique et en informatique quantique théorique. En particulier, nous étendons notre théorie équationnelle complète des circuits optiques à une théorie équationnelle complète pour les circuits quantiques, résolvant ainsi un problème ouvert des dernières décennies.
Les ordinateurs quantiques exploitent les principes de la physique quantique pour encoder et traiter l'information, avec le potentiel de surpasser les capacités des ordinateurs classiques dans certains domaines. Cette thèse explore l'une des technologies majeures du calcul quantique : l'optique linéaire, où les calculs sont effectués à l'aide de photons traversant des circuits d'optique linéaire.Si ces circuits sont bien compris et simulables à petite échelle, leur véritable intérêt apparaît à grande échelle lorsqu'ils atteignent des régimes hors de portée du calcul classique. Cette thèse s'intéresse à cette transition sous deux aspects : sur le plan calculatoire d'une part, en développant des modèles plus efficaces pour repousser les limites des simulations classiques, et sur le plan formel d'autre part, en modélisant à un niveau plus abstrait les circuits optiques et leurs interactions.En simulation, l'un des défis majeurs est le calcul efficace des probabilités de sortie des circuits. Nous présentons dans cette thèse de nouveaux algorithmes pour calculer plusieurs de ces probabilités, où l'utilisation de la mémoire est optimisée pour significativement réduire le temps de calcul. Ce travail mène au développement de Perceval, une plateforme logicielle open-source dédiée au calcul quantique photonique.Sur le plan théorique, nous introduisons un cadre formel et diagrammatique qui capture pleinement la structure des processus d'optique linéaire. Plus précisément, nous utilisons le formalisme des langages graphiques pour modéliser ces circuits. Nous établissons une théorie équationnelle complète, démontrant que deux circuits équivalents d'optique linéaire peuvent toujours être réécrits localement avec notre ensemble d'équations.Enfin, nous montrons comment nos contributions ont des applications à la fois en physique et en informatique quantique théorique. En particulier, nous étendons notre théorie équationnelle complète des circuits optiques à une théorie équationnelle complète pour les circuits quantiques, résolvant ainsi un problème ouvert des dernières décennies.
Langages graphiques pour le contrôle quantique et l'optique linéaire Dans le modèle usuel de calcul quantique, des opérations sur des données quantiques sont contrôlées de manière essentiellement classique. Un contrôle lui aussi quantique est cependant possible, mais a été peu étudié en comparaison. En particulier, il manque au contrôle quantique un formalisme permettant de l'exprimer de manière simple afin de raisonner efficacement sur des processus l'impliquant. La première contribution de cette thèse est de poser les fondations d'un cadre formel dédié au contrôle quantique, sous la forme d'un langage graphique. Notre principal résultat concernant ce langage est l'introduction d'une théorie équationnelle complète, c'est à dire d'un ensemble d'équations permettant de transformer un diagramme, par réécriture locale successive, en n'importe quel autre diagramme représentant le même programme ou processus physique. Une deuxième contribution est l'application de ce formalisme d'une part au problème de l'optimisation des ressources dans les processus impliquant un contrôle quantique, et d'autre part à la caractérisation de l'équivalence observationnelle des canaux de communication quantiques. La troisième contribution de cette thèse est l'introduction d'un langage pour les circuits optiques linéaires. Nous l'équipons d'une théorie équationnelle complète, ainsi que d'une forme normale simple, accessible par un système de réécriture fortement normalisant et confluent. La dernière contribution de cette thèse, peut-être la plus importante, est l'introduction d'une théorie équationnelle complète pour le langage des circuits quantiques. Nous nous appuyons pour cela sur une correspondance entre les circuits quantiques et les circuits optiques, qui nous permet de transférer la théorie équationnelle déjà obtenue pour les circuits optiques.
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 (mesures intermédiaires non incluses dans la sortie du circuit), 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.
Algorithmes quantiques pour les équations aux dérivées partielles : circuits quantiques et applications physiques Les simulations classiques actuelles des phénomènes physiques présentent de nombreuses limitations, en particulier lorsqu'il s'agit de systèmes complexes tels que les fluides turbulents, les plasmas ou les matériaux quantiques fortement corrélés. Ces simulations rencontrent souvent des difficultés liées à des coûts de calculs élevés, une mise à l'échelle limitée à travers plusieurs dimensions ou échelles temporelles, ainsi qu'à la complexité de capturer des dynamiques intrinsèquement non-linéaires ou chaotiques. Même avec l'accès à des ressources de calcul haute performance (HPC), la résolution précise des dynamiques à fine échelle ou des évolutions sur de longues périodes reste un défi majeur. Le développement de nouvelles méthodes numériques est donc essentiel, tant pour la recherche académique que pour les applications industrielles. Les ordinateurs quantiques émergent comme de nouveaux outils numériques pour l'étude de tels systèmes et la résolution des équations aux dérivées partielles qui les modélisent. Grâce aux propriétés de superposition et d'intrication des qubits, les calculs numériques peuvent être réalisés de manière inédite, offrant des avantages théoriques prometteurs pour certains problèmes. Dans ce contexte, cette thèse contribue au développement et à la compréhension des algorithmes quantiques, allant de la conception de circuits quantiques à la résolution numérique d'équations différentielles partielles et ordinaires. Dans une première partie, des circuits quantiques efficaces sont présentés pour l'implémentation de routines couramment utilisées dans les algorithmes quantiques (opérations multi-contrôlées, préparation d'états quantiques, opérations diagonales), ainsi que pour une nouvelle routine : la transformée de Laplace quantique. Ces routines limitaient l'efficacité des algorithmes quantiques en raison d'implémentations génériques dont la complexité croissait de manière exponentielle avec le nombre de qubits. Désormais, ces tâches peuvent être réalisées à l'aide de circuits quantiques adaptés qui exploitent la structure des problèmes physiques. Dans une seconde partie, des schémas numériques quantiques sont introduits pour résoudre des équations de transport anisotropes et des équations différentielles ordinaires hamiltoniennes non linéaires. Ces schémas se composent de trois étapes (initialisation, évolution et mesure) et reposent sur des approximations en différences finies d'ordre élevé et des formules de Trotterisation. Des protocoles efficaces pour mesurer des grandeurs d'intérêt sont présentés, et une nouvelle analyse numérique, basée sur la norme vectorielle plutôt que sur la norme d'opérateur générique, est introduite. Cette approche permet d'atteindre une précision donnée tout en réduisant le nombre de pas de temps par un facteur qui croît de manière exponentielle avec le nombre de qubits. De plus, une étude de différentes transformations de Madelung non linéaires est présentée afin de résoudre certaines équations fluides sur ordinateur quantique. Les différents résultats de cette thèse sont illustrés par des simulations classiques des algorithmes quantiques ainsi que par des simulations sur des processeurs quantiques actuels. Ce travail pose les bases de la simulation pratique de systèmes physiques classiques, aussi bien sur les dispositifs quantiques actuels de type NISQ (noisy intermediate-scale quantum) que sur les futurs ordinateurs quantiques tolérants aux erreurs.
Vérification pratique des transformations de circuits quantiques 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 (mesures intermédiaires non incluses dans la sortie du circuit), 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.
L'informatique quantique est basée sur des phénomènes de physique quantique, tels que superposition et intrication et elle promet de révolutionner le monde de l'informatique. La photonique est une plateforme de premier plan pour réaliser l'informatique quantique tolérante aux erreurs. Elle possède plusieurs qualités : fonctionnement à température ambiante, fabricabilité à grande échelle à l'aide des fonderies existantes pour les puces de silicium et compatibilité avec les communications optique pour interconnecter différents ordinateurs quantiques.Notre objectif principal est d'automatiser la conception de circuits quantiques photoniques et de leurs interconnexions. Avant de pouvoir fabriquer un véritable ordinateur quantique photonique, il est essentiel de simuler numériquement et d'optimiser les circuits correspondants, qui sont en pratique construits à partir de composants gaussiens tels que des squeezers, des séparateurs de faisceaux, des déphaseurs et des détections homodynes. Pour atteindre l'universalité, nous avons également besoin d'effets non gaussiens, qui peuvent être fournis par des détecteurs résolvant le nombre de photons. Nous concevons des circuits à partir de cette boîte à outils et les optimisons pour diverses applications en utilisant divers algorithmes de descente de gradient, dont certains que nous avons adaptés à notre objectif.Les principaux apports sont :1. En photonique, les représentations de l'espace de Fock et de l'espace de phase sont des formalismes utiles pour décrire les états et les transformations quantiques. Nous introduisons une représentation unifiée dans l'espace de Fock de tous les objets gaussiens en termes d'une seule relation de récurrence linéaire qui peut générer de manière récursive leurs amplitudes dans l'espace de Fock.2. On retrouve la règle de composition des opérations gaussiennes dans l'espace de Fock, qui permet d'obtenir la bonne phase globale lors de la composition des opérations gaussiennes (normalement absente), et donc d'étendre notre modèle à des états qui s'écrivent comme combinaisons linéaires de gaussiennes.3. Notre représentation récursive est différentiable, permettant à calculer des gradients. Nous adaptons ensuite l'optimisation basée sur les gradients au problème d'optimisation des circuits. Nous implémentons un optimiseur Euclidien afin d'optimiser chaque composant. Ensuite, nous étudions deux manières de prendre en compte la géométrie: d'abord, nous appliquons l'optimisation Riemannienne, en combinant toutes les opérations gaussiennes en une transformation globale pour trouver ensuite la transformation optimisée, et la décomposer en composants optiques fondamentaux. Deuxièmement, nous généralisons une version complexe du gradient naturel pour les circuits afin d'accélérer le processus d'apprentissage.4. Nous donnons également quelques stratégies optimales basées sur les tâches pour utiliser nos relations de récurrence. De nouveaux algorithmes sont proposés pour calculer, par exemple, les amplitudes d'un état mixte et la matrice de transformation des interféromètres. De plus, nous dérivons un algorithme de contraction rapide pour les transformations gaussiennes, qui nous permet de "fusionner" le calcul des amplitudes d'une transformation gaussienne et son action sur n'importe quel état.5. Avec la simulation sur des circuits quantiques photoniques différentiables construits à partir de la relation de récurrence, nous pouvons concevoir automatiquement des circuits quantiques photoniques. Nous donnons la préparation de l'état comme premier exemple ; nous trouvons des circuits capables de produire des états de haute fidélité dans un temps raisonnable. Nous pouvons aussi optimiser un interféromètre à 216 modes pour rendre une expérience d'échantillonnage de boson gaussien difficile à usurper.6. Nous avons rendu ce travail accessible dans diverses bibliothèques open source: TheWalrus, StrawberryFields, Poenta et MrMustard.