OpenAI-líkan hefur afsannað lykiltilgátu í strjálli rúmfræði

Í nærri 80 ár hafa stærðfræðingar rannsakað spurningu sem virðist einföld við fyrstu sýn: ef þú setur $n$ punkta í planið, hversu mörg pör punkta geta verið nákvæmlega 1 einingu í fjarlægð hvor frá öðru?

Þetta er einingarfjarlægðarvandamálið á planinu, sem Paul Erdős setti fyrst fram árið 1946. Þetta er ein af þekktustu spurningunum í flétturúmfræði, auðvelt að setja hana fram en ótrúlega erfitt að leysa. Bókin Research Problems in Discrete Geometry frá árinu 2005, eftir Brass, Moser og Pach, lýsir því sem „hugsanlega þekktasta (og einfaldasta að útskýra) vandamálið í flétturúmfræði“. Noga Alon, leiðandi fléttufræðingur við Princeton, lýsir því sem „einu af uppáhaldsvandamálum Erdős“. Erdős bauð jafnvel peningaverðlaun fyrir lausn á þessu vandamáli.

Í dag kynnum við tímamótaniðurstöðu varðandi einingarfjarlægðarvandamálið. Allt frá upphaflegu verki Erdős, hefur sú skoðun verið ríkjandi að „ferningsnetsmíðar“ sem sýndar eru hér neðar væru í meginatriðum bestar til að hámarka fjölda para í einingarfjarlægð. Innra OpenAI-líkan hefur hrakið þessa langvarandi tilgátu með því að leggja fram óendanlega fjölskyldu dæma sem skila margliðubótum. Sönnunin hefur verið yfirfarin af hópi utanaðkomandi stærðfræðinga. Þeir hafa einnig skrifað fylgiskýrslu sem útskýrir röksemdafærsluna og veitir frekari bakgrunn og samhengi fyrir mikilvægi niðurstöðunnar.

Niðurstaðan er einnig athyglisverð vegna þess hvernig hún fékkst. Sönnunin kom frá nýju almennu rakalíkani, en ekki frá kerfi sem var þjálfað sérstaklega fyrir stærðfræði, hannað til að leita í gegnum sönnunaraðferðir eða miðað sérstaklega að einingarfjarlægðarvandamálinu. Sem hluta af víðtækari viðleitni til að prófa hvort háþróuð líkön geti lagt sitt af mörkum til framarlega rannsókna, metum við það á safni Erdős-vandamála. Í þessu tilviki skilaði það af sér sönnun sem leysti hið opna vandamál.

Þessi sönnun er mikilvægur áfangi fyrir stærðfræði- og gervigreindarsamfélögin. Þetta markar fyrsta skipti sem þekkt óleyst vandamál, sem er miðlægt í undirgrein stærðfræðinnar, hefur verið leyst sjálfstætt af gervigreind. Það sýnir einnig dýpt raka sem þessi kerfi styðja nú. Stærðfræði býður upp á sérlega skýran prófunarvettvang fyrir rök: vandamálin eru nákvæm, hægt er að sannreyna hugsanlegar sannanir og löng röksemdafærsla gengur aðeins upp ef rökin haldast frá upphafi til enda. Aðferðin sem notuð var til að leysa vandamálið er einnig athyglisverð. Sönnunin nýtir óvæntar og háþróaðar hugmyndir úr algebrulegri talnafræði til að takast á við grunnlæga rúmfræðilega spurningu.

Fields-verðlaunahafinn Tim Gowers, sem skrifar í fylgigreininni, kallar niðurstöðuna „tímamót í stærðfræði gervigreindar“. Samkvæmt leiðandi talnafræðingnum Arul Shankar: „Að mínu mati sýnir þessi grein að núverandi gervigreindarlíkön eru meira en aðeins hjálpartæki fyrir mannlega stærðfræðinga – þau geta sett fram frumlegar og snjallar hugmyndir og síðan leitt þær til lykta“.

Sönnunin er aðgengileg hér⁠(opnast í nýjum glugga). Fylgigreinin eftir fremstu utanaðkomandi stærðfræðinga er aðgengileg hér⁠(opnast í nýjum glugga). Stytt útgáfa af hugsanaþræði líkansins er að finna hér⁠(opnast í nýjum glugga).

