Une IA prétend résoudre un problème vieux de 90 ans : l’assistant de preuve était cassé

Fin juillet, une IA a affirmé haut et fort : « La conjecture de Collatz, qui résiste aux mathématiciens depuis près de 90 ans, a été réfutée par mes soins, voici le contre-exemple. » La preuve fournie était une vérification automatique exécutable ligne par ligne par ordinateur, en apparence inattaquable. Mais avant même que le monde ne puisse s’enthousiasmer, la réalité s’est imposée : ce contre-exemple n’était qu’une hallucination engendrée par une faille de validité (soundness bug) au cœur de l’outil de vérification lui-même. Un comble, sachant que cet outil existe précisément pour éliminer toute hallucination de l’IA.

Cette histoire mérite d’être racontée en détail depuis le début. Elle soulève une question sur laquelle nous faisons tous un pari collectif : jusqu’à quel point pouvons-nous faire confiance à ce que raconte une IA ?

Comprendre ce problème vieux de 90 ans

Les règles de la conjecture de Collatz sont d’une simplicité accessible à n’importe quel élève d’école primaire : choisissez un nombre entier positif. S’il est pair, divisez-le par 2 ; s’il est impair, multipliez-le par 3 et ajoutez 1. Répétez ensuite la même opération sur le résultat obtenu.

Prenons un exemple à partir de 6. 6 étant pair, on le divise par 2 pour obtenir 3. 3 étant impair, 3 * 3 + 1 donne 10. 10 est pair, divisé par 2 donne 5. 5 est impair, ce qui donne 16. La suite se déroule ainsi : 16 -> 8 -> 4 -> 2 -> 1. Que se passe-t-il une fois arrivé à 1 ? 1 étant impair, 1 * 3 + 1 nous ramène à 4, s’enfermant dans une boucle infinie 4-2-1. La question posée est donc toute simple : quel que soit le nombre de départ, finit-on toujours par tomber dans ce cycle 4-2-1 ?

Formulée en 1937 par le mathématicien allemand Lothar Collatz, cette conjecture n’a jamais été démontrée et aucun contre-exemple n’a jamais été trouvé. Les ordinateurs ont testé tous les nombres jusqu’à (2^{68}) (soit plus de 295 quintillions), et chacun d’eux est revenu à 1. Mais les mathématiciens restent imperturbables : vérifier des milliards de nombres ne constitue pas une preuve, tout comme observer des millions de cygnes blancs ne prouve pas que tous les cygnes sont blancs. Le grand mathématicien hongrois Paul Erdős a résumé la situation par cette formule célèbre : « Les mathématiques ne sont peut-être pas encore prêtes pour ce genre de problèmes. » La difficulté réside dans sa simplicité trompeuse : des règles élémentaires, mais une logique aussi glissante qu’une anguille.

Fig. : Arbre numérique de la conjecture de Collatz — tous les nombres atteignant 1 en moins de 20 étapes sont rattachés à cet arbre. Source : Wikipedia (All Collatz sequences of a length inferior to 20)

Comment s’est préparée la « trouée » de l’IA

Le 25 juillet, l’informaticien Raman Kumar a publié un dépôt de code contenant une prétendue « réfutation » : un grand nombre spécifique dont on affirmait qu’il ne revenait jamais à 1, renversant ainsi la conjecture. Le principal argument de vente était que cette réfutation s’appuyait sur une preuve vérifiable par machine conçue avec l’aide d’une IA.

Pour mesurer l’impact de cette annonce, il faut comprendre un concept fondamental. Ces dernières années, une pratique s’est répandue dans la communauté mathématique : traduire une démonstration sous forme de code dans un langage informatique spécialisé, puis la soumettre à un « compilateur de preuves » nommé Lean. Lean agit comme le correcteur le plus impitoyable : il décortique chaque étape de la démonstration et la vérifie ligne à ligne. Si une étape saute un maillon logique, il dresse aussitôt un drapeau rouge et rejette la preuve. Une démonstration validée par Lean est théoriquement irréprochable — et c’est précisément son objectif de conception : remplacer l’inattention et les biais de la relecture humaine par la rigueur froide de la machine.

Le poids de cet outil est considérable : noyaux de sécurité de systèmes d’exploitation, protocoles sous-jacents de cryptomonnaies et des dizaines de milliers de théorèmes mathématiques reposent sur cette « vérification mécanique ». Dans l’industrie, on allait jusqu’à le présenter comme l’arme ultime contre les hallucinations des IA : peu importe que l’IA raconte des absurdités, tant que la machine fait barrage.

Ainsi, lorsque Kumar a exhibé un « contre-exemple vérifié par Lean », la première réaction des spécialistes a été la stupeur : si la preuve avait réellement franchi le contrôle de la machine, le problème vieux de 90 ans s’effondrait. La nouvelle s’est propagée à toute vitesse sur les réseaux sociaux sous des titres percutants : « Une IA terrasse un problème mathématique vieux de 90 ans ».

La vérité : le correcteur s’est trompé lui-même

Le rebondissement fut immédiat. Le 28 juillet, un autre chercheur a réduit la réfutation à une contradiction logique minimale et a ouvert un ticket d’incident sur le dépôt officiel de Lean sous le numéro #14576. Le titre de l’incident était glacial : « kernel accepts ill-typed projection, allowing proof of false without premises. » (le noyau accepte une projection mal typée, permettant de prouver le faux sans prémisses).

