Les circuits quantiques, éléments fondamentaux de l’informatique quantique, font l’objet d’une attention croissante dans le domaine de la recherche scientifique. Une équipe de chercheurs japonais propose une nouvelle approche pour vérifier leur fonctionnement, ouvrant ainsi de nouvelles perspectives pour le développement de cette technologie de pointe.
L’informatique quantique représente un domaine en pleine expansion, exploitant les lois de la physique quantique pour résoudre des problèmes computationnels complexes. Les circuits quantiques jouent un rôle crucial dans ce domaine, servant de modèles pour la conception et l’implémentation d’algorithmes quantiques avant leur déploiement sur du matériel spécialisé.
Ces circuits se composent d’une séquence d’opérations quantiques, incluant des portes quantiques, des mesures et des initialisations de qubits. Les qubits, unités de base de l’information quantique, sont manipulés par ces portes pour effectuer des calculs complexes.
Une nouvelle approche de vérification symbolique
Face aux défis posés par la vérification des circuits quantiques, le professeur assistant Canh Minh Do et le professeur Kazuhiro Ogata de l’Institut japonais des sciences et technologies avancées (JAIST) ont développé une approche innovante. Leur méthode, basée sur la vérification de modèle symbolique, utilise les lois de la mécanique quantique et des opérations matricielles de base.
Le Dr Do explique : «Considérant le succès des méthodes de vérification de modèle pour les circuits classiques, la vérification de modèle des circuits quantiques est une approche prometteuse. Nous avons développé une approche symbolique pour la vérification de modèle des circuits quantiques en utilisant les lois de la mécanique quantique et des opérations matricielles de base à l’aide du langage de programmation Maude.»
Maude : un outil puissant pour la spécification formelle
Le langage Maude, choisi pour cette étude, offre des capacités avancées pour la spécification et la vérification de systèmes complexes. Il est équipé d’un vérificateur de modèle de Logique Temporelle Linéaire (LTL), permettant de vérifier si les systèmes satisfont les propriétés spécifiées.
Les chercheurs ont formellement spécifié les circuits quantiques dans Maude, représentant les opérations quantiques comme des opérations matricielles de base. Les propriétés désirées du système ont été exprimées en LTL, permettant une vérification automatique à l’aide du vérificateur de modèle intégré à Maude.
Application à des protocoles de communication quantique
Cette approche a été appliquée avec succès à plusieurs protocoles de communication quantique précoces, tels que le codage superdense, la téléportation quantique, et le partage de secrets quantiques. Les chercheurs ont notamment identifié une faille dans la version originale de la téléportation de porte quantique, proposant une version révisée dont la correction a été confirmée.
Ces résultats soulignent l’importance de l’approche proposée pour la vérification des circuits quantiques. Cependant, les chercheurs reconnaissent certaines limitations de leur méthode, nécessitant des recherches supplémentaires.
Le Dr Do envisage l’avenir avec optimisme : «Nous visons à étendre notre raisonnement symbolique pour gérer davantage de portes quantiques et des raisonnements plus complexes sur les opérations de nombres complexes. Nous souhaitons également appliquer notre approche symbolique à la vérification de modèle des programmes quantiques et des protocoles de cryptographie quantique.»
La vérification du fonctionnement prévu des circuits quantiques s’avère cruciale pour l’avenir de l’informatique quantique. Dans ce contexte, l’approche présentée marque une étape importante vers un cadre général pour la vérification et la spécification des circuits quantiques, ouvrant la voie à une informatique quantique plus fiable et performante.
Article : « Symbolic model checking quantum circuits in Maude » – DOI: 10.7717/peerj-cs.2098
