Anthropic koristi AI za matematičku provjeru softvera

Anthropic i Theorem su 22. oktobra predstavili rezultate rada u kojem je Claude pomagao da se matematički provjere određena svojstva softvera otvorenog koda. Prema njihovoj objavi, obuhvaćeno je 239 testnih ulaznih tačaka u 123 biblioteke. To nije potvrda da su sve te biblioteke potpuno bezbjedne.

Dokaz umjesto uvjerljivog odgovora

Formalna provjera znači da se precizno definiše tvrdnja o programu, a zatim napravi matematički dokaz koji poseban alat može provjeriti. AI ovdje pomaže u izradi dokaza; njegova uvjerljivost nije kriterijum tačnosti. Dobijene dokaze provjerava sistem Rocq.

Razlika je praktična. Testiranje obično traži primjer u kojem program griješi. Formalni dokaz pokušava da pokrije sve ulaze unutar jasno definisanih granica. Ako su te granice uske, i zaključak mora ostati uzak.

Broj 123 ne znači 123 potpuno provjerene biblioteke

Anthropic navodi da su provjeravani konkretni programi za testiranje, uz ograničenja poput ulaza manjih od 64 MB, rada u jednoj niti i određene konfiguracije za RISC-V procesore. Rezultat se zato ne može automatski prenijeti na svaki server, verziju biblioteke ili način njenog korišćenja.

Javni repozitorijum Theorema, pregledan 25. oktobra, sadrži dokaze za 60 ulaznih tačaka u 25 biblioteka. To je objavljeni podskup, a ne drugi zbir cijelog istraživanja. Dokumentacija izričito upozorava da je model Linux procesa nepotpun i da dokaz zavisi od njegovih pretpostavki.

Dokazi se odnose na prevedene programe, odnosno binarne datoteke, a ne samo na izvorni kod. U navedenim uslovima porede njihovo izvršavanje sa verzijama koje sadrže dodatne provjere grešaka. To nije obećanje da aplikacija nema logičke propuste ili da je otporna na svaki napad.

Šta firma treba da traži od dobavljača

Naša urednička procjena je da ovakav pristup može biti vrijedan za komponente od kojih zavisi veliki broj aplikacija. Ipak, oznaka „AI provjereno” sama ne govori dovoljno. Dobavljač treba da navede tačnu verziju, dokazano svojstvo, pretpostavke i postupak ponovne provjere poslije izmjene koda.

Ovo nije razlog da se preskoče ažuriranja, ljudski pregled ili redovno testiranje. Za razvojne timove sljedeće pitanje nije samo koliko dokaza AI može da napiše, već koliko njih drugi mogu da ponove i primijene na stvarne sisteme.

Odvojeni primjer upotrebe AI-ja u otkrivanju ranjivosti opisali smo u tekstu o PHP-u i objavljenim ispravkama.

AI pomogao da se otkriju kritični propusti u PHP-u

Istraživači uz pomoć AI-ja pokazali su ozbiljnost propusta u PHP-u, softveru iza brojnih poslovnih sajtova. Ispravke su objavljene, ali njihovo postojanje ne znači da ih je vaš hosting već primijenio.

AI BalkanVladimir Sukara

Izvori

Anthropic: formalna provjera softvera, 22. oktobar 2026.

Theorem: javni repozitorijum dokaza i ograničenja, pregledano 25. oktobra 2026.

Za provjerene AI vijesti i praktična objašnjenja, pridružite se AI Balkanu besplatno.