Collatz : comment une fausse preuve assistée par IA a trompé deux vérificateurs

Lean vérifie une preuve traduite en code

La formalisation consiste à écrire un énoncé mathématique et sa démonstration dans un langage qu’un ordinateur peut contrôler. Dans Lean, le noyau est la partie du logiciel chargée de vérifier que la preuve respecte les règles logiques. L’intérêt est de ne pas se fier seulement à un raisonnement qui paraît convaincant, qu’il ait été rédigé par une personne ou par une IA.^[1]

Mais ce contrôle est lui-même exécuté par un programme. Pour réduire la dépendance à une seule implémentation, une preuve peut être soumise à un second noyau, développé séparément. C’est le rôle de nanoda, un vérificateur de preuves Lean écrit en Rust. Deux implémentations différentes peuvent repérer des erreurs que l’une d’elles laisserait passer.^[2]

Deux défauts différents, une même fausse preuve

Dans le noyau officiel de Lean, un contrôle manquait lors du traitement de certaines constructions de types imbriquées, qui servent à définir des objets mathématiques. Un argument mal formé pouvait ainsi échapper à la vérification et faire accepter une preuve de faux. Le bilan précise que cette voie passait par la métaprogrammation, c’est-à-dire du code qui construit et transmet directement des déclarations au noyau. Il s’agissait d’un bogue d’implémentation, pas d’une faille dans la théorie logique de Lean.^[2]

Nanoda effectuait bien le contrôle absent de Lean. En revanche, il omettait de vérifier le nom du type dans une autre opération, appelée projection. La fausse preuve était construite de façon que l’expression ignorée par Lean soit acceptée par l’ancienne version de nanoda. Les deux logiciels n’avaient donc pas le même bogue : le code exploitait deux faiblesses distinctes pour franchir les deux contrôles.^[2]

La version utilisée compte ici autant que l’indépendance des logiciels. Le dépôt de Ramana Kumar avait passé une version de nanoda vieille d’une semaine. Or son défaut avait déjà été signalé et corrigé une semaine avant le signalement du bogue de Lean. Un contrôle supplémentaire ne protège pas contre une faille corrigée si l’on continue d’utiliser la version vulnérable.^[2]

Des correctifs rapides et davantage de vérificateurs

Le bilan de Leonardo de Moura donne une chronologie précise : Ramana Kumar a publié son dépôt le 25 juillet. Le 28 juillet, Kiran Gopinathan a réduit le problème à une petite preuve de faux et signalé le défaut. L’équipe a proposé un correctif une heure après ce signalement, puis publié des versions corrigées. Des tests ont aussi été ajoutés pour vérifier que cet exploit et un cas apparenté restent détectés.^[2]

Les recherches de défauts ont également été poursuivies avec une IA spécialisée en cybersécurité, avec l’aide de Daniel Selsam, chez OpenAI. Selon le bilan, d’autres erreurs de programmation du noyau ont été trouvées et corrigées ; nanoda les détectait toutes. Ce résultat illustre l’utilité du contrôle croisé, malgré l’échec observé dans le cas de Collatz.^[2]

New Scientist rapporte aussi que la prochaine version de Lean doit intégrer quatre noyaux par défaut. Le principe est de rendre plus difficile la construction d’une fausse preuve capable de tromper toutes les implémentations. Cette diversité réduit le risque sans l’annuler : l’incident montre précisément qu’un même code peut exploiter des défauts différents dans plusieurs vérificateurs.^[1]