Veille du 11 novembre 2026 — vérification formelle · portes dérobées neuronales · édition de poids

Les 3 articles les plus chauds de la veille du 11 novembre 2026. 🔥

🔥 Top 3

1. Introducing AlphaProof Code : a breakthrough in verifying complex software at depth

Prouver mathématiquement qu’un morceau de code fait exactement ce qu’il prétend, sans bug possible : c’est la vérification formelle, le graal de la sécurité logicielle. Jusqu’ici, elle s’arrêtait aux schémas sur papier, parce que passer du design au code réel qui tourne sur les téléphones coûtait des années de travail humain.

DeepMind vient de le faire sur Signal, la messagerie qui protège les conversations de millions de personnes. Son nouveau cadre, AlphaProof Code, orchestre plusieurs modèles de langage : des agents propulsés par Gemini Carbon ont produit plus de six millions de lignes de Lean, un langage où chaque preuve est vérifiée automatiquement par la machine. Quatre semaines au lieu d’années.

Le point important n’est pas la vitesse. C’est la cible : le code compilé, celui qui s’exécute vraiment, et pas seulement la spécification cryptographique. C’est précisément dans l’écart entre les deux que se logent les vulnérabilités. Les chercheurs ont aussi réinjecté deux bugs réels déjà corrigés dans une copie isolée du code. À chaque fois, le système a produit une preuve que la version était non sûre.

Les humains n’ont pas disparu : ils ont validé les objectifs de sécurité et relu 1 % des preuves, celles que les agents signalaient comme ambiguës. Le reste, Lean le contrôle seul.

Les artefacts sont publiés en open source, et DeepMind évoque déjà les firmwares d’implants médicaux ou les logiciels de réseaux électriques. Reste une question ouverte : combien d’équipes accepteront de financer des preuves plutôt que des scanners de vulnérabilités ?

🔗 deepmind.google

2. Microsoft Research backdoored an AI agent by directly editing fewer than 10 dormant neurons

Moins de dix neurones. C’est toute la surface qu’il a fallu à Microsoft Research pour installer une porte dérobée dans un agent IA.

Un réseau de neurones, ce n’est qu’une immense collection de paramètres numériques, les « poids », ajustés pendant l’entraînement. Quelques milliards pour un modèle courant. L’équipe en a modifié moins de dix, choisis parmi les neurones qu’on dit dormants : des unités qui ne s’activent presque jamais sur les requêtes habituelles.

Le procédé est malin. Un neurone qui ne réagit pas en temps normal ne change rien au comportement visible. Les tests de sécurité classiques, ceux qui consistent à discuter avec l’agent et à noter ses réponses, ne voient rien passer. Le modèle reste serviable et conforme.

Sauf quand on appuie sur le déclencheur. Là, la porte s’ouvre.

Conséquence directe pour l’audit : vérifier les réponses d’un modèle ne dit rien de ce qu’il cache. Il faut lire les poids, comparer les versions, traquer les écarts anormaux. Un travail d’inspection numérique, pas de conversation.

Reste l’angle mort, et il est large : qui vérifie réellement les poids d’un agent avant sa mise en production ?

🔗 www.reddit.com

3. Tree-Ising: Repairing Language Models with Bit-Level Ising Edits

Réparer un modèle de langage sans agent, sans générer un seul token, pour environ 0,90 dollar de temps GPU. C’est ce que revendique Tree-Ising, et le point de comparaison donne le vertige.

L’équipe MIT derrière le weight-space programming (l’idée de lire et réécrire directement les poids d’un réseau) avait confié la réparation de Qwen3.5-0.8B à un agent GPT-6. Bilan : 158 tours, 89,7 millions de tokens, 50 passes avant. Score sur MATH-500 : 51,7%. Tree-Ising, sans aucun LLM dans la boucle, atteint 54,6% et passe devant sur les cinq benchmarks de maths.

La méthode attaque les poids au format BF16, la version compressée sur 16 bits des paramètres. Un modèle qui tourne en rond dans son raisonnement se corrige en touchant quelques bits : un changement de signe ici, un décalage d’exposant là. Chaque poids devient un chemin dans un arbre d’états, et la réparation se reformule en problème d’Ising, c’est-à-dire un lot de variables binaires qu’on ajuste pour minimiser une énergie. Une petite instance par ligne de sortie de la matrice, résolue sur GPU par recuit simulé.

