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.

Anons: nowy numer "Notices of the AMS" o dowodach formalnych

Jako sie rzekło w tytule, najnowszy numer szczęśliwie dostępnego w internecie za darmo, czasopisma "Notices of the AMS" poświęcony jest formalnym i wspomaganym maszynowo systemom dowodzenia twierdzeń. Jakoś tak się złożyło, że jest to interesujące postscriptum do miłej pogawędki jaką parę miesięcy temu odbyła się tu. Można formalizację lubić, cenić, bądź uważać ją za płochą igraszkę czy wręcz perwersję intelektualną. Jednakże, kiedy się zastanowić i zdać sobie sprawę jak skomplikowany jest gmach matematyki, jak rośnie, można też wyobrazić sobie pewien rodzaj niepokoju, czy natręctwa jakie dręczy wielu matematyków, że gdzieś w jego środku tkwi jakiś błąd. Opisane w Notices metody to swoista terapia, ale i być może punkt wyjścia do matematyki przyszłości.
Oczywiście metody formalne wychodza poza matematykę. Bezawaryjny hardware czy software jest kluczem w wielkich przedsięwzięciach których stawką są ogromne pieniądze, życie ludzkie, środowisko naturalne. Wyniki badań nad formalnym wspomaganiem dowodzenia użyte do weryfikacji poprawności programów (każdy z nich jest przecież czymś w rodzaju teorii matematycznej) to być może jedyna droga by znaleźć tego Graala.
Co ciekawe wśród projektów tego typu - ładny akcent polski. Poczesne miejsce wśród nich zajmuje rozwijany od lat siedemdziesiątych w środowisku matematyków związanych a Uniwersytetem Warszawskim i Uniwersytetem w Białymstoku, ale w istocie będącym projektem międzynarodowym - system Mizar.
Mam i inne skojarzenie (też trochę szowinistyczne) a może i wspomnienie. Systemy weryfikacji twierdzeń opierają się na ciekawych systemach podstaw matematyki, konkurencyjnych w stosunku do teorii mnogości ZFC i lepiej od niej przystosowanych do "zmechanizowania". Ciekawe w tym kontekście wydaje mi się przeanalizowanie potencjału zapomnianych już dziś ale wielce oryginalnych systemów Leśniewskiego: prototetyki, ontologii i mereologii. W pewnym okresie swej pracy zawodowej (dawno dawno temu w odległej galaktyce) odbywałem dyskusję na temat ich potencjalnej przydatności w świecie komputerów. Niestety - wówczas też przyszedł kryzys, inwestorom zabrakło pieniędzy i wiary, fima splajtowała spektakularnie, a mnie potem zabrakło zapału i samozaparcia, żeby poważnie się ich nauczyć i rozwinąć nieśmiałe pomysły.

Formalizmy

