Résumé technique : La vérification des données est l'avenir des copilotes de l'informatique quantique

Énoncé du problème

La génération et la compilation de programmes quantiques exigent un niveau de précision qui entre en conflit avec le raisonnement statistique inhérent aux grands modèles de langage (LLM). Les tâches d'informatique quantique impliquent de traverser plusieurs couches d'abstraction (des descriptions de circuits de haut niveau aux arrangements de portes de bas niveau) et de respecter des contraintes mathématiques rigoureuses (ex. : l'unitarité, la topologie du matériel, la fidélité des portes). Contraurs aux tâches de langage naturel où les erreurs peuvent être tolérées ou lissées, la génération de programmes quantiques exige une tolérance zéro pour les erreurs ; une seule séquence de portes invalide viole les lois physiques fondamentales.

Les approches actuelles basées sur les LLM font face à trois limitations critiques :

1. Solutions infaisables : Sans vérification des données, les solutions infaisables sont mathématiquement inévitables en raison de la nature statistique des LLM, quel que soit le passage à l'échelle des modèles.
2. Rareté des données : Les jeux de données quantiques complets et vérifiés sont extrêmement difficiles à générer. Les jeux de données existants (ex. : QDataSet) ont nécessité des mois de temps de calcul sur HPC pour ne couvrir que de petits systèmes (1-2 qubits).
3. Contraintes de l'espace de recherche : Le sous-espace valide des circuits quantiques est exponentiellement petit par rapport à l'espace de conception total, limité par l'unitarité et les contraintes matérielles. Les architectures de LLM actuelles ne peuvent pas fournir intrinsèquement les mécanismes de vérification nécessaires pour naviguer dans cet espace.

Méthodologie et cadre de travail

L'article propose un changement de paradigme passant d'une approche de « l'inférence seule » ou du « filtrage a posteriori » vers des architectures axées sur la vérification (verification-first). Les auteurs définissent trois positions centrales soutenues par des arguments théoriques et des expériences préliminaires :

1. La vérification des données comme exigence minimale (P1)

Les auteurs soutiennent que les données d'entraînement doivent être formellement vérifiées avant d'être incluses dans l'ensemble d'entraînement.

• Concept : Un « modèle conscient de la vérification » est entraîné exclusivement sur des données où chaque exemple satisfait des contraintes de correction spécifiques au domaine (ex. : prouvées via des prouveurs de théorèmes automatisés comme Lean ou Z3).
• Justification : S'entraîner sur des données non vérifiées (ex. : des dépôts de code de faible qualité) constitue un « empoisonnement implicite des données ». Contrairement au langage naturel, où des volumes massifs de données compensent le bruit, un seul exemple invalide dans les données de circuits quantiques viole l'unitarité, indépendamment des exemples valides environnants. Cela conduit à un phénomène d'« anti-mise à l'échelle » où davantage de données non vérifiées amplifient les erreurs plutôt que de les diluer.
• Mécanisme : Les jeux de données vérifiés permettent aux modèles d'internaliser les contraintes sous forme de structures apprises plutôt que d'approximations statistiques.

2. Des contraintes a priori plutôt qu'un filtrage a posteriori (P2)

La vérification doit contraindre le processus de génération avant la sortie, plutôt que de filtrer les sorties après la génération.

• Justification : Dans la conception de circuits quantiques, la fraction de conceptions valides diminue exponentiellement à mesure que le nombre de composants (qubits/portes) augmente. Pour un espace de conception croissant selon $O(d^n)$, les contraintes réduisent les conceptions valides à $O(\delta^n)$ où $\delta < d$.
• Conséquence : S'appuyer sur un filtrage a posteriori (générer de nombreux candidats et rejeter les invalides) entraîne des coûts computationnels exponentiels et une probabilité de succès déclinante. La vérification doit être intégrée comme une primitive architecturale pour empêcher les chemins invalides pendant la génération de tokens.

3. Paradigme de la vérification d'abord pour l'IA appliquée à la recherche (P3)

Les auteurs préconisent l'extension de cette approche de vérification d'abord à d'autres domaines scientifiques régis par des lois physiques ou des axiomes mathématiques (ex. : découverte de médicaments, science des matériaux, conception d'ingénierie).

