Najväčšie matematické vydanie OpenAI rieši 4 000 problémov s Lean-overenými dôkazmi

OpenAI vydalo rozsiahlu zbierku matematického výskumu, ktorý bol vytvorený interným modelom, a tým poskytlo matematikom prístup k stovkám výsledkov generovaných strojom.

Zbierka je dostupná v verejnom repozitári na GitHub-e a obsahuje 722 rukopisov usporiadaných do 372 výskumných rodín. Tieto práce pokrývajú oblasti čistej matematiky, teoretickej informatiky a matematickej fyziky.

Niektoré výsledky sa zaoberajú problémami, ktoré si vyžadujú dlhé reťazce matematického uvažovania. OpenAI tiež zverejnilo formalizované verzie mnohých dôkazov v jazyku Lean, čo umožňuje počítačom overiť základné argumenty.

Stovky výsledkov

Repozitár pokrýva problémy týkajúce sa teórie čísel, teórie zložitosti, geometrie a matematickej fyziky. Niektoré výsledky sa rozširujú aj do oblastí, kde malé pokroky môžu vyžadovať značné technické úsilie.

„Vydávame širokú škálu nových matematických výsledkov vyprodukovaných interným modelom. Konzultovali sme s nezávislou poradnou skupinou pre matematiku a umelú inteligenciu na Inštitúte pokročilých štúdií a čerpali sme z ich rady a…“

Jedným z príkladov je exponent iracionality čísla pí. Tento údaj meria, ako blízko môžu racionálne čísla aproximovať číslo pí. Model vyprodukoval výsledok, ktorý sa zaoberá matematickým správaním tejto aproximácie.

Ďalšia výskumná rodina skúma NP-ťažkosť. Tieto problémy sa nachádzajú v rámci teórie výpočtovej zložitosti a týkajú sa úloh, ktoré sú považované za ťažké na efektívne riešenie. Práca modelu pridáva matematické výsledky do tejto širšej oblasti výskumu.

Iné rukopisy sa zaoberajú otázkami týkajúcimi sa Mahlerových konjektúr, aritmetických postupností a faktorov voľných skupín. Zbierka tiež obsahuje práce o kvantových Heisenbergových feromagnetoch a relativistických Vlasov-Maxwellových rovniciach.

OpenAI zoskupil súvisiace rukopisy do výskumných rodín, aby ukázal, ako jednotlivé výsledky súvisia. Repozitár tiež identifikuje 10 rodín s skrátenými súhrnmi uvažovania modelu.

Lean pridáva overenie

Lean poskytuje dôležitú overovaciu vrstvu pre toto vydanie. Programovací jazyk umožňuje výskumníkom prekladať matematické tvrdenia a dôkazy do formálneho kódu.

Počítač potom môže skontrolovať, či každý logický krok vyplýva z uvedených predpokladov. To však automaticky nezakladá, že každý výskumný nárok v zbierke je správny.

Mnohé rukopisy stále nemajú formálne verzie v Leane. OpenAI uvádza, že pridá ďalšie formalizácie, keď výskumníci dokončia overovaciu prácu.

Repozitár tiež sleduje revízie článkov a poskytuje usmernenia pre citácie. To poskytuje výskumníkom jasnejší záznam, keď autori opravujú alebo rozširujú predchádzajúci rukopis. OpenAI vyvinulo proces vydania s radami od nezávislej poradnej skupiny pre matematiku a umelú inteligenciu na Inštitúte pokročilých štúdií.

Model testoval tisíce problémov

OpenAI tiež zverejnilo podrobnosti o rozsahu svojej matematickej evaluácie. Model sa pokúsil o približne 4 000 problémov.