Er datamaskiner klare til å løse dette notorisk uhåndterlige matematikkproblemet?

Ms Tech | SuperRembo via codingtrain

Dataforskeren Marijn Heule er alltid på utkikk etter en god matematisk utfordring. Heule, som er førsteamanuensis ved Carnegie Mellon University, har et imponerende rykte for å løse vanskelige matematiske problemer med beregningsverktøy. Resultatet hans fra 2016 med det boolske pythagoras trippelproblem var et enormt bevis som fanget overskrifter: To hundre terabyte mattebevis er det største noensinne . Nå bruker han en automatisert tilnærming for å angripe den forlokkende enkle Collatz-formodningen.

Først foreslått (ifølge noen beretninger) på 1930-tallet av den tyske matematikeren Lothar Collatz, gir dette tallteoriproblemet en oppskrift, eller algoritme, for å generere en numerisk sekvens : Start med et hvilket som helst positivt heltall. Hvis tallet er partall, del på to. Hvis tallet er oddetall, multipliser med tre og legg til én. Og så gjør det samme, igjen og igjen. Formodningen hevder at sekvensen alltid vil ende opp på 1 (og deretter kontinuerlig gå gjennom 4, 2, 1).

Tallet 5, for eksempel, genererer bare seks termer:

5, 16, 8, 4, 2, 1

Tallet 27 går gjennom 111 ledd, svinger opp og ned - når dets høyde når 9 232 - før det til slutt lander på 1.

Tallet 40 genererer en annen kort sekvens:

40, 20, 10, 5, 16, 8, 4, 2, 1

Til dags dato har formodningen blitt sjekket av datamaskinen for alle startverdier opp til nesten 300 milliarder milliarder og hvert tall når til slutt 1.

De fleste forskere tror formodningen er sann. Det har lokket mengder av matematikere og ikke-matematikere, men ingen har fremlagt et bevis. På begynnelsen av 1980-tallet erklærte den ungarske matematikeren Paul Erdős: Matematikk er ennå ikke klar for slike problemer.

Det vi ønsker å vite er om mennesker eller datamaskiner er flinkere til å løse slike problemer.

Marijn Heule

Og han har nok rett, sier Heule. For Heule er Collatz sin lokke ikke så mye utsiktene til et gjennombrudd som det er å fremme automatiserte resonneringsteknikker. Etter å ha puslet med det i fem år, la Heule og hans samarbeidspartnere, Scott Aaronson og Emre Yolcu, nylig ut en papir på arXiv preprint-serveren. Selv om vi ikke lykkes med å bevise Collatz-formodningen, skriver de, mener vi at ideene her representerer en interessant ny tilnærming.

Det er en edel fiasko, sier Aaronson, en dataforsker ved University of Texas i Austin. En fiasko fordi de ikke beviste formodningen. Noble fordi de gjorde fremskritt i en annen forstand: Heule ser på det som et utgangspunkt for å avgjøre om mennesker eller datamaskiner er flinkere til å bevise slike problemer.

Oversette matematikk til beregning

For mange matematiske problemer er datamaskiner håpløse, siden de ikke har tilgang til det enorme oeuvre av matematikk samlet gjennom historien. Men noen ganger utmerker datamaskiner seg der mennesker er håpløse. Fortell en datamaskin hvordan en løsning ser ut – gi den et mål og et veldefinert søkerom – og så kan datamaskinen finne den med brute force. Selv om det er et spørsmål om debatt om beregningsresultater utgjør meningsfulle tillegg til den matematiske kanonen. Det tradisjonelle synet er at bare menneskelig kreativitet og intuisjon, via konsepter og ideer, utvider rekkevidden til matematikk, mens fremskritt via databehandling ofte blir avfeid som ingeniørkunst.

Relatert historie

Denne algoritmen kan fortelle hvilke tallsekvenser et menneske vil finne interessante Resultatet antyder at maskiner en dag kan trenes til å oppdage matematisk eleganse og skjønnhet.