• Concept : Ces domaines partagent des problèmes d'« abstraction fuyante » (leaky abstraction) et de « non-décomposabilité », où des choix localement optimaux ne garantissent pas l'optimalité globale. Des architectures conscientes de la vérification sont nécessaires pour gérer ces contraintes strictes.

Résultats expérimentaux

Pour étayer la Position 1, les auteurs ont mené une évaluation utilisant un jeu de données dérivé de corpus de circuits MAJ/UMA (Majority/UnMajority-and-Add) vérifiés.

• Configuration : 34 LLM publics (allant de 270M à 120B de paramètres) ont été testés sur 70 000 questions à choix multiples concernant l'optimisation d'additions quantiques (2 à 8 qubits). La vérité terrain est le circuit présentant le score pondéré minimal de comptage Toffoli, de profondeur et de nombre total de portes.
• Précision : Les modèles entraînés ou affinés avec des connaissances de vérification (ex. : gemma3:12b, gpt-oss:120b) ont atteint une précision comprise entre 0,60 et 0,79. En revanche, les modèles génériques sans conscience de la vérification stagnaient près de la ligne de base aléatoire (0,21–0,29).
• Calibration : Les modèles conscients de la vérification ont démontré une quantification de l'incertitude supérieure. Les modèles gpt-oss attribuaient 60 à 80 % de confiance aux réponses correctes, tandis que les modèles gemma3 restaient dans la plage de 20 à 35 %.
• Modes de défaillance : Plusieurs modèles (ex. : variantes de mixtral:8x7b, deepseek-r1) ont obtenu un score inférieur à la ligne de base aléatoire en raison de sorties malformées (refus verbeux ou explications au lieu de réponses par lettre unique), renforçant l'idée que sans entraînement à la vérification, les modèles ne peuvent pas s'engager de manière fiable dans des tâches formellement contraintes.
• Analyse de l'espace de recherche : Les auteurs ont généré un jeu de données de 200 000 conceptions d'additionneurs vérifiées. Ils ont noté que bien que le nombre total de configurations de portes possibles pour les modules MAJ/UMA sur des profondeurs de 3 à 6 dépasse les 148 billions, la vérification formelle n'a identifié qu'environ 200 000 conceptions valides (un ratio de $\approx 10^{-9}$), illustrant la nature prohibitive du filtrage a posteriori.

Contributions clés

1. Définition formelle des modèles conscients de la vérification : Distinction entre les modèles entraînés sur des contraintes vérifiées et ceux entraînés sur des dépôts de code non vérifiés.
2. Trois positions centrales : Établir que la vérification des données est une exigence minimale, que les contraintes doivent être a priori, et que ce paradigme est essentiel pour l'IA scientifique.
3. Preuve empirique : Fournir des données quantitatives montrant que sans vérification des données, les LLM échouent à atteindre une précision élevée ou une calibration appropriée sur les tâches d'optimisation quantique, quel que soit l'échelle des paramètres.
4. Identification de l'« abstraction fuyante » : Souligner comment la génération de programmes quantiques nécessite de fusionner les niveaux d'abstraction (ex. : conception de modules vs décomposition de portes) d'une manière qui rend l'optimisation locale insuffisante pour la correction globale.

Signification et directions futures

L'article soutient que pour que l'IA soit viable dans des domaines régis par des lois physiques ou mathématiques strictes, la vérification doit passer du statut de « réflexion après coup » à celui de « fondation architecturale ».

Les auteurs proposent deux directions de recherche futures spécifiques :

• FD1 (Architecture) : Les architectures de copilotes quantiques doivent intégrer la vérification formelle (ex. : théorie des ensembles de satisfaisabilité ou spécifications symboliques) directement dans la boucle de génération de tokens du LLM, transformant la vérification d'un filtre binaire en un guide d'exploration structuré.
• FD2 (Benchmarks) : La communauté a besoin de benchmarks riches en contraintes couplés à des oracles de vérification exécutables. Ceux-ci devraient s'étendre au-delà des simples additionneurs pour inclure la multiplication modulaire, la transformée de Fourier quantique et le routage spécifique au matériel, permettant des standards reproductibles pour la comparaison entre systèmes.

L'article conclut que bien que les arguments se concentrent sur l'informatique quantique, les principes s'appliquent largement à tout domaine où la correction est binaire, où les solutions valides occupent un sous-espace exponentiellement petit et où des méthodes de vérification formelle existent.