跳至內容

邏輯理論家

維基百科，自由的百科全書

邏輯理論家（英語：Logic Theorist）是由艾倫·紐厄爾、司馬賀和約翰·克里夫·肖（英語：John Clifford Shaw）於1955年和1956年間編寫的計算機程序，是首個可以自動進行推理的程序，被稱為「史上首個人工智能程序」。[a]它最後證明了在懷特黑德和羅素合作撰寫的數學原理中首52個定理中的38個，在當中更是找到既新穎又優雅的證明。[2]

歷史

1955年，當紐厄爾和西蒙開始研發邏輯理論家時，人工智能領域尚未存在，就連術語「人工智能」也在第二年的夏天才開始使用。[b]

西蒙本身是一位政治科學家，當時他已經在研究官僚如何運作以及持續拓展他的有限理性理論（為此他後來得到諾貝爾獎）。研究商業組織時需要人工智能擁有像人類一樣決策和解決問題的洞察力。西蒙記得在20世紀50年代初向蘭德諮詢時看到一台打印機在印地圖，使用普通字母和標點符號作為符號。他意識到可以整理和排列符號的機器也可以模擬決策過程，甚至可以模擬人類的思考過程。[4][5]

打印地圖的程序是由研究物流和組織理論的蘭德公司科學家紐厄爾編寫的。對於紐厄爾來說，決定性的時刻是在1954年奧利弗·塞爾弗里奇（Oliver Selfridge）到蘭德來描述他在模式匹配方面的工作。觀看演示時，紐厄爾忽然明白簡單的可編程單元的交互如何實現複雜的行為，包括人類的智能行為。他後來說：「這一切都發生在一個下午。」[6]這是科學界人物頓悟的罕見時刻。

「我的感覺很清晰，這是一條新的道路，我將會走下去；我並不是每次也有這種感覺。」[7]

紐厄爾和西蒙開始討論教機器思考的可能性。他們的首個程序是要能夠證明數學定理的，於伯特蘭·羅素和阿爾弗雷德·諾思·懷特黑德撰寫的數學原理中可找到。他們還有來自蘭德的計算機程序員約翰·克里夫·肖（英語：John Clifford Shaw）幫忙開發該程序。（紐厄爾說「克里夫是三人中真正的計算機科學家」[8]）。首個版本是手工模擬的：他們將程序編寫到3x5卡片上，正如西蒙回憶的那樣：

在1956年1月，我讓我的妻子與三個孩子們跟一批研究生聚集在一起。我們給了小組的每個成員一張卡片，使每一張卡片將對應於計算機程序的一個組成部分……這就是大自然模仿藝術模仿自然。[9]

他們成功地證明了該程序可以像一位才華橫溢的數學家般成功地證明定理。然後，克里夫能夠在蘭德的聖莫尼卡工廠裡面的計算機上運行該程序。1956年夏天，約翰·麥卡錫、馬文·閔斯基、克勞德·香農和納撒尼爾·羅切斯特組織了一次會議，是關於「人工智能」（麥卡錫為了該會議而創造的術語）的。紐威爾和西蒙自豪地向小組介紹了邏輯理論家，但當聽眾反應冷淡時，他們感到有些驚訝。帕梅拉·麥科杜克寫道：「可以肯定當時除了紐維爾和西蒙之外，沒有人能夠感受到他們所做的事情具有長遠意義。」[10]西蒙承認「我們對這一切可能相當傲慢」[11]並補充道：

他們不想聽我們的介紹，我們也肯定不想聽到他們的回應：我們有東西要向他們展示！……在某種程度上，這是有點兒諷刺的，因為我們已經滿足了他們的期望；其次，他們沒有太在意它。[12]

邏輯理論家很快就證明了數學原理第2章中的前52個定理中的首38個，當中定理2.85的證明實際上比羅素和懷特黑德手抄的證明更優雅。西蒙能夠向拉塞爾本人展示新的證明，他「高興地回答」。[2]他們試圖將新的證明發表到《符號邏輯學報》中，但它被拒絕的理由是一個基本數學定理的新證明並不值得注意，顯然忽略了其中一個作者是計算機程序的事實。[13][2]

紐厄爾和西蒙建立了長久的合作夥伴關係，創建了其中一個最早的人工智能實驗室卡內基科技（英語：Carnegie Tech），並開發和發展了一系列富有影響力的人工智能程序和理念，包括通用解難器、Soar及認知統一理論。

邏輯理論家對人工智能的影響

邏輯理論家引入了幾個對人工智能研究至關重要的概念：