Le gain ne tient pas qu’à l’élégance. 13 à 17% de poids modifiés en moins, 2,2 fois moins de bits retournés, quatre passes avant au lieu de cinquante. Sur Qwen3.5-2B, la même recette fait bondir la précision GSM8K de 21,6% à 69,4%.

Les auteurs ont même exécuté un sous-problème à huit variables sur un processeur quantique IBM Heron. Huit variables, autant dire une preuve de principe symbolique. Reste le vrai obstacle : combien de boucles de raisonnement compte un modèle de 70 milliards de paramètres, et combien de ces petits problèmes faudra-t-il résoudre avant que la note de GPU ne rejoigne celle des tokens ?

🔗 Hugging Face

📦 Le reste de la veille

• Contrastive Discovery: Open-Ended Scientific Discovery over Competing Explanations — Ce travail propose une méthode où des agents LLM évaluent des hypothèses concurrentes plutôt qu’une seule, une approche réutilisable pour la découverte scientifique automatisée.

• Google Gemini routes personal Drive files and emails to human annotators — L’article rapporte que Google Gemini transmettrait des fichiers Drive et des courriels personnels à des annotateurs humains, une révélation sur la confidentialité des données confiées aux assistants IA.

• Show HN: Get your coding agent off ~2019 JavaScript, onto modern web primitives — Projet Show HN proposant de remplacer du JavaScript ancien par des primitives natives du navigateur comme CSS.highlights et

  , avec un pattern concret réutilisable.

• AI usage generates a fragile codebase — Analyse soutenant que l’usage intensif de l’IA produit des bases de code fragiles, un sujet de fond pour les équipes qui intègrent des agents dans leur développement.

• Apple has new Mac app coming to make running local AI models easy — Apple préparerait une application Mac facilitant l’exécution locale de modèles d’IA, un signal important pour l’écosystème de l’inférence sur poste de travail.

• Fable 5.2 not only has guardrails against AI acceleration, its capabilities were capped in training too — L’article affirme que les garde-fous d’un modèle récent s’accompagnent d’un plafonnement volontaire de ses capacités, alimentant le débat sur la censure des modèles.

• Locating the source of a mysterious beep with Claude — Récit d’une utilisation de Claude pour localiser l’origine d’un bip intermittent dans une maison, illustrant une démarche de diagnostic assistée par modèle.

• Introducing Our Smallest, Most Efficient Model: Muse Ember — Meta dévoile Muse Ember, un petit modèle efficace destiné à concurrencer les offres légères d’Anthropic et d’OpenAI, dans un segment déjà dense.

• Continual-ARC: Measuring Skill Acquisition over a Working Lifetime — Continual-ARC propose un cadre d’évaluation de l’acquisition de compétences par des agents sur une longue durée, en combinant plusieurs domaines et types d’apprenants.

• Emergent Biological Capabilities in a Foundation Model for Molecular Interactions — Bonbon est un modèle de fondation entraîné sur 3 200 milliards de tokens de données biologiques multimodales, dont les capacités émergentes dépassent l’objectif d’entraînement initial.

• Genie 4: A new generation of world simulation — Genie 4 présente un modèle de monde générant des simulations en temps réel d’un réalisme inédit, une démonstration visuelle marquante pour l’entraînement d’agents.

• Gemini 4 Carbon is now available — Google annonce la disponibilité de Gemini 4 Carbon, un nouveau modèle frontier qui intéresse les développeurs d’agents par ses capacités de raisonnement, mais sans détail technique dans l’extrait.

• Tracking Anthropic-discovered vulnerabilities — Recensement des vulnérabilités découvertes par Anthropic, une ressource de suivi utile mais limitée à un périmètre restreint.

• CoreWeave bond yield tops 16% as AI credit stress rises — Le rendement obligataire de CoreWeave dépasse 16 pour cent, signe de tensions financières sur le crédit lié à l’IA, un indicateur macroéconomique sans portée technique directe.

• The Surprising Effectiveness of Deleting Weights in LLM Post-Training — Une étude explore l’élagage de poids en post-entraînement des LLM et suggère des effets contre-intuitifs sur les performances.

… et 66 autres articles consultés.