„OpenAI“ tiesiog priartino išmaniųjų sutarčių apsaugą prie AI perėmimo
Naujausias „OpenAI“ matematikos proveržis gali priartinti automatizuotą teoremą, kuri priartėtų prie išmaniųjų sutarčių saugos darbo eigos.
Rugsėjo 8 d. dirbtinio intelekto įmonė pranešė, kad maždaug 10 000 vienu metu dirbančių AI agentų sukūrė Navier-Stokes skysčių judėjimo problemą po maždaug 88 valandų. Formalizacijai ir patikrinimui programinės įrangos tikrinimo asistente Lean prireikė dar 17 valandų naudojant GPT-6 Astra.
Sistema sukūrė analitinį įrodymą, parodantį, kad iš pradžių lygus skystis gali sukurti išskirtinumą per ribotą laiką, išlaikant baigtinę energiją, nustatant Tūkstantmečio premijos formuluotės C ir D atvejus. „OpenAI“ išleido įrodymą ir „Lean“ formalizavimą nepriklausomam patikrinimui.
Kriptovaliutų kūrėjams greitesnė reikšmė yra šiame procese. Oficialus patikrinimas naudoja matematines specifikacijas ir teoremą, įrodančią, kad išmanusis sutarties kodas veikia taip, kaip numatyta, o tai yra sritis, kurioje, vadovaujant žmogui, patikrinimas gali būti brangus ir reikalaujantis daug darbo.
AI galėtų perkelti saugumo kliūtis prieš srovę
OpenAI eksperimento mastas labai panašus į scenarijų, kurį matematikas Terence’as Tao aprašė penkias dienas prieš paskelbimą.
Tao perspėjo, kad autonominės AI sistemos, paremtos didžiuliais skaičiavimo ištekliais, ilgainiui gali sukurti sudėtingus Navier-Stokes sprendimus ir oficialiai juos patikrinti tokiose sistemose kaip Lean, o didžioji dalis pasikartojančio atradimo proceso nebus viešai matoma.
Jo rūpestis buvo susijęs su tuo, ką mokslininkai gali prarasti kelyje. Nesėkmingi metodai ir tarpiniai atradimai dažnai suteikia įžvalgų, kurios nepatenka į galutinį įrodymą, o iš esmės autonominė sistema gali duoti teisingą rezultatą, neperduodama žmonėms tokio paties supratimo gylio.
Šis rūpestis susijęs su išmaniųjų sutarčių saugumu, nes teoremų įrodinėjimas tampa labiau automatizuotas.
„Ethereum“ dokumentuose teigiama, kad oficialus patikrinimas nustato, ar sutartis atitinka nekilnojamojo turto kūrėjų iš anksto nurodytas savybes. Prastai parašytos arba neišsamios specifikacijos gali leisti išvengti pažeidžiamumo aptikimo net ir sėkmingai patvirtinus.
Pajėgesnės AI sistemos galėtų sumažinti darbo, reikalingo kuriant įrodymus, svarbą, tuo pačiu padidinant svarbą nuspręsti, ką tie įrodymai turėtų apimti. Prieigos kontrolė, išėmimo sąlygos, apskaitos invariantai ir privilegijuotos funkcijos vis tiek turi būti tiksliai išreikštos, kad tikrintojas galėtų juos išbandyti.
Tai galėtų pakeisti oficialių „DeFi“ protokolų, tiltų ir žetonų turinčių išteklių platformų tikrinimo ekonomiką, kai rankų pastangos apribojo šios technikos panaudojimo mastą.
Kitas bandymas yra tai, ar sistemas, galinčias valdyti mokslinių tyrimų matematiką, galima pritaikyti gamybos programinei įrangai ir pateikti įrodymus, kuriuos kūrėjai ir auditoriai gali prasmingai tikrinti.
Įmonės, galinčios derinti automatinį teoremų įrodinėjimą su griežtu specifikacijų kūrimu, galėtų patikrinti daugiau sutarčių prieš įdiegdamos, tuo pat metu sutelkdamos žmogiškąsias žinias nustatydamos gedimus, kurių niekada neturi atsirasti.
