CP v2

Tag: Justin Sun Prize

  • „Justin Sun Prize“ ir „MathDB“ startuoja su 50 uždavinių pilotu: prizai iki 1 mln. eurų ir Lean patikra

    „Justin Sun Prize“ ir „MathDB“ startuoja su 50 uždavinių pilotu: prizai iki 1 mln. eurų ir Lean patikra

    „Justin Sun Prize“ kartu su matematikos tyrimų platforma „MathDB“ pradeda 50 uždavinių pilotinę programą, kurioje numatomi prizai iki 1 mln. eurų vienam uždaviniui. Organizatoriai teigia, kad tikslas yra sukurti aiškesnę, patikrinamą ir skaidresnę tvarką, kaip vertinami proveržiai fundamentinėje matematikoje.

    Pilotas apima skirtingo lygio uždavinius, tarp jų minimi ir vieni garsiausių atvirų klausimų, pavyzdžiui, P ir NP problema bei Rymano hipotezė. Bendra idėja paprasta: apdovanojamas ne tik rezultatas, bet ir jo patikimumas bei gebėjimas jį aiškiai perteikti.

    Sprendimų pateikimas ir pirminė peržiūra vyks per „MathDB“, kuri priims pateiktus darbus, tikrins Lean formalizacijas ir vertins aiškinamąją medžiagą. Tuo pat metu „Justin Sun Prize“ atskirai vertins tinkamumą, autorystę, pirmenybę ir kitas programos sąlygas.

    „DI keičia tai, kaip greitai galima tyrinėti matematiką, tačiau vien greitis dar nėra mokslinė pažanga“, – sakė „Justin Sun Prize“ įkūrėjas Justinas Sunas.

    Pasak organizatorių, atlygis bus skaidomas į tris dalis: 50 proc. skiriama už patį matematinį sprendimą, 30 proc. už Lean formalizaciją ir 20 proc. už aiškų, suprantamą išdėstymą. Tokia struktūra atspindi pastarųjų metų tendenciją akademiniame pasaulyje daugiau dėmesio skirti ne tik idėjai, bet ir jos patikrinamumui bei pakartojamumui.

    Formalus įrodymų tikrinimas kompiuteriu yra viena sparčiausiai augančių krypčių šiuolaikinėje matematikoje ir kompiuterių moksle. Lean tipo įrankiai leidžia įrodymus aprašyti taip, kad juos galėtų patikrinti įrodymų tikrintuvai, o tai mažina klaidų riziką ir palengvina kitų tyrėjų darbą, kai tenka remtis itin sudėtingais rezultatais.

    „MathDB“ projektą vysto Kalifornijos technologijos instituto profesorius Tony Yue Yu ir jo komanda, kurie šiame pilote prižiūrės mokslinę dalį. Platforma apibūdinama kaip didelės apimties matematikos apibrėžimų, teoremų, hipotezių ir atvirų problemų duomenų bazė, jungianti aiškinamuosius tekstus su formalizavimo galimybėmis.

    „Sprendžiant fundamentinį uždavinį dažnai gaunama daug daugiau nei atsakymas į pradinį klausimą: atsiveria netikėti ryšiai, atsiranda naujų įrankių ir krypčių“, – sakė Tony Yue Yu.

    Organizatoriai pabrėžia, kad visi apdovanojimai bus teikiami tik atlikus pilną tinkamumo patikrą ir laikantis kovos su pinigų plovimu bei sankcijų reikalavimų. Detalios pilotui atrinktų uždavinių sąlygos ir pateikimo procedūros bus skelbiamos programos kanaluose per „MathDB“ ir „Justin Sun Prize“.

    Tokio tipo prizai atspindi platesnę tendenciją: didėjant dirbtinis intelektas įrankių vaidmeniui moksle, vis svarbesnis tampa patikimumo standartas, kurį galima nepriklausomai patikrinti. Pilotinė programa bando sujungti tris dalykus į vieną grandinę: idėją, jos mašininį patvirtinimą ir aiškų paaiškinimą, kad rezultatas būtų naudingas platesnei bendruomenei.

  • Justinas Sunas įsteigė „Justin Sun Prize“: iki 900 000 eurų už proveržius matematikos įrodymuose

    Justinas Sunas įsteigė „Justin Sun Prize“: iki 900 000 eurų už proveržius matematikos įrodymuose

    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.