Claude d'Anthropic écrit désormais du code et en prouve automatiquement la sécurité
decoder ·
Anthropic s'est associée à Theorem pour démontrer que son modèle d'IA, Claude, peut générer automatiquement des preuves mathématiques vérifiant l'exactitude du code logiciel existant. Lors d'un projet récent, Claude a produit environ 180 millions de lignes de code de preuve pour 123 bibliothèques open-source issues du projet OSS-Fuzz de Google en seulement quelques semaines. Ce processus autonome consistait à traduire les tests de plantage en problèmes mathématiques et à analyser le code machine compilé, avec un outil indépendant appelé Rocq chargé de vérifier les résultats. Au cours de cette phase de vérification, Claude a identifié des centaines de bugs passés inaperçus pendant des années par les méthodes de test conventionnelles, y compris des failles de sécurité critiques dans des lecteurs PDF largement utilisés. Toutefois, ces preuves formelles sont soumises à des limitations strictes : elles ne s'appliquent qu'à des architectures de processeurs spécifiques, à des programmes monothread et à des entrées inférieures à 64 Mo. Bien que le coût informatique reste élevé, Anthropic note que les nouveaux modèles deviennent plus efficaces, nécessitant moins de tokens pour résoudre des preuves similaires. L'entreprise vise à rendre la vérification formelle pilotée par l'IA aussi courante que les tests logiciels standards, transformant potentiellement la manière dont les développeurs font confiance au code généré par l'IA et le révisent.
decoder