Claude produit 180 millions de lignes de preuves

LLéna

Anthropic et Theorem ont utilisé Claude pour générer, en quelques semaines, environ 180 millions de lignes de preuves formelles couvrant 123 bibliothèques open source, selon Brief IA. Le travail a été mené par l’équipe Frontier Red Team d’Anthropic avec Theorem, dont les ingénieurs ont conçu les outils et les fondations formelles. Pour lancer la génération, Claude s’est appuyé sur des tests de plantage issus d’OSS-Fuzz, dans le but de construire des preuves formelles pour des logiciels utilisés dans ces bibliothèques. L’opération a permis de détecter plusieurs centaines de bugs que les méthodes de test traditionnelles n’avaient pas repérés, et Claude a aussi pu corriger certains défauts. Les preuves sont contrôlées automatiquement par Rocq, un vérificateur indépendant, mais leur validité est limitée à des conditions précises : une architecture de processeur donnée, un fonctionnement mono-thread et des entrées de moins de 64 mégaoctets. Autrement dit, la vérification ne garantit pas que les mêmes résultats s’appliquent à toutes les configurations ou à des fichiers plus volumineux. Anthropic indique que chaque preuve mobilise des centaines de millions de tokens, sans communiquer le coût total du projet. L’entreprise et les chercheurs présentent la génération comme largement autonome et nécessitant très peu d’examen humain, mais les éléments disponibles ne détaillent pas davantage ce degré d’autonomie.