推理為搜索
邏輯理論家用到了搜索樹：搜索樹的根是最初的假設，每條分支都是推論，於是樹中的某個地方將會是該程序旨在證明的命題，每條分岔路都是一個形式證明（英語：Formal proof）——使用邏輯規則推導出的一系列陳述，這些陳述從假設到要證明的命題。
啟發式
紐厄爾和西蒙意識到搜索樹會指數增長，他們需要使用「經驗法則」來確定哪些路徑不太可能導出解決方案，然後再「修剪」一些分支。他們稱這規則「啟發式」，出自喬治·波利亞在其關於數學證明的經典著作《怎樣解題》（紐維爾曾在斯坦福大學攻讀過波利亞的課程）。[14]啟發式算法將成為人工智能研究的一個重要領域，並且仍然是克服指數增長搜索招致組合爆炸（英語：Combinatorial explosion）的重要方法。
列表處理
為了在計算機上實現邏輯理論，這三位研究人員開發了一種編程語言，名為資訊處理語言。

哲學意涵

帕梅拉·麥科杜克寫道，邏輯理論家「積極地展示了機器具有創意和智能」。[2]因此，它代表了人工智能發展和我們對智能的理解的里程碑。

1956年1月，西蒙着名地告訴給其中一班研究生，「聖誕節期間，艾倫·紐厄爾與我發明了一台會思考的機器」[15][16]，

並寫道：

我們發明了一種能夠以非數字方式思考的計算機程序，從而解決了古老的心物問題，解釋了由物質組成的系統如何具有心靈的屬性。[17]

「機器可以像人一樣有思想」的這種說法後來被哲學家約翰塞爾命名為「強人工智能」。到目前為止，它仍然是一個嚴肅的辯論主題。

邏輯理論家令帕梅拉·麥科杜克都受到啟發，一種新的心理理論——資訊處理模型（有時稱為心靈計算理論）因而首次亮相。她寫道，「這種觀點將成為他們後期工作的核心，並且在他們看來，這是二十世紀理解思想的核心，因為達爾文的自然選擇原則是在十九世紀理解生物學。」[18]紐厄爾和西蒙後來將這個提議正式化為物理符號系統假設。


筆記

  1. ^ 邏輯理論家通常被認為是第一個真正的人工智能計劃，儘管約翰·克里夫·肖（英語：John Clifford Shaw）的跳棋程序更早。克里斯托弗斯特拉奇（英語：Christopher Strachey）也在1951年寫了一個跳棋程序。[1]
  2. ^ 「人工智能」一詞是由約翰·麥卡錫在1956年達特矛斯會議的提案中創造的。據丹尼爾·克雷維爾（英語：Daniel Crevier）所言，是次會議「被普遍認為是新科學的官方誕生日期。」[3]

引文

  1. ^ Crevier 1993，第44頁.
  2. ^ 2.0 2.1 2.2 2.3 McCorduck 2004，第167頁.
  3. ^ Crevier 1993，第49–50頁.
  4. ^ Crevier 1993，第41–44頁.
  5. ^ McCorduck 2004，第148頁.
  6. ^ McCorduck 2004，第157–158頁.
  7. ^ McCorduck 2004，第158–159頁.
  8. ^ McCorduck 2004，第169頁.
  9. ^ Crevier 1993，第45頁.
  10. ^ McCorduck 2004，第124頁.
  11. ^ Crevier 1993，第48頁.
  12. ^ Crevier 1993，第49頁.
  13. ^ Crevier 1993，第146頁.
  14. ^ Crevier 1993，第43頁.
  15. ^ McCorduck 2004，第138頁.
  16. ^ CMU Libraries: Problem Solving Research. [2019-05-03]. （原始內容存檔於2020-02-18）. 
  17. ^ Crevier 1993，第46頁.
  18. ^ McCorduck 2004，第127頁.

參考

  • Crevier, Daniel (1993), AI: The Tumultuous Search for Artificial Intelligence, New York, NY: BasicBooks, ISBN 0-465-02997-3, pp. 44–46.
  • McCorduck, Pamela (2004), Machines Who Think (2nd ed.), Natick, MA: A. K. Peters, Ltd., ISBN 1-56881-205-1, pp. 161–170.
  • Russell, Stuart J.; Norvig, Peter (2003), Artificial Intelligence: A Modern Approach (2nd ed.), Upper Saddle River, New Jersey: Prentice Hall, ISBN 0-13-790395-2, p. 17.

外部連結

取自「https://zh.wikipedia.org/w/index.php?title=逻辑理论家&oldid=72891740」