Látum $u(n)$ tákna mesta mögulega fjölda para punkta í einingarfjarlægð meðal $n$ punkta á planinu. Auðvelt er að smíða dæmi sem ná línulegum vaxtarhraða: ef $n$ punktar eru settir á línu fást $n-1$ pör, en ferningslaga net gefur um $2n$ pör. Sú áður best þekkta smíði, sem er fengin úr endurkvörðuðu ferninganeti, reynist gefa enn meira: $n^{1 + C / \log \log(n)}$ fyrir einhvern fasta $C$. Þar sem $\log \log(n)$ stefnir á óendanlegt þegar $n$ stefnir á óendanlegt, stefnir viðbótarliðurinn í veldisvísinum á $0$, sem þýðir að þessar smíðar ná vexti sem er aðeins örlítið hraðari en línulegur. Um áratugaskeið var almennt talið að þetta hlutfall væri í raun það besta sem hægt væri að ná og að engin gerð gæti skilað verulega betri árangri en ferningsnetið. Í tæknilegum skilningi setti Erdős fram þá tilgátu að efra mark væri $n^{1+o(1)}$, þar sem viðbótarliðurinn $o(1)$ táknar lið sem stefnir á $0$ þegar $n$ stefnir á óendanlegt.

Nýja niðurstaða okkar afsannar þessa tilgátu. Nánar tiltekið smíðar sönnunin fyrir óendanlega mörg gildi $n$ skipanir $n$ punkta með að minnsta kosti $n^{1+\delta}$ pörum í einingarfjarlægð, fyrir einhvern fastan veldisvísi $\delta > 0$. (Upprunalega gervigreindarsönnunin gefur ekki upp skýrt gildi fyrir $\delta$, en væntanleg endurbót eftir Will Sawin, stærðfræðiprófessor við Princeton-háskóla, hefur sýnt að velja má $\delta=0{,}014$.)

Saga vandamálsins hjálpar til við að skýra hvers vegna niðurstaðan kemur á óvart. Best þekkta neðra markið hafði í meginatriðum haldist óbreytt frá upphafri smíði Erdősar árið 1946. Bestu efri mörkin, $O(n^{4/3})$, eiga rætur að rekja til rannsókna Spencer, Szemerédi og Trotter árið 1984, og þrátt fyrir síðari betrumbætur og tengdar formgerðarlegar rannsóknir Székely, Katz og Silier, Pach, Raz og Solymosi og annarra hafa efri mörkin í meginatriðum haldist óbreytt. Sem vísbendingu til stuðnings tilgátunni rannsökuðu Matoušek og Alon-Bucić-Sauermann vandamálið fyrir óevklíðskar fjarlægðir í sléttunni og sönnuðu að „flestar“ þessara óevklíðsku fjarlægða uppfylla tilgátuna í einhverjum skilningi.

Það kemur á óvart að lykilþættir smíðinnar koma úr allt öðrum hluta stærðfræðinnar, sem kallast algebruleg talnafræði og rannsakar hugtök á borð við þáttun í útvíkkunum á heiltölunum, sem kallast algebruleg talnasvið.

Í megindráttum hefst sönnunin á kunnuglegri rúmfræðilegri hugmynd og þróar hana í óvænta átt.

Neðra markið sem Erdős setti upphaflega fram má skilja út frá Gauss-heiltölunum: tölum á forminu $a+bi$, þar sem $a$ og $b$ eru heiltölur og $i$ er kvaðratrótin af $-1$. Gauss-heiltölurnar útvíkka venjulegu heiltölurnar og hafa, líkt og þær, eiginleika á borð við einkvæma þáttun í frumþætti. Slíkar útvíkkanir á venjulegu heiltölunum eða ræðu tölunum eru þekktar sem algebruleg talnasvið. Í nýju röksemdafærslunni er Gauss-heiltölunum skipt út fyrir flóknari alhæfingar úr algebrulegri talnafræði, sem hafa ríkari samhverfur og geta skapað mun fleiri mismun með einingarlengd.

Nákvæma röksemdafærslan notar verkfæri á borð við óendanlega klasasviðsturna og Golod–Shafarevich kenningu til að sýna að talnasvið sem röksemdafærslan krefst séu í raun til. Þessar hugmyndir voru vel þekktar meðal fræðimanna í algebrulegri talnafræði, en það kom mjög á óvart að þessi hugtök hefðu þýðingu fyrir rúmfræðilegar spurningar í Evklíðska-planinu.

