Mimo to dla wielu badaczy sztucznej inteligencji ta formalna niemożliwość (nierozstrzygalność) nie była i nie jest przeszkodą w konstruowaniu maszyn cyfrowych dowodzących wielu ważnych twierdzeń. Okazuje się, że metoda algorytmiczna jako nieefektywna z logicznego punktu widzenia jest efektywna w praktyce. Jak to możliwe?

Po prostu sam algorytm nie wystarcza. Jego rygorystyczna moc musi być uzupełniona o inne jeszcze reguły dowodzenia. Pokazują to prace nad maszynami dowodzącymi, jakie prowadzili klasycy sztucznej inteligencji: Newell, Shaw, Simon czy Gelernter. Trzej pierwsi w 1958 roku napisali program zwany powszechnie Teoretykiem Logiki (Logic Theory Machine), który na JOHNNIAC-u był w stanie, dzięki napisanemu przez nich pierwszemu językowi maszynowemu do przetwarzania zestawów symboli (IPL), udowodnić kilka z twierdzeń epokowego dzieła logiki matematycznej "Principia Mathematica" B. Russella i A. Whiteheada. Szybko okazało się jednak, że mimo tej efektywności Teoretyka Logiki klasa twierdzeń matematycznych niemożliwych do udowodnienia przez niego jest większa niż udowodnionych algorytmicznie. Badacze zdali sobie sprawę, że w sytuacji rosnącej złożoności i kosztów obliczeń, jakie maszyna cyfrowa musi wykonać w celu rozpatrzenia wygenerowanego dowolnego ciągu wyrażeń, musi ona stosować dodatkowo metodę heurystyczną. Inaczej mówiąc, maszyna musi testować generowane ciągi pod kątem prawdopodobieństwa bycia właściwym twierdzeniem w dowodzie, a tego zwykły algorytm nie potrafi. Automatycznie stosowany algorytm musi być "inteligentnie" oceniony przez właściwą heurystykę. Robi tak zresztą człowiek, gdy dowodzi, spekuluje czy mówi. I tak powstał w 1958 roku słynny Rozwiązywacz Ogólnych Problemów (gdyby dosłownie przetłumaczyć jego oryginalną nazwę General Problem Solver), który był dziełem Newella i Simona. Łącząc w swym działaniu metody algorytmiczne i heurystyczne był, jak wierzyli jego twórcy, nie tylko konkretną maszyną, ale również maszynowym modelem inteligencji ludzkiej.

Krzemowy matematyk?

Szerokie zastosowanie maszyn cyfrowych w dowodzeniu matematycznych twierdzeń bardzo szybko przyczyniło się do postępu w programowaniu, jak również dało okazję matematykom, metodologom i filozofom nauki do nowego spojrzenia na naturę dowodu, a szerzej metody poznania prawd formalnych i przyrodniczych. Porzucono maszynowe dowodzenie w stylu Teoretyka Logiki jako bardzo proste (przekształcanie wyrażeń to nazbyt mechaniczna robota, nawet jak na maszynę cyfrową) i zabrano się za trudniejsze i ambitniejsze zadania.

Zastosowanie metod algorytmiczno-heurystycznych w programowaniu coraz szybszych komputerów nie kazało zbyt długo czekać na sukcesy. Jednym z bardziej spektakularnych było udowodnienie w 1976 roku przez amerykańskich matematyków K. Appela i W. Hakena tzw. problemu czterech barw, który mówił, że do sporządzenia mapy tak, aby obszary pomalowane na ten sam kolor nie stykały się, wystarczą cztery barwy. Hipotezę, że sprawdzi się to w odniesieniu do 2000 różnych map, obaj matematycy przetestowali, pisząc odpowiedni program dla komputera IBM 360, który po blisko tysiącu godzin pracy potwierdził ją (człowiek musiałby liczyć to przez ponad 10 milionów godzin!).

W istocie rzeczy komputerowy dowód problemu czterech barw nie sprowadził się do zwykłego obliczania, lecz rozłożenia go na szeregi podproblemów (przekładu na teorię grafów), dla których dopiero program komputerowy znajdował częściowe rozwiązania. Przy rozwiązywaniu tego zagadnienia maszyna cyfrowa współpracowała z człowiekiem - "widziała" całość ciągów dowodowych, testowała heurystycznie wysunięte hipotezy, zaś człowiek "podpowiadał" jej kierunek obliczeń. Taka komputerowa metoda dowodzenia jest swoistym dialogiem maszyny i człowieka.

Matematycy stosujący komputery w dowodzeniu czy sprawdzaniu hipotez twierdzą, że są one użytecznymi narzędziami poznawczymi, gdyż pozwalają nie tylko na szybkość liczenia, co również na skrótowość myślenia, twórcze wnikanie w istotę matematycznych zagadnień. Wizualizacja danych, rozbudowywanie graficznego interfejsu użytkownika i komputera daje niektórym z nich nawet okazję do mówienia o nowym rodzaju metod matematycznych - "wideodowodach". Symulacja komputerowa, wirtualizacja podstawowych tworów matematycznych: liczb, brył geometrycznych, funkcji, pozwala rzeczywiście na dogłębne ich poznanie. Naoczność odgrywa równie ważną rolę, jak samo obliczanie czy intuicyjny wgląd. Do starego sporu o naturę poznania matematycznego włączają się matematycy pracujący z komputerami i głoszący prymat zmysłowości i eksperymentu. "Gdyby nie możliwość zobaczenia obrazu, który mniej więcej odpowiadał temu, w co wierzyliśmy, nigdy by się nam nie powiodło" - stwierdził D. Hoffman, który zajmuje się badaniem szczególnych obiektów matematycznych - helikoid i ich powierzchni. "Odkryte" i "zobaczone" przez komputer zostały następnie udowodnione tradycyjnymi metodami formalnymi.

Nie wszyscy matematycy są zdania, że maszyny cyfrowe wnoszą istotny wkład do matematyki. Są tacy, którzy nie używają tych maszyn w ogóle (nawet jako edytorów tekstu!). Ich argumenty są przy tym równie ważne jak zwolenników skomputeryzowanej matematyki. Gdy w 1993 roku matematyk A. Wiles z Princeton University podał dowód słynnego Wielkiego Twierdzenia Fermata, które nie miało rozwiązania przez ponad 350 lat, to wywołał zrozumiałą sensację. Udało mu się podać poprawny dedukcyjny dowód, nie stosując przy tym szczególnie rozbudowanych obliczeń (które musiałaby wykonać maszyna). Wprawdzie do dzisiaj matematycy starają się zrozumieć i potwierdzić prawdziwość dowodu Wilesa, to on sam uważa, że stosowanie metod komputerowych nie jest w matematyce konieczne, ani nawet efektywne. Ich nauczenie się odciąga bowiem matematyka od prawdziwie twórczego, intuicyjnego, niemechanicznego myślenia.

I tak za sprawą komputerów odżywa w matematyce i w eksperymentalnych naukach przyrodniczych stary problem, który zajmował pitagorejczyków, Platona i innych: jaka jest natura poznania prawdy, czy dowodzić znaczy tyle samo co ujmować prawdę, czy widzieć można tyle samo co poznawać intuicyjnie, czy prawdy matematyczne są konstruowane (przez komputery) czy odkrywane?

Dr Marek Hetmański jest adiunktem na Wydziale Filozofii i Socjologii UMCS w Lublinie, zajmuje się komutacyjną koncepcją umysłu oraz społecznymi i psychologicznymi skutkami informatyki.

e-mail: [email protected]