Des agents d’IA de Google trouvent des programmes quantiques jusqu’à 290 fois moins coûteux, prouvés avec Lean

Le 6 novembre 2026, Google DeepMind et Google Quantum AI ont décrit des équipes d’agents d’IA qui écrivent des programmes quantiques et prouvent qu’ils sont corrects. Un agent est un logiciel d’IA qui enchaîne seul des tâches. Par rapport aux meilleures références publiées, ces programmes coûtent jusqu’à 290 fois moins cher sur une fonction mathématique, et 10,9 fois moins sur une simulation utile à la recherche sur la fusion. Les 25 auteurs les présentent dans un article sur arXiv, le serveur où les chercheurs publient leurs travaux avant toute relecture par une revue.

La preuve compte parce qu’un grand programme quantique ne peut pas être testé en grandeur réelle. Conçu pour des milliers de qubits, les unités d’information d’un ordinateur quantique, il est trop gros pour être simulé sur un ordinateur classique. Aucun ordinateur quantique ne sait encore l’exécuter. Les agents écrivent donc leurs preuves dans Lean, un assistant de preuve qui n’accepte une démonstration qu’après en avoir vérifié chaque étape.

Les équipes d’agents partageaient aussi un wiki, un site de notes commun, et se retrouvaient lors de « conférences » à heures fixes. Selon les auteurs, environ un quart des gains vient de ces conférences, en moyenne sur trois problèmes scientifiques.

Des circuits testés aux programmes prouvés

Selon l’article de Google, les programmes quantiques produits par l’IA n’ont jusqu’ici été testés que sur des circuits simulables par un ordinateur classique, donc assez petits ou assez simples. Un circuit quantique est la suite d’opérations qu’exécute un ordinateur quantique. Le 16 octobre, Anthropic annonçait ainsi que son IA Claude avait conçu des circuits quantiques jusqu’à 39 fois moins coûteux que les meilleurs publiés, chacun testé sur un ordinateur classique.

Pour remplacer le test par la preuve, les chercheurs de Google écrivent d’abord dans Lean une spécification. C’est un énoncé formel qui fixe ce que le programme doit calculer, avec quelle précision, et comment compter son coût.

Pour quatre des cinq problèmes, ce coût est le nombre de qubits logiques multiplié par le nombre de portes T. Un qubit logique est un qubit corrigé des erreurs, celui avec lequel calculera une future machine. Une porte T est une opération élémentaire particulièrement chère sur ces machines.

Les agents remplissent ensuite les trous de la spécification : le programme, son coût annoncé et les preuves qui valident l’un et l’autre. Lean signale chaque étape fausse, et les agents corrigent jusqu’à ce que Lean accepte les preuves.

Un arbitre automatique et un wiki commun

Chaque chercheur a configuré sa propre équipe d’agents : cadre logiciel, modèles de langage, consignes et répartition du travail. Les équipes vont d’un agent unique à des groupes hiérarchisés qui se partagent la conception, l’analyse des erreurs et l’écriture des preuves. L’article ne nomme pas les modèles de langage, les IA sur lesquelles reposent les agents.

Comme les agents peuvent modifier tous les fichiers de leur espace de travail, les auteurs préviennent qu’ils risquent d’exploiter des failles. Un agent pourrait affaiblir l’énoncé d’un théorème, changer une définition ou ajouter un axiome, une affirmation admise sans preuve. Un vérificateur externe rejoue donc chaque soumission sur une installation vierge. Avec l’outil Lean Comparator, il contrôle que les théorèmes visés et leurs définitions sont restés identiques à la spécification figée.

Les résultats vérifiés rejoignent le wiki commun : la meilleure solution pour chaque problème, des fichiers Lean réutilisables et des notes sur les pistes abandonnées. En règle générale, une nouvelle solution doit baisser le coût d’au moins 5 % par rapport à la meilleure solution en place.

Toutes les quatre heures, les équipes se retrouvent aussi en « conférence » sur un forum partagé, pour se poser des questions, critiquer des affirmations et proposer des constructions. Rien de ce qui s’y dit ne compte avant d’avoir été vérifié de façon indépendante, puis publié dans le wiki.

Cinq problèmes, cinq gains

Le premier problème est une recherche de Grover en parallèle, une méthode quantique pour trouver des éléments marqués dans une liste en lançant plusieurs requêtes à la fois. Les programmes vérifiés demandent jusqu’à 1,22 fois moins de tours de requêtes que la référence pour trouver un élément, et jusqu’à 1,41 fois moins pour les trouver tous.

