Verslininkas Justinas Sunas pranešė įkuriantis „Justin Sun Prize“ – naują tarptautinę iniciatyvą, kuri apdovanos proveržius matematikoje ir formaliame įrodymų tikrinime. Organizatorių teigimu, prizas kuriamas kaip decentralizuota akademinių uždavinių sistema, kurioje svarbiausia ne institucinis svoris, o pats patikrinamas rezultatas.
Skelbiama, kad didžiausia vieno uždavinio premija gali siekti iki 900 000 eurų. Apdovanojimų mechanizmas remiasi viešu uždavinių sąrašu, o laimėtoju laikomas pirmasis, pateikęs reikalavimus atitinkantį sprendimą ir mašiniškai patikrinamą formalizuotą įrodymą.
Kaip veiks apdovanojimas?
Pasak iniciatorių, „Justin Sun Prize“ atsisako tradicinių nominacijų, rekomendacijų ir cikliškų komisijų darbo ritmų. Vietoje to prizas siejamas tiesiogiai su konkrečiais matematikos uždaviniais, o įrodymo kokybė vertinama pagal griežtą formalizavimą ir verifikavimą.
Praktikoje tai reiškia, kad apdovanojimą teoriškai gali gauti bet kas, jei tik pateikiamas sprendimas atitinka taisykles ir gali būti patikrintas formaliomis priemonėmis. Iniciatyva taip pat pabrėžia, kad nėra skirties tarp žmogaus darbo ir DI indėlio, jei galutinis įrodymas yra patikrinamas.
Pirmieji laimėtojai ir Navier–Stokso uždavinys
Kartu paskelbti ir pirmieji „Justin Sun Prize“ laureatai už sprendimus bei formalizuotus įrodymus, susijusius su 66 matematikos uždaviniais. Didžiausias apdovanojimas, kaip skelbiama pranešime, atiteko „OpenAI“ tyrėjų komandai už sprendimą ir formalizuotą įrodymą, siejamą su trimačių Navier–Stokso lygčių egzistavimo ir glodumo problema.
Navier–Stokso lygtys aprašo skysčių ir dujų judėjimą, todėl jų taikymai svarbūs nuo aerodinamikos iki klimato modelių. Ši tema ypač žinoma dėl to, kad 2000 metais Clay Mathematics Institute ją įtraukė į Septynių tūkstantmečio uždavinių sąrašą, kuriame už sprendimą numatyta 900 000 eurų siekianti premija.
Kodėl akcentuojama formalioji verifikacija?
Pastaraisiais metais matematikoje ir programų inžinerijoje vis didesnį vaidmenį įgauna formali verifikacija, kai įrodymas ar algoritmo teisingumas pateikiamas taip, kad jį gali patikrinti specialios sistemos. Tai mažina dviprasmybių riziką ir leidžia tiksliau atsekti, kokiomis prielaidomis remiamasi.
„Justin Sun Prize“ koncepcija remiasi būtent šiuo principu: apdovanojamas ne vien idėjos originalumas, bet ir tai, ar įrodymas gali būti patvirtintas mašiniškai. Organizatorių teigimu, taip siekiama spartinti fundamentinius tyrimus ir geriau prisitaikyti prie pokyčių, kuriuos į mokslą atneša DI įrankiai.
„Mano turtas kilo iš matematikos ir į matematiką sugrįš“, – sakė Justinas Sunas.
Pranešime taip pat teigiama, kad uždavinių sąrašas bus nuolat pildomas ir viešai atnaujinamas, o jau įtraukti uždaviniai nebus šalinami. Nurodoma, kad apdovanojimų išmokėjimo įrašai bus fiksuojami blokų grandinėje, o pati iniciatyva akcentuoja atvirumą, viešą naudą ir atvirąjį kodą.
Numatoma, kad prizas galės būti išmokamas stabiliosiomis kriptovaliutomis, o mokėjimo būdas bus pasirenkamas laimėtojo. Organizatorių tikinimu, tai turėtų supaprastinti tarptautinius atsiskaitymus, tačiau praktinis įgyvendinimas ir skaidrumo standartai taps vienu svarbiausių aspektų, nuo kurių priklausys iniciatyvos patikimumas akademinėje bendruomenėje.