En OpenAI-model har modbevist en central formodning i diskret geometri
I næsten 80 år har matematikere studeret et bedragerisk simpelt spørgsmål: Hvis man placerer punkter i planen, hvor mange par af punkter kan så have præcis afstanden mellem sig?
Dette er problemet med enhedsafstanden i det plane rum, som Paul Erdős først stillede i 1946. Det er et af de mest kendte spørgsmål inden for kombinatorisk geometri, let at formulere og utroligt svært at løse. I bogen fra 2005 Research Problems in Discrete Geometry af Brass, Moser og Pach kaldes det "muligvis det bedst kendte (og nemmest at forklare) problem inden for kombinatorisk geometri". Noga Alon, en fremtrædende kombinatoriker ved Princeton, beskriver det som "et af Erdős’ yndlingsproblemer." Erdős udlovede endda en pengepræmie for at løse dette problem.
I dag kan vi fortælle om et gennembrud i enhedsafstandsproblemet. Siden Erdős’ oprindelige arbejde har den fremherskende opfattelse været, at de „kvadratiske gitter“-konstruktioner, der er vist længere nede, i det væsentlige var optimale til at maksimere antallet af par med enhedsafstand. En intern OpenAI-model har modbevist denne langvarige formodning ved at give en uendelig familie af eksempler, som giver en polynomiel forbedring. Beviset er blevet gennemgået af en gruppe eksterne matematikere. De har også skrevet en ledsagende artikel, der forklarer argumentet og giver yderligere baggrund og kontekst for resultatets betydning.
Resultatet er også bemærkelsesværdigt på grund af måden, det blev fundet på. Beviset kom fra en ny generel ræsonneringsmodel, snarere end fra et system trænet specifikt til matematik, understøttet til at søge gennem bevisstrategier eller målrettet enhedsafstandsproblemet i særdeleshed. Som led i en bredere indsats for at teste, om avancerede modeller kan bidrage til banebrydende forskning, evaluerede vi den på en samling af Erdős-problemer. I dette tilfælde frembragte den et bevis, der løste det åbne problem.
Dette bevis er en vigtig milepæl for matematik- og AI-fællesskaberne. Det markerer første gang, at et fremtrædende åbent problem, centralt for et delområde af matematikken, er blevet løst autonomt af AI. Det demonstrerer også dybden af den ræsonnering, som disse systemer nu understøtter. Matematik giver et særligt klart testmiljø for ræsonnering: Problemerne er præcise, potentielle beviser kan kontrolleres, og et langt argument virker kun, hvis ræsonneringen hænger sammen fra begyndelse til slutning. Metoden, hvormed problemet blev løst, er også bemærkelsesværdig. Beviset bringer uventede, sofistikerede idéer fra algebraisk talteori i spil på et elementært geometrisk spørgsmål.
Fields-medaljevinderen Tim Gowers kalder i den ledsagende artikel resultatet „en milepæl i AI-matematik“. Ifølge den førende talteoretiker Arul Shankar „viser denne artikel efter min mening, at nutidens AI-modeller går videre end blot at være hjælpere for menneskelige matematikere – de er i stand til at få originale geniale idéer og derefter føre dem ud i livet“.
Beviset er tilgængeligt her(åbner i et nyt vindue). Den ledsagende artikel af førende eksterne matematikere er tilgængelig her(åbner i et nyt vindue). Du kan finde en forkortet version af modellens tankerække her(åbner i et nyt vindue).
Tidligere kendt konstruktion af mange enhedsafstande fra et reskaleret kvadratisk gitter.
Lad være det størst mulige antal par med enhedsafstand blandt punkter i planen. Eksempler, der opnår lineær vækstrate, er lette at konstruere: Hvis man placerer punkter på en linje, får man par, mens et kvadratisk gitter giver omkring par. Den hidtil bedst kendte konstruktion, der bygger på et skaleret kvadratisk gitter, viser sig at give endnu mere: for en konstant . Da går mod uendelig med , går det ekstra led i eksponenten mod , hvilket betyder, at disse konstruktioner kun opnår vækst en smule hurtigere end lineær. I årtier troede man bredt, at denne rate i det væsentlige var den bedst mulige, og at ingen konstruktion kunne forbedre det kvadratiske gitter væsentligt. Teknisk set formodede Erdős en øvre grænse på , hvor det ekstra angiver et led, der går mod med .
Vores nye resultat modbeviser denne formodning. Mere præcist konstruerer beviset for uendeligt mange værdier af konfigurationer af punkter med mindst par med enhedsafstand for en fast eksponent . (Det oprindelige AI-bevis giver ikke en eksplicit , men en kommende forfinelse af Princetons matematikprofessor Will Sawin har vist, at man kan tage .)
Problemets historie hjælper med at forstå, hvorfor resultatet er overraskende. Den bedst kendte nedre grænse havde været stort set uændret siden Erdős’ oprindelige konstruktion fra 1946. Den bedst kendte øvre grænse, , stammer fra arbejde af Spencer, Szemerédi og Trotter i 1984, og trods senere forfinelser og relateret strukturelt arbejde af Székely, Katz og Silier, Pach, Raz og Solymosi samt andre, er den øvre grænse forblevet stort set uændret. Som evidens til fordel for formodningen studerede Matoušek og Alon-Bucić-Sauermann problemet med ikke-euklidiske afstande i planen og beviste, at "de fleste" af disse ikke-euklidiske afstande i en vis forstand følger formodningen.
Overraskende nok kommer konstruktionens nøgleingredienser fra en helt anden del af matematikken, kendt som algebraisk talteori, som studerer begreber som faktorisering i udvidelser af heltallene, kendt som algebraiske tallegemer.
Efter at have verificeret det indledende bevis undersøgte vi vores modellers succesrate på dette problem med varierende mængder testtidsberegning. Resultaterne vises her.
På et højt niveau begynder beviset med en velkendt geometrisk idé og skubber den i en uventet retning.
Erdős’ oprindelige nedre grænse kan forstås gennem de gaussiske heltal: tal på formen , hvor og er heltal, og er kvadratroden af . De gaussiske heltal udvider de almindelige heltal og har ligesom dem egenskaber som entydig primfaktorisering. Sådanne udvidelser af de almindelige heltal eller rationale tal kaldes algebraiske tallegemer. Det nye argument erstatter de gaussiske heltal med mere komplicerede generaliseringer fra algebraisk talteori med rigere symmetrier, som kan skabe mange flere forskelle af enhedslængde.
Det præcise argument bruger værktøjer som uendelige klasselegemetårne og Golod–Shafarevich-teori til at vise, at de tallegemer, argumentet kræver, faktisk eksisterer. Disse idéer var velkendte blandt algebraiske talteoretikere, men det kom som en stor overraskelse, at disse begreber har implikationer for geometriske spørgsmål i det euklidiske plan.
Dette resultat markerer et vigtigt øjeblik i samspillet mellem AI og matematik: Et AI-system har autonomt løst et langvarigt åbent problem i centrum af et aktivt felt. Det giver også et tidligt glimt af en ny form for samarbejde mellem AI og menneskelige matematikere. I dette tilfælde tegner det ledsagende arbejde af eksterne matematikere et væsentligt rigere billede end den oprindelige løsning alene.
Som Thomas Bloom skriver i den ledsagende note:
„Når jeg vurderer vigtigheden og indflydelsen af et AI-genereret bevis, er et spørgsmål, jeg stiller mig selv: Har dette lært os noget nyt om problemet? Forstår vi diskret geometri bedre nu? Jeg mener, at svaret er et modereret ja: Dette viser, at talteoretiske konstruktioner har meget mere at sige om den slags spørgsmål, end vi havde mistanke om; desuden kan den nødvendige talteori være meget dyb. Der er ingen tvivl om, at mange algebraiske talteoretikere i de kommende måneder vil se nøje på andre åbne problemer i diskret geometri.“
Den uventede forbindelse mellem algebraisk talteori og diskret geometri, som løsningen afslører, er en del af det, der gør resultatet bemærkelsesværdigt. Det afgør ikke blot en specifik formodning, men kan give matematikere en bro til at begynde at udforske yderligere relaterede problemer.
Bloom peger også på en bredere mulighed:
„Grænserne for viden er meget ujævne, og de kommende måneder og år vil uden tvivl byde på lignende succeser i mange andre områder af matematikken, hvor langvarige åbne problemer løses af en AI, der afslører uventede forbindelser og presser det eksisterende tekniske apparat til dets grænse. AI hjælper os med mere fuldt ud at udforske matematikkens katedral, som vi har bygget gennem århundreder; hvilke andre usete vidundere venter i kulissen?“
Dette resultat giver et lovende eksempel: AI bidrager ikke kun med en løsning, men med en matematisk opdagelse, hvis betydning bliver klarere og rigere gennem efterfølgende menneskelig forståelse.
Læringen er større end dette særlige resultat. Bedre matematisk ræsonnering kan gøre AI til en stærkere forskningspartner: noget, der kan holde sammen på vanskelige tankespor, forbinde idéer på tværs af fjerne vidensområder, fremhæve lovende spor, som eksperter måske ikke har prioriteret, og hjælpe forskere med at gøre fremskridt på problemer, der ellers ville være for komplekse eller tidskrævende at tage fat på.
Disse evner betyder noget ud over matematikken. Hvis en model kan holde et kompliceret argument sammenhængende, forbinde idéer på tværs af fjerne vidensområder og producere arbejde, der holder til ekspertgranskning, så er det også nyttige evner inden for biologi, fysik, materialeforskning, ingeniørvidenskab og medicin, og de er en del af vores langsigtede vej mod mere automatiseret forskning: systemer, der kan hjælpe forskere og ingeniører med at udforske flere idéer og forfølge sværere tekniske spørgsmål.
AI er ved at begynde at spille en meget seriøs rolle i de kreative dele af forskning, og vigtigst af alt i AI-forskningen selv. Selv om denne fremgang ikke er uventet, understreger den den hast, vi føler omkring at forstå denne næste fase af AI-udviklingen, udfordringerne ved at tilpasse meget intelligente systemer og fremtiden for samarbejde mellem mennesker og AI.
Den fremtid afhænger stadig af menneskelig dømmekraft. Ekspertise bliver mere værdifuld, ikke mindre. AI kan hjælpe med at søge, foreslå og verificere. Mennesker vælger de problemer, der betyder noget, fortolker resultaterne og beslutter, hvilke spørgsmål der skal forfølges derefter.