Le gain de 290 fois porte sur la fonction arcsinus, qui retrouve un angle à partir de son sinus. Les algorithmes quantiques s’en servent pour charger des nombres dans un état quantique, c’est-à-dire dans les qubits.

La référence, un circuit publié en 2018 par Thomas Häner, Martin Roetteler et Krysta Svore, demande plus de 440 000 portes T sur 245 qubits. Le circuit des agents en utilise 3 698 sur 100 qubits. Une fois les qubits multipliés par les portes T, le coût est divisé par 290.

Le problème lié à la fusion nucléaire modélise la vitesse à laquelle le combustible absorbe l’énergie des particules alpha, des noyaux d’hélium libérés par les réactions de fusion. Le modèle place une particule alpha et 218 électrons au milieu de 216 protons fixes.

La référence, une estimation de 2024, demande 5 650 qubits logiques ; trois des auteurs du nouvel article l’ont cosignée. Le nouveau programme se contente de 4 374 qubits logiques et d’environ 8 fois moins de portes T, pour un coût 10,9 fois plus bas. Son idée principale est de placer les électrons sur une grille dans l’espace, où la physique interdit d’en trouver plus de deux au même point.

Les deux derniers problèmes relèvent de la chimie. Le premier simule le mouvement d’une molécule du type étudié pour les réactions déclenchées par la lumière, en traitant ses 47 noyaux et 187 électrons comme des particules quantiques. Le coût est divisé par 8,08.

Le second calcule les niveaux d’énergie du composé I, une forme éphémère des cytochromes P450, les enzymes qui dégradent la plupart des médicaments. Le coût est divisé par 2,49, avec 333 qubits logiques au lieu de 481.

Le poids des conférences entre équipes

Les auteurs attribuent leurs meilleures solutions à la collaboration entre équipes. Sept équipes ont travaillé sur le problème de la molécule, et le record a changé de mains sept fois après le premier essai. La plus forte baisse, 34 %, est partie d’une proposition faite en conférence par une équipe, puis affinée et prouvée par une deuxième.

Les auteurs ont aussi estimé d’où viennent les gains sur les trois problèmes scientifiques, une fois le wiki et les conférences en service. En moyenne, 61 % de la baisse de coût vient d’idées trouvées au sein d’une équipe, 15 % du wiki et 24 % des conférences. L’article reconnaît que la part de chaque canal est souvent difficile à isoler.

Les impasses circulaient aussi : une note démontrant qu’un raccourci ne pouvait pas marcher a arrêté deux propositions venues d’autres équipes.

D’autres projets s’appuient sur Lean

D’autres équipes construisent les mêmes outils dans Lean. Le 13 octobre, Mingsheng Ying et ses coauteurs ont présenté QEDIA, une bibliothèque Lean ouverte, faite de définitions et de preuves réutilisables, pour vérifier des programmes quantiques. Un agent de preuve fondé sur un modèle de langage l’a construite sous supervision humaine. L’article de Google la cite comme un travail mené en parallèle.

Le 21 octobre, Lei Zhang et ses coauteurs ont publié Lean-QuantumAlg, un ensemble de neuf algorithmes quantiques formalisés par l’IA, c’est-à-dire traduits en énoncés que Lean peut vérifier. La liste va jusqu’à des attaques quantiques contre le chiffrement RSA-2048. Selon l’article de Google, ces projets vérifient des algorithmes déjà connus, alors que son propre système utilise la preuve pour en chercher de moins coûteux.

L’usage de Lean avec l’IA dépasse aussi le quantique. En octobre, l’entreprise Axiom Math a utilisé des agents d’IA pour traduire une preuve de 15 000 pages en code Lean en 24 jours. Le 6 novembre, la jeune entreprise PSI a affirmé qu’un modèle inédit d’Anthropic avait démontré une conjecture quantique vieille de 18 ans, avec 648 théorèmes vérifiés dans Lean.

Le 9 novembre, Anthropic a indiqué qu’une équipe de 1 000 agents Claude Fable 5.2 avait formalisé le dernier théorème de Fermat en 30 heures. Selon Anthropic, une première formalisation, menée par une version de recherche non publiée de Claude, avait pris 11 jours.

Les limites reconnues par l’article

Les trois programmes de simulation restent trop gourmands pour les machines des prochaines années. Selon l’article, beaucoup d’applications utiles demandent entre un milliard et un million de milliards d’opérations. Les premiers processeurs tolérants aux fautes, capables de corriger leurs propres erreurs, devraient en traiter environ un million. Les auteurs écrivent qu’il faudra encore gagner plusieurs ordres de grandeur, soit plusieurs facteurs dix, pour que leurs simulations tiennent sur ces machines.

