Et forsøk på å takle den uoppnåelige Collatz-formodningen er en “edel fiasko” som viser løftet om automatiserte resonnementsteknikker.
av
2. juli 2021 
Ms Tech | SuperRembo via kodingstog
Datavitenskapsmannen Marijn Heule er alltid på utkikk etter en god matematisk utfordring. En lektor ved Carnegie Mellon University, Heule, har et imponerende rykte for å løse vanskelige matteproblemer med beregningsverktøy. Hans 2016-resultat med det “Boolske Pythagoras trippelproblemet” var et enormt bevis for overskrift: “To hundre terabyte matte bevis er størst noensinne.” Nå bruker han en automatisert tilnærming for å angripe den oppmuntrende enkle Collatz-formodningen.
Først foreslått (ifølge noen kontoer) 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 jevnt, divider med to. Hvis tallet er odde, multipliserer du med tre og legger til en. Og gjør det samme, igjen og igjen. Antagelsen hevder at sekvensen alltid vil ende opp med 1 (og deretter kontinuerlig sykle gjennom 4, 2, 1).
Antallet 5 genererer for eksempel bare seks termer:
5, 16, 8, 4, 2, 1
Tallet 27 går gjennom 111 termer, oscillerende opp og ned — i høyden når det til 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
Hittil har antagelsen blitt sjekket av datamaskinen for alle startverdier opp til nesten 300 milliarder milliarder kroner, og hvert tall når til slutt 1.
De fleste forskere mener antagelsen er sann. Det har lokket mange matematikere og ikke-matematikere, men ingen har gitt bevis. Tidlig på 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 sannsynligvis rett,” sier Heule. For Heule er ikke Collatz's allure utsiktene til et gjennombrudd, da det fremmer automatiserte resonnementsteknikker. Etter å ha puslet med det i fem år, la Heule og hans samarbeidspartnere, Scott Aaronson og Emre Yolcu, nylig ut et papir på arXiv preprint-serveren. “Selv om vi ikke lykkes med å bevise Collatz-formodningen,” skriver de, “tror vi at ideene her representerer en interessant ny tilnærming.”
“Det er en edel fiasko,” sier Aaronson, datavitenskapsmann ved University of Texas i Austin. En fiasko fordi de ikke beviste antagelsen. Edelt fordi de gjorde fremgang i en annen forstand: Heule ser på det som et utgangspunkt for å avgjøre om mennesker eller datamaskiner er flinkere til å bevise slike problemer.
Oversettelse av matematikk til beregning
For mange matteproblemer er datamaskiner håpløse, siden de ikke har tilgang til det store matematikkproduktet 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økeområde – og deretter kan datamaskinen med grov kraft finne den. Selv om det er et spørsmål om debatt om beregningsresultater utgjør meningsfylte 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 avvist som ingeniørvitenskap.
Relatert historie
Denne algoritmen kan fortelle hvilke tallsekvenser et menneske vil finne interessante. Resultatet antyder at maskiner en dag kan bli trent til å oppdage matematisk eleganse og skjønnhet.
På en måte er datamaskinen og Collatz-formodningen en perfekt match. For det ene, som Jeremy Avigad, en logiker og professor i filosofi ved Carnegie Mellon, bemerker begrepet en iterativ algoritme grunnlaget for datavitenskap – og Collatz-sekvenser er et eksempel på en iterativ algoritme, som går trinnvis i henhold til til en deterministisk regel. På samme måte er det et vanlig problem innen informatikk å vise at en prosess avsluttes. “Datavitenskapsmenn vil generelt vite at algoritmene deres avsluttes, det vil si at de alltid returnerer et svar,” sier Avigad. Heule og hans samarbeidspartnere utnytter den teknologien for å takle Collatz-formodningen, som egentlig bare er et avslutningsproblem.
“Det fine med denne automatiserte metoden er at du kan slå på datamaskinen og vente.”
Jeffrey Lagarias
Heules ekspertise er med et beregningsverktøy som kalles en “SAT-løser” – eller en “tilfredshet” -løser, et dataprogram som avgjør om det er en løsning for en formel eller et problem gitt et sett med begrensninger. Selv om det er avgjørende, når det gjelder 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, uttrykker det: “Representasjon betyr mye, mye.”
Et langskudd, men verdt å prøve
Da Heule først nevnte å takle Collatz med en SAT-løser, tenkte Aaronson: “Det er ingen vei i helvete dette vil fungere.” Men han var lett overbevist om at det var verdt et forsøk, siden Heule så subtile måter å transformere dette gamle problemet som kan gjøre det smidig. Han hadde lagt merke til at et samfunn av dataforskere brukte SAT-løsere for å lykkes med å finne avslutningsbevis for en abstrakt representasjon av beregning kalt et “omskrivningssystem.” Det var et langskudd, men han foreslo til Aaronson at det å transformere Collatz-formodningen til et omskrivningssystem kan gjøre det mulig å få et avslutningsbevis for Collatz (Aaronson hadde tidligere bidratt til å transformere Riemann-hypotesen til et beregningssystem, kodet det i en liten Turing maskin). Den kvelden designet Aaronson systemet. “Det var som lekser, en morsom øvelse,” sier han.
“I en veldig bokstavelig forstand kjempet jeg med en Terminator — i det minste en avslutningssetning. ”
Scott Aaronson
Aaronsons system fanget Collatz-problemet med 11 regler. Hvis forskerne kunne få et avslutningsbevis for dette analoge systemet, ved å anvende de 11 reglene i hvilken som helst rekkefølge, ville det bevise Collatz-formodningen sant.
Heule prøvde med moderne verktøy for å bevise avslutningen av omskrivingssystemer, som ikke fungerte – det var skuffende om ikke så overraskende. “Disse verktøyene er optimalisert for problemer som kan løses i løpet av et øyeblikk, mens enhver tilnærming for å løse Collatz sannsynligvis krever dager om ikke år med beregning,” sier Heule. Dette ga motivasjon til å finpusse deres tilnærming og implementere egne verktøy for å transformere omskrivingsproblemet til et SAT-problem.
En representasjon av 11-regelens omskrivingssystem for Collatz-antagelsen.MARIJN HEULE Aaronson skjønte at det ville være mye lettere å løse systemet minus en av de 11 reglene – etterlate et “Collatz-lignende” system, en lakmusprøve for det større målet. Han ga en utfordring mellom mennesker og datamaskiner: Den første som løser alle delsystemer med 10 regler, vinner. Aaronson prøvde for hånd. Heule prøvd av SAT-løseren: Han kodet systemet som et tilfredsstillelsesproblem – med enda et smart lag med representasjon, og oversatte systemet til datamaskinens lingo av variabler som kan være enten 0s og 1s – og la deretter SAT-løseren kjøre på kjernene , søker etter bevis på avslutning.
Systemet her følger Collatz-sekvensen for startverdien 27—27 er øverst til venstre i den diagonale kaskaden, 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 til og med, divider med 2; ellers multipliser med 3, legg til 1, og del deretter resultatet med 2. MARIJN HEULE De lyktes begge i å bevise at systemet avsluttes med de forskjellige settene med 10 regler. Noen ganger var det en triviell oppgave for både det menneskelige og programmet. Heules automatiserte tilnærming tok maksimalt 24 timer. Aaronsons tilnærming krevde betydelig intellektuell innsats, og tok noen timer eller til og med en dag – ett sett med ti regler han aldri klarte å bevise, selv om han bestemt tror at han kunne ha, med mer innsats. “I bokstavelig forstand kjempet jeg med en Terminator,” sier Aaronson – “i det minste en avslutningsteoriprover.” av Collatz-problemet. Disse triksene utgjorde hele forskjellen – påskynde avslutningsbevisene for 10-regelundersystemene og reduserte driftstiden til bare sekunder.
“Hovedspørsmålet som gjenstår,” sier Aaronson, “er: Hva med hele settet med 11? Du prøver å kjøre systemet på hele settet, og det kjører bare for alltid, noe som kanskje ikke burde sjokkere oss, for det er Collatz-problemet. ”
Som Heule ser det, har de fleste undersøkelser innen automatisert resonnement en blinde øye for problemer som krever mye beregning. Men basert på hans tidligere gjennombrudd mener han at disse problemene kan løses. Andre har forvandlet Collatz som et omskrivingssystem, men det er strategien å bruke en finjustert SAT-løsning i stor skala med formidabel beregningskraft som kan få trekkraft mot et bevis.
Så langt har Heule kjørt Collatz-undersøkelsen ved å bruke rundt 5000 kjerner (prosesseringsenhetene som driver datamaskiner; forbrukerdatamaskiner har fire eller åtte kjerner). Som Amazon Scholar har han en åpen invitasjon fra Amazon Web Services om å få tilgang til “praktisk talt ubegrensede” ressurser – så mange som en million kjerner. Men han er tilbakeholden med å bruke betydelig mer.
“Jeg vil ha noen indikasjoner på at dette er et realistisk forsøk,” sier han. Ellers føler Heule at han vil kaste bort ressurser og tillit. “Jeg trenger ikke 100% tillit, men jeg vil virkelig ha noen bevis for at det er en rimelig sjanse for at det kommer til å lykkes.”
Supercharging a transformation
“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 har vært kunnskapens keeper, sammenstilt kommenterte bibliografier og redigert en bok om emnet “The Ultimate Challenge.” For Lagarias kom den automatiserte tilnærmingen til å tenke på et papir fra 2013 av Princeton-matematikeren John Horton Conway, som tenkte at Collatz-problemet kan være blant en unnvikende klasse av problemer som er sanne og “ubesluttsomme” – men samtidig ikke beviselig ubesluttsomme. Som Conway bemerket: “… kan det til og med være at påstanden om at de ikke er bevisbare ikke i seg selv er bevisbar, og så videre.”
“Hvis Conway har rett,” sier Lagarias, “vil det ikke være noen bevis, automatisert eller ikke, og vi vil aldri vite svaret. ”