Czy komputery są gotowe do rozwiązania tego notorycznie nieporęcznego problemu matematycznego?

Pani Tech | SuperRembo przez codingtrain

Informatyk Marijn Heule zawsze szuka dobrego matematycznego wyzwania. Profesor nadzwyczajny na Carnegie Mellon University, Heule ma imponującą reputację w rozwiązywaniu trudnych problemów matematycznych za pomocą narzędzi obliczeniowych. Jego wynik w 2016 roku z problemem trójek Boole'a Pitagorasa był ogromnym, chwytającym za nagłówki dowodem: Dwustu terabajtowy dowód matematyczny jest największy w historii . Teraz wdraża zautomatyzowane podejście do ataku na urzekająco prostą hipotezę Collatza.

Po raz pierwszy zaproponowany (według niektórych relacji) w latach 30. XX wieku przez niemieckiego matematyka Lothara Collatza, ten problem teorii liczb dostarcza przepisu lub algorytmu generowania liczb sekwencja : Zacznij od dowolnej dodatniej liczby całkowitej. Jeśli liczba jest parzysta, podziel przez dwa. Jeśli liczba jest nieparzysta, pomnóż przez trzy i dodaj jeden. A potem rób to samo, raz za razem. Przypuszczenie zakłada, że ​​sekwencja zawsze kończy się na 1 (a następnie ciągle przechodzi przez 4, 2, 1).

Na przykład liczba 5 generuje tylko sześć terminów:

5, 16, 8, 4, 2, 1

Liczba 27 przechodzi przez 111 wyrazów, oscylując w górę i w dół — na swojej wysokości sięgającej 9232 — zanim ostatecznie wyląduje na 1.

Liczba 40 generuje kolejną krótką sekwencję:

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

Do tej pory przypuszczenie zostało sprawdzone komputerowo pod kątem wszystkich wartości początkowych do prawie 300 miliardów miliardów i każda liczba ostatecznie osiąga 1.

Większość badaczy uważa, że ​​przypuszczenie jest prawdziwe. Przyciągnęło to rzesze matematyków i niematematyków, ale nikt nie przedstawił dowodu. We wczesnych latach osiemdziesiątych węgierski matematyk Paul Erdős oświadczył: Matematyka nie jest jeszcze gotowa na takie problemy.

Chcemy wiedzieć, czy ludzie czy komputery są lepsi w rozwiązywaniu takich problemów.

Marijn Heule

I prawdopodobnie ma rację, mówi Heule. Dla Heule urok Collatza to nie tyle perspektywa przełomu, ile rozwój technik automatycznego wnioskowania. Po pięciu latach majstrowania przy tym Heule i jego współpracownicy, Scott Aaronson i Emre Yolcu, opublikowali niedawno papier na serwerze preprintów arXiv. Chociaż nie udaje nam się udowodnić przypuszczenia Collatza, piszą oni, uważamy, że przedstawione tu idee reprezentują interesujące nowe podejście.

To szlachetna porażka, mówi Aaronson, informatyk z University of Texas w Austin. Porażka, ponieważ nie udowodnili przypuszczenia. Szlachetny, ponieważ poczynili postępy w innym sensie: Heule postrzega to jako punkt wyjścia do ustalenia, czy ludzie lub komputery są lepsi w udowadnianiu takich problemów.

Tłumaczenie matematyki na obliczenia

W przypadku wielu problemów matematycznych komputery są beznadziejne, ponieważ nie mają dostępu do ogromnego dorobku matematyki nagromadzonego przez historię. Ale czasami komputery przodują tam, gdzie ludzie są beznadziejni. Powiedz komputerowi, jak wygląda rozwiązanie — daj mu cel i dobrze zdefiniowaną przestrzeń wyszukiwania — a następnie z brutalną siłą komputer może je znaleźć. Chociaż to kwestia debata czy wyniki obliczeń stanowią sensowne dodatki do kanonu matematycznego. Tradycyjny pogląd jest taki, że tylko ludzka kreatywność i intuicja, poprzez koncepcje i idee, poszerzają zasięg matematyki, podczas gdy postępy w dziedzinie informatyki są często odrzucane jako inżynieria.

Powiązana historia

Algorytm ten potrafi określić, które sekwencje liczbowe uznają za interesujące dla człowieka Wynik sugeruje, że pewnego dnia maszyny można będzie wyszkolić w dostrzeganiu matematycznej elegancji i piękna.

W pewnym sensie komputer i hipoteza Collatza idealnie do siebie pasują. Po pierwsze, jak zauważa Jeremy Avigad, logik i profesor filozofii w Carnegie Mellon, pojęcie algorytmu iteracyjnego leży u podstaw informatyki – a sekwencje Collatza są przykładem algorytmu iteracyjnego, postępującego krok po kroku zgodnie z do deterministycznej reguły. Podobnie pokazywanie, że proces się kończy, jest częstym problemem w informatyce. Informatycy generalnie chcą wiedzieć, że ich algorytmy się kończą, co oznacza, że ​​zawsze zwracają odpowiedź, mówi Avigad. Heule i jego współpracownicy wykorzystują tę technologię, aby rozwiązać hipotezę Collatza, która tak naprawdę jest tylko problemem z zakończeniem.

