Zijn computers klaar om dit notoir logge wiskundeprobleem op te lossen?

mevrouw Tech | SuperRembo via codeertrein

Informaticus Marijn Heule is altijd op zoek naar een goede wiskundige uitdaging. Heule, universitair hoofddocent aan de Carnegie Mellon University, heeft een indrukwekkende reputatie voor het oplossen van hardnekkige wiskundige problemen met rekenhulpmiddelen. Zijn resultaat in 2016 met het Boolean Pythagorean triples-probleem was een enorm bewijs dat de krantenkoppen haalde: Wiskundebewijs van tweehonderd terabyte is grootste ooit . Nu implementeert hij een geautomatiseerde aanpak om het verleidelijk eenvoudige vermoeden van Collatz aan te vallen.

Voor het eerst voorgesteld (volgens sommige verslagen) in de jaren 1930 door de Duitse wiskundige Lothar Collatz, biedt dit probleem met de getaltheorie een recept, of algoritme, voor het genereren van een numerieke volgorde : Begin met een willekeurig positief geheel getal. Als het getal even is, deel je door twee. Als het getal oneven is, vermenigvuldig dan met drie en tel er één bij op. En doe dan hetzelfde, steeds weer opnieuw. Het vermoeden stelt dat de reeks altijd op 1 zal eindigen (en dan continu door 4, 2, 1) gaat.

Het getal 5 genereert bijvoorbeeld slechts zes termen:

5, 16, 8, 4, 2, 1

Het getal 27 doorloopt 111 termen, oscilleert op en neer - op een hoogte van 9.232 - voordat het uiteindelijk bij 1 landt.

Het getal 40 genereert nog een korte reeks:

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

Tot op heden is het vermoeden door de computer gecontroleerd op alle startwaarden tot bijna 300 miljard miljard en elk getal bereikt uiteindelijk 1.

De meeste onderzoekers geloven dat het vermoeden waar is. Het heeft massa's wiskundigen en niet-wiskundigen verleid, maar niemand heeft een bewijs geleverd. Begin jaren tachtig verklaarde de Hongaarse wiskundige Paul Erdős: de wiskunde is nog niet klaar voor dergelijke problemen.

Wat we willen weten is of mensen of computers zulke problemen beter kunnen oplossen.

Marijn Heule

En waarschijnlijk heeft hij gelijk, zegt Heule. Voor Heule is de allure van Collatz niet zozeer het vooruitzicht van een doorbraak, maar het bevorderen van geautomatiseerde redeneertechnieken. Na er vijf jaar aan te hebben gesleuteld, plaatsten Heule en zijn medewerkers, Scott Aaronson en Emre Yolcu, onlangs een papier op de arXiv preprint-server. Hoewel we er niet in slagen het vermoeden van Collatz te bewijzen, zo schrijven ze, zijn we van mening dat de ideeën hier een interessante nieuwe benadering vertegenwoordigen.

Het is een nobele mislukking, zegt Aaronson, een computerwetenschapper aan de Universiteit van Texas in Austin. Een mislukking omdat ze het vermoeden niet hebben bewezen. Edel omdat ze op een andere manier vooruitgang boekten: Heule beschouwt het als een startpunt om te bepalen of mensen of computers zulke problemen beter kunnen bewijzen.

Wiskunde vertalen naar rekenen

Voor veel wiskundige problemen zijn computers hopeloos, omdat ze geen toegang hebben tot het enorme oeuvre van wiskunde dat door de geschiedenis is vergaard. Maar soms blinken computers uit waar mensen hopeloos zijn. Vertel een computer hoe een oplossing eruitziet - geef het een doel en een goed gedefinieerde zoekruimte - en dan kan de computer het met brute kracht vinden. Al is het een kwestie van debat of computationele resultaten een zinvolle toevoeging zijn aan de wiskundige canon. De traditionele opvatting is dat alleen menselijke creativiteit en intuïtie, via concepten en ideeën, het bereik van wiskunde vergroten, terwijl vooruitgang via informatica vaak wordt afgedaan als engineering.

Verwant verhaal

Dit algoritme kan vertellen welke nummerreeksen een mens interessant zal vinden Het resultaat suggereert dat machines ooit kunnen worden getraind om wiskundige elegantie en schoonheid te herkennen.

In zekere zin zijn de computer en het vermoeden van Collatz een perfecte match. Ten eerste, zoals Jeremy Avigad, een logicus en hoogleraar filosofie aan Carnegie Mellon opmerkt, ligt het idee van een iteratief algoritme aan de basis van de informatica - en Collatz-sequenties zijn een voorbeeld van een iteratief algoritme, dat stap voor stap verloopt volgens naar een deterministische regel. Evenzo is het aantonen dat een proces eindigt een veelvoorkomend probleem in de informatica. Computerwetenschappers willen over het algemeen weten dat hun algoritmen eindigen, dat wil zeggen dat ze altijd een antwoord teruggeven, zegt Avigad. Heule en zijn medewerkers maken gebruik van die technologie om het vermoeden van Collatz aan te pakken, wat eigenlijk slechts een beëindigingsprobleem is.