L’essentiel du gain de 290 fois sur l’arcsinus vient d’une recherche contrôlée par de simples tests sur ordinateur classique. Les agents ont d’abord exploré une famille restreinte de circuits, qu’un ordinateur classique vérifie en quelques secondes. Ils y ont trouvé un coût plus de 200 fois inférieur à celui de la référence. Lean a permis d’aller plus loin, et une dernière baisse de 11 % du coût est venue de circuits sortis de cette famille.

Deux éléments jouent en faveur de la référence de 2018. Elle visait une erreur d’environ un millionième, moins exigeante que celle fixée par la tâche, un huit-millionième. Les auteurs ne retiennent aussi qu’une borne basse de son coût, sa valeur minimale possible. En sens inverse, ils notent qu’un circuit plus récent de calcul de racine carrée pourrait rendre la référence jusqu’à trois fois moins coûteuse.

Lean vérifie chaque preuve par rapport à sa spécification, mais c’est aux chercheurs de juger si cette spécification décrit bien la physique. Les agents y ont d’ailleurs trouvé des failles. Ils ont par exemple exploité la façon dont étaient comptées les portes Toffoli, une autre opération de base, pour afficher un coût plus bas sans améliorer le circuit. Chercheurs et équipes d’agents ont refermé ces failles en corrigeant la spécification.

Le modèle de coût ignore aussi les codes correcteurs d’erreurs, le routage des qubits et leur disposition sur la puce.

Les humains gardent les décisions clés : des chercheurs ont choisi les problèmes, écrit les spécifications et configuré leurs équipes. Pour les auteurs, confier à l’IA la découverte d’algorithmes prouvés « déplace l’endroit où s’applique l’effort humain ». L’article est une prépublication, et sa bibliothèque Lean doit être publiée en code source ouvert « prochainement ».

Notre analyse

Pour la conception d’algorithmes quantiques par l’IA, le goulot d’étranglement était la vérification, limitée aux circuits qu’un ordinateur classique peut simuler. Cet article montre des agents qui travaillent sur des programmes de plusieurs milliers de qubits, avec une preuve à la place du test impossible. Chaque gain annoncé est un coût prouvé sur le papier : rien n’a tourné sur un ordinateur quantique.

L’article présente ces économies comme une moitié du chemin vers des machines utiles ; les progrès du matériel font l’autre. Pour les chercheurs, le travail se déplace du calcul de circuits à la main vers l’écriture de spécifications assez strictes pour que les agents ne puissent pas les contourner. Deux questions restent ouvertes : quels modèles ont fait le travail, et quelle puissance de calcul il a demandé.

Les prochaines étapes sont la publication de la bibliothèque Lean, avec ses spécifications et ses solutions, puis la relecture de l’article par une revue. Des équipes extérieures pourront alors rejouer les preuves et éprouver elles-mêmes les spécifications.

Sources

• Discovering formally verified quantum programs with AI, Sergey Shirobokov, Ben Jaderberg et al. (Google DeepMind, Google Quantum AI), arXiv, 6 novembre 2026
• Optimizing Quantum Circuits for Arithmetic, Thomas Häner, Martin Roetteler et Krysta Svore, arXiv, 31 mai 2018
• Quantum computation of stopping power for inertial fusion target design, Nicholas C. Rubin et al., arXiv (publié dans PNAS en 2024), 23 août 2023
• comparator: A trustworthy judge for Lean proofs from untrusted sources, Lean FRO, GitHub, consulté le 10 novembre 2026
• QEDIA: Quantum Program Verification in Lean, Yuanjie Ren, Zhicheng Zhang, Junyi Liu, Jinzheng Li, Yidi Qi et Mingsheng Ying, arXiv, 13 octobre 2026
• Lean-QuantumAlg: A Framework for AI Agents to Produce Quantum Algorithms that Humans Can Trust, Lei Zhang, Mingrui Jing, Yusheng Zhao, Jiahong Liu et Xin Wang, arXiv, 21 octobre 2026
• Introducing Claude Fable 5.2 and Claude Mythos 5.2, Anthropic, 9 novembre 2026

Image d’en-tête : graphique MACCUS, données de Shirobokov et al. (Google DeepMind, Google Quantum AI), arXiv 2611.09822, 6 novembre 2026