Wśród wielu przyjemności, frajd i uciech jakimi usłane było i jest moje dotychczasowe życie, poczesne miejsce zajmuje praca w pewnej, nie istniejącej już firmie na B, gdzie za więcej niż godziwe pieniądze, z jednym tylko wyznaczonym celem - stworzyć coś olśniewającego - mogłem oddawać się przez parę miesięcy studiom i eksperymentom, za które nikt inny by mi nigdy nie zapłacił złamanego grosza. Oczywiście wszystko w nadziei że, ów szczytny cel zostanie osiągnięty.
Zagadnienia z jakimi walczyłem w owym czasie (pomijając wewnątrzkorporacyjną politykę, ową nieodłączną, mroczną towarzyszkę wszelkich dzieleń skór na niedźwiedziach) to software'owe systemy agentowe, protokoły komunikacyjne i socjalne owych agentów i przede wszystkim różnorakie wykorzystanie ontologii formalnych do komunikacji między agentami, organizacji ich społecznego życia i bazy dla ich rozumowania o świecie jaki im, biednym niewolnikom, chcieliśmy stworzyć.
Pojęcie ontologie formalne, nie jest do końca formalne i może znaczyć wiele rzeczy. Ogólnie jednak są to pewne teorie wyrażone w jakimś sformalizowanym języku plus pewne reguły wnioskowania. Ontologiczną częścią (tym co istnieje z punktu widzenia owych teorii) są stałe, predykaty, funkcje itp. Przy ich użyciu za pomocą stosownych operatorów logicznych i predykatów pochodzących z języka w którym zapisujemy ontologie (który dla niej samej staje się metajęzykiem) możemy opisać prawa świata którego formalną reprezentację konstruujemy. Na ogół czynimy to w ten sposób by zamodelować jakiś fragment istniejącego świata (zawodowiec w swoim żargonie powiedziałby, że dokonujemy konceptualizacji owego fragmentu), jakiejś konkretnej dziedziny, aktywności czy czegoś w tym rodzaju. Potem dzięki możliwościom formalnego wnioskowania, możemy w pewien sposób mechanizować rozumowania w naszej teorii - czy to by uzyskać rygorystyczne dowody pewnych własności owego świata, czy to po to, by mogła naszej konceptualizacji używać maszyna lub maszyny.
Zabawy z ontologiami formalnymi w świecie komputerów to względnie nowa rzecz. Wiązało się z nimi w czasach (historia nieustannie przyspiesza skoro o czymś co miało miejsce sześć lub siedem la temu mówimy "w owych czasach") wielkie, częściowo tylko spełnione nadzieje. Wokół tej idei osnuta była cała koncepcja "semantic web" promowana przez Berner's Lee i W3 Consortium, języki do modelowania ontologii jak DAML lub OIL, projekty jak SUO , czy w końcu technologie związane z serwisami internetowymi jak UDDI. Nie wspomnę już o dawniejszych i fantastycznych rozmachem pomysłach z kręgu sztucznej inteligencji w rodzaju Cyc.
Oczywiście nic tu nie jest naprawdę nowe. Formalizacja wnioskowań znana była już Arystotelesowi, który zostawił kodyfikację sylogizmów (fragmentu logiki zaledwie)- ziarnko z którego po stuleciach i perturbacjach wyrosła współczesna logika symboliczna.
Euklides dokonał formalnej konceptualizalizacji intuicji przestrzennych i praktycznej wiedzy mierniczej tworząc swój system geometrii. Gdyby go zapisać w sformalizowanym języku (co uczynił np. Hilbert) mielibyśmy nowoczesną formalną teorię matematyczną - z pewnego punktu widzenia więc ontologię formalną.
Patrząc na geometrię - najstarszą tak porządnie rozwiniętą naukę formalną - można dostrzec zawiłości związane z modelowaniem rzeczywistości w języku. Np. byty które egzystują w świecie geometrii Euklidesa to punkty i proste. Nie mające odnośnika w rzeczywistości którą geometria stara się z pewnego punktu widzenia opisać, żadnych odnośników. Możemy scierpieć dzisiaj, bogatsi o bez mała dwa tysiące lat rozwoju matematyki, że są to byty abstrakcyjne - ale rozwiązując zadanie geometryczne i tak będziemy bazgrać na papierze figury. Co więcej, pojęcie punktu, choć łatwo przystaniemy na to, że jest to dobra i zręcznie dobrana intuicja - dręczy nas w różnych tam paradoksach Zenona z Elei, odbija się czkawką w piętrowych konstrukcjach continuum itp. Alfred Tarski - współtwórca Teorii Modeli (a jakże), działu matematyki (właściwie metamatematyki) który relację między matematyczną rzeczywistością i jej formalizmem bada stworzył np. system geometrii, gdzie bytem pierwotnym nie był punkt ale kula i dla takiego systemu podał aksjomatykę. W takim systemie nie istnieją z kolei punkty - tylko ciała rozciągłe. Dziś niektórzy naukowcy próbujący nauczyć komputery rozumowań na temat przestrzeni sięgają po ową geometrię jako ontologię przestrzeni.
Odkrycia współczesnej fizyki i teorie próbujące je wyjaśnić też coraz częściej sięgają po geometrię w której pojęcie punktu traci sens. Tak jest np. z geometrią nieprzemienną Connesa modnym, trudnym i ważnym ostatnio działem matematyki, z którą również pewna grupa fizyków teoretyków wiąże wielkie nadzieje.
Formalizacja to także docenione narzędzie w rękach filozofów usiłujących przedrzeć się przez pułapki i śliskości języka naturalnego. Miast używać tego niedoskonałego narzędzia, rekonstruują pojęcia i relacje między nimi w postaci formalnej. Czy badając ten swój sformalizowany twór oglądają to o czym myśleli ? Znajdują w nim rzeczy nowe i zaskakujące? Teoretycznie powinni. Przecież geometria Euklidesa pozostaje żywa interesująca i zaskakująca do dzisiaj mimo osczędności pojęć i aksjomatyki.
Takiego "uformalnienia" pewnych rozważań na gruncie epistemologii fenomenalistycznej dokonał Rudolf Carnap w 1928 roku w pracy Der logische Aufbau Der Welt idąc w ślady Bertranda Russela i jego Our Knowledge of External World. To spojrzenie jest z kolei punktem wyjścia do ciekawej próby rekonstrukcji pojawienia się logiki, abstrakcyjnej myśli i w końcu nauki z czysto biologicznych predyspozycji którą podjął Willard Van Orman Quine w książce pod polskim tytułem Od bodźca do nauki. Właśnie zacząłem ją czytać i to ona sprowokowała mnie do dzisiejszego postu i wspominek z firmy na B.