{"id":183972,"date":"2026-10-23T11:41:12","date_gmt":"2026-10-23T09:41:12","guid":{"rendered":"https:\/\/prohoster.info\/blog\/news\/anthropic-razvivaet-tehniku-dlya-formalnoj-verifikaczii-sushhestvuyushhego-po-pri-pomoshhi-ai"},"modified":"2026-10-23T11:41:16","modified_gmt":"2026-10-23T09:41:16","slug":"anthropic-develops-technique-for-formal-verification-of-existing-software-using-ai","status":"publish","type":"post","link":"https:\/\/prohoster.info\/et\/blog\/news\/anthropic-develops-technique-for-formal-verification-of-existing-software-using-ai","title":{"rendered":"Anthropic arendab tehnika olemasoleva tarkvara formaalseks valideerimiseks AI abil","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
Ettev\u00f5te Anthropic esitles katsete tulemusi AI-mudelite kasutamisest olemasolevate projektide usaldusv\u00e4\u00e4rsuse ja ohutuse formaalseks kinnitamiseks. Katse k\u00e4igus genereeriti AI-mudelite abil 123 avatud raamatukogu, mis olid testitud OSS Fuzzi infrastruktuuris, matemaatilised t\u00f5endid m\u00e4luga seotud vigade puudumise kohta. <\/p>\n
Kontroll viidi l\u00e4bi RISC-V arhitektuuri kompileeritud assembleri koodi tasandil. Kokku genereeriti umbes 180 miljonit t\u00f5endit Rocq Proveri verifitseerimise s\u00fcsteemi jaoks (umbes 600 tuhat rida binaarfaili kohta koos 18 tuhande RISC-V k\u00e4suga). T\u00f5endid loodi olemasolevate fuzzing-testide automaatse \u00fcleviimise kaudu formaalsetesse spetsifikatsioonidesse, mille j\u00e4rel AI mudel Claude t\u00f5endas, et k\u00f5igi kuni 64 MB suuruste sisendandmete korral ei esine programmis t\u00f5rkeid. <\/p>\n
T\u00f5endite koostamise k\u00e4igus suutis AI-mudel tuvastada ja ette valmistada parandusi sadadele vigadele, mis olid varem fuzzing-testimise k\u00e4igus t\u00e4helepanuta j\u00e4\u00e4nud. Muuhulgas avastati haavatavusi, mis p\u00f5hjustavad puhver\u00fclekannet teatud sisendandmete t\u00f6\u00f6tlemisel (nt CVE-2026-56132 libexpatis), samuti loogilisi vigu. Lisaks kasutati AI-mudelit zlib algoritmi rakenduse vastavuse t\u00f5endamiseks Linuxi tuumas spetsifikatsioonile RFC 1950.<\/p>\n
Rust'i keeles genereeriti ka Python'i keele alamkogumi t\u00f5lgendaja, mille jaoks koostati Verus'i t\u00f6\u00f6riistade abil formaalne t\u00f5end vastavusest CPython'i semantikaga. CPython'i k\u00e4itumise v\u00f5rdlemiseks viidi l\u00e4bi \u00fcle 1.7 miljoni juhuslikult genereeritud Python'i programmi. 99,95% juhtudest olid nende programmide tulemused uues rakenduses ja CPython'is identsed, samas kui avastatud erinevused osutusid tuntud \u00e4\u00e4rmisteks juhtudeks.<\/p>\n
Teostatud formaalne verifikatsioon tagab vastavuse spetsifikatsioonile, kuid ei v\u00e4lista t\u00e4ielikult turvaprobleemide tekkimist, kuna formaalseteks ei j\u00e4\u00e4 riskid, mis on seotud mitme l\u00f5ime, d\u00fcnaamilise sidumise ja reaalse riistvara ebanormaalse k\u00e4itumisega. Pakutava l\u00e4henemise peamine eelis on otsene t\u00f6\u00f6tamine binaarfailidega, mis v\u00f5imaldab v\u00e4ltida olemasoleva koodi \u00fcmberkirjutamist formaalselt verifitseeritavates keeltes. \n Allikas: opennet.ru<\/a> <\/p>","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"excerpt":{"rendered":"