Anthropic Claude demonstrează matematic siguranța codului și repară erori vechi de zece ani

Anthropic a demonstrat că inteligența artificială poate depăși etapa simplei generări de cod, trecând la verificarea matematică a siguranței acestuia. Printr-o colaborare cu startup-ul Theorem, modelul Claude a produs circa 180 de milioane de linii de cod de demonstrație formală, găsind sute de erori critice pe care testele software convenționale le-au ratat ani la rând.

Ce s-a întâmplat

Echipa Frontier Red Team din cadrul Anthropic și specialiștii de la Theorem au folosit Claude pentru a verifica automat 123 de biblioteci open-source incluse în proiectul de securitate OSS-Fuzz al Google. În loc să scrie software de la zero, modelul a tradus testele de eroare în probleme matematice, a analizat codul mașină compilat și a generat demonstrații riguroase verificate ulterior de programul independent Rocq, aproape fără intervenție umană.

În timpul acestui proces, Claude nu doar că a produs dovezi matematice, dar a identificat și remediat sute de erori ascunse. Printre acestea s-a numărat o vulnerabilitate logică nedetectată de peste un deceniu, dar și zeci de breșe într-un cititor PDF utilizat la scară largă, găsite într-o singură săptămână. Deși sistemul are limite stricte — funcționează deocamdată doar pe o arhitectură fixă de procesor, pentru programe cu un singur fir de execuție și date de intrare sub 64 MB —, eficiența crește rapid: versiunea Opus 5.5 a rezolvat jumătate dintre sarcini cu 40% mai puține jetoane de calcul față de Opus 5.

De ce contează în România

Pentru industria de tehnologie și outsourcing din România, unde dezvoltarea de software, testarea automată și auditul de securitate sunt piloni importanți, tranziția spre verificarea formală asistată de AI este o schimbare de paradigmă. Până în prezent, demonstrarea matematică a lipsei de erori necesita decenii de muncă specializată și era rezervată exclusiv sistemelor critice din aviație sau spațiul militar.

Dacă instrumentele de verificare autonomă devin o rutină accesibilă, companiile de IT din România le-ar putea folosi pentru a reduce drastic timpul alocat depanării și revizuirii manuale a codului. Mai mult, securizarea infrastructurii deschise pe care o folosesc și produsele locale — precum bibliotecile OpenSSL sau cURL, vizate deja pe foaia de parcurs Theorem — va ridica standardul de siguranță pentru toate aplicațiile financiare și enterprise dezvoltate local.

Cum poți încerca

Sistemul complet de verificare automată descris în cercetare reprezintă un experiment avansat dezvoltat alături de Theorem și nu este integrat în interfața web comercială Claude. Fluxul autonom bazat pe verificatorul Rocq necesită resurse mari de calcul și o infrastructură tehnică dedicată, fără un buton de activare directă pentru publicul larg.

Dezvoltatorii pot totuși folosi versiunile Claude Opus prin interfața Anthropic sau prin API pentru a analiza cod sursă existent, a genera scenarii complexe de testare și a căuta erori greu de observat. Cei interesați de metodologia matematică pot explora asistentul de demonstrații Rocq și instrumentele proiectului Google OSS-Fuzz, disponibile gratuit în format open-source.