På en måte passer datamaskinen og Collatz-formodningen perfekt. For det første, som Jeremy Avigad, en logiker og professor i filosofi ved Carnegie Mellon bemerker, er forestillingen om en iterativ algoritme grunnlaget for informatikk – og Collatz-sekvenser er et eksempel på en iterativ algoritme, som fortsetter trinn for trinn i henhold til til en deterministisk regel. På samme måte er det et vanlig problem innen informatikk å vise at en prosess avsluttes. Dataforskere ønsker generelt å vite at algoritmene deres avsluttes, det vil si at de alltid returnerer et svar, sier Avigad. Heule og hans samarbeidspartnere utnytter denne teknologien for å takle Collatz-formodningen, som egentlig bare er et oppsigelsesproblem.

Det fine med denne automatiserte metoden er at du kan slå på datamaskinen og vente.

Jeffrey Lagarias

Heules ekspertise er med et beregningsverktøy kalt en SAT-løser - eller en tilfredsstillelsesløser, et dataprogram som bestemmer om det finnes en løsning for en formel eller et problem gitt et sett med begrensninger. Selv om det er avgjørende, i tilfelle av en matematisk utfordring, trenger en SAT-løser først problemet oversatt, eller representert, i termer som datamaskinen forstår. Og som Yolcu, doktorgradsstudent ved Heule, sier det: Representasjon betyr mye.

Et langskudd, men verdt et forsøk

Da Heule først nevnte å takle Collatz med en SAT-løser, tenkte Aaronson: Det er ingen måte i helvete at dette kommer til å fungere. Men han var lett overbevist om at det var verdt et forsøk, siden Heule så subtile måter å transformere dette gamle problemet på som kunne gjøre det bøyelig. Han hadde lagt merke til at et fellesskap av informatikere brukte SAT-løsere for å finne avslutningsbevis for en abstrakt representasjon av beregninger kalt et omskrivingssystem. Det var et langskudd, men han foreslo for Aaronson at å transformere Collatz-formodningen til et omskrivingssystem kan gjøre det mulig å få et avslutningsbevis for Collatz (Aaronson hadde tidligere hjulpet med å transformere Riemann-hypotesen til et beregningssystem, og kodet den i en liten Turing maskin). Den kvelden designet Aaronson systemet. Det var som en lekseoppgave, en morsom øvelse, sier han.

'I en veldig bokstavelig forstand kjempet jeg mot en Terminator - i det minste en avslutningsteorembevis.'

Scott Aaronson

Aaronsons system fanget Collatz-problemet med 11 regler. Hvis forskerne kunne få et avslutningsbevis for dette analoge systemet, ved å bruke de 11 reglene i hvilken som helst rekkefølge, ville det bevise at Collatz-formodningen var sann.

Heule prøvde med toppmoderne verktøy for å bevise avslutningen av omskrivingssystemer, noe som ikke fungerte – det var skuffende om ikke så overraskende. Disse verktøyene er optimalisert for problemer som kan løses på et minutt, mens enhver tilnærming for å løse Collatz sannsynligvis krever dager om ikke år med beregning, sier Heule. Dette ga motivasjon til å finpusse sin tilnærming og implementere sine egne verktøy for å transformere omskrivingsproblemet til et SAT-problem.

En representasjon av omskrivingssystemet med 11 regler for Collatz-formodningen.

MARINE HEULE

Aaronson regnet med at det ville være mye lettere å løse systemet minus en av de 11 reglene – å forlate et Collatz-lignende system, en lakmusprøve for det større målet. Han utstedte en menneske-mot-datamaskin-utfordring: Den første som løser alle delsystemer med 10 regler vinner. Aaronson prøvde for hånd. Heule prøvd av SAT-løser: Han kodet systemet som et tilfredsstillelsesproblem – med nok et smart lag med representasjon, og oversatte systemet til datamaskinens språk med variabler som kan være enten 0-er og 1-er – og lot deretter SAT-løseren kjøre på kjernene , søker etter bevis på oppsigelse.

Systemet her følger Collatz-sekvensen for startverdien 27—27 er øverst til venstre i diagonalkaskaden, 1 er nederst til høyre. Det er 71 trinn, i stedet for 111, siden forskerne brukte en annen, men ekvivalent versjon av Collatz-algoritmen: hvis tallet er partall så del på 2; ellers multipliser med 3, legg til 1 og del deretter resultatet på 2.

MARINE HEULE

