Teoretyk logiki - Logic Theorist

Logic Theorist to program komputerowy napisany w 1956 roku przez Allena Newella , Herberta A. Simona i Cliffa Shawa . Był to pierwszy program celowo zaprojektowany do automatycznego wnioskowania i jest nazywany „pierwszym programem sztucznej inteligencji ”. To ostatecznie udowodnić 38 z pierwszych 52 twierdzeń Whitehead i Russell „s Principia Mathematica , i znaleźć nowe i bardziej eleganckie dowody dla niektórych.

Historia

W 1955 roku, kiedy Newell i Simon rozpoczęli pracę nad teoretykiem logiki, dziedzina sztucznej inteligencji jeszcze nie istniała. Nawet sam termin („sztuczna inteligencja”) nie zostałby ukuty aż do następnego lata.

Simon był politologiem, który już stworzył klasyczną pracę na temat funkcjonowania biurokracji, a także rozwinął swoją teorię ograniczonej racjonalności (za którą później otrzymał Nagrodę Nobla ). Badanie organizacji biznesowych wymaga, podobnie jak sztuczna inteligencja , wglądu w naturę rozwiązywania ludzkich problemów i podejmowania decyzji . Simon pamięta konsultacje w RAND Corporation na początku lat pięćdziesiątych i widział drukarza, który pisze mapę, używając zwykłych liter i znaków interpunkcyjnych jako symboli. Zdał sobie sprawę, że maszyna, która może manipulować symbolami, może równie dobrze symulować podejmowanie decyzji, a być może nawet proces ludzkiego myślenia.

Program, który wydrukował mapę, został napisany przez Newella, naukowca RAND badającego teorię logistyki i organizacji . Dla Newella decydującym momentem był rok 1954, kiedy Oliver Selfridge przyszedł do RAND, aby opisać swoją pracę nad dopasowywaniem wzorców . Oglądając prezentację, Newell nagle zrozumiał, w jaki sposób interakcja prostych, programowalnych jednostek może osiągnąć złożone zachowanie, w tym inteligentne zachowanie istot ludzkich. „To wszystko wydarzyło się w ciągu jednego popołudnia” – powiedział później. Był to rzadki moment naukowego objawienia.

„Miałem takie poczucie jasności, że to była nowa ścieżka, którą zamierzałem zejść. Nie miałem tego odczucia zbyt wiele razy. Jestem dość sceptyczny, więc zwykle nie odchodzę całkowicie pochłonięty – bez istnienia z dwu- lub trzypoziomową świadomością, tak że pracujesz, i świadomym tego, że pracujesz, świadomym konsekwencji i implikacji, normalnym sposób myślenia. Nie. Całkowicie pochłonięty przez dziesięć do dwunastu godzin.

Newell i Simon zaczęli rozmawiać o możliwości nauczenia maszyn myślenia. Ich pierwszym projektem był program, który może okazać się twierdzeń matematycznych, takich jak te stosowane w Bertranda Russella i Alfred North Whitehead „s Principia Mathematica . W opracowaniu programu skorzystali z pomocy programisty komputerowego Cliffa Shawa , również z firmy RAND. (Newell mówi, że „Cliff był prawdziwym informatykiem z całej trójki”).

Pierwsza wersja była symulowana ręcznie: program zapisali na kartach 3x5 i, jak wspominał Simon:

W styczniu 1956 roku zebraliśmy żonę i troje dzieci wraz z kilkoma doktorantami. Każdemu członkowi grupy rozdaliśmy jedną z kart, tak aby każda stała się w efekcie elementem programu komputerowego... Oto natura imitująca sztukę naśladującą naturę.

Udało im się pokazać, że program może z powodzeniem dowodzić twierdzeń, a także utalentowanego matematyka. W końcu Shaw był w stanie uruchomić program na komputerze w zakładzie RAND w Santa Monica.

