Vai datori ir gatavi atrisināt šo bēdīgi smagnējo matemātikas uzdevumu?

Ms Tech | SuperRembo, izmantojot kodēšanas vilcienu

Datorzinātniece Marijna Heule vienmēr meklē labu matemātisko izaicinājumu. Kārnegija Melona universitātes asociētajam profesoram Heulei ir iespaidīga reputācija neatrisināmu matemātikas problēmu risināšanā ar skaitļošanas rīkiem. Viņa 2016. gada rezultāts ar Būla Pitagora trīskāršu problēmu bija milzīgs virsrakstu piesaistošs pierādījums: Divsimt terabaitu matemātikas pierādījums ir visu laiku lielākais . Tagad viņš izmanto automatizētu pieeju, lai uzbruktu valdzinoši vienkāršajam Kolaca pieņēmumam.

Šo skaitļu teorijas problēmu pirmo reizi ierosināja (saskaņā ar dažiem ziņojumiem) pagājušā gadsimta 30. gados vācu matemātiķis Lotārs Kolats. secība : sāciet ar jebkuru pozitīvu veselu skaitli. Ja skaitlis ir pāra, dala ar divi. Ja skaitlis ir nepāra, reiziniet ar trīs un pievienojiet vienu. Un tad dariet to pašu, atkal un atkal. Minējums apgalvo, ka secība vienmēr beigsies ar 1 (un pēc tam nepārtraukti ciklos pa 4, 2, 1).

Piemēram, skaitlis 5 ģenerē tikai sešus vārdus:

5, 16, 8, 4, 2, 1

Skaitlis 27 cirkulē cauri 111 terminiem, svārstoties uz augšu un uz leju — tā augstumā sasniedzot 9232 —, pirms galu galā piezemējas pie 1.

Skaitlis 40 ģenerē vēl vienu īsu secību:

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

Līdz šim pieņēmumi ir pārbaudīti ar datoru visām sākuma vērtībām līdz gandrīz 300 miljardiem miljardu, un katrs skaitlis galu galā sasniedz 1.

Lielākā daļa pētnieku uzskata, ka minējums ir patiess. Tas ir vilinājis daudzus matemātiķus un ne-matemātiķus, taču neviens nav radījis pierādījumus. Astoņdesmito gadu sākumā ungāru matemātiķis Pols Erdēss paziņoja: Matemātika vēl nav gatava šādām problēmām.

Mēs vēlamies zināt, vai cilvēki vai datori labāk risina šādas problēmas.

Marijna Heule

Un viņam, iespējams, ir taisnība, saka Heule. Heulei Kolaca valdzinājums ir ne tik daudz izrāviena izredzes, cik automatizētu spriešanas metožu attīstība. Pēc piecu gadu ilgas pūlēšanās ar to Heule un viņa līdzstrādnieki Skots Āronsons un Emre Jolku nesen publicēja papīrs arXiv priekšdrukas serverī. Lai gan mums neizdodas pierādīt Collatz minējumus, viņi raksta, mēs uzskatām, ka šeit esošās idejas pārstāv interesantu jaunu pieeju.

Tā ir cēla neveiksme, saka Āronsons, datorzinātnieks no Teksasas Universitātes Ostinā. Neveiksme, jo viņi nepierādīja minējumu. Cēls, jo viņi guva panākumus citā nozīmē: Heule to uzskata par sākumpunktu, lai noteiktu, vai cilvēki vai datori spēj labāk pierādīt šādas problēmas.

Matemātikas tulkošana aprēķinos

