Kutatás · Wired ·
Az AI-val a formális szoftververifikáció is elérhetőbbé válhat
Egy Stanford-kutató AI-eszközzel fél napnál rövidebb idő és 500 dollárnál kevesebb költség mellett végzett el egy mérnöki munkát, amelyhez három szakértőnek öt hónap kellett.
Chuyue Sun kutatásában az AI a Signal üzenetküldő alkalmazás titkosításáért felelős kód egy részét ellenőrizte. A formális verifikáció célja régóta, hogy matematikai módszerekkel bizonyítsák a szoftver hibamentességét, de a folyamat hosszú és munkaigényes.
A &Truth vállalat 70 millió dollárt gyűjtött, a Harmonic pedig 295 millió dollár finanszírozást kapott. Az Anthropic és a Theorem közösen jelentette be, hogy AI-val segítettek hibákat találni nyílt forráskódú szoftverekben, amelyeket korábbi tesztek sem találtak meg. A technológia még prototípus-fázisban van.
Szkeptikusok szerint a módszer nem szűri ki a felhasználói hibákat és a hardverhibákat, a hibakereső AI-szoftvert fejlesztő Antithesis vezetője szerint pedig csak kimerítő tesztelés igazolhatja, hogy a biztosíték valós. A cégek közlése szerint Boeing-gépekben, Amazon-szerverekben és több mint 2,5 milliárd aktív Apple-eszközben is van legalább részben formálisan ellenőrzött szoftver.
Miért számít?
Ha az AI csökkenti a verifikáció költségét, a módszer a kritikus rendszereken túl is elterjedhet, a vevők fizetési hajlandósága viszont még nem ismert. Elterjedés a kritikus rendszereken túl
Eredeti cím: The ‘Pain in the Ass’ Math That Could Save Vibe Coding From Itself
Címkék: formális verifikáció, biztonság, szoftverfejlesztés