Latem 1956 roku John McCarthy , Marvin Minsky , Claude Shannon i Nathan Rochester zorganizowali konferencję na temat tego, co nazwali „ sztuczną inteligencją ” (termin ukuty na tę okazję przez McCarthy'ego). Newell i Simon z dumą przedstawili grupie teoretyka logiki i byli nieco zaskoczeni, gdy program spotkał się z letnim przyjęciem. Pamela McCorduck pisze, że „dowody są takie, że nikt oprócz Newella i Simona nie wyczuwał dalekosiężnego znaczenia tego, co robili”. Simon wyznaje, że „prawdopodobnie byliśmy w tym wszystkim dość aroganccy” i dodaje:

Nie chcieli słyszeć od nas, a my na pewno nie chcieliśmy słyszeć od nich: mieliśmy im coś do pokazania ! ... W pewnym sensie było to ironiczne, ponieważ zrobiliśmy już pierwszy przykład tego, o co im chodziło; a po drugie, nie zwracali na to większej uwagi.

Teoretyk logiki wkrótce udowodnił 38 z pierwszych 52 twierdzeń w rozdziale 2 Principia Mathematica . Dowód twierdzenia 2.85 był w rzeczywistości bardziej elegancki niż dowód tworzony mozolnie ręcznie przez Russella i Whiteheada. Simon był w stanie pokazać nowy dowód samemu Russellowi, który „odpowiedział z zachwytem”. Próbowali opublikować nowy dowód w The Journal of Symbolic Logic, ale został on odrzucony ze względu na to, że nowy dowód elementarnego twierdzenia matematycznego nie był godny uwagi, najwyraźniej pomijając fakt, że jeden z autorów był programem komputerowym.

Newell i Simon nawiązali trwałe partnerstwo, zakładając jedno z pierwszych laboratoriów sztucznej inteligencji w Carnegie Institute of Technology i rozwijając szereg wpływowych programów i pomysłów związanych ze sztuczną inteligencją , w tym GPS , Soar i ich ujednoliconą teorię poznania .

Wpływ teoretyka logiki na sztuczną inteligencję

Teoretyk logiki przedstawił kilka koncepcji, które miałyby kluczowe znaczenie dla badań nad sztuczną inteligencją:

Rozumowanie jako wyszukiwanie
Teoretyk logiki zbadał drzewo poszukiwań : korzeń był wstępną hipotezą , każda gałąź była dedukcją opartą na regułach logiki. Gdzieś na drzewie był cel: propozycja, którą program zamierzał udowodnić. Ścieżka po gałęziach, która prowadziła do celu, była dowodem  – serią twierdzeń, z których każde wydedukowano za pomocą reguł logiki, które prowadziły od hipotezy do twierdzenia do udowodnienia.
Heurystyka
Newell i Simon zdali sobie sprawę, że drzewo wyszukiwania będzie rosło wykładniczo i że muszą „przyciąć” niektóre gałęzie, używając „zasad praktycznych”, aby określić, które ścieżki prawdopodobnie nie doprowadzą do rozwiązania. Nazwali te doraźne zasady „ heurystyka ”, używając terminu wprowadzonego przez George Pólya w swojej klasycznej książce o dowodu matematycznego , jak go rozwiązać . (Newell uczęszczał na kursy od Pólyi w Stanford ). Heurystyka stałaby się ważnym obszarem badań nad sztuczną inteligencją i pozostaje ważną metodą przezwyciężenia trudnej do opanowania eksplozji kombinatorycznej gwałtownie rosnących wyszukiwań.
Przetwarzanie listy
Aby wdrożyć Logic Theorist na komputerze, trzej badacze opracowali język programowania, IPL , który wykorzystywał tę samą formę przetwarzania list symbolicznych, która później stała się podstawą języka programowania McCarthy's Lisp , ważnego języka nadal używanego przez badaczy sztucznej inteligencji.

Implikacje filozoficzne

Pamela McCorduck pisze, że teoretyk logiki był „pozytywnym dowodem na to, że maszyna może wykonywać zadania uważane dotychczas za inteligentne, twórcze i wyjątkowo ludzkie”. I jako taki stanowi kamień milowy w rozwoju sztucznej inteligencji i ogólnie w naszym rozumieniu inteligencji.

Simon w styczniu 1956 roku powiedział na zajęciach dla absolwentów: „W Boże Narodzenie Al Newell i ja wynaleźliśmy myślącą maszynę” i pisał:

[Wynaleźliśmy] program komputerowy zdolny do myślenia nienumerycznego iw ten sposób rozwiązaliśmy czcigodny problem umysł-ciało , wyjaśniając, w jaki sposób system złożony z materii może mieć właściwości umysłu.

To stwierdzenie, że maszyny mogą mieć umysły tak jak ludzie, zostało później nazwane przez filozofa Johna Searle'a „ silną sztuczną inteligencją ” . Do dnia dzisiejszego pozostaje poważnym tematem debaty.

Pamela McCorduck widzi także w Logic Theorist debiut nowej teorii umysłu, modelu przetwarzania informacji (czasami nazywanego komputacjonizmem ). Pisze, że „ten pogląd stałby się kluczowy dla ich późniejszej pracy i, ich zdaniem, tak samo kluczowy dla zrozumienia umysłu w dwudziestym wieku, jak zasada doboru naturalnego Darwina była dla zrozumienia biologii w dziewiętnastym wieku”. Newell i Simon później sformalizowali tę propozycję jako hipotezę fizycznych systemów symboli .

Uwagi

Cytaty

Bibliografia

Linki zewnętrzne