Dans cette thèse, nous étudions la vérifiabilité des calculs quantiques dans un contexte oraculaire. D'une part, nous connaissons plusieurs problèmes à oracle offrant démontrablement une séparation entre BPP et BQP. De l'autre, plusieurs techniques de preuves interactives ont été développées dans les vingt dernières années pour rendre les calculs quantiques faits par une machine BQP vérifiables par une machine BPP. Malheureusement, aucune de ces techniques ne relativise trivialement aux problèmes à oracles. Ceci nous mène à la question suivante : est-ce que ces problèmes à oracles admettent eux aussi des preuves interactives entre un prouveur BQP et un vérificateur BPP, ou est-ce qu'il serait démontrablement impossible d'en trouver une? Nous passerons en revue les principales techniques de preuves interactives dans le monde non relativisé, ainsi que les principaux problèmes à oracles séparant BQP de BPP. Puis, nous nous attarderons sur le problème de Simon et le problème Forrelation, pour lesquels nous introduisons dans cette thèse les premières preuves interactives avec prouveur BQP et vérificateur BPP mais légèrement quantique (et nous laissons ouverte la question à savoir s'il existe une telle preuve interactive avec un vérificateur BPP purement classique).
Dans cette thèse, nous étudions la vérifiabilité des calculs quantiques dans un contexte oraculaire. D'une part, nous connaissons plusieurs problèmes à oracle offrant démontrablement une séparation entre BPP et BQP. De l'autre, plusieurs techniques de preuves interactives ont été développées dans les vingt dernières années pour rendre les calculs quantiques faits par une machine BQP vérifiables par une machine BPP. Malheureusement, aucune de ces techniques ne relativise trivialement aux problèmes à oracles. Ceci nous mène à la question suivante : est-ce que ces problèmes à oracles admettent eux aussi des preuves interactives entre un prouveur BQP et un vérificateur BPP, ou est-ce qu'il serait démontrablement impossible d'en trouver une? Nous passerons en revue les principales techniques de preuves interactives dans le monde non relativisé, ainsi que les principaux problèmes à oracles séparant BQP de BPP. Puis, nous nous attarderons sur le problème de Simon et le problème Forrelation, pour lesquels nous introduisons dans cette thèse les premières preuves interactives avec prouveur BQP et vérificateur BPP mais légèrement quantique (et nous laissons ouverte la question à savoir s'il existe une telle preuve interactive avec un vérificateur BPP purement classique).
Cette thèse est consacrée à la complexité basée sur le paradigme des preuves interactives. Les classes ainsi définies ont toutes en commun qu’un ou plusieurs prouveurs, infiniment puissants, tentent de convaincre un vérificateur, de puissance bornée, de l’appartenance d’un mot à un langage. Nous abordons ici le modèle classique, où les participants sont des machines de Turing, et le modèle quantique, où ceux-ci sont des circuits quantiques. La revue de littérature que comprend cette thèse s’adresse à un lecteur déjà familier avec la complexité et l’informatique quantique. Cette thèse présente comme résultat la caractérisation de la classe NP par une classe de preuves interactives quantiques de taille logarithmique. Les différentes classes sont présentées dans un ordre permettant d’aborder aussi facilement que possible les classes interactives. Le premier chapitre est consacré aux classes de base de la complexité ; celles-ci seront utiles pour situer les classes subséquemment présentées. Les chapitres deux et trois présentent respectivement les classes à un et à plusieurs prouveurs. La présentation du résultat ci-haut mentionné est l’objet du chapitre quatre.
La recherche en informatique quantique a pris de l’ampleur dans les deux dernières décennies, notamment grâce aux financements massifs des gouvernements et de l’industrie dans les technologies quantiques. L’ordinateur quantique promet de résoudre des problèmes qui jusqu’à présent restaient insurmontables à cause du temps déraisonnable qu’il faudrait pour les résoudre sur les ordinateurs classiques les plus puissants. L’idée de l’ordinateur quantique consiste à utiliser des propriétés quantiques de la matière, telles que l’intrication et la superposition quantique des états, pour effectuer des calculs d’une nouvelle manière. L’informatique quantique requiert un nouveau type d’ordinateur où les bits d’information classique, généralement représentés par la présence ou non de courant à l’entrée d’un transistor, sont remplacés par des bits quantiques aussi appelés qubits, et qui sont représentés par l’état d’un système quantique. De plus, il est nécessaire de développer de nouveaux algorithmes capables d’être implémentés sur un ordinateur quantique et capables de tirer parti de l’avantage quantique. Cette thèse porte sur ces deux composantes complémentaires : la construction de portes logiques, un bloc fondamental de tout ordinateur, et la création de meilleurs algorithmes pour résoudre des problèmes pertinents sur ces machines. Parmi les plateformes les plus avancées pour l’ordinateur quantique, on trouve les circuits supraconducteurs, qui sont la plateforme sur laquelle ont misé Google, IBM, Alice&Bob, Nord Quantique et bien d’autres compagnies. Malgré les avancées des dernières décennies, de nombreux défis restent à être relevés pour que les machines existantes soient en mesure de résoudre des problèmes pertinents et surpassent les ordinateurs classiques. L’un des défis auquel cette thèse s’attaque est la réalisation de portes logiques à deux qubits rapides et à haute fidélité. La rapidité est cruciale pour pouvoir réaliser le plus d’opérations possible avant que les qubits ne perdent leur cohérence quantique, et une haute fidélité est requise pour minimiser les erreurs de calcul et permettre d’implémenter de la correction d’erreurs quantiques. De plus, certains qubits supraconducteurs sont connus pour être affectés par une interaction indésirable, l’interaction ZZ qui, même si relativement faible, affecte la fidélité des portes logiques quantiques, empêchant d’atteindre des fidélités supérieures à 99.9% nécessaires à la correction d’erreurs. En parallèle avec l’amélioration des composantes de l’ordinateur quantique, il est important de développer des applications pour ce nouveau type de machine. Parmi les approches étudiées, les algorithmes quantiques variationnels (VQA) sont ceux qui sont les plus susceptibles d’être déployés sur les ordinateurs quantiques de petites tailles existants. Ce sont des algorithmes hybrides qui nécessitent à la fois de la puissance de calcul classique et quantique. Ces algorithmes semblent prometteurs pour résoudre de nombreux problèmes concrets d’intérêt industriel, comme obtenir les propriétés de molécules ou trouver les solutions de problèmes d’optimisation combinatoire. En effet, ces problèmes peuvent être formulés sous forme d’un Hamiltonien et résolus en déterminant son état fondamental. Dans ce but, les VQAs utilisent un circuit quantique paramétré appelé ansatz, dont les paramètres sont optimisés pour s’approcher de l’état fondamental. Un premier défi consiste à trouver un ansatz qui permette, pour un problème donné, de converger le plus efficacement possible vers la solution. Un deuxième défi est de trouver un circuit fait de portes logiques facilement implémentables sur les plateformes physiques actuelles. Les travaux effectués dans cette thèse apportent des contributions à ces deux défis. Dans la première partie de la thèse, nous introduisons le dispositif que nous avons conçu et qui permet de réaliser des portes d’intrication paramétrique entre deux qubits supraconducteurs. Cette approche a permis à nos collaborateurs du groupe d’Andrew Houck de l’Université de Princeton de réaliser expérimentalement une opération de type √iSWAP en 15 ns avec une fidélité de 98.8%, et ce dans un dispositif où l’interaction ZZ est supprimée. Dans la seconde partie de la thèse, nous avons développé un ansatz pour les VQAs permettant de résoudre le modèle de Fermi Hubbard. Ce nouvel ansatz utilise les avantages de deux ansätze préexistants, et permet d’obtenir l’énergie et l’état fondamental du FHM avec une précision de plusieurs ordres de grandeur supérieure aux ansätze standards, et ce en réduisant significativement le nombre de portes d’intrication CNOT qui sont généralement imparfaites et longues à implémenter.
La recherche des scénarios de défaillance d'un système est un problème bien connu dans le monde industriel, et il peut être résolu en recherchant les chemins dans le graphe des états de ce système. La difficulté réside dans le fait qu'on ne cherche pas un seul ou une partie de ces chemins, on cherche tous ces chemins. Dans ce papier, on propose notre approche quantique afin de trouver tous les chemins dans ce graphe des états entre un sommet source et les sommets marquants. Notre approche se base sur les marches quantiques pour déterminer tous les chemins possibles au lieu de les traiter un par un classiquement, aussi notre approche est capable de déterminer tous ces chemins dans le même temps avec seulement ⌈ K×n ln 2 ⌉ + n qubits et n+2 oracles pour le cas où on essaie de déterminer seulement les scénarios avec des défaillances et les scénarios avec une possibilité d'une seule réparation durant la période du scénario. Nous avons testé notre approche sur le graphe des états d'un petit système de quatre composants et nous avons pu trouver tous les scénarios de défaillance de ce système. Malheureusement, nous ne pouvons pas tester sur des grands systèmes en raison du nombre des qubits disponibles aujourd'hui dans les ordinateurs quantiques, ce qui limite ce travail dans le cas d'utilisation. Le but de ce papier est de préparer une version quantique qui permet de résoudre ce problème dans l'attente de la mise à l'échelle des ordinateurs quantiques.
Les calculateurs quantiques promettent de résoudre des problèmes insolvables pour les ordinateurs classiques. En particulier, manipuler des états superposés et intriqués de bits quantiques est une voie naturelle pour étudier la physique des systèmes quantiques à N particules. Avec les avancées rapides des technologies quantiques, nous avons pu voir émerger les premiers processeurs quantiques, nommés processeurs "NISQ" (de l'anglais "Noisy-Intermediate-Scale-Quantum"). Les progrès de ces machines ouvrent de nouveaux chemins aux physiciens pour simuler des systèmes quantiques. Cependant, leur taille limitée et les erreurs liées à la décohérence limitent fortement leur usage aujourd'hui. La conception d'algorithmes quantiques efficaces, résistant aux erreurs, est un défi considérable. Ce travail de thèse s'attelle à comprendre les capacités des processeurs quantiques à simuler des systèmes quantiques à N corps, avec une attention particulière aux applications pour la physique de la matière condensée. Dans un premier temps, nous abordons le sujet du calcul de l'état fondamental d'Hamiltoniens, à l'aide d'un algorithme variationnel quantique-classique (nommée l'algorithme VQE, de l'anglais « Variational Quantum Eigensolver »). Nous évaluons les performances de cette méthode sur le modèle de Hubbard, grâce à différentes métriques, comme la fidélité, l'énergie et les propriétés physiques des solutions obtenues. Nous démontrons, malgré des performances prometteuses en simulant un calculateur quantique sans bruit, que le niveau de bruit des machines contemporaines rend impossible la réalisation d'un calcul significatif. En revanche, certains états quantiques aux propriétés intéressantes peuvent avoir une forme simple. Leur préparation sur un calculateur quantique est un problème pertinent dans le but d'initialiser un calcul quantique avec ces états pour les amener vers des régimes où ils perdent leur forme simple. Pour illustrer ceci, nous prenons l'exemple du modèle Affleck-Lieb-Kennedy-Tasaki (AKLT), le premier modèle de chaîne de spin entier antiferromagnétique possédant une solution simple vérifiant la conjecture d'Haldane. Nous proposons deux schémas pour préparer les états AKLT, l'un suivant leur construction naturelle en projetant des paires de qubits sur leur sous-espace triplet, l'autre utilisant leur forme de réseaux de tenseurs. Nous analysons l'implémentation de ces méthodes en fonction de la taille du système, avec une réalisation expérimentale sur un processeur quantique. Enfin, nous explorons la synergie entre les méthodes de réseaux de tenseurs et les calculateurs quantiques bruités pour simuler la dynamique hors-équilibre de systèmes de spins. La simulation de dynamique quantique est une tâche naturelle pour les calculateurs quantiques, mais atteindre des temps longs est fortement limité par le bruit. D'autre part, les réseaux de tenseurs sont également limités aux temps courts, contraints par la quantité d'intrication qu'ils peuvent encoder. Nous proposons d'utiliser le meilleur des deux mondes : la dynamique à temps court est simulée efficacement par un réseau de tenseur, compilée vers des circuits quantiques de faible profondeur pour poursuivre l'évolution temporelle sur le calculateur quantique. Nous étudions les performances de ce schéma hybride quantique-classique en regardant la fidélité des états obtenus et la production d'intrication, avec une validation expérimentale. Finalement, nous proposons d'optimiser les circuits quantiques approximant l'opérateur évolution temporelle grâce à des réseaux de tenseurs, résultant en une simulation quantique classiquement améliorée utilisant moins de ressources 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.
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.