En collaboration avec son partenaire Theorem, Anthropic a utilisé son modèle d’IA Claude pour tenter de prouver mathématiquement que des logiciels existants fonctionnent correctement. Le projet portait sur 123 bibliothèques open source du projet de sécurité OSS-Fuzz de Google. En quelques semaines, environ 180 millions de lignes de code de preuve ont été générées, et des centaines de bugs que les tests traditionnels n’avaient pas détectés auraient également été découverts.
Entre « les tests ont réussi » et « la correction est prouvée »
Quand on parle de vérifier la qualité d’un logiciel, beaucoup pensent aux tests : on lui fournit des données et l’on vérifie qu’il renvoie le résultat attendu. Mais les tests ne permettent de vérifier que les cas que l’on a essayés. Ils ne disent pas comment le logiciel se comportera dans des situations qui n’ont pas été testées.
C’est là qu’intervient la vérification formelle. Elle consiste à traiter le comportement d’un programme comme un problème mathématique et à prouver qu’il fonctionnera nécessairement correctement dans les limites des conditions définies. En théorie, la méthode est puissante, mais elle demandait des efforts considérables. La vérification du petit noyau de système d’exploitation seL4, par exemple, aurait mobilisé une équipe de spécialistes pendant 20 années-personnes au total. Il n’est donc pas surprenant que cette approche ait été réservée à des cas extrêmes, comme les logiciels de commande des avions de ligne.
Cette fois, la Frontier Red Team d’Anthropic s’est associée à Theorem pour confier ce travail de preuve à Claude. Il ne s’agissait pas de lui faire écrire du nouveau code. Le modèle a pris des logiciels existants, transformé les tests de détection des plantages en problèmes mathématiques, analysé jusqu’au code machine après compilation, puis assemblé un grand nombre de preuves.
Un autre programme pour « noter » les preuves
Si une IA déclare elle-même que les preuves qu’elle a rédigées sont « validées », cela n’a guère de valeur. Le mécanisme de vérification des preuves est donc particulièrement intéressant. Les preuves générées sont automatiquement contrôlées par Rocq, un programme de vérification indépendant. Selon Anthropic, ce processus nécessite très peu l’intervention de réviseurs humains.
L’équipe de recherche qualifie ce processus de génération de preuves de « entièrement autonome ». Toutefois, les outils utilisés pour produire les preuves et leur fondement formel ont été créés par les humains de Theorem. Il serait plus juste de dire que l’IA a rédigé d’un seul coup une quantité considérable de preuves sur un terrain préparé par des humains, plutôt que d’affirmer qu’elle a tout créé de zéro.
Des centaines de bugs découverts au fil des preuves
En avançant dans les preuves, Claude a rencontré des centaines de bugs et était également autorisé à les corriger lui-même. Selon les chercheurs, beaucoup ne se manifestaient que dans des conditions très limitées, par exemple avec des fichiers d’entrée extrêmement volumineux ou un ordre particulier d’accès à la mémoire. Il n’est pas étonnant qu’ils aient échappé aux tests habituels.
Des exemples concrets sont également cités. Lors de la vérification d’un lecteur PDF largement utilisé, autant de bugs de sécurité que le logiciel en signale habituellement en un an ont été découverts en une semaine. Dans une autre application, une erreur logique passée inaperçue pendant plus de dix ans aurait aussi été mise au jour.
Un autre point à ne pas négliger concerne les cas où la preuve n’a pas pu être menée à son terme. Anthropic explique que même lorsqu’une preuve échoue, de véritables bugs peuvent apparaître au cours de la tentative. La preuve ne sert donc pas uniquement à délivrer un « certificat de réussite » : elle joue aussi le rôle d’une sonde qui débusque les bugs. Plutôt que de remplacer les tests habituels, elle semble les compléter.
Ne pas se méprendre sur la portée de la « vérification formelle »
Il serait toutefois dangereux d’interpréter « vérifié formellement » comme « exempt de tout défaut ». Anthropic reconnaît lui-même que les preuves ne sont valables que dans des conditions strictes. Le cadre envisagé se limite à une configuration de processeur spécifique, à des programmes à un seul thread et à des données d’entrée de moins de 64 MB. Or, dans la réalité, les bibliothèques fonctionnent sur des matériels et avec des configurations variés.
Le coût n’est pas négligeable non plus. Selon les cas, plusieurs centaines de millions de tokens peuvent être nécessaires pour une seule preuve. Le coût total du projet n’a pas été communiqué. En revanche, de petites expériences supplémentaires ont montré que les preuves pouvaient être réutilisées et que les modèles plus récents tendaient à gagner en efficacité. Opus 5.5 nécessiterait environ 40 % de tokens en moins qu’Opus 5 pour résoudre la moitié des preuves.
La question n’est plus « peut-elle écrire des programmes ? »
Si l’IA peut écrire du code et en garantir la correction sous certaines conditions, la question change. Il ne s’agit plus de demander « l’IA sait-elle programmer ? », mais « peut-elle prouver la sécurité du code qu’elle a écrit ? ». Ce changement est loin d’être anodin pour les équipes de développement qui s’inquiètent de la fiabilité du code généré par l’IA. Si l’IA peut vérifier elle-même son code, elle pourrait aussi alléger la charge des révisions humaines et réduire les coûts non seulement de la vérification, mais de l’ensemble du processus de développement.
Anthropic estime que, dans un avenir proche, la vérification formelle par l’IA deviendra aussi courante que les tests habituels. La feuille de route de Theorem prévoit notamment des logiciels d’infrastructure essentiels comme glibc, OpenSSL et cURL.
L’essentiel est ici de savoir lire non pas le « contenu » d’une preuve, mais ses « hypothèses ». Dans quel environnement et pour quelles entrées cette preuve a-t-elle été conçue ? À l’heure où l’on confie aussi les vérifications à l’IA, la capacité des humains à examiner ces hypothèses pourrait bien être le dernier rempart en matière de sécurité.
コメント