Anthropic kynnti niðurstöður tilrauna með gervigreindarlíkönum til að staðfesta formlega áreiðanleika og öryggi núverandi verkefna. Í tilrauninni voru gervigreindarlíkön notuð til að búa til stærðfræðilegar sannanir fyrir fjarveru minnisvillna fyrir 123 opna hugbúnaðarbókasöfn sem prófuð voru í OSS Fuzz innviðunum.
Staðfestingin var framkvæmd á þýddu samsetningarkóðastigi fyrir RISC-V arkitektúrinn. Heildarmagn myndaðra sönnunargagna nam um það bil 180 milljónum kóðalína fyrir Rocq Prover staðfestingarkerfið (um það bil 600 línur í hverri tvíundarskrá með 18 RISC-V skipunum). Sönnunargögnin voru búin til með því að breyta sjálfkrafa núverandi fuzzingprófum í formlegar forskriftir, og að lokum sannaði Claude AI líkanið að forritið er gallalaust fyrir öll inntaksgögn allt að 64 MB.
Í sönnunarferlinu gat gervigreindarlíkanið greint og undirbúið lagfæringar á hundruðum villna sem áður höfðu ekki verið greindar með fuzz-prófunum. Meðal annars voru þar á meðal veikleikar í biðminnisviðflæði við vinnslu ákveðinna inntaksgagna (t.d. CVE-2026-56132 í libexpat), sem og rökvillur. Ennfremur var gervigreindarlíkanið notað til að sanna samræmi útfærslu kjarnans á zlib reikniritinu. Linux RFC 1950 forskriftir.
Túlkur fyrir undirmengi af Python var einnig búinn til í Rust, og fyrir hann var formleg sönnun á samræmi við merkingarfræði CPython útbúin með Verus verkfærakistunni. Til að bera saman hegðun við CPython voru yfir 1.7 milljónir handahófskenndra Python forrita keyrð. Í 99.95% tilfella voru niðurstöður keyrslu þessara forrita í nýju útfærslunni og í CPython samsvörun, og öll frávik sem fundust voru þekkt jaðartilvik.
Formleg staðfesting tryggir að forskriftir séu í samræmi við kröfur, en hún útilokar ekki öryggisvandamál að fullu, þar sem áhætta af völdum fjölþráðavandamála, breytilegra tengja og óeðlilegrar hegðunar á raunverulegum vélbúnaði er enn óformleg. Lykilkostur við þessa aðferð er að hún vinnur beint með tvíundarskrár, sem útilokar þörfina á að endurskrifa núverandi kóða í formlega staðfestanlegum tungumálum.
Heimild: opennet.ru
