Points clés
- Anthropic et son partenaire Theorem ont utilisé Claude pour vérifier mathématiquement du code logiciel existant et générer des preuves formelles de sa correction.
- Le modèle a produit environ 180 millions de lignes de code de preuve pour 123 bibliothèques open source en quelques semaines seulement. Ce faisant, Claude a détecté des centaines de bugs que les tests conventionnels n'avaient pas repérés.
- Si l'IA peut écrire du code et prouver qu'il est correct, l'automatisation du logiciel pourrait faire un grand bond en avant. Anthropic veut que la vérification formelle avec l'IA devienne aussi courante que les tests standards.
Anthropic a utilisé Claude pour prouver mathématiquement que du code existant est correct. Cette approche s'attaque à un problème fondamental des logiciels générés par l'IA, mais s'accompagne de limites pratiques strictes.
Prouver qu'un logiciel fonctionne sans erreur dans toutes les circonstances a toujours été d'un coût prohibitif. Une équipe de spécialistes a eu besoin de 20 personnes-années rien que pour vérifier formellement le petit noyau de système d'exploitation seL4, si bien que la méthode était réservée aux cas extrêmes comme le logiciel avionique d'Airbus.
Le Frontier Red Teamd'Anthropic, en collaboration avec son partenaire Theorem, a laissé Claude prendre en charge le travail de preuve. Le modèle a produit environ 180 millions de lignes de code de preuve mathématique en quelques semaines seulement, en s'appuyant sur des programmes de test issus de 123 bibliothèques open source du projet de sécurité OSS-Fuzz de Google.
Plutôt que d'écrire du nouveau code, Claude a vérifié des logiciels existants en traduisant des tests de plantage en problèmes mathématiques, en analysant le code machine compilé et en produisant des preuves étendues. Un programme de vérification indépendant appelé Rocq contrôle automatiquement ces preuves, et selon Anthropic, le processus ne nécessite presque aucun relecteur humain. Les chercheurs parlent de génération de preuves « entièrement autonome », bien que les outils et les fondations formelles aient été construits par des humains chez Theorem.Ad
Claude détecte des bugs que des années de tests ont manqués
Tout en générant des preuves, Claude est tombé sur des centaines de bugs et a été autorisé à les corriger lui-même. Beaucoup auraient échappé aux tests conventionnels parce qu'ils ne se manifestent que dans des conditions très spécifiques, comme des fichiers d'entrée inhabituellement volumineux ou une séquence particulière d'accès, selon les chercheurs.
Par exemple, lors d'une effort de vérification d'un lecteur PDF largement utilisé, l'équipe a trouvé autant de bugs de sécurité en une semaine qu'il en est habituellement signalé pour ce logiciel en une année entière. Dans une autre application, Claude a détecté une erreur logique qui était passée inaperçue pendant plus d'une décennie. Même lorsqu'une preuve complète échoue finalement, dit Anthropic, la tentative fait quand même apparaître de vrais bugs.
Ce que la vérification formelle peut et ne peut pas faire
Anthropic reconnaît que « formellement vérifié » ne signifie pas « sans erreur ». Les preuves ne valent que sous des conditions strictes : une architecture de processeur spécifique, des programmes mono-thread et des entrées de moins de 64 Mo. En pratique, ces bibliothèques fonctionnent sur des matériels différents et dans des configurations différentes.
Le coût de calcul est élevé, les preuves individuelles consommant des centaines de millions de tokens. Anthropic ne communique pas le coût total du projet. Mais si l'IA peut vérifier son propre code, les développeurs peuvent avoir davantage confiance dans les logiciels générés par l'IA et passer moins de temps à les relire. Cela économise des coûts non seulement sur la vérification, mais sur l'ensemble du processus de programmation. Un essai plus restreint a également montré que les preuves sont réutilisables, et les modèles plus récents gagnent en efficacité : Opus 5.5 résout la moitié des preuves avec environ 40 pour cent de tokens en moins qu'Opus 5.Ad
Le projet renforce l'argument en faveur de l'automatisation du logiciel. Si l'IA peut écrire du code et garantir sa correction dans des conditions définies, la question passe de « L'IA sait-elle programmer ? » à « L'IA peut-elle prouver que le code qu'elle écrit est sûr ? » Si la réponse est oui, les conséquences pourraient aller bien au-delà des outils de programmation actuels.
Exemple à l'appui : Anthropic s'attend à ce que la vérification formelle avec l'IA devienne bientôt aussi pratique que les tests standards, et La feuille de route de Theorem cible déjà des infrastructures critiques comme glibc, OpenSSL et cURL.
Source : Anthropic