Het mooie van deze geautomatiseerde methode is dat u de computer kunt aanzetten en kunt wachten.

Jeffrey Lagarias

Heule's expertise is met een computationeel hulpmiddel dat een SAT-oplosser wordt genoemd - of een verzadigingsoplosser, een computerprogramma dat bepaalt of er een oplossing is voor een formule of probleem, gegeven een reeks beperkingen. Hoewel cruciaal, in het geval van een wiskundige uitdaging, moet een SAT-oplosser eerst het probleem vertaald of weergegeven hebben in termen die de computer begrijpt. En zoals Yolcu, een promovendus bij Heule, het stelt: Representation matters, a lot.

Een longshot, maar het proberen waard

Toen Heule voor het eerst zei dat hij Collatz met een SAT-oplosser moest aanpakken, dacht Aaronson: dit gaat in godsnaam niet werken. Maar hij was er snel van overtuigd dat het de moeite van het proberen waard was, aangezien Heule subtiele manieren zag om dit oude probleem te transformeren waardoor het plooibaar zou kunnen worden. Het was hem opgevallen dat een gemeenschap van computerwetenschappers SAT-oplossers gebruikte om met succes beëindigingsbewijzen te vinden voor een abstracte weergave van berekeningen, een herschrijfsysteem. Het was een longshot, maar hij suggereerde Aaronson dat het transformeren van het vermoeden van Collatz in een herschrijfsysteem het mogelijk zou kunnen maken om een ​​beëindigingsbewijs voor Collatz te krijgen (Aaronson had eerder geholpen om de Riemann-hypothese om te zetten in een computersysteem, door het te coderen in een kleine Turing machine). Die avond ontwierp Aaronson het systeem. Het was als een huiswerkopdracht, een leuke oefening, zegt hij.

'In heel letterlijke zin vocht ik tegen een Terminator - in ieder geval een bewijzer van de beëindigingsstelling.'

Scott Aaronson

Het systeem van Aaronson legde het Collatz-probleem vast met 11 regels. Als de onderzoekers een beëindigingsbewijs voor dit analoge systeem zouden kunnen krijgen, door die 11 regels in willekeurige volgorde toe te passen, zou dat bewijzen dat het vermoeden van Collatz waar is.

Heule probeerde met ultramoderne tools de beëindiging van herschrijfsystemen te bewijzen, wat niet werkte - het was teleurstellend, zo niet zo verrassend. Deze tools zijn geoptimaliseerd voor problemen die in een minuut kunnen worden opgelost, terwijl elke benadering om Collatz op te lossen waarschijnlijk dagen, zo niet jaren rekenwerk vereist, zegt Heule. Dit gaf de motivatie om hun aanpak aan te scherpen en hun eigen tools te implementeren om het herschrijfprobleem om te zetten in een SAT-probleem.

Een weergave van het herschrijfsysteem met 11 regels voor het vermoeden van Collatz.

MARIJN HEULE

Aaronson dacht dat het veel gemakkelijker zou zijn om het systeem op te lossen, minus één van de 11 regels, waardoor een Collatz-achtig systeem overblijft, een lakmoesproef voor het grotere doel. Hij vaardigde een mens-versus-computer-uitdaging uit: de eerste die alle subsystemen oplost met 10 regels, wint. Aaronson probeerde het met de hand. Heule geprobeerd door SAT-oplosser: hij codeerde het systeem als een verzadigingsprobleem - met nog een andere slimme representatielaag, waarbij het systeem werd vertaald naar het computerjargon van variabelen die 0-en en 1-en kunnen zijn - en liet zijn SAT-oplosser vervolgens op de kernen draaien , op zoek naar bewijs van beëindiging.

Het systeem volgt hier de Collatz-reeks voor de startwaarde 27-27 is linksboven in de diagonale cascade, 1 is rechtsonder. Er zijn 71 stappen in plaats van 111, aangezien de onderzoekers een andere, maar equivalente versie van het Collatz-algoritme gebruikten: als het getal even is, deel dan door 2; anders vermenigvuldig je met 3, tel je 1 op en deel je het resultaat door 2.

MARIJN HEULE

Ze slaagden er allebei in te bewijzen dat het systeem eindigt met de verschillende sets van 10 regels. Soms was het een triviale onderneming, zowel voor de mens als voor het programma. De geautomatiseerde aanpak van Heule duurde maximaal 24 uur. De aanpak van Aaronson vergde een aanzienlijke intellectuele inspanning, die een paar uur of zelfs een dag in beslag nam - een set van 10 regels die hij nooit heeft kunnen bewijzen, hoewel hij er vast van overtuigd is dat hij dat met meer moeite had kunnen doen. In heel letterlijke zin vocht ik tegen een Terminator, zegt Aaronson - in ieder geval een bewijzer van de beëindigingsstelling.