De lyktes begge i å bevise at systemet avsluttes med de ulike settene med 10 regler. Noen ganger var det en triviell virksomhet, både for mennesket og programmet. Heules automatiserte tilnærming tok maksimalt 24 timer. Aaronsons tilnærming krevde betydelig intellektuell innsats, som tok noen timer eller til og med en dag – ett sett med 10 regler han aldri klarte å bevise, selv om han er overbevist om at han kunne ha mer innsats. I en veldig bokstavelig forstand kjempet jeg mot en Terminator, sier Aaronson – i det minste et termineringsteorem som beviser.

Yolcu har siden finjustert SAT-løseren, og kalibrert verktøyet for å passe bedre med naturen til Collatz-problemet. Disse triksene gjorde hele forskjellen – å øke hastigheten på termineringsbevisene for 10-regelundersystemene og redusere kjøretiden til bare sekunder.

Hovedspørsmålet som gjenstår, sier Aaronson, er: Hva med hele settet på 11? Du prøver å kjøre systemet på hele settet, og det kjører bare for alltid, noe som kanskje ikke burde sjokkere oss, fordi det er Collatz-problemet.

Slik Heule ser det, har mest forskning innen automatisert resonnement et blindt øye for problemer som krever mye beregning. Men basert på sine tidligere gjennombrudd tror han at disse problemene kan løses. Andre har forvandlet Collatz har har omskrive systemet , men det er strategien for å bruke en finjustert SAT-løser i skala med formidabel datakraft som kan få trekkraft mot et bevis.

Så langt har Heule kjørt Collatz-undersøkelsen ved å bruke rundt 5000 kjerner (behandlingsenhetene som driver datamaskiner; forbrukerdatamaskiner har fire eller åtte kjerner). Som Amazon Scholar har han en åpen invitasjon fra Amazon Web Services til å få tilgang til praktisk talt ubegrensede ressurser – så mange som én million kjerner. Men han er motvillig til å bruke betydelig mer.

Jeg vil ha en indikasjon på at dette er et realistisk forsøk, sier han. Ellers føler Heule at han ville kaste bort ressurser og tillit. Jeg trenger ikke 100 % tillit, men jeg vil virkelig gjerne ha noen bevis på at det er en rimelig sjanse for at det kommer til å lykkes.

Superlader en transformasjon

Det fine med denne automatiserte metoden er at du kan slå på datamaskinen, og vente, sier matematikeren Jeffrey Lagarias, ved University of Michigan. Han har lekt med Collatz i omtrent femti år og blitt kunnskapsholder, kompilerte kommenterte bibliografier og redigerte en bok om emnet, Den ultimate utfordringen. For Lagarias brakte den automatiserte tilnærmingen tankene på en 2013 papir av Princeton-matematikeren John Horton Conway, som mente at Collatz-problemet kan være blant en unnvikende klasse av problemer som er sanne og uavgjørelige - men med en gang ikke beviselig uavgjørelige. Som Conway bemerket: … det kan til og med være at påstanden om at de ikke er bevisbare ikke i seg selv kan bevises, og så videre.

Hvis Conway har rett, sier Lagarias, vil det ikke være noe bevis, automatisert eller ikke, og vi vil aldri vite svaret.

Mennesket som uten tvil har kommet nærmest er matematikeren Terence Tao, ved University of California, Los Angeles. I 2019 beviste Tao at Collatz-formodningen er det nesten sant for nesten alle tall (avhenger nesten av to forskjellige tekniske definisjoner, likevel i henhold til den enkle engelske betydningen).

Tao mener et menneskelig bevis på formodningen ville være mer matematisk meningsfylt - å komme til Hvorfor av det - enn et databevis. Men å ha et stort uløst problem som faller til en automatisert bevis kan overdrive en revolusjonerende transformasjon i hvordan matematikere bruker datahjelp i arbeidet sitt, sier han. Med et problem så vanskelig som dette, vil vi ta den innsikten vi kan få.

Det Heule og hans samarbeidspartnere virkelig er ute etter, er imidlertid et scenario slik at – ved å bruke denne tilnærmingen, med dette problemet – lykkes datamaskinen der mennesket svikter, eller omvendt. På dette tidspunktet vet vi ikke om disse teknikkene er mye sterkere enn hva mennesker kan gjøre for hånd eller ikke, eller om mennesker kan gjøre ting som datamaskinen ikke kan gjøre, sier Heule. Det vi ønsker å vite er om mennesker eller datamaskiner er flinkere til å løse slike problemer.

For det formål, la oss se hvem som løser Collatz-antagelsen først.

gjemme seg