Kriptovaliutų ekosistemos veikėjas ir TRON įkūrėjas Justin Sun paskelbė įsteigiantis Justin Sun Prize – matematikos ir formalaus verifikavimo premiją, kurios didžiausias apdovanojimas už vieną uždavinį sieks iki 930 000 eurų. Iniciatyva pristatoma kaip atviras „uždavinių sąrašu“ paremtas mechanizmas, kuriame sprendimų kokybę lemia ne autoriaus statusas, o įrodymo griežtumas ir galimybė jį patikrinti mašina.
Organizatorių teigimu, premija skirta proveržiams fundamentiniuose moksluose, ypač matematikoje, taip pat mašininio formalaus įrodymų tikrinimo srityje. Skirtingai nei tradiciniai apdovanojimai, čia nenumatomas nominavimo ciklas ar karjeros nuopelnų vertinimas: prizas siejamas su konkrečiu uždaviniu, o laimi pirmasis pateikęs reikalavimus atitinkantį sprendimą.
Pagrindas – patikrinami įrodymai
Premijos modelis remiasi formalia verifikacija, kai matematiniai įrodymai perrašomi į specialias formalias kalbas ir tikrinami įrodymų tikrintuvais. Tokia praktika pastaraisiais metais sparčiai plinta akademinėje bendruomenėje, nes mažina žmogiškų klaidų tikimybę ir leidžia tiksliau atsekti, kurios įrodymo grandys yra kritinės.
Ši kryptis išpopuliarėjo ir dėl to, kad didėja įrodymų sudėtingumas, o recenzavimo procesas ne visada pajėgia vienodai giliai patikrinti visas detales. Formali verifikacija laikoma viena iš perspektyvių priemonių, galinčių sustiprinti mokslo patikimumą srityse, kur klaidos gali išlikti nepastebėtos metų metus.
Pirmieji laureatai ir diskusijos
Kartu paskelbta ir pirmoji laureatų banga: pranešime teigiama, kad įvertinti sprendimai bei formalizuoti įrodymai, susiję su 66 matematikos uždaviniais. Taip pat nurodoma, kad didžiausias prizas atiteko „OpenAI“ tyrėjų komandai už suformuluotą sprendimą ir formalizaciją, siejamą su Navjė–Stokso egzistavimo ir glotnumo uždaviniu.
Vis dėlto būtent ši dalis neišvengiamai kelia klausimų, nes Navjė–Stokso uždavinys yra vienas iš Clay Matematikos instituto Tūkstantmečio problemų, o tokio masto proveržiai paprastai sulaukia plataus nepriklausomo patvirtinimo, recenzavimo ir viešų diskusijų. Dėl to tikėtina, kad akademinė bendruomenė vertins ne tik paskelbimą, bet ir tai, ar pateikti įrodymai yra prieinami, reprodukuojami ir praeina nepriklausomą tikrinimą.
Kur čia vieta DI?
Premijos sumanytojai akcentuoja, kad iniciatyva pritaikyta laikotarpiui, kai matematikos ir programinės įrangos kūrimo procesuose vis dažniau dalyvauja DI. Tokiu atveju formali verifikacija tampa natūralia jungtimi tarp žmogaus suformuluotos idėjos ir mašininio patikrinimo, leidžiančio aiškiai įvertinti, ar rezultatas tikrai įrodomas.
Tačiau kartu tai reiškia ir naują standartą: neužtenka pateikti įtikinamai skambančios argumentacijos ar dalinio skaičiavimo, jei premijos kriterijus yra formaliai patikrintas kodas. Praktikoje tai gali paskatinti kurti atviresnes įrodymų bazes, didinti skaidrumą ir aiškiau atskirti hipotezes nuo griežtai patvirtintų teiginių.
„Mano turtas kilo iš matematikos ir grįš į matematiką“, – sakė Justin Sun.
Pranešime taip pat nurodoma, kad prizų išmokėjimai bus atliekami stabiliosiomis kriptovaliutomis, o išmokėjimų apskaita fiksuojama blokų grandinėje. Toks sprendimas gali suteikti daugiau viešo atsekamumo, tačiau reali iniciatyvos vertė galiausiai priklausys nuo to, ar uždavinių sąrašas, įrodymų kodas ir tikrinimo procedūros bus iš tiesų viešos, aiškios ir nuosekliai prižiūrimos.
Matematikos bendruomenei svarbiausias klausimas išlieka paprastas: ar premija taps patikimu postūmiu formalios verifikacijos kultūrai, ar tik dar vienu garsiu pažadu. Jei organizatoriai užtikrins atvirą prieigą, nepriklausomą patikrą ir aiškius standartus, iniciatyva gali papildyti tradicinius apdovanojimus tuo, ko jiems dažnai trūksta – mašiniškai patikrinamu, viešai audituojamu mokslo rezultatu.
Leave a Reply