Verified Pauli-Product Measurement Compilation for Fault-Tolerant Quantum Computation

Les ordinateurs quantiques promettent de résoudre des problèmes actuellement impossibles même pour les supercalculateurs les plus puissants, du déchiffrement de codes complexes à la simulation de nouveaux matériaux. Cependant, ces machines sont incroyablement fragiles. La moindre perturbation due à la chaleur ou aux vibrations peut provoquer l'effondrement de leurs calculs. Pour survivre, les scientifiques construisent des ordinateurs quantiques tolérants aux fautes, qui utilisent des codes de correction d'erreurs spéciaux pour protéger l'information. Au lieu de stocker des données sur une seule particule délicate, ces systèmes répartissent l'information sur de nombreuses particules, en vérifiant et en corrigeant constamment les erreurs. Le défi réside dans la traduction : comment prendre un algorithme de haut niveau et le convertir en les opérations spécifiques de bas niveau que ces machines corrigées d'erreurs peuvent réellement exécuter ?

La méthode standard pour beaucoup de ces machines futures implique une technique appelée chirurgie de réseau (lattice surgery). Imaginez une grande feuille de tissu représentant la mémoire de l'ordinateur. Pour effectuer un calcul, vous ne vous contentez pas de basculer un interrupteur ; vous cousez des morceaux de ce tissu ensemble et les séparez selon des motifs précis. Ces points de couture ne sont pas des fils physiques, mais plutôt des mesures conjointes de groupes de particules. L'ordinateur mesure la façon dont ces groupes se rapportent les uns aux autres, enregistre le résultat sous la forme d'un simple bit de donnée, puis utilise cette donnée pour décider de la marche à suivre. Ce processus, connu sous le nom de mesure de produit Pauli, est le langage fondamental de ces futures machines. Le problème est que les outils logiciels utilisés pour traduire les algorithmes conçus par l'homme en ce langage n'ont pas été vérifiés. Si un compilateur commet une erreur lors de la traduction, l'ensemble du calcul pourrait échouer et, comme le processus est si complexe, il est difficile de savoir où l'erreur s'est produite.

Une équipe de chercheurs de l'Université de Californie à Los Angeles a comblé cette lacune en créant un système qui prouve mathématiquement que la traduction est correcte. Ils ont développé un nouveau langage spécifiquement pour ces programmes basés sur la mesure et ont construit un compilateur qui traduit les circuits quantiques standards en ce langage. Crucialement, ils n'ont pas seulement écrit du code ; ils ont utilisé un outil de vérification formelle appelé Lean pour construire une preuve mathématique rigoureuse que leur compilateur préserve le comportement de l'algorithme original. Cela signifie que pour chaque étape du compilateur, il existe un certificat garantissant que la sortie est exactement ce que l'entrée était censée produire, jusqu'aux probabilités spécifiques des résultats.

Les chercheurs se sont concentrés sur deux tâches principales : l'abaissement (lowering) et l'optimisation. L'abaissement est le processus consistant à prendre une porte quantique standard, comme une rotation ou une porte logique, et à la décomposer en la séquence de mesures et de corrections requise par le matériel de chirurgie de réseau. L'optimisation consiste à réorganiser ces mesures pour rendre le processus plus rapide et plus efficace. Dans leur travail, ils ont prouvé que leur compilateur peut prendre un circuit, le traduire en instructions de mesure, puis appliquer des règles pour fusionner et réordonner ces instructions sans changer le résultat final. Ils ont vérifié que leur compilateur gère correctement les « états magiques » (magic states), qui sont des ressources spéciales nécessaires pour effectuer certains types de calculs, et qu'il garde les résultats de mesure privés cachés du monde extérieur tout en garantissant que les résultats publics restent accessibles.

Lorsqu'ils ont testé leur système sur une suite de trente-cinq petits circuits quantiques, les résultats ont été concrets et mesurables. Le compilateur vérifié a traduit avec succès chaque entrée valide, produisant un certificat qui confirmait que la traduction était correcte. En termes de performance, les techniques d'optimisation qu'ils ont vérifiées ont réduit le nombre de cycles de mesure logique nécessaires pour exécuter ces circuits d'une médiane de 17,9 %. Pour certains circuits spécifiques, la réduction était encore plus élevée, atteignant près de 29 %. Cette réduction est significative car, dans ces systèmes tolérants aux fautes, chaque cycle de mesure prend du temps et consomme des ressources ; réduire le nombre de cycles se traduit directement par un ordinateur plus rapide et plus efficace.

L'équipe a également démontré comment gérer les calculs approximatifs, qui sont nécessaires lorsqu'une rotation mathématique parfaite ne peut être construite exactement. Ils ont créé une méthode pour borner l'erreur introduite par ces approximations, garantissant que le résultat final reste dans une limite définie par l'utilisateur. Ils ont montré que leur système pouvait sélectionner la meilleure version possible d'un circuit parmi une liste de candidats, choisissant celui qui respectait la limite d'erreur tout en utilisant le moins de ressources. Ce processus de sélection a également été vérifié, ce qui signifie que l'ordinateur ne pouvait pas accidentellement choisir un circuit trop imprécis ou trop lent.

Ce travail représente un passage de l'espoir que le compilateur fonctionne à la certitude qu'il fonctionne. En construisant une preuve vérifiée par machine pour l'ensemble du pipeline de compilation, les chercheurs ont éliminé une source majeure d'incertitude dans la voie vers l'informatique quantique à grande échelle. Ils ont montré qu'il est possible de prendre un algorithme complexe, de le traduire dans le langage spécifique du matériel corrigé d'erreurs, et de l'optimiser pour la vitesse, tout en maintenant une garantie mathématique que la logique reste intacte. Le système a traité avec succès des circuits allant jusqu'à 433 qubits, prouvant que ce niveau de vérification peut passer à l'échelle pour des problèmes substantiels. Bien que le matériel physique pour exécuter ces circuits soit encore en cours de développement, cette fondation logicielle garantit que, lorsque les machines arriveront, les instructions qui leur seront envoyées seront dignes de confiance.