OpenAI objavil 722 matematičnih rokopisov, ki jih je ustvaril interni model

OpenAI je 6. oktobra objavil zbirko matematičnih rezultatov, ki jih je ustvaril še neobjavljen interni model umetne inteligence. Javni repozitorij vsebuje 722 rokopisov, razvrščenih v 372 skupin sorodnih rezultatov. Pri delu dokazov je priložen tudi zapis v jeziku Lean, ki omogoča računalniško preverjanje.[2][3]

Obseg je velik, vendar številka 722 ne pomeni 722 neodvisno potrjenih rešitev odprtih problemov. Skupine lahko združujejo glavni rezultat, spremljajoče argumente, posledice ali alternativne dokaze. OpenAI opozarja, da so rezultati na različnih stopnjah preverjanja in da lahko nekateri brez formalnega zapisa vsebujejo napake.[3]

Kaj je v zbirki

Med objavljenimi trditvami so negativna rešitev Hilbertovega desetega problema nad racionalnimi števili, dokaz iracionalnosti Catalanove konstante in rezultat, ki ga katalog označuje kot rešitev kvazi-Riemannove hipoteze.[5]

Prvi problem sprašuje, ali bi lahko obstajal splošen algoritem, ki za polinomsko enačbo s celoštevilskimi koeficienti odloči, ali ima racionalno rešitev. Objavljeni rokopis trdi, da tak algoritem ne obstaja. Pri Catalanovi konstanti gre za vprašanje, ali lahko določeno matematično konstanto zapišemo kot razmerje dveh celih števil; katalog navaja dokaz, da tega ne moremo.[5]

Rezultata o kvazi-Riemannovi hipotezi ne smemo zamenjati z dokazom Riemannove hipoteze. Katalog opisuje območje brez ničel za določene matematične funkcije, med njimi Riemannovo funkcijo zeta: realni del argumenta je večji od 7/8. To je drugačna trditev od znamenite Riemannove hipoteze.[5]

To so opisi rezultatov, ki jih je objavil OpenAI, ne naša neodvisna potrditev pravilnosti njihovih dokazov.

Kako preveriti dokaz, ki ga napiše AI

Pri matematiki prepričljivo besedilo ne zadostuje. Napačen korak lahko razveljavi dolg argument, četudi je preostanek videti smiseln.

OpenAI zato ob delu rokopisov objavlja formalizacije v Leanu. V takem zapisu so matematične trditve in koraki dokaza izraženi dovolj natančno, da jih lahko preveri računalnik. Repozitorij vsebuje knjižnico formalnih dokazov in navodila za dodatno preverjanje z orodjem Comparator.[2][4][6]

Formalno preverjanje zmanjša odvisnost od presoje, ali besedilo zveni pravilno. Še vedno pa je treba pregledati, kaj natanko je bilo formalizirano, katere predpostavke uporablja dokaz in ali formalna trditev ustreza tisti v rokopisu. Sam obstoj datotek Lean zato ni razlog, da celotno zbirko razglasimo za potrjeno.

Koliko dela je opravil model

Po podatkih OpenAI je model med vrednotenjem dobil približno 4.000 problemov. Večina rezultatov je nastala po enakem postopku; povprečna poraba računske moči za posamezen rezultat naj bi ustrezala približno trem uram razmišljanja v ChatGPT Pro z internim modelom. To je primerjava računske porabe, ne podatek o času človeškega raziskovalca ali obljuba za trenutno javno različico ChatGPT.[3]

Podjetje je objavilo tudi deset skrajšanih povzetkov modelovega razmišljanja. Ti omogočajo vpogled v izbrane primere, vendar niso popoln zapis vseh poskusov. Model, ki je ustvaril rezultate, ob tej objavi še ni javno dostopen; OpenAI navaja, da pripravlja njegovo odgovorno izdajo.[2][3]

Za matematično skupnost je zbirka predvsem veliko novega materiala za pregled. Repozitorij predvideva popravke in nove različice, pri čemer naj bi stare ostale dostopne.[3] Za oceno dosežka bo pomembno, kateri dokazi prestanejo preverjanje, kako se navezujejo na obstoječo literaturo in katere rezultate lahko raziskovalci uporabijo pri nadaljnjem delu.