OpenAI avaldas 722 matemaatikakäsikirja — kontroll leidis tõestustes lünki

11. oktoober 2026, kell 20:00|Autor: QUASA toimetus|4 min lugemist| 2

OpenAI avaldas 6. oktoobril GitHubis 722 matemaatikakäsikirja 372 tulemuste perekonnas ning võttis 7. oktoobril neist kolm märgivea tõttu tagasi. Suur avaldatud kogu annab matemaatikutele väited ja tõestused uurimiseks, kuid käsikirjade arv ei näita, kui paljud tulemused on sõltumatult läbi vaadatud.

OpenAI avalikus matemaatikakogus on pärast tagasivõtmisi 719 käsikirja; ettevõtte arvestuse järgi on Leani formaliseering olemas 300 juhtiva tulemuse kohta ehk ligikaudu 42 protsendil kogu käsikirjade arvust. Formaliseeringu olemasolu on oluline kontrollietapp, ent see ei ütle üksinda, kas fail tõestab täpselt käsikirjas sõnastatud väite. Just tekstilise ja formaalse tõestuse vastavuses on sõltumatu analüüs leidnud konkreetseid lünki.

Mida OpenAI tegelikult avaldas

Kogu koosneb käsikirjadest ja neid toetavatest tõestusmaterjalidest, mille tootis OpenAI seni avaldamata sisemudel. Tulemuste perekond võib sisaldada põhitulemust, sellega seotud argumente, järeldusi või alternatiivseid tõestusi. Seetõttu ei võrdu käsikirjade hulk sama arvu üksteisest sõltumatute lahendatud probleemidega: ühe töö järeldus võib toetuda teises esitatud konstruktsioonile.

Tagasivõtmiste põhjus näitab sellise sõltuvuse kaalu. Ühes käsikirjas olnud märgiviga muutis kehtetuks selle argumendi ning konstruktsiooni, mida kasutasid kaks seotud tööd. Ühe vea parandamine ei oleks seega tähendanud ainult ühe tekstirea muutmist, vaid oleks nõudnud ka sõltuvate väidete uuesti põhjendamist. OpenAI on avaldanud paranduste ja versioonide jälgimise korra, nii et muudetud töid saab eristada varem avaldatud kujudest.

Käsikirja avaldamine annab erialale võimaluse väidet hinnata, kuid ei võrdu eelretsenseeritud tulemusega. Matemaatik peab muu hulgas kontrollima eeldusi, tõestuse vahepealseid samme ja seost varasema kirjandusega. Kui väide osutub õigeks, vajab eraldi hindamist ka see, mida see seniste tulemuste kõrval juurde annab. Need küsimused jäävad oluliseks ka siis, kui töö juurde on lisatud formaalne fail.

Kolm eri taset tõestuse kontrollimisel

Leani kontroll puudutab täpselt seda väidet ja argumenti, mis on formaliseeritud. Käsikiri esitab lugejale matemaatilise tulemuse ning loomulikus keeles kirjutatud põhjenduse. Leani fail väljendab väite formaalses keeles ja laseb süsteemil kontrollida, kas esitatud sammud järgivad selle reegleid. Sõltumatu eksperdihinnang peab lisaks tuvastama, kas formaalsed definitsioonid ja eeldused vastavad käsikirja omadele.

See eristus ei vähenda formaalse tõestuse väärtust. Masinkontroll võib avastada lubamatu järeldussammu ja annab tugeva kinnituse failis täpselt sõnastatud tulemusele. Kontroll ei loe aga käsikirja samamoodi nagu matemaatik: ta ei otsusta automaatselt, kas tekstis lubatud tugevam väide on failis tõestatud või kas seal kasutatud põhjendus on Leani omaga sisuliselt sama.

Võimalik on ka olukord, kus tekstiline argument sisaldab viga, ent formaliseerimise käigus leitakse samale väitele uus korrektne tõestus. Siis võib Leani fail olla veatu, ilma et see parandaks lugejale avaldatud argumenti. Vastupidisel juhul võib tekstis esitatud mõte olla põhjendatav, kuid sellele lähim formaliseering kasutada tugevamaid eeldusi. Kummalgi juhul tuleb väidete ja tõestuste vastavus eraldi kindlaks teha.

Kaks lahknevust Navier–Stokesi töös

A. Bastounise, F. Circelli ja A. C. Hanseni Navier–Stokesi tõestuse analüüs võrdleb ühes hinnangus käsikirja nelja täiendava sisendtuletise eeldust Leani viie tuletise nõudega ning leiab teises hinnangus muutunud piiri ja tõestuskäigu; autorid piiritlevad oma järelduse sõnadega „We do not make claims about the correctness of OpenAI’s NL proof”. Analüüs käsitleb OpenAI varem avaldatud Navier–Stokesi tööd, mitte kogu oktoobris avaldatud käsikirjade hulka. See annab siiski konkreetse näite probleemist, mis tekib siis, kui formaalset faili esitletakse tekstilise tõestuse kinnitusena.

Esimeses näites hinnatakse, kui palju sisendfunktsiooni tuletisi on vaja soovitud väljundi kontrollimiseks. Leani väide nõuab üht täiendavat tuletist rohkem kui tekstis esitatud hinnang. See pole pelgalt erinev tähistus: lisatingimus kitsendab olukordi, mille kohta tõestatud piir kehtib. Seega võib fail korrektselt tõestada nõrgema tulemuse, jättes käsikirja tugevama sõnastuse endiselt eraldi põhjendamist vajavaks.

Teine näide puudutab rõhuvoo hinnangut, mida kasutatakse Navier–Stokesi argumendi ühes vaheetapis. Tekstiline piir sõltub ühest nimetatud suurusest, sellele lähim Leani hinnang toob sisse täiendava suuruse. Ka meetod muutub: tekst toetub Riesz’i teisenduse ühele hinnangule, formaalne argument kasutab teist normi ja Sobolevi teoreemi. Täiendavat suurust ei saa lihtsalt avaldisest kustutada, et saada tagasi käsikirjas väidetud kuju.

Need tähelepanekud ei otsusta iseenesest, kas OpenAI tekstiline Navier–Stokesi tõestus on õige või vale. Need näitavad täpsemat ja vahetumat probleemi: avaldatud tekst ja sellele viidatud formaalne kontroll ei tõenda neis kohtades ühesugust väidet ühesuguse argumendiga. Kui neid käsitletakse ühe ja sama tõestuse kahe esitusena, jääb lugejale eksitav mulje kontrolli ulatusest.

Miks tulemuste esitust kritiseeritakse

Matemaatikute jaoks sõltub tulemuse usaldusväärsus sellest, kas väite autor suudab selle sisu, eeldusi ja sõltuvusi selgitada ning küsimustele vastata. Mahukas avaldamine teeb selle töö nähtavaks paljudele uurijatele korraga, kuid nihutab suure osa sisulisest kontrollist nende õlule. Formaalse faili olemasolu aitab ainult seal, kus selle seos käsikirjaga on samuti läbi töötatud.

OpenAI paranduste jälg ja tagasivõtmised teevad üksikute tööde staatuse selgemaks, kuid muudavad ka sõltuvuste jälgimise hädavajalikuks. Kui ühe käsikirja argument muutub, võib üle vaadata tulla töö, mis seda kasutab, isegi kui viimase enda arvutused pole muutunud. Järgnev sõltumatu kontroll määrab seetõttu, milliseid avaldatud väiteid saab kasutada uute tulemuste kindla lähtekohana.

Loe ka:

Jaga: