Sprowokowany zabawnym artykułem...

Ponieważ zapronumerowałem wieści o świeżo pojawiających się w niektórych działach serwisu arXiv artykułach, trzymam rękę na pulsie. Przedwczoraj właśnie serwis zaanonsował mi, jak się okazało zabawny i ciekawy, artykulik niejakiego Dorona Zeilbergera. Tytuł jest nieco krzykliwy: "Teaching the Computer how to Discover(!) and then Prove(!!) (all by Itself(!!!)) Analogs of Collatz's Notorious 3x+1 Conjecture".
Zanim po krótce objaśnię o czym ten artykuł, podywaguję (co lubię najbardziej). Zeilberger jest m.in. współautorem (z Petkovsekem i Wilfem) głośnej swego czasu książki "A=B" . W książce tej o ile dobrze pamiętam ćwiczy się intensywnie (choć nie jedynie) automatyczne odkrywanie i dowodzenie identyczności różnych sum z symbolem Newtona w roli głównej. Jest to pewna forma uprawiania wspomaganej komputerowo matematyki w której nie walczy się o ogólność podejścia komputerowego (np. żeby maszyna potrafiła twórczo podejść do udowodnienia bądź nawet odkrycia dowolnego twierdzenia jakiejś teorii), ale raczej eksploatuje się pewne szczególne podejście które daje dużo dobrych twierdzeń jakiejś szczególnej postaci - np. tożsamości - powielając bądź lekko wariując jedną metodę.
W ogóle, to jest historia, która mnie trochę bawi z tymi algorytmami z książki "A=B". Rosyjski matematyk Jurij Matiasiewicz, sławny dzięki zadaniu coup de grace słynnemu X problemowi Hilberta, w pracach z końca lat 90-tych (choćby tu ) pokazał metody tłumaczenia twierdzeń z teorii liczb na tożsamości z użyciem symbolu Newtona, w typie zbliżonym do tych, o których mowa u Zelbergera, Wilfa i Petkoveska. W niektórych pracach wprost nawiązuje on do książki "A=B" wyrażając nadzieję, że uda się kiedyś dzięki jego translacjom, przez (automatyczne) udowodnienie takich tożsamości dowodzić twierdzeń o innej bardziej interesującej matematycznie treści. W szczególności, w pracy Matjasiewicza, którą tu linkuję zajmuje się on translacją do tożsamości dwumiennych starej hipotezy zwanej "problemem Collatza", czasem "problemem Ulama", względnie "problem 3x+1". Zagadnienie jest dobrze znane i szeroko opisywane nie będę go więc tu przedstawiał w szczegółach.
Zeilberger, że zatoczę w moich dygresjach koło, we wspomnianym na początku artykule zajmuje się rodziną problemów formalnie podobnych do problemu Collatza, analizując strukturę dowodów (podanych przez ludzi) dla pewnych przypadków szczególnych. Następnie, pokazuje w jaki sposób można przymusić komputer do postępowania według podobnego schematu: generowania konkretnych przypadków zagadnienia za pomocą metod "rachunkowych" , znajdowania wzorca spełanianego przez przypadki satysfakcjonujące, tworzenia na tej bazie hipotezy (pewnej z góry znanej twórcy programu postaci, ale zależnej od wielu parametrów ustalonych przez komputer w krokach poprzednich), generowania (jeśli się uda) dowodu, który też jest konstruowany według pewnego szczególnego, znanego apriori schematu. Konkretna realizacja tego schematu jest jednak wyszukiwana przez komputer. W efekcie, maszyna wypluwa szereg twierdzeń i dowodów o całkiem interesującej matematycznie treści, wysycając potencjał tkwiący w zaszytych w algorytmie schematach.
Poruszam się tu na dużym poziomie ogólności więc po szczegóły odsyłam bezpośrednio do wzmiankowanej pracy. Nie jest to ani typowa praca matematyczna, ani lektura trudna pojęciowo a i napisana jest leciutko. Sądzę, że jest, bez wielkiego trudu, do przejścia dla tzw. zdolnego licealisty. Niezbyt zawiłe ćwiczenie z nierówności trójkąta, indukcji matematycznej i zrozumienia sposobu działania algorytmów.
Kilka myśli, a może i jakiś morał.
Po pierwsze, w typowym myśleniu o automatycznym dowodzeniu twierdzeń rozważa, się mniej więcej coś takiego:
Przestrzenią w której się poruszamy jest skierowany graf (drzewo właściwie) możliwych wywodów, węzłami którego są wywody, tj. zbiory (być może puste) stwierdzeń.
Wywody w węzłach mają tę własność, że wywód w węźle na końcu strzałki jest powtórzeniem wywodu z początku strzałki z dopisanym aksjomatem lub stwierdzeniem będącym logiczną konsekwencją stwierdzeń wchodzących w skład wywodu z początku strzałki.
Abstrakcyjnie pojęty algorytm automatycznego dowodzenia przeszukuje według pewnej strategii owe drzewo starając się znaleźć nasze twierdzenie jako jeden z elementów wywodu w którymś węźle¹. Pułapka leży w tym, że przestrzeń poszukiwań (ów graf) jest ogromny i startegie prostackie, nie mają szans. Strategie wyrafinowane mają wbudowaną w siebie jakąś podpowiedź (heurystykę). To co proponuje Zeilberger to, w tych terminach, bardzo silna heurystyka, która ryzykując chybienie celu przeszukuje bardzo mały ale obiecujący obszar przestrzeni. Ta strategia może nieźle działać: jesteśmy w stanie zidentyfikować pewne "metody" czy "schematy" dowodzenia które aplikują się w wielu sytuacjach. Jesteśmy w stanie podać sposoby generowania skomplikowanych ale schematycznych prób dowodzenia czegoś. Np. (ograniczając sie jedynie do hasła "indukcja matematyczna"), przez piętrowe dowody indukcyjne albo przez stopniowe wzmacnianie hipotez indukcyjnych jak w pracy Zeilbergera. W takich sytuacjach mechanizacja jest możliwa i może być bardzo efektywna. Oczywiście czytelność takich dowodów jest problematyczna: człowiek może nie być w stanie ogarnąć, dajmy na to, kilkunastopiętrowej indukcji. Może być tak oczywiście, że jakieś teorie wyższego poziomu pozwolą zrezygnować z niezrozumiałych dowodów na rzecz prostszych, z wyższego punktu widzenia niejako przeprowadzonych (ale wtedy same te teorie ukryją w sobie prawdopodobnie całą złożoność). Ale raczej sądzę, że zagadnienia typu np. hipotezy Robbinsa staną się jednak domeną komputerów. Pozostaje wierzyć w maszyny i cieszyć się wynikami. Nie można apriori wykluczyć, ze są twierdzenia, które po prostu dadzą się tylko tak udowodnić - jeśli chcemy więc znać prawdę być może będziemy skazani, również w matematyce, na zaufanie do maszyn.
Ciekawym aspektem pracy Zeilbergera jest też mechanizacja procesu stawiania hipotez. Tu do indukcji matematycznej dochodzi indukcja empiryczna, ale to zupełnie inny temat, zresztą lekko tylko tam poruszony. To zagadnienie - moim zdaniem centralne dla rozwoju tzw. Sztucznej Inteligencji - zasługuje na osobne potraktowanie, na co, w tym sprowokowanym lekturą pracy Zeilerbergera poście, nie znajduję miejsca (ale w przyszłości, kto wie...).
Dołączam się w końcu do apelu autora artykułu: może któryś z nadpobudliwych intelektualnie młodych kolegów, zamiast myśleć o hackowaniu kolejnej strony czy ściąganiu zabezpieczeń z kolejnego programu, zająłby się uczciwszym, a stawiającym wyższe poprzeczki jego umiejętnościom, zajęciem i podjął się dalszych eksperymentów w duchu tych o których mowa w dyskutowanej pracy? Autor tego bloga pewnie chciałby, ale jeśli zdoła to uczynić to chyba dopiero na emeryturze (jeśli dożyje i nie będzie musiał żebrać).


¹Często konstruuje się ten graf inaczej: wychodzi się od zaprzeczenia twierdzenia wyjściowego, aksjomatów i zachowując regułę wynikania z poprzedzajacych wywodów szuka się sprzecznosci.