Piękno tej zautomatyzowanej metody polega na tym, że możesz włączyć komputer i czekać.

Jeffrey Lagarias

Heule ma wiedzę specjalistyczną z narzędziem obliczeniowym zwanym solverem SAT – lub solverem spełniającym wymagania, programem komputerowym, który określa, czy istnieje rozwiązanie dla formuły lub problemu przy danym zestawie ograniczeń. Chociaż co najważniejsze, w przypadku matematycznego wyzwania, osoba rozwiązująca SAT najpierw potrzebuje przetłumaczenia lub przedstawienia problemu w sposób zrozumiały dla komputera. I jak mówi Yolcu, doktorant z Heule: Reprezentacja ma duże znaczenie.

Daleka droga, ale warto spróbować

Kiedy Heule po raz pierwszy wspomniał o walce z Collatzem za pomocą solwera SAT, Aaronson pomyślał: Nie ma mowy, żeby to zadziałało. Ale był łatwo przekonany, że warto spróbować, ponieważ Heule widział subtelne sposoby na przekształcenie tego starego problemu, które mogłyby go uelastycznić. Zauważył, że społeczność informatyków używa solwerów SAT, aby z powodzeniem znaleźć dowody zakończenia dla abstrakcyjnej reprezentacji obliczeń zwanej systemem przepisywania. To była długa droga, ale zasugerował Aaronsonowi, że przekształcenie hipotezy Collatza w system przepisywania może umożliwić uzyskanie dowodu zakończenia dla Collatza (Aaronson wcześniej pomagał przekształcić hipotezę Riemanna w system obliczeniowy, kodując ją w małym Turingu). maszyna). Tego wieczoru Aaronson zaprojektował system. To było jak zadanie domowe, zabawne ćwiczenie, mówi.

— W bardzo dosłownym sensie walczyłem z Terminatorem, a przynajmniej z twierdzeniem o zakończeniu.

Scott Aaronson

System Aaronsona uchwycił problem Collatza za pomocą 11 zasad. Gdyby badacze mogli uzyskać dowód terminacji dla tego analogicznego systemu, stosując te 11 reguł w dowolnej kolejności, to udowodniłoby, że przypuszczenie Collatza jest prawdziwe.

Heule próbował z najnowocześniejszymi narzędziami do udowodnienia zakończenia systemów przepisywania, które nie działały – było to rozczarowujące, jeśli nie tak zaskakujące. Narzędzia te są zoptymalizowane pod kątem problemów, które można rozwiązać w ciągu minuty, podczas gdy każde podejście do rozwiązania Collatza prawdopodobnie wymaga dni, jeśli nie lat obliczeń, mówi Heule. To dostarczyło motywacji do doskonalenia swojego podejścia i wdrożenia własnych narzędzi w celu przekształcenia problemu przepisywania w problem SAT.

Reprezentacja 11-zasadowego systemu przepisywania dla przypuszczenia Collatza.

MORSKI HEULE

Aaronson doszedł do wniosku, że znacznie łatwiej byłoby rozwiązać system bez jednej z 11 zasad — pozostawiając system podobny do Collatza, papierek lakmusowy dla większego celu. Postawił wyzwanie człowiek kontra komputer: wygrywa ten, kto jako pierwszy rozwiąże wszystkie podsystemy z 10 regułami. Aaronson próbował ręcznie. Heule wypróbowany przez solver SAT: zakodował system jako problem spełnialności — z jeszcze jedną sprytną warstwą reprezentacji, tłumacząc system na język zmiennych komputera, które mogą być zerami i jedynkami — a następnie pozwolił, aby jego solver SAT działał na rdzeniach , szukając dowodów wypowiedzenia.

Tutaj system podąża za sekwencją Collatza dla wartości początkowej 27-27 znajduje się w lewym górnym rogu kaskady ukośnej, 1 jest w prawym dolnym rogu. Jest 71 kroków, a nie 111, ponieważ naukowcy zastosowali inną, ale równoważną wersję algorytmu Collatza: jeśli liczba jest parzysta, to podziel przez 2; w przeciwnym razie pomnóż przez 3, dodaj 1, a następnie podziel wynik przez 2.

MORSKI HEULE

Obojgu udało się udowodnić, że system kończy się różnymi zestawami 10 reguł. Czasem było to przedsięwzięcie banalne, zarówno dla człowieka, jak i dla programu. Zautomatyzowane podejście Heule zajęło maksymalnie 24 godziny. Podejście Aaronsona wymagało znacznego wysiłku intelektualnego, zabierającego kilka godzin lub nawet dzień – jeden zestaw 10 zasad, których nigdy nie zdołał udowodnić, choć głęboko wierzy, że mógłby to zrobić przy większym wysiłku. W bardzo dosłownym sensie walczyłem z Terminatorem, mówi Aaronson – przynajmniej dowodzącym twierdzeniem o zakończeniu.

