A Machine-Verified Proof of a Quantum-Optimization Conjecture

Résumé Technique : Une preuve vérifiée par machine d'une conjecture d'optimisation quantique

Énoncé du Problème
L'article traite d'un problème ouvert de longue date en optimisation quantique concernant la performance de l'algorithme d'optimisation approximative quantique (QAOA). Plus précisément, il cible la conjecture de Farhi, Goldstone et Gutmann (FGG) [1], qui postule que pour le problème du « anneau de désaccord » (équivalent au problème MaxCut sur un graphe cyclique ou un modèle d'Ising antiferromagnétique unidimensionnel avec conditions aux limites périodiques), un circuit QAOA de profondeur $p$ atteint un ratio d'approximation optimal exact de :
$$r^*_p = \frac{2p + 1}{2p + 2}$$
Cette conjecture est valable pour une taille de système $n$ paire dans le régime $2p + 2 \leq n$. Bien que la borne supérieure $r^*_p \leq (2p+1)/(2p+2)$ ait été établie via une décomposition exacte de l'énergie résiduelle en modes de quantité de mouvement indépendants [21], l'existence d'un ensemble de $2p$ angles variationnels qui sature simultanément cette borne pour tous les modes restait non prouvée. La difficulté centrale réside dans la résolution d'un système de $2p$ équations transcendantes dérivées des rotations SO(3) des couches QAOA, où une solution n'est pas garantie par un simple comptage de paramètres.

Méthodologie
Les auteurs ont employé un paradigme « générer-puis-certifier », combinant l'autoformalisation guidée par l'humain avec un grand modèle de langage (LLM) et un assistant de preuve formelle.

1. Formalisation : L'équipe s'est appuyée sur une bibliothèque existante de Lean 4 pour l'information quantique (développée dans le cadre de travaux parallèles sur la cryptographie quantique vérifiée par machine [29]). Ils ont étendu cette bibliothèque pour formaliser les composants du QAOA, le hamiltonien de coût d'Ising, l'opérateur de mélange, et la décomposition exacte du problème en modes de quantité de mouvement découplés en utilisant la transformation de Jordan-Wigner et le formalisme des pseudospins d'Anderson.
2. Isolation de l'écart : Le problème ouvert a été réduit à un énoncé formel unique dans Lean : l'existence d'angles $\gamma, \beta$ tels que l'énergie résiduelle par mode s'annule pour tous les $p$ modes de quantité de mouvement simultanément.
3. Construction de preuve pilotée par l'IA : Le LLM, Claude Fable 5, a été chargé de construire une preuve pour cet énoncé. Le processus a utilisé une boucle de rétroaction agentique (Fig. 1) :
   • Le modèle a généré des plans de preuve en langage naturel.
   • Il a effectué des vérifications numériques internes via Python pour valider les constructions candidates avant la formalisation.
   • Il a tenté de formaliser la preuve en Lean 4.
   • Le compilateur et le noyau Lean ont fourni des diagnostics (erreurs de type, objectifs ouverts), que le modèle a utilisés pour réviser sa stratégie.
4. Vérification : Le résultat final est une preuve Lean 4 qui compile proprement en utilisant les axiomes classiques standards de Mathlib [3]. La vérification humaine s'est limitée à s'assurer que l'énoncé formel codait fidèlement la conjecture originale ; la dérivation logique a été entièrement certifiée par la machine.

Contributions Clés et Résultats
L'article présente la première preuve vérifiée par machine de la conjecture FGG. La preuve, générée par le LLM et vérifiée par Lean, révèle une symétrie dynamique cachée dans le problème qui transforme une question d'existence difficile en une construction explicite :

• Réduction de Symétrie : La preuve identifie que la dynamique par mode, bien que décrite à l'origine par des rotations SO(3), peut être élevée au revêtement double SU(2). Cela réduit le problème à une grandeur géométrique à un seul qubit.
• Connexion avec le Traitement du Signal Quantique (QSP) : Les auteurs démontrent que le propagateur QAOA pour chaque mode correspond à une séquence de Traitement du Signal Quantique (QSP). Cela mappe la condition de pilotage (diriger l'état vers l'axe du coût) à l'exigence qu'une entrée hors diagonale spécifique d'un polynôme de Laurent à valeurs SU(2) s'annule à des nœuds spécifiques.
• Construction Explicite : En exploitant les contraintes de parité du polynôme QSP (paires de classe-L), le modèle construit un polynôme unique $T(w)$ qui s'annule aux $p$ nœuds de quantité de mouvement requis. La normalisation de ce polynôme au mode non pilotable ($k=\pi$) produit naturellement la constante $1/(2p+2)$, confirmant la borne conjecturée.
• Récupération des Angles : En utilisant le théorème de factorisation de Haah [39], la preuve réassocie explicitement le polynôme construit aux angles du QAOA, démontant qu'un ensemble valide de paramètres existe.

Signification
L'article revendique une importance sur deux fronts principaux :

1. Résolution d'une conjecture de dix ans : Il tranche la puissance expressive exacte du QAOA de profondeur-$p$ sur l'anneau de désaccord, fournissant une garantie de performance rigoureuse pour un benchmark canonique en optimisation combinatoire.
2. Validation de la vérification formelle assistée par l'IA : Ce travail démontre que les LLM peuvent naviguer avec succès dans un raisonnement mathématique complexe lorsqu'ils sont couplés à des outils de vérification formelle. La méthodologie prouve que les modèles peuvent découvrir des structures mathématiques non triviales (telles que la connexion entre QAOA et QSP) et que le risque d'« hallucination » dans les arguments mathématiques longs peut être atténué par une boucle de vérification déterministe. Les auteurs notent que cette approche est applicable à d'autres conjectures ouvertes en information quantique et dans des domaines scientifiques plus larges où les problèmes peuvent être formulés de manière formelle.

L'article conclut que la preuve est frappante non seulement pour son résultat, mais aussi pour sa structure, qui unifie les symétries de fermions libres, la dynamique SU(2) et la théorie QSP — une voie qui n'avait pas été explorée auparavant dans la littérature sur cette conjecture spécifique.