Daudzām matemātikas problēmām datori ir bezcerīgi, jo tiem nav piekļuves milzīgajam matemātikas darbam, kas uzkrāts vēstures gaitā. Bet dažreiz datori izceļas tur, kur cilvēkiem ir bezcerība. Pastāstiet datoram, kā izskatās risinājums — piešķiriet tam mērķi un precīzi definētu meklēšanas vietu, un tad dators to varētu atrast ar brutālu spēku. Lai gan tas ir jautājums debates vai skaitļošanas rezultāti ir nozīmīgi papildinājumi matemātiskajam kanonam. Tradicionālais uzskats ir tāds, ka tikai cilvēka radošums un intuīcija, izmantojot jēdzienus un idejas, paplašina matemātikas sasniedzamību, turpretim sasniegumi ar skaitļošanas palīdzību bieži tiek noraidīti kā inženierija.

Saistīts stāsts

Šis algoritms var pateikt, kuras skaitļu virknes cilvēkam šķitīs interesantas Rezultāts liecina, ka kādu dienu mašīnas varētu apmācīt pamanīt matemātisko eleganci un skaistumu.

Savā ziņā dators un Collatz minējums ir ideāli saderīgi. Pirmkārt, kā atzīmē Džeremijs Avigads, Kārnegija Melona loģiķis un filozofijas profesors, iteratīvā algoritma jēdziens ir datorzinātņu pamatā, un Collatz sekvences ir iteratīvā algoritma piemērs, kas notiek soli pa solim saskaņā ar uz deterministisku likumu. Līdzīgi parādīšana, ka process beidzas, ir izplatīta problēma datorzinātnēs. Datorzinātnieki parasti vēlas zināt, ka viņu algoritmi beidzas, proti, viņi vienmēr sniedz atbildi, saka Avigads. Heule un viņa līdzstrādnieki izmanto šo tehnoloģiju, lai risinātu Collatz pieņēmumu, kas patiesībā ir tikai izbeigšanas problēma.

Šīs automatizētās metodes skaistums ir tāds, ka varat ieslēgt datoru un gaidīt.

Džefrijs Lagariass

Heules zināšanas ir saistītas ar skaitļošanas rīku, ko sauc par SAT risinātāju, vai apmierinošības risinātāju, datorprogrammu, kas nosaka, vai formulai vai problēmai ir risinājums, ņemot vērā ierobežojumu kopumu. Lai gan izšķiroši svarīgi ir tas, ka matemātiskas problēmas gadījumā SAT risinātājam vispirms ir jātulko vai jāattēlo problēma datoram saprotamā veidā. Un kā saka Heules doktorantūras students Yolcu: reprezentācijai ir liela nozīme.

Tāls, bet pamēģināšanas vērts

Kad Heule pirmo reizi pieminēja Collatz risināšanu ar SAT risinātāju, Āronsons nodomāja: 'Nav nekāda veida, kā tas darbosies'. Taču viņš bija viegli pārliecināts, ka ir vērts mēģināt, jo Heule redzēja smalkus veidus, kā pārveidot šo veco problēmu, kas varētu padarīt to elastīgu. Viņš pamanīja, ka datorzinātnieku kopiena izmanto SAT risinātājus, lai veiksmīgi atrastu beigu pierādījumus abstraktam skaitļošanas attēlojumam, ko sauc par pārrakstīšanas sistēmu. Tas bija tālu, taču viņš ierosināja Āronsonam, ka Kolatza pieņēmuma pārveidošana par pārrakstīšanas sistēmu varētu ļaut iegūt Kolaca beigu pierādījumu (Āronsons iepriekš bija palīdzējis pārveidot Rīmaņa hipotēzi skaitļošanas sistēmā, iekodējot to nelielā Tjūringa sistēmā mašīna). Tajā vakarā Āronsons izstrādāja sistēmu. Viņš saka, ka tas bija kā mājasdarbs, jautrs vingrinājums.

'Ļoti burtiskā nozīmē es cīnījos ar terminatoru — vismaz beigu teorēmas pārbaudītāju.'

Skots Āronsons

Āronsona sistēma tvēra Kolaca problēmu ar 11 noteikumiem. Ja pētnieki varētu iegūt šīs analoģiskās sistēmas izbeigšanas pierādījumu, piemērojot šos 11 noteikumus jebkurā secībā, tas pierādītu, ka Collatz minējums ir patiess.

