Kompania Anthropic prezantoi rezultatet e eksperimenteve p\u00ebr p\u00ebrdorimin e modeleve AI p\u00ebr verifikimin formal t\u00eb besueshm\u00ebris\u00eb dhe siguris\u00eb s\u00eb projekteve ekzistuese. Gjat\u00eb eksperimentit, p\u00ebrmes modeleve AI p\u00ebr 123 biblioteka t\u00eb hapura, t\u00eb testuara n\u00eb infrastruktur\u00ebn OSS Fuzz, u gjeneruan prova matematikore p\u00ebr munges\u00ebn e gabimeve gjat\u00eb pun\u00ebs me memorien. <\/p>\n
Kontrolli u krye n\u00eb nivelin e kodit t\u00eb kompiluar t\u00eb assembler-it p\u00ebr arkitektur\u00ebn RISC-V. Sasia totale e provave t\u00eb gjeneruara arriti rreth 180 milion rreshta kodi p\u00ebr sistemin e verifikimit Rocq Prover (rreth 600 mij\u00eb rreshta p\u00ebr skedarin binar me 18 mij\u00eb instruksione RISC-V). Provat u formuan p\u00ebrmes automatizimit t\u00eb transformimit t\u00eb testeve ekzistuese t\u00eb fuzzing n\u00eb specifikime formale, pas t\u00eb cilave modeli AI Claude provonte se, p\u00ebr t\u00eb gjitha t\u00eb dh\u00ebnat hyr\u00ebse deri n\u00eb 64 MB, programi nuk kishte d\u00ebshtime. <\/p>\n
Gjat\u00eb procesit t\u00eb nd\u00ebrtimit t\u00eb provave, modeli AI ishte n\u00eb gjendje t\u00eb identifikonte dhe p\u00ebrgatiste korrigjime p\u00ebr qindra gabime q\u00eb m\u00eb par\u00eb nuk ishin v\u00ebrtetuar gjat\u00eb testimit t\u00eb fuzzing. Midis t\u00eb tjerash, u identifikuan vulnerabilitete q\u00eb \u00e7onin n\u00eb mbushjen e tamponit gjat\u00eb p\u00ebrpunimit t\u00eb t\u00eb dh\u00ebnave t\u00eb caktuara hyr\u00ebse (p.sh., CVE-2026-56132 n\u00eb libexpat), si edhe gabime logjike. P\u00ebrve\u00e7 k\u00ebsaj, modeli AI u p\u00ebrdor p\u00ebr t\u00eb provuar p\u00ebrputhshm\u00ebrin\u00eb e zbatimit t\u00eb algoritmit zlib n\u00eb b\u00ebrtham\u00ebn Linux me specifikimin RFC 1950.<\/p>\n
Po ashtu, n\u00eb gjuh\u00ebn Rust u gjenerua nj\u00eb interpretues p\u00ebr nj\u00eb n\u00ebngrup t\u00eb gjuh\u00ebs Python, p\u00ebr t\u00eb cilin, me ndihm\u00ebn e veglave Verus, u p\u00ebrgatit nj\u00eb prov\u00eb formale p\u00ebr p\u00ebrputhshm\u00ebrin\u00eb me semantik\u00ebn e CPython. P\u00ebr krahasimin e sjelljes me CPython, u ekzekutuan m\u00eb shum\u00eb se 1.7 milion programe Python t\u00eb gjeneruara rast\u00ebsisht. N\u00eb 99.95% t\u00eb rasteve, rezultatet e ekzekutimit t\u00eb k\u00ebtyre programeve n\u00eb implementimin e ri dhe n\u00eb CPython p\u00ebrputheshin, nd\u00ebrsa diferencat e identifikuara ishin raste t\u00eb njohura kufitare.<\/p>\n
Verifikimi formal i kryer garanton p\u00ebrputhshm\u00ebrin\u00eb me specifikimin, por nuk p\u00ebrjashton plot\u00ebsisht shfaqjen e problemeve me sigurin\u00eb, pasi risqet e shkaktuara nga problemet me multithreading, lidhjen dinamike dhe sjelljen anormale t\u00eb pajisjeve reale nuk mbeten t\u00eb formalizuara. Avantazhi ky\u00e7 i qasjes s\u00eb propozuar \u00ebsht\u00eb puna direkt me skedar\u00ebt binar\u00eb, e cila lejon shmangien e nevoj\u00ebs p\u00ebr t\u00eb rib\u00ebr\u00eb kodin ekzistues n\u00eb gjuh\u00ebt e verifikueshme formalisht. \n Burimi: opennet.ru<\/a> <\/p>","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"excerpt":{"rendered":"