La cryptographie a un goulot de validation
Mise à jour : deux preuves contrôlées ne font pas encore consensus
OpenAI et Anthropic affirment désormais que leurs modèles ont réfuté indépendamment l'hypothèse du temps exponentiel, ou ETH.
Les deux laboratoires ont publié des artefacts Lean.
Cela ne signifie pas que la communauté informatique a accepté le résultat.
La distinction compte, car ETH n'est pas un benchmark obscur. C'est une hypothèse fondamentale utilisée pour montrer que des centaines de problèmes ne peuvent pas être résolus beaucoup plus vite. Sa réfutation redessinerait la carte de la théorie de la complexité.
Elle ne démontrerait pas que P est égal à NP. Elle ne rendrait pas SAT facile. Et elle ne transformerait pas soudain les problèmes d'optimisation difficiles d'aujourd'hui en tâches pratiques.
L'artefact de recherche d'Anthropic le précise lui-même : l'algorithme annoncé est purement asymptotique et ne dit rien sur la résolution pratique de formules.
Voilà exactement le type de résultat pour lequel « Lean l'a vérifié » semble clore le débat.
En réalité, c'est le début d'un processus d'examen bien plus intéressant.
La preuve formelle a une frontière
Un assistant de preuve répond à une question précise :
Cette dérivation formelle établit-elle cet énoncé formel dans cette logique ?
C'est une question extrêmement précieuse. Elle élimine une immense catégorie d'erreurs de calcul, de cas oubliés et de raisonnements séduisants mais incomplets. Un modèle ne peut pas embobiner le noyau de Lean.
Mais ce noyau ne sait pas ce que l'article voulait affirmer.
Anthropic le dit sans détour. Son court fichier MainResults.lean contient les théorèmes que le lecteur doit examiner. Lean contrôle les preuves qui les sous-tendent mais, comme le précise le dépôt, aucune machine ne vérifie que le fichier dit bien la même chose que l'article.
Le projet rend cet écart exceptionnellement visible. Il fige les versions de Lean et Mathlib, consigne les axiomes standards utilisés, relie les énoncés de l'article à leurs équivalents formels et soumet la preuve à nanoda, un second noyau écrit indépendamment.
Nous obtenons ainsi des éléments solides sur la dérivation.
Cela n'établit pas automatiquement la correspondance entre l'article et le théorème, la pertinence de chaque choix d'encodage ni l'interprétation du résultat.
OpenAI expose une autre frontière. Sa note sur le périmètre de la formalisation Lean vérifie un algorithme de comptage exact, en temps sous-exponentiel, pour des formules CNF de largeur fixe. Mais la borne contrôlée contient un facteur log log n supplémentaire par rapport à la borne plus fine de l'article associé.
Les deux bornes suffiraient à réfuter ETH si l'énoncé formel, la preuve et leur interprétation résistent tous à l'examen.
Ce ne sont tout de même pas des affirmations identiques.
Voilà à quoi ressemble la vérification formelle quand le titre dépasse le fichier du théorème : la preuve peut être contrôlée tandis que l'affirmation scientifique exige encore un rapprochement humain minutieux.
OpenAI publie un processus de revue, pas un tour d'honneur
La décision la plus importante d'OpenAI n'est peut-être pas la publication de la preuve Lean.
C'est le vocabulaire qui l'accompagne.
L'entreprise décrit ses nouveaux manuscrits comme des données de recherche brutes qu'il faut transformer en compréhension scientifique. Pour l'affirmation sur ETH, elle a constitué un groupe extérieur dirigé par Russell Impagliazzo, Ramamohan Paturi et Ryan Williams.
Impagliazzo et Paturi ont contribué à formuler ETH.
Les participants ne sont pas rémunérés, n'ont signé aucun accord de confidentialité et restent libres de publier leurs propres conclusions. OpenAI a accepté de fournir les données brutes et de financer une conférence pendant laquelle le domaine pourra examiner l'affirmation et ses conséquences.
Cela ne certifie pas le résultat.
À ce stade, cela fait quelque chose de plus utile : séparer la découverte de son acceptation.
Le modèle a produit un artefact. L'assistant de preuve a contrôlé une dérivation formelle. Des spécialistes doivent maintenant comprendre l'argument, comparer les affirmations formelles et informelles, le replacer dans la littérature et décider ce qui en découle.
Ce sont des tâches différentes.
Les réduire à « l'IA a résolu ETH » ferait disparaître la partie la plus mature de cette publication.
Le mot « vérifié » a désormais besoin de niveaux
Les laboratoires d'IA produisent des artefacts techniques plus vite que les communautés expertes ne peuvent les absorber. Une étiquette binaire ne résistera pas à ce volume.
Il nous faut une échelle de validation :
- Contrôlé par un noyau : la preuve formelle passe dans un petit vérificateur de confiance.
- Énoncé audité : les spécialistes conviennent que le théorème formel exprime l'affirmation visée.
- Correspondance auditée : l'article, le théorème, les encodages et l'implémentation décrivent le même résultat.
- Compris indépendamment : des chercheurs extérieurs peuvent reconstruire l'argument, pas seulement relancer le vérificateur.
- Situé scientifiquement : la communauté comprend ce que le résultat change, ce qu'il laisse ouvert et quels travaux antérieurs dépendaient de l'hypothèse abandonnée.
Les publications d'OpenAI et d'Anthropic semblent solides au premier niveau.
Elles fournissent un matériau inhabituellement riche pour atteindre les suivants.
Elles n'ont pas gravi toute l'échelle simplement parce que les contrôles sont au vert.
Ce n'est pas du scepticisme envers les méthodes formelles. C'est précisément ce qui les rend utiles. Elles divisent une grande question floue en plusieurs questions plus petites dont les réponses peuvent être examinées séparément.
La nouvelle unité de publication est toute la pile de revue
L'article scientifique traditionnel réunissait la découverte, l'explication et la persuasion dans un même document.
La recherche produite par IA a besoin d'une unité de publication plus épaisse :
- l'argument en langage naturel,
- l'énoncé formel exact,
- la preuve contrôlée par machine,
- les dépendances figées et les axiomes autorisés,
- une table de correspondance entre l'article et la formalisation,
- une expertise extérieure,
- et un historique public de ce qui a été accepté, corrigé ou rejeté.
L'artefact de preuve n'est pas une annexe décorative.
Le processus de revue n'est pas un délai protocolaire.
Ensemble, ils constituent le produit.
Si les affirmations sur ETH tiennent, ce sera un résultat majeur en théorie de la complexité et une démonstration saisissante de découverte assistée par IA.
Si un décalage caché les modifie ou les invalide, ces publications nous auront tout de même appris quelque chose d'important sur l'évaluation de la science produite par machine.
Dans les deux cas, la leçon est déjà visible.
Quand les modèles peuvent générer des preuves plus vite que les humains ne peuvent les comprendre, la validation ne peut pas s'arrêter à « le fichier compile ».
C'est là que la compréhension commence.
Mise à jour : le vérificateur de preuves déplace le goulot
Anthropic et Theorem viennent de produire environ 180 millions de lignes de preuve vérifiée par machine.
Personne n'a besoin de les lire.
Ce n'est pas une plaisanterie sur la documentation. C'est précisément l'intérêt du projet.
Le 22 octobre, Anthropic a publié un travail de vérification formelle dans lequel Claude a corrigé des bugs, puis démontré qu'aucun crash n'était atteignable depuis 239 points d'entrée de fuzzing répartis dans 123 bibliothèques open source, sous un ensemble précis de conditions. Les preuves portent sur des instructions RISC-V compilées, pas sur le code source. Rocq, un assistant de preuve, vérifie que chacune satisfait son théorème.
Selon Anthropic, les preuves qui ont abouti représentent environ 180 millions de lignes de Rocq. Une preuve typique en compte près de 600 000.
Dans un processus de revue ordinaire, ce volume serait absurde.
Ici, il devient surtout une facture de calcul. Le vérificateur ne se fatigue pas, ne survole pas les passages répétitifs et ne se laisse pas impressionner par une notation assurée. La preuve satisfait le théorème dans la logique de Rocq, ou elle échoue.
C'est un vrai changement dans l'économie de la validation décrite dans cet article.
Ce n'est pas la fin de la validation.
Le jugement humain rare se déplace vers une surface plus petite et plus importante :
Qu'avons-nous exactement demandé à la machine de prouver ?
Le résultat va plus loin qu'un nouveau scanner de sécurité
Le fuzzing cherche une entrée qui fait échouer un programme. Il peut exécuter des milliers de milliards de tests sans jamais établir qu'aucune entrée défaillante n'existe.
Anthropic et Theorem ont transformé des cibles OSS-Fuzz existantes en énoncés formels portant sur des binaires compilés. Pour les cibles traitées avec succès, Claude a généré des preuves qui couvrent chaque entrée modélisée dans les limites annoncées, pas seulement celles que le fuzzer a eu la chance d'essayer.
Le processus a aussi fait remonter des bugs que les tests n'avaient pas trouvés. Une preuve ne peut pas se fermer tant qu'il reste un contre-exemple atteignable. Les tentatives qui échouent deviennent donc une manière de localiser le code ou l'hypothèse qui empêche le théorème d'être vrai.
Cette combinaison compte.
Un scanner IA dit : « J'ai trouvé un autre bug possible. »
Une preuve vérifiée dit : « Pour ce binaire précis, ce point d'entrée précis, cette propriété précise et ces hypothèses précises, il n'existe aucun contre-exemple. »
La seconde affirmation est plus étroite.
Elle est aussi beaucoup plus forte.
L'annexe technique indique que Claude a généré environ un milliard de lignes de Rocq pendant ses tentatives. Environ 180 millions ont été conservées dans les preuves validées. Plus de la moitié d'une preuve typique correspond à des données émises par des outils, et le contrôle d'une seule preuve peut demander de trente minutes à plusieurs heures de calcul CPU.
Cela ne ressemble pas à un ingénieur en méthodes formelles devenu un peu plus rapide.
Cela ressemble à une production de preuves devenue une charge industrielle.
L'énoncé du théorème devient la frontière du produit
Le titre public se résume facilement en « Claude a prouvé que 123 bibliothèques ne peuvent pas planter ».
C'est trop large.
Les affirmations réelles portent sur certains points d'entrée de fuzzing, dans des binaires RISC-V statiques précis, exécutés dans un modèle formel de processus Linux. Le travail suppose une exécution mono-thread, un budget mémoire fixe, musl plutôt que l'environnement glibc dynamique courant sous Linux, ainsi que des comportements modélisés du système d'exploitation.
Il ne prouve pas que chaque bibliothèque entière est correcte.
Il ne couvre pas le code inaccessible depuis le point d'entrée choisi.
Il ne détecte pas toutes les erreurs de mémoire ou de logique que l'AddressSanitizer et le harnais n'expriment pas.
Il ne prouve pas que les appelants utilisent correctement la bibliothèque.
Et le dépôt public des preuves ne contient pour l'instant qu'un sous-ensemble du travail annoncé : 60 points d'entrée dans 25 bibliothèques, pas les 239 points d'entrée des 123 bibliothèques. C'est assez pour permettre une inspection extérieure, mais pas pour reproduire indépendamment le résultat complet mis en avant.
Le dépôt décrit ses propres limites avec une précision bienvenue. Il indique que les preuves publiées portent sur des binaires RISC-V statiques déterminés, que son modèle Linux Process Semantics est incomplet et qu'aucune preuve publiée n'exclut une exécution qui ne se termine jamais.
Voilà à quoi ressemble une vérification formelle responsable.
Pas « le logiciel est sûr ».
Mais « ce théorème tient pour cet artefact dans ce modèle ».
On peut vérifier une preuve et prouver la mauvaise chose
La vérification formelle change la nature des erreurs encore possibles.
Elle supprime en grande partie le besoin de faire confiance à l'auteur de la preuve. Rocq la contrôle mécaniquement. Un modèle ne peut pas embobiner le noyau avec une prose élégante.
Mais le vérificateur ne peut pas dire si le théorème capture la propriété qui compte pour les utilisateurs.
Il ne peut pas dire si la sémantique formelle de RISC-V et de Linux reproduit assez fidèlement la vraie machine.
Il ne peut pas dire si l'absence de crash exclut la faille pertinente dans le modèle de menace.
Il ne peut pas dire si le binaire x86 ou ARM déployé se comporte comme le binaire RISC-V vérifié.
Il ne peut pas dire si un correctif a préservé le comportement voulu par les mainteneurs.
Anthropic signale directement ce dernier risque. Claude pouvait modifier le code avant d'en produire la preuve, ce qui ouvre une voie évidente au contournement de l'objectif : rendre le théorème facile en supprimant ou en court-circuitant le comportement. L'équipe dit avoir pénalisé les patchs, récompensé les changements de comportement minimaux, journalisé les modifications et les avoir auditées.
Ces contrôles sont utiles.
Ils montrent aussi que la spécification et la politique de modification font désormais partie du périmètre de sécurité.
Quand la production de preuves devient bon marché, le travail humain précieux consiste à définir le théorème, examiner le modèle de confiance, relire les correctifs et décider si l'artefact vérifié correspond à la production.
La preuve peut être parfaitement valide tandis que l'affirmation d'assurance est fausse.
L'artefact public compte plus que le nombre de lignes
Cent quatre-vingts millions de lignes : c'est le chiffre irrésistible.
Le dépôt est la publication la plus importante.
Theorem y fournit les énoncés, les binaires, les traces de provenance, les versions d'outils épinglées, les axiomes autorisés, les instructions de contrôle et les workflows de vérification continue. Un tiers peut examiner l'affirmation, relier le binaire à ses entrées de compilation et lancer le vérificateur sans faire confiance à Claude.
C'est la bonne architecture pour un travail technique généré par IA.
Ne demandons pas à une personne de lire tout ce que le modèle a produit.
Réduisons la surface de confiance. Figeons-la. Publions-la. Rendons l'affirmation décisive exécutable. Laissons un petit vérificateur rejeter l'immense artefact.
L'écart restant doit rester visible, pas être lissé par un résumé.
Ici, ces écarts séparent le résultat complet annoncé du sous-ensemble public, RISC-V des architectures réellement déployées, la couverture d'une cible de fuzzing de la correction d'une bibliothèque, et l'absence de crash d'une sécurité plus large.
Ces réserves n'annulent pas le résultat.
Elles le définissent.
La vérification formelle pourrait devenir une étape normale du build
Theorem propose désormais OSS Verify gratuitement aux projets open source éligibles. Les mainteneurs peuvent soumettre leur recette de compilation et leurs cibles de fuzzing, recevoir en privé les bugs découverts en chemin, puis obtenir des preuves Rocq portant sur leurs binaires.
Un workflow concret se dessine :
- Écrire un test qui échoue quand une propriété est violée.
- Le soumettre au fuzzing pour trouver rapidement les contre-exemples faciles.
- Utiliser des agents pour corriger ou expliquer les échecs restants.
- Transformer le harnais en théorème portant sur l'artefact compilé.
- Laisser un vérificateur établir qu'aucun contre-exemple couvert ne subsiste.
- Conserver le théorème, la provenance du binaire, les hypothèses et la version du vérificateur avec la release.
Les tests ne disparaissent pas.
Ils deviennent le premier filtre, peu coûteux, et une source de spécifications.
La vérification formelle ne certifie pas tout le produit.
Elle transforme certaines affirmations de sécurité en artefacts de build dont l'échec est déterministe.
C'est bien plus utile que de traiter « formellement vérifié » comme un label.
Le nouveau bilan
Claude n'a pas prouvé que 123 bibliothèques open source étaient exemptes de bugs.
Anthropic et Theorem ont démontré quelque chose de plus crédible et, en pratique, de plus important : les modèles de pointe peuvent générer d'immenses preuves portant sur du logiciel compilé réel, et un petit noyau indépendant peut les contrôler sans faire confiance au modèle.
Le goulot s'est déplacé.
Un humain n'a plus besoin de relire chaque étape de la preuve.
Il faut encore choisir la bonne propriété, examiner la sémantique de confiance, relire les patchs, relier le binaire vérifié à la production et décrire le résultat sans le gonfler.
L'avenir de la validation technique contiendra peut-être bien plus de preuves générées par machine qu'une personne ne pourra jamais en absorber.
Cela peut fonctionner.
Mais seulement si l'affirmation de confiance rétrécit à mesure que la pile de preuves grandit.
Mise à jour : le vérificateur doit être vérifié
Google vient de transformer le goulot décrit dans cet article en produit.
Le 14 octobre, Google Research a ouvert Deep Review au public. Selon Google, une version antérieure a été utilisée sur plus de 16 000 soumissions volontaires à STOC, ICML, NeurIPS et ICLR.
Le service accepte les PDF et le texte brut, offre deux revues gratuites par semaine à chaque utilisateur et propose une API pour les usages plus intensifs. Google dit qu'il peut examiner le raisonnement mathématique, la cohérence logique, les protocoles expérimentaux, les citations et les comparaisons avec les travaux antérieurs. Le système vise aussi des documents qui dépassent la recherche : dossiers de conception, présentations, contrats et rapports financiers.
C'est une réponse raisonnable à l'abondance technique produite par l'IA.
Si les modèles accélèrent la production d'affirmations, utilisons des modèles pour accélérer leur contrôle.
Mais une traduction produit dangereuse se cache dans cette phrase.
« Le modèle l'a relu » peut très vite devenir « le document a été vérifié ».
Ce ne sont pas les mêmes états.
Deep Review paraît utile. Les éléments qui l'étayent sont sérieux. Son architecture va bien plus loin que demander au même chatbot de critiquer sa propre réponse.
Il produit tout de même une revue par IA qu'une personne qualifiée doit évaluer.
Le goulot de validation n'a pas disparu.
Il dispose maintenant d'une API.
C'est un pipeline de revue, pas un prompt malin
Deep Review repose sur un système agentique en quatre étapes.
Un premier agent découpe le document en sections logiques. Une étape de budgétisation attribue davantage de calcul aux passages denses. Des agents spécialisés examinent les sections en parallèle tout en conservant l'accès au document complet. Un dernier agent synthétise les résultats, vérifie la cohérence entre les sections et utilise des outils externes pour étayer ses conclusions.
Cette architecture compte.
Un long document technique n'est pas une seule question. Une preuve peut dépendre d'une définition donnée 30 pages plus tôt. Une expérience peut contredire une affirmation de l'introduction. Un graphique peut ne pas soutenir la conclusion écrite juste à côté. Un appel unique au modèle peut épuiser son budget de raisonnement utile, se concentrer sur les sections faciles ou accepter une déclaration impressionnante sans la tester.
Le système de Google répartit l'attention, puis rassemble les résultats.
Nous retrouvons la même leçon que pour tous les agents : le modèle compte, mais le harnais détermine sa capacité à mener un travail prolongé.
Le produit intéressant n'est pas Gemini qui annonce : « J'ai trouvé trois problèmes. »
C'est la machine qui décide où chercher, combien d'effort consacrer, quelles preuves récupérer et comment réunir des constats contradictoires.
Deep Review est donc plus crédible qu'un simple prompt de relecture.
Cela ne rend pas sa sortie vraie par construction.
Plusieurs agents coordonnés peuvent partager le même angle mort. Un agent de synthèse peut polir une critique erronée jusqu'à la rendre plus autoritaire. L'ancrage externe peut confirmer l'existence d'un article sans prouver que celui-ci soutient l'affirmation. Davantage d'inférence peut améliorer le rappel tout en produisant plus de faux positifs plausibles qu'un humain devra examiner.
Deux agents IA qui se contrôlent ne constituent pas une revue par les pairs.
Ils constituent une réunion.
Les résultats sont prometteurs et plus étroits que le produit
L'article sur le Paper Assistant Tool de Google offre davantage qu'une démonstration de lancement.
Sur un sous-ensemble filtré du benchmark SPOT comprenant 29 erreurs connues d'équation ou de preuve dans 26 articles de mathématiques et d'informatique rétractés, le pipeline a détecté 89,7 % des erreurs. Une revue zero-shot par Gemini 3.1 Pro en a détecté 55,2 %.
C'est un résultat important.
C'est aussi une évaluation signée par Google d'un système Google, sur un petit sous-ensemble sélectionné, avec un évaluateur sur modèle conçu pour l'étude et dont les décisions ont été auditées par l'un des auteurs. Elle mesure le rappel sur des erreurs connues. Elle n'établit pas combien de fausses alertes le système produirait sur des articles ordinaires et corrects, dans des domaines inconnus, face à des documents adversariaux ou sur des sujets juridiques et financiers.
Les pilotes menés avec les conférences apportent des éléments utiles en conditions réelles.
Dans le bilan publié par ICML, 92,1 % des répondants ont déclaré qu'ils réutiliseraient l'outil. Parmi ceux dont les articles comportaient des résultats théoriques, 35,4 % disent qu'il a trouvé une lacune importante ayant demandé plus d'une heure de correction. Parmi les auteurs d'expériences, 31 % disent que les retours les ont conduits à en lancer de nouvelles.
Ces chiffres sont impressionnants.
Un autre chiffre mérite la même visibilité.
Dans l'enquête combinée STOC-ICML de l'article, seuls 55,8 % puis 64,8 % des répondants ont qualifié les retours de majoritairement ou entièrement fondés.
Cela ne fait pas de Deep Review un mauvais système.
Cela nous indique la mission pour laquelle il est prêt.
Deep Review est une puissante revue de précontrôle. Il peut signaler les endroits où un auteur devrait ralentir, reproduire un résultat, expliquer une hypothèse, relancer une expérience ou consulter un expert.
Ce n'est pas un tampon de certification.
Les limites du pilote jouaient un rôle essentiel
Les déploiements auprès des conférences étaient soigneusement encadrés.
Les auteurs choisissaient de participer. Les retours restaient privés. Ils arrivaient avant la soumission. Ils étaient séparés de la revue officielle. Les auteurs restaient responsables de décider quels constats étaient corrects. Le programme NeurIPS avertissait explicitement que le modèle pouvait présenter un énoncé juste comme faux ou manquer une vraie erreur.
C'est un bon modèle opérationnel.
L'IA aide l'auteur à trouver le travail qui reste à faire.
Elle ne décide pas si l'article est accepté.
Le lancement public étend le système à un territoire beaucoup plus large. Google suggère maintenant de relire des documents juridiques et financiers, où une critique apparemment rigoureuse peut influencer des contrats, des obligations réglementaires, des investissements et des litiges.
Les éléments publics ne démontrent pas encore une performance équivalente dans ces domaines.
Repérer que deux clauses se contredisent est utile.
Décider laquelle est applicable relève du jugement juridique.
Repérer un désaccord entre un tableau et un paragraphe est utile.
Décider si une prévision financière est prudente n'est pas une tâche de cohérence interne.
Le produit doit préserver cette frontière dans son interface et dans son API.
Une revue terminée signifie que le système a fini de chercher.
Elle ne signifie pas que le document est validé.
Chaque constat a besoin d'un reçu
Le meilleur agent de revue devrait être plus facile à auditer que le document qu'il examine.
Pour chaque constat important, le système devrait produire un reçu comprenant :
- l'affirmation ou le passage exact examiné
- le type de problème : logique, mathématique, empirique, factuel, juridique ou éditorial
- la source, le calcul, l'appel d'outil ou le contre-exemple qui étaye le constat
- les hypothèses nécessaires pour que la critique soit valable
- un niveau de confiance et une description de ce qui reste incertain
- un chemin de reproduction lorsque la reproduction est possible
- le modèle, le harnais, les outils et leur version
- la décision de l'auteur ou du réviseur : accepté, rejeté, corrigé ou non résolu
Cette dernière ligne est essentielle.
Une critique rejetée ne devrait pas disparaître. Elle devrait rester attachée au dossier avec la raison du rejet. Sans cela, les équipes ne peuvent ni mesurer les faux positifs récurrents, ni comparer les versions du modèle, ni voir qu'un autre réviseur soulève plus tard le même problème avec de meilleures preuves.
Les affirmations à fort enjeu exigent aussi de l'indépendance.
Si un modèle a aidé à écrire le document, un autre passage de la même famille de modèles ne devrait pas compter comme vérification indépendante. Il faut une autre méthode, un autre modèle ou fournisseur, des contrôles exécutables et une expertise humaine du domaine. Il faut conserver les désaccords au lieu de demander à un agent de synthèse de les fondre dans un paragraphe fluide.
L'objectif n'est pas un texte qui ressemble à un consensus.
C'est une preuve inspectable.
La politique de données fait partie de la revue
Une autre différence sépare les pilotes de conférences du produit public.
Le pilote NeurIPS prévoyait la suppression des soumissions et des retours dans les sept jours suivant le programme. Google indique que les documents envoyés au service public Deep Review ne servent pas à l'entraînement, mais restent stockés pendant un an afin d'être consultables dans l'interface.
Ce choix produit peut être raisonnable.
Ce n'est pas une note de bas de page pour un théorème inédit, un projet de brevet, une analyse de sécurité, un litige ou un plan financier.
Avant d'envoyer un document, les équipes doivent décider si cette durée de conservation lui convient. Une intégration par API devrait exposer la conservation, la suppression, la région, les accès et l'audit comme des paramètres, pas les enfouir dans une page de politique.
Le système est conçu pour découvrir les risques cachés dans des documents sensibles.
Il ne devrait pas en créer silencieusement un nouveau autour d'eux.
La nouvelle conclusion
Deep Review est l'un des produits agentiques les plus utiles lancés cette année parce qu'il s'attaque à une vraie contrainte au lieu d'ajouter du contenu à la pile.
Son architecture est réfléchie, il dispose d'éléments tirés de vrais pilotes auprès de conférences et son premier rôle, comme outil privé pour les auteurs, est raisonnable.
Le risque n'est pas que l'outil soit inutile.
Le risque est que son utilité se transforme en autorité plus vite que les preuves ne le permettent.
Appelez cela un précontrôle.
Rendez chaque constat auditable.
Laissez les décisions lourdes de conséquences à des experts responsables.
Utilisez des méthodes indépendantes pour obtenir une vérification indépendante.
Et ne transformez jamais une réponse d'API en coche verte simplement parce que le mot review apparaît dans l'endpoint.
L'IA peut aider à accélérer la validation.
Évitons maintenant d'automatiser la fausse assurance au même rythme.
La version courte
Claude n'a pas cassé Internet.
C'est la première chose à dire.
Le 28 juillet, Anthropic a publié une recherche sur la découverte de faiblesses cryptographiques avec Claude. En utilisant Claude Mythos Preview, des chercheurs d'Anthropic ont trouvé une attaque améliorée contre HAWK, un candidat de signature post-quantique examiné dans le processus du NIST, et une attaque plus rapide contre une version réduite d'AES.
Anthropic est explicite sur la limite : ces résultats n'affectent pas les systèmes de production aujourd'hui. HAWK est un schéma candidat, pas une plomberie déjà déployée sur Internet. Le résultat AES concerne une version de recherche affaiblie à 7 tours, pas l'AES-128 complet à 10 tours dont les systèmes dépendent réellement.
Très bien.
Mais l'histoire reste importante.
Pas parce qu'il faut paniquer sur les mots de passe.
Pas parce que Claude serait soudain un magicien avec un crochet de serrurier.
La leçon utile est plus simple, et plus gênante :
L'IA rend la production de résultats de recherche moins chère que leur validation.
Anthropic dit que l'attaque contre HAWK a demandé environ 60 heures de travail assisté par Claude, et que chacun des deux principaux résultats a coûté à peu près 100 000 dollars en coûts d'API. Le résultat sur l'AES réduit a pris environ une semaine à Mythos pour être découvert, mais les chercheurs ont ensuite passé des centaines d'heures à apprendre assez de cryptographie pour le valider. Anthropic dit que deux chercheurs ont eu besoin de presque un mois pour prendre confiance dans le résultat AES.
C'est ça, le vrai changement produit.
Le modèle peut proposer, chercher, coder, tester, abandonner, puis proposer encore.
L'humain doit toujours savoir si quelque chose est vrai.
Très futuriste. On a automatisé la partie difficile et découvert une partie encore plus difficile derrière.
C'est de l'accélération de recherche, pas de la magie
La cryptographie est un bon endroit pour rester discipliné sur les affirmations.
Le domaine suppose déjà une revue adversariale. Un nouveau chiffrement est proposé, attaqué, révisé, débattu, benchmarké, cassé, défendu, puis parfois standardisé après des années d'examen. L'échec n'est pas embarrassant de la même manière que dans un lancement produit. L'échec fait partie de la méthode.
C'est pour cela que le résultat d'Anthropic sur HAWK n'est pas seulement un titre inquiétant.
HAWK était dans un processus de revue conçu précisément pour faire apparaître ce genre de faiblesse avant le déploiement. Anthropic dit que Claude Mythos a trouvé une symétrie non exploitée jusque-là dans la structure de réseau utilisée par HAWK, puis l'a utilisée pour accélérer la récupération de clé. L'effet immédiat est que certaines tailles de clés proposées pour HAWK semblent beaucoup plus faibles que prévu, au point qu'il faudrait les doubler pour retrouver le même niveau de sécurité.
C'est important pour ce candidat.
Cela ne veut pas dire que la cryptographie post-quantique est cassée.
Cela ne veut pas dire que tous les schémas à base de réseaux sont condamnés.
Cela veut dire que le processus de revue vient de recevoir un nouvel attaquant.
C'est exactement le fonctionnement normal de la cryptographie.
Le résultat AES est encore plus facile à mal lire. Anthropic dit que Mythos a amélioré des attaques contre une version AES-128 à 7 tours, en réduisant le travail d'une attaque meet-in-the-middle existante d'environ 200 à 800 fois selon la manière dont on mesure le temps d'exécution.
Là encore : AES-128 complet a 10 tours.
Les chercheurs étudient des versions réduites pour comprendre les marges, pas parce que votre banque utilise secrètement un AES jouet.
La bonne conclusion n'est donc pas :
"L'IA a cassé le chiffrement."
C'est :
"L'IA devient utile dans le type de recherche adversariale technique dont dépend la cryptographie."
Moins spectaculaire.
Plus important.
La boucle agentique est l'instrument
La partie la plus intéressante n'est pas que Claude ait répondu à une question de cryptographie.
C'est la manière dont le travail s'est déroulé.
Anthropic décrit un harness proche de Claude Code, avec plusieurs agents de travail, des outils sandboxés, Python, Sage, l'accès à des travaux cryptographiques publiés, et assez d'autonomie pour lancer des expériences de calcul. Pour HAWK, l'opérateur humain n'était pas expert en cryptographie à base de réseaux. Anthropic dit que l'humain donnait surtout une forme de gestion de projet : garder la trace des idées, utiliser telle bibliothèque, vérifier telle affirmation.
C'est différent de demander à un chatbot :
"Trouve une faiblesse cryptographique."
Le modèle ne produisait pas seulement du texte. Il lisait des papiers, formulait des hypothèses, écrivait du code, testait des idées, rejetait des pistes, coordonnait des sous-agents et construisait des pipelines de vérification.
C'est le même motif que l'on retrouve partout dans les agents IA :
Le modèle compte.
Le harness compte autant.
Les outils comptent.
Les logs comptent.
La capacité à lancer beaucoup d'essais compte.
La capacité à conserver des idées partielles compte.
L'utilisateur est moins un rédacteur de prompt qu'un chef de projet de recherche.
Ce dernier point est inconfortable, parce qu'il sonne à la fois puissant et très facile à exagérer. Une personne non experte avec un modèle fort et un bon échafaudage agentique peut pousser dans un territoire d'experts, mais le dernier kilomètre appartient toujours à l'expertise. L'histoire AES d'Anthropic le prouve elle-même. Le modèle a trouvé l'idée rapidement. Les humains ont ensuite dû faire le travail lent : décider si l'idée était réelle.
Ce n'est pas une note de bas de page.
C'est le goulot.
La vérification devient la compétence rare
L'industrie IA parle beaucoup de "scientifiques IA".
Voilà à quoi cette expression ressemble quand elle arrête d'être un slogan.
Le résultat n'est pas une réponse polie.
C'est une pile d'hypothèses, d'expériences, de code, de logs, de pistes abandonnées, de preuves partielles et d'un résultat étrangement intéressant.
Quelqu'un doit le valider.
Quelqu'un doit connaître la littérature.
Quelqu'un doit reproduire l'attaque.
Quelqu'un doit vérifier les hypothèses.
Quelqu'un doit distinguer le nouveau du redécouvert.
Quelqu'un doit décider si le résultat compte dans un vrai modèle de menace.
Quelqu'un doit coordonner la divulgation.
Quelqu'un doit prévenir le NIST, les auteurs, les vendeurs, les gouvernements ou les utilisateurs sans transformer par accident un résultat de recherche en tutoriel d'exploitation.
Voici le futur moins glamour de la science accélérée par IA :
la file de revue s'allonge.
Si les modèles peuvent produire de la recherche plausible plus vite que les humains ne peuvent la valider, la question institutionnelle clé n'est pas seulement de créer plus de découvertes. C'est de savoir comment les trier sans se noyer.
Cela dépasse largement la cryptographie.
Découverte de médicaments.
Matériaux.
Démonstration de théorèmes.
Recherche sécurité.
Biologie.
Design de puces.
Chaque domaine où un système IA peut proposer à bas coût des milliers d'affirmations techniques aura besoin d'une meilleure machine de validation.
Le goulot se déplace de l'imagination vers la vérification.
Magnifique. La revue par les pairs était trop rapide et trop reposante de toute façon.
Ne confondez pas confiance et exactitude
Un des détails les plus étranges du billet d'Anthropic est que Claude a d'abord résisté au travail sur AES.
Anthropic dit que les premiers essais faisaient conclure à Claude qu'améliorer les attaques contre AES était globalement trop difficile. Les chercheurs l'ont poussé à continuer, à chercher un résultat publiable, et à ne pas fuir vers des cibles plus simples. Mythos a finalement produit l'idée de Möbius Bridge derrière l'attaque améliorée sur AES réduit.
C'est fascinant.
C'est aussi un avertissement.
Le modèle peut avoir tort quand il est trop pessimiste.
Le modèle peut avoir tort quand il est trop confiant.
Le modèle peut avoir raison pour des raisons difficiles à auditer.
Le modèle peut créer assez de matière technique pour que l'humain se retrouve en retard.
C'est pour cela que "le modèle pense avoir trouvé quelque chose" n'est pas un résultat.
C'est une piste.
En ingénierie logicielle, une piste peut souvent être testée vite. Le test passe-t-il ? L'exploit se reproduit-il ? Le patch marche-t-il ? Même là, c'est désordonné.
En cryptographie, l'objet est plus abstrait. Une preuve peut cacher une mauvaise hypothèse. Une attaque peut dépendre de ressources impossibles. Un résultat peut être mathématiquement valide et pratiquement sans effet. Un raccourci peut être une vieille littérature avec un nouveau nom.
Donc l'interface de la recherche IA ne devrait pas être un écran de victoire.
Elle devrait être une salle de preuves.
Montrez le raisonnement.
Montrez le code.
Montrez les tentatives ratées.
Montrez les étapes de reproduction.
Montrez les hypothèses.
Montrez où le modèle devine.
Montrez ce qu'un expert humain doit encore vérifier.
Si le lab IA ne peut pas produire cela, il n'a pas produit de recherche. Il a produit une affirmation avec une jolie typographie.
Le double usage devient plus tranchant
La cryptanalyse est à double usage par nature.
Trouver une faiblesse peut rendre le monde plus sûr si cela arrive avant le déploiement, avant que des attaquants l'exploitent, et avant qu'un standard fragile ne soit verrouillé.
Trouver une faiblesse peut aussi rendre le monde moins sûr si elle touche un système déployé et se diffuse plus vite que les défenseurs ne peuvent patcher ou migrer.
Anthropic dit avoir suivi des procédures de divulgation responsable, consulté des universitaires, partagé des copies en avance avec des partenaires gouvernementaux et industriels américains, et coordonné la divulgation HAWK avec les auteurs du schéma et la liste publique du NIST.
C'est la bonne forme.
C'est aussi l'aperçu d'un problème beaucoup plus dur.
Que se passe-t-il quand un modèle trouve une faiblesse pratique dans un cryptosystème déployé ?
Que se passe-t-il quand il en trouve dix ?
Que se passe-t-il quand un modèle ouvert plus faible peut reproduire la méthode ?
Que se passe-t-il quand les mainteneurs concernés manquent de ressources, que le chemin de migration est lent, et que les attaquants peuvent lancer la même recherche ?
C'est là que l'histoire "l'IA pour la défense" cesse d'être simplement rassurante.
Oui, les modèles capables peuvent aider les défenseurs.
Ils peuvent aussi compresser le temps entre découverte et exploitation.
La réponse saine n'est pas de prétendre que la capacité n'existe pas. La réponse saine est de construire les processus de divulgation, de triage, de contrôle d'accès, de logs et de remédiation d'urgence avant le premier résultat vraiment pratique.
La cryptographie possède déjà une partie de cette culture.
La plupart des industries, non.
Ce que les builders doivent en tirer
La plupart des équipes produit ne conçoivent pas de signatures post-quantiques.
Cette histoire devrait quand même changer leur manière de penser l'IA dans le travail technique.
Si vous utilisez l'IA pour la recherche sécurité, la revue de code, le design de protocoles, l'analyse compliance, le travail scientifique ou n'importe quel domaine où l'exactitude compte, demandez :
- Le système conserve-t-il assez de preuves pour qu'un humain puisse auditer le résultat ?
- Peut-il reproduire la découverte depuis un environnement propre ?
- Peut-il séparer les pistes spéculatives des affirmations vérifiées ?
- Peut-il suivre quelle source ou quelle expérience a changé son avis ?
- Plusieurs agents peuvent-ils être en désaccord utilement au lieu de converger vers la même erreur ?
- Un expert humain peut-il inspecter le travail sans lire un milliard de tokens ?
- L'organisation peut-elle trier les résultats générés par modèle selon la gravité, la nouveauté et le niveau de confiance ?
- La divulgation peut-elle arriver avant que l'excitation publique devienne un risque opérationnel ?
Ce sont des questions produit.
Pas seulement des questions de recherche.
Les outils IA pour domaines experts ne seront pas jugés seulement sur le nombre d'idées qu'ils génèrent. Ils seront jugés sur leur capacité à aider les humains à vérifier, prioriser et agir prudemment sur ces idées.
Le prochain assistant de recherche ne devrait pas seulement dire :
"J'ai trouvé quelque chose."
Il devrait dire :
"Voici l'affirmation, voici les preuves, voici ce qui a échoué, voici ce qui pourrait la falsifier, voici qui doit la relire, et voici pourquoi il ne faut pas encore publier le communiqué."
Pénible ?
Oui.
Utile ?
Extrêmement.
Le fond de l'histoire
Le résultat cryptographique d'Anthropic est un signal clair parce qu'il est excitant et limité à la fois.
Pas de panique sur la crypto de production.
Pas de remplacement instantané des experts.
Pas de preuve que chaque modèle devrait recevoir chaque chiffrement.
Mais pas non plus de rejet facile.
Un modèle de pointe, placé dans le bon échafaudage agentique, semble capable de faire de la recherche adversariale sérieuse dans un domaine où l'exactitude est difficile, les enjeux élevés, et l'expertise humaine rare.
Cela devrait rendre les builders moins impressionnés par la production brute et beaucoup plus obsédés par la validation.
Le prochain goulot n'est pas de savoir si l'IA peut produire plus d'affirmations.
Elle le peut.
Le goulot est de savoir si les humains, les institutions et les outils peuvent distinguer quelles affirmations méritent de devenir réalité.