Heule mēģināja ar vismodernākajiem rīkiem pierādīt pārrakstīšanas sistēmu pārtraukšanu, kas nedarbojās — tas bija vilšanās, ja ne tik pārsteidzoši. Šie rīki ir optimizēti problēmām, kuras var atrisināt vienā minūtē, savukārt jebkurai pieejai Collatz risināšanai, iespējams, ir nepieciešamas vairākas dienas, ja ne gadi, saka Heule. Tas radīja motivāciju uzlabot savu pieeju un ieviest savus rīkus, lai pārveidotu pārrakstīšanas problēmu par SAT problēmu.

11 kārtulu pārrakstīšanas sistēmas attēlojums Collatz pieņēmumam.

JŪRAS HĒLE

Āronsons uzskatīja, ka būtu daudz vieglāk atrisināt sistēmu, atskaitot vienu no 11 noteikumiem, atstājot Kolatzam līdzīgu sistēmu, kas ir lakmusa papīrs lielākam mērķim. Viņš izdeva izaicinājumu cilvēks pret datoru: pirmais, kurš atrisina visas apakšsistēmas ar 10 noteikumiem, uzvar. Āronsons mēģināja ar roku. Heule mēģināja SAT risinātājs: viņš iekodēja sistēmu kā apmierināmības problēmu — ar vēl vienu gudru attēlojuma slāni, pārveidojot sistēmu datora mainīgo lielumu valodā, kas var būt gan 0s, gan 1s — un pēc tam ļāva savam SAT risinātājam darboties uz kodoliem. , meklējot pierādījumus par pārtraukšanu.

Sistēma šeit seko Collatz secībai sākuma vērtībai 27–27 atrodas diagonālās kaskādes augšējā kreisajā stūrī, 1 ir apakšējā labajā stūrī. Ir 71 solis, nevis 111, jo pētnieki izmantoja citu, bet līdzvērtīgu Collatz algoritma versiju: ​​ja skaitlis ir pāra, tad dala ar 2; pretējā gadījumā reiziniet ar 3, pievienojiet 1 un pēc tam daliet rezultātu ar 2.

JŪRAS HĒLE

Viņiem abiem izdevās pierādīt, ka sistēma beidzas ar dažādām 10 noteikumu kopām. Dažreiz tas bija triviāls pasākums gan cilvēkam, gan programmai. Heule automatizētā pieeja aizņēma ne vairāk kā 24 stundas. Āronsona pieeja prasīja ievērojamas intelektuālas pūles, kas prasīja dažas stundas vai pat dienu — vienu 10 noteikumu kopumu, ko viņam nekad neizdevās pierādīt, lai gan viņš ir stingri pārliecināts, ka viņš varētu to izdarīt ar lielāku piepūli. Ļoti burtiskā nozīmē es cīnījos ar terminatoru, saka Āronsons — vismaz beigu teorēmas pārbaudītājs.

Kopš tā laika Yolcu ir precīzi noregulējis SAT risinātāju, kalibrējot rīku, lai tas labāk atbilstu Collatz problēmas būtībai. Šie triki radīja visu atšķirību — paātrinot 10 kārtulu apakšsistēmu beigu pierādījumus un saīsinot izpildes laiku līdz tikai sekundēm.

Galvenais jautājums, kas paliek, saka Āronsons, ir: Kā ir ar pilnu 11 komplektu? Jūs mēģināt palaist sistēmu pilnā komplektā, un tā darbojas mūžīgi, kas, iespējams, nedrīkst mūs šokēt, jo tā ir Collatz problēma.