Yolcu heeft sindsdien de SAT-oplosser verfijnd en de tool gekalibreerd om beter te passen bij de aard van het Collatz-probleem. Deze trucs maakten het verschil: het versnellen van de beëindigingsbewijzen voor de subsystemen met 10 regels en het terugbrengen van de looptijd tot slechts enkele seconden.

De belangrijkste vraag die overblijft, zegt Aaronson, is: hoe zit het met de volledige set van 11? Je probeert het systeem op de volledige set te laten draaien en het werkt gewoon voor altijd, wat ons misschien niet zou moeten schokken, want dat is het Collatz-probleem.

Zoals Heule het ziet, heeft het meeste onderzoek naar geautomatiseerd redeneren een oogje dicht voor problemen die veel rekenwerk vereisen. Maar op basis van zijn eerdere doorbraken gelooft hij dat deze problemen kunnen worden opgelost. Anderen hebben getransformeerde Collatz hebben heeft herschrijf systeem , maar het is de strategie om een ​​nauwkeurig afgestemde SAT-oplosser op grote schaal te hanteren met formidabele rekenkracht die aan kracht zou kunnen winnen in de richting van een bewijs.

Tot dusver heeft Heule het Collatz-onderzoek uitgevoerd met ongeveer 5.000 kernen (de verwerkingseenheden die computers aandrijven; consumentencomputers hebben vier of acht kernen). Als Amazon Scholar heeft hij een open uitnodiging gekregen van Amazon Web Services om toegang te krijgen tot praktisch onbeperkte bronnen - tot wel een miljoen cores. Maar hij is terughoudend om aanzienlijk meer te gebruiken.

Ik wil een indicatie dat dit een realistische poging is, zegt hij. Anders zou Heule middelen en vertrouwen verspillen. Ik heb geen 100% vertrouwen nodig, maar ik zou graag enig bewijs hebben dat er een redelijke kans is dat het gaat lukken.

Een transformatie aanjagen

Het mooie van deze geautomatiseerde methode is dat je de computer kunt aanzetten en kunt wachten, zegt de wiskundige Jeffrey Lagarias van de Universiteit van Michigan. Hij speelt al zo'n vijftig jaar met Collatz en wordt bewaarder van de kennis, stelt geannoteerde bibliografieën samen en redigeert een boek over het onderwerp, De ultieme uitdaging. Voor Lagarias deed de geautomatiseerde aanpak denken aan een papier uit 2013 door de Princeton-wiskundige John Horton Conway, die mijmerde dat het Collatz-probleem misschien tot een ongrijpbare klasse van problemen behoort die waar en onbeslisbaar zijn - maar tegelijkertijd niet aantoonbaar onbeslisbaar. Zoals Conway opmerkte: … het kan zelfs zo zijn dat de bewering dat ze niet bewijsbaar zijn, zelf niet bewijsbaar is, enzovoort.

Als Conway gelijk heeft, zegt Lagarias, zal er geen bewijs zijn, geautomatiseerd of niet, en we zullen het antwoord nooit weten.

De mens die aantoonbaar het dichtst in de buurt komt, is de wiskundige Terence Tao van de Universiteit van Californië, Los Angeles. In 2019 bewees Tao dat het vermoeden van Collatz is: bijna waar voor bijna alle getallen (betrouwt bijna op twee verschillende technische definities, niettemin in overeenstemming met de gewone Engelse betekenis).

Tao gelooft dat een menselijk bewijs van het vermoeden wiskundig zinvoller zou zijn - om tot de... waarom ervan — dan een computerbewijs. Maar als een groot onopgelost probleem wordt toegewezen aan een geautomatiseerde bewijzer, zou dit een revolutionaire transformatie kunnen stimuleren in de manier waarop wiskundigen computerhulp gebruiken in hun werk, zegt hij. Met een probleem dat zo hardnekkig is als dit, nemen we alle inzichten die we kunnen krijgen.

Waar Heule en zijn medewerkers echter echt naar op zoek zijn, is een scenario waarbij - met deze benadering, met dit probleem - de computer slaagt waar de mens faalt, of omgekeerd. Op dit moment weten we niet of deze technieken veel sterker zijn dan wat mensen met de hand kunnen doen of niet, of dat mensen dingen kunnen doen die de computer niet kan, zegt Heule. Wat we willen weten is of mensen of computers zulke problemen beter kunnen oplossen.

Laten we daarom kijken wie het vermoeden van Collatz als eerste oplost.

zich verstoppen