CP v2

Tag: Formalioji verifikacija

  • Justin Sun įsteigė matematikos premiją iki 930 000 eurų: prizai už įrodomas užduotis ir DI

    Justin Sun įsteigė matematikos premiją iki 930 000 eurų: prizai už įrodomas užduotis ir DI

    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.

  • 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.