Pēc Heule domām, lielākā daļa pētījumu automatizētās spriešanas jomā nepieredz problēmas, kas prasa daudz aprēķinu. Taču, pamatojoties uz viņa iepriekšējiem atklājumiem, viņš uzskata, ka šīs problēmas var atrisināt. Citiem ir pārveidots Collatz ir ir pārrakstīšanas sistēma , taču tā ir stratēģija, kurā tiek izmantots precīzi noregulēts SAT risinātājs ar milzīgu skaitļošanas jaudu, kas varētu iegūt pierādījumu.

Līdz šim Heule ir veikusi Collatz izmeklēšanu, izmantojot aptuveni 5000 kodolu (procesoru bloki, kas darbina datorus; patērētāju datoriem ir četri vai astoņi kodoli). Kā Amazon Scholar viņam ir atklāts uzaicinājums no Amazon Web Services piekļūt praktiski neierobežotiem resursiem — pat vienam miljonam kodolu. Bet viņš nevēlas izmantot ievērojami vairāk.

Viņš saka, ka es vēlos dažas norādes, ka tas ir reālistisks mēģinājums. Pretējā gadījumā Heule uzskata, ka viņš izšķiež resursus un uzticību. Man nav vajadzīga 100% pārliecība, bet es patiešām vēlētos iegūt pierādījumus tam, ka ir pamatota iespēja, ka tas izdosies.

Pārveidojuma uzlādēšana

Šīs automatizētās metodes skaistums ir tāds, ka varat ieslēgt datoru un gaidīt, saka matemātiķis Džefrijs Lagariass no Mičiganas universitātes. Viņš ir spēlējies ar Kolacu apmēram piecdesmit gadus un kļuvis par zināšanu glabātāju, veidojot anotētas bibliogrāfijas un rediģējot grāmatu par šo tēmu, Ultimate Challenge. Lagariasam automatizētā pieeja lika prātā a 2013. gada papīrs Prinstonas matemātiķis Džons Hortons Konvejs, kurš domāja, ka Kolaca problēma varētu būt viena no nenotveramām problēmu klasēm, kas ir patiesas un neatrisināmas, taču vienlaikus nav pierādāmas neatrisināmas. Kā atzīmēja Konvejs: … var pat būt, ka apgalvojums, ka tie nav pierādāmi, pats par sevi nav pierādāms utt.

Ja Konvejam ir taisnība, Lagarias saka, pierādījumu nebūs, automatizētu vai nē, un mēs nekad neuzzināsim atbildi.

Cilvēks, kurš, iespējams, ir nonācis vistuvāk, ir matemātiķis Terenss Tao no Kalifornijas universitātes Losandželosā. 2019. gadā Tao pierādīja, ka Kolaca minējums ir tāds gandrīz taisnība gandrīz visiem skaitļiem (gandrīz paļaujas uz divām dažādām tehniskām definīcijām, tomēr saskaņā ar vienkāršu angļu valodas nozīmi).

Tao uzskata, ka cilvēka pierādījums pieņēmumam būtu matemātiski nozīmīgāks — lai tiktu pie tā kāpēc no tā — nekā datora pierādījums. Taču, ja liela neatrisināta problēma nonāks automātiskā pārbaudītāja rokās, tas var izraisīt revolucionāras pārmaiņas matemātiķu darbā ar datoru palīdzību, viņš saka. Ja problēma ir tik neatrisināma, kā šī, mēs gūsim visu iespējamo ieskatu.

Tomēr Heule un viņa līdzstrādnieki patiešām vēlas izveidot tādu scenāriju, ka, izmantojot šo pieeju, ar šo problēmu dators gūst panākumus tur, kur cilvēkam neizdodas, vai otrādi. Šobrīd mēs nezinām, vai šīs metodes ir daudz spēcīgākas par to, ko cilvēki var darīt ar rokām, vai arī cilvēki var darīt lietas, ko dators nevar izdarīt, saka Heule. Mēs vēlamies zināt, vai cilvēki vai datori labāk risina šādas problēmas.

Šim nolūkam redzēsim, kurš pirmais atrisina Collatz minējumu.

paslēpties