Claude di Anthropic scrive codice e ne dimostra automaticamente la sicurezza
decoder ·
Anthropic ha collaborato con Theorem per dimostrare che il suo modello di intelligenza artificiale, Claude, può generare automaticamente dimostrazioni matematiche che verificano la correttezza del codice software esistente. In un recente progetto, Claude ha prodotto circa 180 milioni di righe di codice di dimostrazione per 123 librerie open source del progetto OSS-Fuzz di Google in poche settimane. Questo processo autonomo ha comportato la traduzione dei test di crash in problemi matematici e l'analisi del codice macchina compilato, con i risultati verificati da uno strumento indipendente chiamato Rocq. Durante questa fase di verifica, Claude ha identificato centinaia di bug passati inosservati dai metodi di testing convenzionali negli anni, incluse gravi vulnerabilità di sicurezza in lettori PDF ampiamente utilizzati. Tuttavia, queste dimostrazioni formali sono soggette a limitazioni rigorose, applicandosi solo a specifiche architetture di processore, programmi single-threaded e input inferiori a 64 MB. Sebbene il costo computazionale rimanga elevato, Anthropic segnala che i modelli più recenti stanno diventando più efficienti, richiedendo meno token per risolvere dimostrazioni simili. L'azienda mira a rendere la verifica formale basata sull'IA una pratica routine quanto il testing software standard, potenzialmente trasformando il modo in cui gli sviluppatori si fidano del codice generato dall'IA e lo revisionano.
decoder