En langage clair : le correcteur prétendument infaillible avait oublié une étape lors de sa vérification centrale. Lors du contrôle de types de données imbriqués, la concordance des noms de types n’a pas été vérifiée à un endroit précis. Résultat : un composant invalide dissimulé dans la « preuve » générée par l’IA s’est glissé par cette fissure. Au moment où la machine déclarait « vérification réussie », elle ne faisait qu’apposer son sceau sur un mirage.

Fig. : Trajectoires des petits nombres sous les règles de Collatz, convergeant vers 1. Source : Wikipedia (Collatz graph, skipping 27)

C’est alors qu’est survenue la scène la plus dramatique. La communauté Lean intègre depuis longtemps un principe de « double assurance » : en parallèle du correcteur officiel du noyau, il existe un vérificateur indépendant tiers (écrit dans un autre langage par une équipe différente), chargé de croiser les résultats du contrôle officiel. Cette hypothèse d’indépendance est le fusible de la chaîne de confiance de la vérification mécanique.

Cette fois, le fusible a sauté. L’analyse post-mortem a confirmé qu’il a fallu toucher simultanément deux bugs totalement indépendants : le noyau officiel a manqué la vérification du type imbriqué, tandis que le vérificateur indépendant a manqué un détail lors du contrôle de projection. Deux bugs tapis dans des coins différents de deux bases de code distinctes se sont déclenchés sous l’effet de la même « réfutation ». Le bug du vérificateur indépendant avait précisément été corrigé une semaine plus tôt, mais la version utilisée par l’IA précédait ce correctif. Le créateur de Lean, Leo de Moura, a reconnu très franchement dans son post-mortem que si l’auteur pensait à une coïncidence de calendrier, on ne pouvait pas exclure que l’IA ait rencontré le rapport de bug dans ses données d’entraînement.

Comment analyser cela sur le plan de l’ingénierie ? Voir deux implémentations indépendantes être traversées par la même balle relève d’une probabilité très faible. Cela traduit soit une poisse extrême, soit le fait que cette réfutation ait été taillée sur mesure pour exploiter la faille. De Moura a livré son propre diagnostic : « Ce genre d’événement continuera de se produire. Les IA sont extrêmement douées pour exploiter les bugs de validité dans les noyaux. » Le bug a été corrigé et déployé une heure après le signalement, ce qui prouve que l’architecture du noyau est saine ; mais pour le débusquer, il aura fallu le retentissement d’une « prétendue avancée de l’IA ».

Qui vérifie les vérificateurs ?

Les répercussions de cette affaire sont encore plus instructives que l’événement lui-même. Une fois la faille mise au jour, OpenAI a dépêché un chercheur en sécurité informatique spécialisé en IA pour auditer le noyau de Lean, ce qui a permis d’extirper plusieurs autres erreurs de programmation — toutes corrigées dans la foulée. En d’autres termes : l’outil conçu pour nous protéger de l’IA dépend désormais de l’IA pour traquer ses propres bugs.

Par ailleurs, le projet « Lean in Lean » (qui vise à réécrire et vérifier le vérificateur au sein même de Lean) ne couvre pas encore la portion de code incriminée, et le fragment de code porté hébergeait le même bug. La vérification est une affaire de strates : le résultat de l’IA est contrôlé par un vérificateur, le vérificateur par une seconde implémentation indépendante, mais qui contrôle la seconde implémentation ? Chaque couche ajoute une étape et un coût supplémentaires, mais il n’existe jamais de « dernière couche ». C’est une réalité d’ingénierie : « vérifié par machine » n’est jamais qu’une propriété probabiliste — plus la vérification est profonde et indépendante, plus la probabilité d’erreur diminue, mais elle n’atteint jamais zéro.

Pour le grand public, le principal bénéfice de cet épisode est de recalibrer les attentes. La prochaine fois qu’un titre proclamera « Une IA résout un problème séculaire » ou « Une IA prouve un théorème », posez-vous une question de plus : l’agent de vérification est-il un humain ou une machine ? Et s’il s’agit d’une machine, la machine elle-même a-t-elle été vérifiée ? Inversement, il n’y a pas lieu d’en déduire un scepticisme nihiliste. Les mathématiques sont sorties totalement indemnes de cette histoire, et la conjecture de Collatz tient toujours debout. Le bug a été rendu public, corrigé et consigné dans un post-mortem exemplaire. Le système a connu un dysfonctionnement, mais sa façon de digérer et réparer le bug est précisément la raison pour laquelle il mérite notre confiance.

La confiance est une chaîne dont n’importe quel maillon peut rompre à tout moment. Les personnes avisées ne prétendent pas que la chaîne est incassable ; elles pensent simplement à inspecter chaque maillon régulièrement. Cette fois, l’IA nous a montré la fissure de l’un de ces maillons — par le biais d’une fausse percée.

Liens de référence :

• Post-mortem de Leo de Moura : Analyse complète du bug de validité du noyau #14576
• Discussion sur Lobsters (ojcl8j) : Échanges de la communauté sur le bug du noyau (48 points)
• Wikipedia : Conjecture de Collatz (Règles, histoire et progrès de la vérification)