123 bibliotekų saugumo savybes Claude pagrindė įrodymais
Anthropic ir Theorem panaudojo Claude matematiniams programų savybių įrodymams. Rezultatai galioja apibrėžtoms sąlygoms, o ne visoms galimoms klaidoms.
Claude sukūrė matematinius saugumo savybių įrodymus 123 atviro kodo bibliotekoms, bendrame projekte su Theorem pranešė Anthropic tyrėjai. Spalio 22 dieną paskelbtame darbe jie aprašo 239 patikrintus įėjimo taškus ir maždaug 180 milijonų Rocq įrodymų kodo eilučių.
Rezultatas nereiškia, kad šiose bibliotekose nebeliko jokių klaidų: įrodymai patvirtina konkrečius teiginius, galiojančius tyrėjų apibrėžtoje vykdymo aplinkoje. Anthropic aiškiai atskiria tokią formalią patikrą nuo bendro pažado, kad programa bus saugi kiekviename kompiuteryje ar naudojimo scenarijuje.
Tyrėjai pradėjo nuo Google OSS-Fuzz projekto bandymų, kuriuose atsitiktinai generuojami ir keičiami duomenys padeda aptikti programos lūžius. Jų metodas tokius bandymus pavertė specifikacijomis: vietoj daugelio atskirų paleidimų siekiama įrodyti, kad pasirinktas bandymas nelūš visoje apibrėžtoje įvesčių aibėje.
Pagal Anthropic aprašymą, Claude dirbo su sukompiliuotomis RISC-V instrukcijomis, o parengtą įrodymą nepriklausomai tikrino Rocq tikrinimo branduolys. Taigi kalbos modelio atsakymas nelaikomas patvirtinimu vien dėl to, kad jis įtikinamai paaiškina programos veikimą ar pateikia ilgą kodą.
Įrodytos savybės apima įprastą programos pabaigą be atminties saugos klaidų ir nepavykusių patikrų, kai įvestis mažesnė nei 64 MB. Tyrime daroma prielaida, kad tai vienos gijos statinis vykdomasis failas su fiksuotu atminties biudžetu, veikiantis Linux sistemoje su RISC-V procesoriumi.
Anthropic nurodo, kad tipinis įrodymas siekė apie 600 tūkstančių eilučių, o vykdomojo failo instrukcijų skaičiaus mediana buvo 18 tūkstančių. Visų tų eilučių žmogui skaityti nereikia, tačiau būtina pasitikėti tikrinimo branduoliu, tiksliais teiginių apibrėžimais ir procesoriaus bei sistemos modeliais.
Bandydamas įrodymus Claude taip pat aptiko ir taisė klaidas, kurios trukdė patvirtinti pasirinktą programos savybę, rašo tyrėjai. Tarp pavyzdžių yra išpakavimo funkcijos klaida, pasireiškianti tik su maždaug 20 MB dydžio ir labai konkrečios struktūros duomenimis.
Kitam paveikslėlio dekoderio trūkumui reikėjo 64 MB įvesties ir daugiau nei 2 GB atminties, nurodoma laboratorijos techniniame aprašyme. Tai paaiškina skirtumą nuo įprastų atsitiktinių bandymų: retą atvejį gali būti sunku sugeneruoti, nors jis priklauso įrodinėjamo teiginio aprėpčiai.
Kartu laboratorija pabrėžia apribojimus: daug realių sistemų naudoja x86 ar ARM procesorius ir dinamines bibliotekas, o ne tyrime pasirinktą aplinką. Ne visi bibliotekų įėjimo taškai patikrinti, o saugos priemonė AddressSanitizer taip pat neaptinka visų įmanomų atminties naudojimo klaidų.
Atskirame 36 užduočių bandyme Opus 5.5 pusei įrodymų prireikė apie 40 procentų mažiau žetonų nei Opus 5, skelbia Anthropic. Leidus agentams dalytis jau parengtais įrodymais, žetonų poreikis sumažėjo 17 procentų, tačiau sudėtingiems projektams skaičiavimo sąnaudos išlieka svarbiu ribojimu.
Anthropic viešina dalį įrodymų ir aplinkos aprašų, kad juos būtų galima nepriklausomai patikrinti bei panaudoti kituose projektuose. Theorem siūlo tą pačią grandinę kitiems atviro kodo darbams; toliau reikės plėsti patikras į daugiau architektūrų ir realistiškesnes vykdymo sąlygas.
Rašome apie dirbtinį intelektą lietuviškai. Kiekvienas straipsnis parengtas pagal nurodytą šaltinį, o nuorodą į originalą rasite kortelėje „Šaltinis“.
