L'IA a vérifié mathématiquement une partie du code de Signal en une demi-journée et pour 500 $, contre cinq mois de travail humain

Chuyue Sun, chercheuse à Stanford, et ses collègues ont créé un outil d'IA qui a mené à bien un projet d'ingénierie en moins d'une demi-journée et pour moins de $500 : vérifier une partie du code qui chiffre les conversations dans la messagerie Signal. Trois spécialistes hautement qualifiés avaient consacré cinq mois au même travail, à la main. La vérification n'avait rien d'ordinaire : elle était formelle. Au lieu de faire passer le programme par des milliers de tests, on démontre mathématiquement qu'il se comporte comme prévu. L'idée n'est pas neuve, mais elle restait jusqu'ici trop coûteuse et trop lente. Aujourd'hui, des start-up dotées de centaines de millions de dollars et de grands laboratoires d'IA misent dessus.

Pourquoi des maths plutôt que des tests

Un test classique montre que le programme n'a pas planté dans les cas qu'on lui a soumis. La vérification formelle démontre qu'il ne plantera dans aucun cas de la classe décrite. Les ingénieurs rédigent des énoncés précis sur l'objectif du programme, puis traduisent le code en formules que des systèmes spécialisés vérifient. Lean, Rocq et Isabelle font partie de ces systèmes.

Mais le travail est lourd. Les spécifications doivent être formulées avec beaucoup de soin. Un exemple simple : une fonction de tri d'un tableau doit renvoyer les mêmes éléments que ceux reçus, simplement dans un autre ordre. Pour un humain, c'est évident ; pour un système mathématique, il faut l'écrire de façon rigoureuse.

La méthode est donc réservée aux cas où une erreur coûte cher. D'après les déclarations des entreprises, du code formellement vérifié se trouve dans les avions de Boeing, sur les serveurs d'Amazon et dans plus de 2,5 milliards d'appareils actifs d'Apple. Il s'agit en général de code lié à la sécurité. Byron Cook, d'Amazon Web Services, explique que la vérification a levé les doutes des clients sur la protection du cloud et accéléré le travail des équipes internes : les erreurs majeures étaient détectées tôt.

Qui mise sur l'IA, et comment

Les start-up veulent automatiser la partie la plus fastidieuse : la rédaction de la description du comportement attendu du programme. Les étapes suivantes, qui traduisent le code dans un format exploitable par les systèmes mathématiques, peuvent d'ailleurs se faire sans IA.

• &Truth. La start-up a levé $70 millions ; Sun l'a rejointe en août, et le lancement public a eu lieu jeudi. Son objectif est de pouvoir, à terme, vérifier du code dans n'importe quel langage de programmation.

Son directeur scientifique, Ilya Sergey, compare l'approche à la construction : les ponts et les bâtiments ne s'effondrent pas parce qu'on les a calculés avant de les bâtir, alors pourquoi ne pas faire de même avec le code ? • Harmonic. Cofondée par Vlad Tenev, patron de Robinhood, l'entreprise a levé $295 millions.

Cette semaine, elle a annoncé que son agent d'IA mathématique Aristotle sait vérifier des programmes en C et des descriptions de puces en Verilog. Des clients potentiels évaluent la technologie, dont les fabricants de puces Tensordyne et Nvidia ; la branche de capital-risque de Nvidia figure parmi les investisseurs. • **Anthropic et Theorem.

** Il y a une semaine, elles ont annoncé avoir trouvé, grâce à l'IA, des erreurs dans des logiciels open source que des milliers de milliards de tests n'avaient pas détectées. Une extension pour Claude, qui aide les développeurs à vérifier leur code, a également été publiée. Le coût du premier projet n'a pas été divulgué.

• Truidic. Fondée par Madan Musuvathi, qui a quitté Microsoft Research après plus de 20 ans de carrière. Selon lui, l'IA est très puissante entre les mains des attaquants, et la vérification peut rendre l'IA sûre.

• Proofcraft. Cette entreprise pratique depuis longtemps la vérification classique. Ses dirigeantes et dirigeants, June Andronick et Gerwin Klein, affirment que le flux de demandes dépasse les capacités de l'entreprise comme celles de ses concurrents.

Des projets open source testent aussi la méthode. La fondation à but non lucratif Beneficial AI Foundation a vérifié cette année, grâce à une subvention d'Anthropic, le même code cryptographique que Sun. Michael Rosenberg, l'un des mainteneurs de la bibliothèque curve25519-dalek, espère un financement pérenne pour ce type de travaux, mais ignore d'où il viendra et ne veut pas dépendre de la bonne volonté des entreprises d'IA.

Où la méthode atteint ses limites

Pour l'instant, la technologie en est au stade du prototype. On ne sait pas combien les clients sont prêts à payer, ni sous quelle forme ils veulent recevoir le produit : directement, ou via des intermédiaires comme Anthropic. Plusieurs entreprises technologiques de taille moyenne ont indiqué à Wired n'avoir vérifié, au maximum, qu'une seule fonction clé de leur produit, voire aucune. Les raisons : le manque d'ingénieurs spécialistes de la vérification, un coût supérieur au risque potentiel, et la crainte que des semaines d'attente pour une vérification ralentissent la sortie des mises à jour. Même Apple doit ajouter avec prudence du nouveau code à sa bibliothèque de chiffrement corecrypto, afin d'avoir le temps de le vérifier.

Des objections de principe existent aussi. La preuve repose sur des hypothèses concernant la façon dont les ordinateurs et les humains interagissent avec le programme. Elle peut ne pas détecter les erreurs d'utilisateur ni les pannes matérielles.

Will Wilson, patron de la start-up Antithesis (recherche de bugs par IA), qualifie la vérification formelle de « piège » pour les amateurs de maths comme lui. Son entreprise a dépensé des millions pour vérifier une partie de sa protection, un processus qu'il a décrit comme « une galère monstre ». Pourtant, son propre outil y a quand même trouvé des erreurs supplémentaires, ainsi que des bugs dans des logiciels de clients que ceux-ci avaient déjà vérifiés formellement.

La conclusion de Wilson : la vérification apporte une certaine confiance, mais seul un test exhaustif peut la confirmer. Vitalik Buterin a lui aussi écrit sur son blog que la vérification formelle n'est pas une panacée, tout en la jugeant importante pour se protéger des cyberattaques menées avec l'aide de l'IA.

Andronick et Klein voient un autre risque : si c'est l'IA qui a rédigé la description du problème, cela crée une « confiance injustifiée » dans le résultat. Une preuve n'est valable que dans la mesure où ce qui est considéré comme correct a été correctement décrit.

Le constat pratique pour les ingénieurs : l'IA réduit fortement le coût de l'étape la plus chère, mais il faudra toujours vérifier les spécifications elles-mêmes et contrôler le travail par des tests. Deux entreprises qui ne vérifient pas formellement leur code seraient prêtes à payer des laboratoires d'IA pour obtenir du code « vérifié » généré par IA. Si cela fonctionne, la vérification formelle sortira du cercle de la NASA et d'Apple.