La validation de programmes quantiques
Un problème majeur en informatique quantique est l’impossibilité d’y transposer les techniques de validation et vérification standards, basées sur la vérification à l’exécution des propriétés attendues du système (principe classique du test logiciel). La physique à l’œuvre interdit en effet la consultation de la valeur d’une donnée en cours d’exécution (cela aurait pour effet de l’effacer) ainsi que le passage à l’échelle d’une stratégie de test (caractère non déterministe du calcul quantique).
Tout scénario réaliste de programmation quantique utile impose donc le développement de méthodes nouvelles et innovantes de vérification de code.
Ces dernières années, nous avons développé Qbricks, un outil de vérification de programmes quantiques basé sur de la preuve formelle. L’outil permet d’écrire explicitement les spécifications attendues d’un programme quantique et fournit des moyens de preuves interactive automatisés pour vérifier que ce programme se comporte conformément à ces spécifications pour toutes les données d’entrée possibles.
Etendre l’analyse à la programmation hybride
Nos travaux les plus récents visent à étendre cette ligne de travail au cas hybride, dans lequel les données classiques et quantiques interagissent.
Le calcul hybride est en effet omniprésent dans la littérature, avec des algorithmes (tels que la résolution de valeurs propres variationnelle quantiques —VQE) qui entremêlent des briques de calcul classiques et des briques quantiques et d’autres algorithmes qui embarquent des calculs quantiques dans des structures de contrôle classique. Par ailleurs, dans le cas général, la plupart des purs algorithmes quantiques (comme l’Estimation de Phase ou la décomposition en facteurs premiers de Shor) gagnent en performance quand ils sont fragmentés en composants plus simples et hybridisés. Dans le calcul quantique de grande échelle, même les primitives purement quantiques sont elles-mêmes implémentées de manière hybride pour qu’on puisse leur appliquer la détection et la correction d’erreurs.
Nous avons d’abord étendu les techniques existantes de vérification d’équivalences, problème crucial pour la validation des briques de compilation et optimisation, du cas purement quantique à différentes classes de calcul hybride.
Le traitement du cas général nécessite quant à lui une refondation du système de représentation symbolique de programmes utilisé dans Qbricks. Ce travail est en cours, et nous avons réalisé des premières expériences d’exécution symbolique de circuits prometteuses.
Tout scénario réaliste de programmation quantique impose d’inventer des méthodes nouvelles de débogage et de vérification de code.
