OpenAI publiskojis plašu matemātikas pētījumu kopumu, ko izstrādājis uzņēmuma iekšējais frontier modelis. Kolekcija matemātiķiem piedāvā piekļuvi simtiem mašīnas ģenerētu rezultātu un ir pieejama publiskā GitHub repozitorijā.

Simtiem manuskriptu dažādās matemātikas jomās

Repozitorijā apkopoti 722 manuskripti, kas sakārtoti 372 pētniecības grupās. Tie aptver tīro matemātiku, teorētisko datorzinātni un matemātisko fiziku, tostarp uzdevumus skaitļu teorijā, sarežģītības teorijā, ģeometrijā un matemātiskajā fizikā.

Vairāki rezultāti skar problēmas, kuru risināšanai nepieciešamas garas un sarežģītas matemātiskās spriešanas ķēdes. Daļa manuskriptu attiecas arī uz jomām, kur pat nelieli sasniegumi var prasīt ievērojamu tehnisku darbu.

Viens piemērs ir π iracionalitātes eksponents. Šis lielums raksturo, cik precīzi racionāli skaitļi var tuvināt skaitli π. Modeļa izstrādātais rezultāts aplūko šādu tuvinājumu matemātisko uzvedību.

Citā pētniecības grupā analizēta NP-sarežģītība. Šie uzdevumi pieder skaitļošanas sarežģītības teorijai un attiecas uz problēmām, kuras tiek uzskatītas par grūti efektīvi atrisināmām. Modeļa darbs papildina plašāku pētījumu kopumu par šādiem jautājumiem.

Pārējie manuskripti skar Mahlēra hipotēzes, aritmētiskās progresijas un brīvo grupu faktorus. Kolekcijā iekļauti arī pētījumi par kvantu Heizenberga feromagnētiem un relativistiskajiem Vlasova–Maksvela vienādojumiem.

Lean nodrošina formālu pierādījumu pārbaudi

OpenAI daudziem pierādījumiem publicējis arī formalizētas versijas Lean programmēšanas valodā. Tā ļauj pētniekiem matemātiskus apgalvojumus un pierādījumus pārvērst formālā kodā.

Pēc tam dators var pārbaudīt, vai katrs loģiskais solis izriet no norādītajiem pieņēmumiem. Tomēr šāda pārbaude pati par sevi automātiski neapstiprina, ka katrs kolekcijā iekļautais pētniecības apgalvojums ir pareizs.

Daudziem manuskriptiem Lean versijas vēl nav izveidotas. OpenAI norāda, ka formalizējumu skaits tiks palielināts, pētniekiem pabeidzot verifikācijas darbu.

Saistītos manuskriptus uzņēmums apvienojis pētniecības grupās, lai parādītu, kā atsevišķie rezultāti ir savstarpēji saistīti. Repozitorijā identificētas arī 10 grupas, kurām pievienoti saīsināti modeļa spriešanas kopsavilkumi. Šie kopsavilkumi ir nodalīti no Lean formalizētajiem pierādījumiem.

Repozitorijs fiksē arī manuskriptu izmaiņas

Repozitorijs seko līdzi publikāciju versiju izmaiņām un piedāvā norādes citēšanai. Tas pētniekiem nodrošina skaidrāku ierakstu gadījumiem, kad autori iepriekšēju manuskriptu labo vai papildina.

Izlaišanas procesu OpenAI veidojis, konsultējoties ar neatkarīgo Matemātikas un mākslīgā intelekta konsultatīvo grupu Institute for Advanced Study. Uzņēmums norāda, ka šīs grupas ieteikumi izmantoti kolekcijas sagatavošanā un publiskošanā.

OpenAI atklājis arī matemātiskās izvērtēšanas mērogu. Pētījumu procesā modelis mēģinājis atrisināt aptuveni 4000 uzdevumu. Pieņemts rezultāts vidēji prasījis apmēram trīs stundas ekvivalenta ChatGPT Pro spriešanas skaitļošanas resursu. Uzņēmums publicējis arī papildu statistiku par mēģinātajiem uzdevumiem un iegūtajiem pētījumu rezultātiem.

OpenAI plāno turpināt rezultātu izvērtēšanu

Uzņēmums norāda, ka spriešanas kopsavilkumi pētniekiem ļauj tuvāk aplūkot, kā modelis piegājis atsevišķiem matemātiskiem jautājumiem. Vienlaikus tie neaizstāj formālos Lean pierādījumus.

OpenAI plāno atbalstīt darbnīcas, konferences un īpašas programmas, kas būs veltītas nozīmīgu ar mākslīgo intelektu ģenerētu matemātikas rezultātu izpratnei. Uzņēmums arī sagaida, ka matemātiķu atsauksmes ietekmēs turpmāko publiskojamo materiālu saturu.

Tādējādi izlaidums nav tikai zinātnisku manuskriptu krājums. Tas vienlaikus demonstrē, kā mašīnu ģenerēta matemātika var tikt iekļauta pētniecības procesā, izmantojot reproducējamus ierakstus, datorā pārbaudāmus pierādījumus un plašāku ieskatu tajā, kā modeļi nonāk pie saviem rezultātiem.