Þessi niðurstaða markar mikilvæg tímamót í samspili gervigreindar og stærðfræði: gervigreindarkerfi hefur sjálfstætt leyst opið vandamál sem hafði lengi staðið óleyst og er í miðpunkti virks rannsóknarsviðs. Það veitir einnig fyrstu innsýn í nýja tegund samstarfs milli gervigreindar og mannlegra stærðfræðinga. Í þessu tilviki dregur tengda verkið sem utanaðkomandi stærðfræðingar unnu upp mun ríkari mynd en upphaflega lausnin ein og sér.

Eins og Thomas Bloom skrifar í meðfylgjandi athugasemd:

„Þegar ég met mikilvægi og áhrif sönnunar sem gervigreind hefur búið til, spyr ég sjálfan mig: hefur hún kennt okkur eitthvað nýtt um vandamálið? Skiljum við strjála rúmfræði betur núna? Ég held að svarið sé já, en með fyrirvara: þetta sýnir að talnafræðilegar smíðir hafa miklu meira að segja um spurningar af þessu tagi en okkur grunaði; enn fremur að sú talnafræði sem til þarf getur verið mjög djúp. Án efa munu margir algebrískir talnafræðingar skoða önnur opin vandamál í strjálli rúmfræði gaumgæfilega á næstu mánuðum.“

Hin óvæntu tengsl milli algebraískrar talnafræði og strjálrar rúmfræði, sem lausnin leiddi í ljós, eru hluti af þess sem gerir niðurstöðuna athyglisverða. Þetta útkljáir ekki einfaldlega tiltekna tilgátu, heldur gæti veitt stærðfræðingum brú til að hefja könnun á frekari skyldum viðfangsefnum.

Bloom bendir einnig til víðtækari möguleika:

„Framarlega á þekkingarsviðinu eru mjög áberandi, og enginn vafi leikur á því að á næstu mánuðum og árum munum við sjá sambærilegan árangur á mörgum öðrum sviðum stærðfræðinnar, þar sem langvarandi opin vandamál verða leyst með því að gervigreind afhjúpi óvænt tengsl og þrýsti núverandi tæknilegu verkfærakerfi til hins ýtrasta. Gervigreind hjálpar okkur að kanna til hlítar dómkirkju stærðfræðinnar sem við höfum byggt upp í aldanna rás. Hvaða önnur óséð undur bíða bak við tjöldin?“

Þessi niðurstaða gefur lofandi dæmi: gervigreind leggur ekki aðeins fram lausn, heldur stærðfræðilega uppgötvun sem mikilvægi hennar verður ljósara og margþættara eftir því sem mannlegur skilningur á henni eykst síðar.

Lærdómurinn hefur víðari þýðingu en þessi tiltekna niðurstaða. Betri stærðfræðileg rök geta gert gervigreind að öflugri samstarfsaðila í rannsóknum: einhverju sem getur haldið utan um flókna hugsanaþræði, tengt hugmyndir þvert á fjarlæg þekkingarsvið, dregið fram spennandi leiðir sem sérfræðingar hafa hugsanlega ekki sett í forgang og hjálpað rannsakendum að ná framförum í vandamálum sem annars væru of flókin eða tímafrek til að takast á við.

Þessi hæfni skiptir máli langt út fyrir stærðfræðina. Ef líkan getur haldið flókinni röksemdafærslu samhangandi, tengt hugmyndir á milli fjarlægra þekkingarsviða og skilað vinnu sem stenst rýni sérfræðinga, eru það einnig gagnlegir hæfileikar í líffræði, eðlisfræði, efnisvísindum, verkfræði og læknisfræði, og þeir eru hluti af vegferð okkar til lengri tíma í átt að meira sjálfvirkum rannsóknum: kerfum sem geta hjálpað vísindamönnum og verkfræðingum að kanna fleiri hugmyndir og takast á við erfiðari tæknileg viðfangsefni.

Gervigreind er að taka mjög veigamikinn þátt í skapandi rannsóknum og, það sem mikilvægast er, í rannsóknum á gervigreind sjálfri. Þótt þessi framþróun sé ekki óvænt, undirstrikar hún hversu brýnt okkur finnst að skilja þennan næsta áfanga í þróun gervigreindar, áskoranirnar við að samræma mjög greind kerfi og framtíð samstarfs manna og gervigreindar.

Sú framtíð veltur enn á mannlegri dómgreind. Sérþekking verður verðmætari, ekki minna verðmæt. Gervigreind getur hjálpað til við að leita, koma með tillögur og sannreyna. Fólk velur þau viðfangsefni sem skipta máli, túlkar niðurstöðurnar og ákveður hvaða spurningar á að kanna næst.