Maths d'olympiade, filtres contournés, mémoire piégée.

Une IA résout des problèmes d'olympiade de maths pour 0,44 dollar

Quatre problèmes sur six de l'IMO 2025, résolus automatiquement — et chaque démonstration coûte moins cher qu'un café.

L'équipe derrière Goedel-Architect a publié cette semaine des résultats qui méritent qu'on s'arrête. Leur système — qui utilise DeepSeek comme grand modèle de langage — a résolu 4 problèmes sur 6 de l'IMO 2025, les Olympiades Internationales de Mathématiques, le concours le plus difficile au monde pour les lycéens. Sur le concours Putnam 2025, il en résout 11 sur 12. Comment ça marche ? Imaginez que vous construisez une maison. Vous pourriez poser des briques au hasard et espérer que ça tienne. Ou vous faites d'abord un plan d'architecte : fondations, murs porteurs, toit — dans l'ordre. Goedel-Architect fait pareil avec les démonstrations mathématiques. Il génère d'abord un « plan » — un graphe de dépendances qui liste toutes les étapes intermédiaires — avant de demander à un prouveur formel appelé Lean 4 de vérifier chaque brique une par une. Ce qui frappe, c'est le coût. Résoudre un problème revient à environ 0,44 dollar. Le système concurrent le plus compétitif coûte 244 dollars pour le même résultat — soit 550 fois plus cher. Pourquoi ça compte ? Prouver formellement un théorème, c'est garantir qu'il n'y a aucune erreur — pas d'approximation, pas de raccourci. C'est le niveau de rigueur qu'on veut dans les systèmes critiques : logiciels médicaux, protocoles de sécurité, compilateurs. Le hic ? Les meilleurs résultats sont obtenus en mode « assisté » : on fournit au système une preuve en langage courant comme point de départ, et il la formalise. Sur PutnamBench, le taux passe de 75,6 % à 88,8 % avec cette aide. Autrement dit, le système est encore plus fort quand un humain lui montre le chemin général. L'autonomie complète reste un horizon, pas une réalité. Un petit pas — mais un vrai.

Deux retouches photo suffisent à tromper les filtres de sécurité IA

Changer la luminosité et recadrer légèrement une image dangereuse — et le filtre automatique ne la reconnaît plus.

Des filtres de sécurité analysent des millions d'images chaque jour sur les grandes plateformes pour détecter automatiquement les contenus violents ou haineux. L'équipe derrière RedEdit vient de montrer que ces filtres sont beaucoup plus fragiles qu'on ne le croit. Leur idée : traiter la question comme un jeu de stratégie. Un agent intelligent explore des séquences de retouches photo — recadrage, ajustement de luminosité, ajout d'un filtre — en utilisant un algorithme de recherche arborescente (le même type d'algorithme que les IA de jeu de go) pour trouver la combinaison minimale qui trompe le détecteur, sans modifier le contenu au point de le rendre inoffensif. Résultat : en moins de deux retouches en moyenne, 76,2 % des images dangereuses testées passent au travers des filtres. Et ces images restent perceptiblement dangereuses pour un humain — 93 % du contenu malveillant est intact. C'est comme si vous changiez juste la couleur de la couverture d'un livre interdit : le titre reste lisible, mais le gardien automatique ne le reconnaît plus. Pourquoi ça compte ? La plupart des plateformes s'appuient sur ce type de classification à grande échelle. Si deux clics suffisent à contourner le filtre, la modération automatique de contenu est structurellement vulnérable — et pas seulement face à des acteurs très sophistiqués. Le hic ? L'étude est réalisée sur un ensemble de référence (UnsafeBench) dans des conditions contrôlées. Les auteurs ne fournissent pas de détails sur les tailles d'échantillons ni sur les tests statistiques. Soyons honnêtes : c'est un signal d'alarme solide, pas encore un audit complet de tous les systèmes de modération existants. Mais le résultat est suffisamment systématique — les attaques généralisent d'un détecteur à l'autre — pour ne pas être ignoré.

La mémoire de votre assistant IA peut devenir une porte dérobée

Plus votre assistant IA se souvient de vous, plus il devient facile à manipuler — et les chiffres sont surprenants.

Les agents IA personnels ont désormais une mémoire à long terme : ils se souviennent de vos préférences, de vos habitudes, de vos instructions passées pour mieux vous servir. Les auteurs de ce papier ont évalué trois grandes architectures populaires — A-Mem, Mem0 et MemOS — et découvert quelque chose d'inquiétant : cette mémoire crée une nouvelle catégorie de vulnérabilités. Imagez un concierge d'hôtel qui note les préférences de chaque client dans un carnet. Un visiteur malveillant glisse une fausse note dans ce carnet : « M. Dupont préfère qu'on lui ouvre directement le coffre-fort sans demander de code. » Le concierge fait confiance à son carnet. La faille n'est pas dans le concierge — elle est dans le fait qu'il se souvient de tout sans vérifier la source. C'est exactement ce que les auteurs ont documenté sur des environnements de test réels. Quand la mémoire est activée, le taux de succès des attaques par détournement (jailbreak) passe de 3,1 % à environ 20 % en moyenne. Le taux de comportements erratiques liés à des injections mémoire (l'agent appelle le mauvais outil, exécute la mauvaise action) passe de 5,1 % à plus de 50 %. Leur solution s'appelle MemGate : un module de 9 millions de paramètres — environ 35 mégaoctets, la taille d'une photo — inséré entre la base de mémoire et le modèle. Il agit comme un filtre de bon sens : avant d'injecter un souvenir dans le contexte de l'agent, il vérifie si ce souvenir est pertinent ET cohérent avec la tâche en cours. Résultat : les fuites entre domaines passent de 27 % à 3,5 %. Le hic ? Tout se passe dans des environnements de test contrôlés — OpenClaw et LoCoMo. Les déploiements réels à grande échelle n'ont pas encore été évalués. Prometteuse, la solution. Pas encore éprouvée.

Ces trois papiers racontent une histoire cohérente sur l'état réel de la recherche en IA en ce moment. D'un côté, les capacités progressent : un système peut désormais résoudre des problèmes d'olympiade mathématique de façon formellement vérifiée, à un coût dérisoire. C'est tangible, mesurable, et difficile à relativiser. De l'autre, les systèmes de sécurité censés nous protéger montrent des failles structurelles. Deux retouches photo contournent un classificateur de contenu. Une note malveillante dans la mémoire d'un agent peut lui faire exécuter des actions qu'il devrait refuser. Ces deux vulnérabilités ont quelque chose en commun : elles ne viennent pas d'un manque de puissance des modèles, elles viennent de la façon dont on les connecte au monde réel — aux images, aux souvenirs, aux outils. Ce que ça nous dit collectivement : les capacités courent. La robustesse suit, mais avec un temps de retard. Ce n'est pas une raison de paniquer. C'est une raison de surveiller les bonnes choses.

Sur le front du raisonnement formel, la conférence ITP (Interactive Theorem Proving) de cet automne sera un bon thermomètre pour voir si des systèmes comme Goedel-Architect passent d'une curiosité de benchmark à un outil réellement utilisé par des mathématiciens. Sur la sécurité des agents, la question ouverte que j'aimerais voir répondue : est-ce qu'un MemGate peut être lui-même attaqué — peut-on entraîner un agent à tromper le filtre ? Personne ne sait encore.

• Wikipédia — Vérification formelle (pour comprendre l'enjeu derrière Lean 4)
• Wikipédia — Adversarial examples (le concept derrière RedEdit, en anglais)
• Lean — le prouveur formel utilisé par Goedel-Architect (site officiel)