Od tego czasu Yolcu dostroił solver SAT, kalibrując narzędzie, aby lepiej pasowało do natury problemu Collatza. Te sztuczki zrobiły różnicę — przyśpieszyły sprawdzanie terminacji dla podsystemów z 10 regułami i skróciły czas pracy do zaledwie kilku sekund.

Główne pytanie, które pozostaje, mówi Aaronson, brzmi: A co z pełnym zestawem 11? Próbujesz uruchomić system na pełnym zestawie i po prostu działa w nieskończoność, co może nie powinno nas szokować, ponieważ to jest problem Collatza.

Jak widzi Heule, większość badań nad automatycznym wnioskowaniem przymyka oko na problemy, które wymagają wielu obliczeń. Ale na podstawie swoich wcześniejszych przełomów wierzy, że te problemy można rozwiązać. Inni mają przekształcony Collatz mam, masz, mamy, macie mają Ma przepisać system , ale jest to strategia używania precyzyjnie dostrojonego solvera SAT na dużą skalę z ogromną mocą obliczeniową, która może zyskać przyczepność do dowodu.

Do tej pory firma Heule przeprowadziła dochodzenie Collatz przy użyciu około 5000 rdzeni (jednostek przetwarzania zasilających komputery; komputery konsumenckie mają cztery lub osiem rdzeni). Jako badacz Amazon ma otwarte zaproszenie od Amazon Web Services, aby uzyskać dostęp do praktycznie nieograniczonych zasobów — aż do miliona rdzeni. Ale niechętnie używa znacznie więcej.

Potrzebuję jakiejś wskazówki, że to realistyczna próba, mówi. W przeciwnym razie Heule uważa, że ​​marnowałby zasoby i zaufanie. Nie potrzebuję 100% pewności, ale naprawdę chciałbym mieć dowody na to, że jest realna szansa, że ​​się uda.

Doładowanie transformacji

Piękno tej zautomatyzowanej metody polega na tym, że można włączyć komputer i czekać, mówi matematyk Jeffrey Lagarias z Uniwersytetu Michigan. Bawił się z Collatzem od około pięćdziesięciu lat i stał się strażnikiem wiedzy, kompilując bibliografie z adnotacjami i redagując książkę na ten temat, Ostateczne wyzwanie. W przypadku Lagarias zautomatyzowane podejście przywodziło na myśl: papier z 2013 r. matematyka z Princeton, Johna Hortona Conwaya, który rozważał, że problem Collatza może należeć do nieuchwytnej klasy problemów, które są prawdziwe i nierozstrzygalne – ale jednocześnie nie da się ich udowodnić. Jak zauważył Conway: …może być nawet tak, że twierdzenie, iż nie są one dowodliwe, nie jest samo w sobie dowodliwe i tak dalej.

Jeśli Conway ma rację, mówi Lagarias, nie będzie żadnego dowodu, zautomatyzowanego lub nie, i nigdy nie poznamy odpowiedzi.

Człowiekiem, który prawdopodobnie jest najbliżej, jest matematyk Terence Tao z Uniwersytetu Kalifornijskiego w Los Angeles. W 2019 roku Tao udowodnił, że hipoteza Collatza jest prawie prawdziwe dla prawie wszystkich liczb (prawie opiera się na dwóch różnych definicjach technicznych, jednak zgodnie z prostym angielskim znaczeniem).

Tao uważa, że ​​ludzki dowód na to przypuszczenie byłby bardziej matematyczny — dotarcie do czemu tego — niż dowód komputerowy. Ale posiadanie poważnego nierozwiązanego problemu w rękach zautomatyzowanego udowadniania może przyspieszyć rewolucyjną transformację w sposobie, w jaki matematycy wykorzystują pomoc komputerową w swojej pracy, mówi. Z tak trudnym do rozwiązania problemem jak ten, wykorzystamy wszelkie spostrzeżenia, jakie możemy uzyskać.

Heule i jego współpracownicy tak naprawdę chcą jednak scenariusza, w którym – stosując takie podejście, z tym problemem – komputer odnosi sukces tam, gdzie człowiek zawodzi, lub na odwrót. W tym momencie nie wiemy, czy te techniki są znacznie silniejsze niż to, co ludzie mogą zrobić ręcznie, czy też nie, czy też ludzie mogą robić rzeczy, których komputer nie może zrobić, mówi Heule. Chcemy wiedzieć, czy ludzie czy komputery są lepsi w rozwiązywaniu takich problemów.

W tym celu zobaczmy, kto pierwszy rozwiąże przypuszczenie Collatza.

ukryć