#2. AI와 인간의 대결(6) : 수학 원리의 증명

#6. 자동화된 추론 논리 이론가 (Logic Theorist)

아서 사무엘(혹은 아서 새뮤얼, Arthur Lee Samuel)이 체커 프로그램을 시연하던 시기에 또 하나의 첫 번째 인공지능 프로그램이 탄생하고 있었습니다. 바로 게임분야가 아닌, 수학 원리의 증명을 인간과 같이 할 수 있을지를 검토한  "논리이론가 (LT, Logic Theorist 혹은 Logic Theory Machine) "입니다. 이 프로그램은 1956년도에 첫 
 시연을 가졌습니다.

 

논리 이론가는 앨런 뉴얼(혹은 앨런 뉴웰, Allen Newell : 1927년 ~ 1992년), 허버트 알렉산더 사이먼(Herbert A. SimonHerbert Alexander Simon : 1916년 ~ 2001년) 및 클리프 쇼(John Clifford Shaw or Cliff Shaw  : 1922년~1991년)가 1956년에 작성한 컴퓨터 프로그램입니다 . 자동화된 추론(automated reasoning)을 수행하기 위해 의도적으로 설계된 최초의 프로그램으로 "최초의 인공 지능 프로그램"이라고도 합니다. 

최초의 인공지능 프로그램

 

이 프로그램은 수학원리(Principia Mathematica : Alfred North Whitehead과 Bertrand Russell의 저서)에서 처음 52개의 정리 중에서 38개를 증명하고 일부에서는 수작업으로 사람이 만든 증명보다 좀 더 멋진 증명을 찾아냈습니다. 사람처럼 수학 원리를 증명할 수 있다는 부분이 획기적입니다.

 

앨런 뉴얼과 허버트 알렉산더 사이먼(이하 '허버트 사이먼')은 지난번 소개드린 인공지능의 용어가 탄생하게 된 존 메카시(John McCarthy)가 주도했던 다트머스 워크숍에 참석했던 인물들입니다. 여기에 RAND Corporation(랜드 연구소, 미국의 대표적인 싱크 탱크 비영리 법인)의 시스템 프로그래머였던 클리프 쇼가 개발에 공동으로 참여하여 논리 이론가 프로그램을 탄생시킨 것입니다.

 

1955년 앨런 뉴얼과 허버트  사이먼이 논리 이론가에 대한 작업을 하기 시작했을 때 인공지능 분야는 아직 본격적으로 태동하지 않았습니다. 이들은 1956년 6월 15일 발행된 Rand Corporation 보고서 P-868에서 "논리 이론 기계(The Logic Theory Machine. A Complex Information Processing System)"라는 제목으로 논리 이론가를 처음으로 설명했습니다.

앨런 뉴얼과 허버트 사이먼의 Logic Theory Machine 보고서 

 

 

논리 이론가는 인공지능 연구의 핵심이 될 몇 가지 개념을 도입했습니다.

첫 번째는 추론을 통한 탐색입니다. 검색 트리(search tree)를 기반으로 탐색을 구현했는데, 검색 트리에서 Root는 초기 가설이었고 각 분기(Branch)는 논리 규칙에 기반한 추론이었습니다. 트리 어딘가에는 프로그램이 증명하고자하는 명제(proposition)가 있는 형태였습니다. 목표를 따라가는 경로가 수학에서의 증명(Proof)이 였습니다. 이는 각각의 논리 규칙을 사용해서 추론되는 증명할 명제에 대한 가설에 대한 표현들입니다.

두 번째는 경험적 방법론(휴리스틱, Heuristics)을 도입한 것입니다. 이들은 경험법(Rule of Thumb)으로 트리가 기하급수적인 탐색공간을 마련하므로, 일부 분기(Branch)를 자르기(Trim)를 해야한다는 것을 알고 적용했습니다. 이러한 규칙을 "휴리스틱(heuristics)"이라고 불렀습니다. 휴리스틱은 인공지능 연구의 중요한 영역이며, 기하급수적으로 증가하는 검색의 조합폭발(혹은 조합 확산 : 문제 복장성이 급격한 증가하는 것. Combinatorial explosion)을 극복하는 중요한 방법으로 남아 있습니다.

세 번째는 목록 형식의 데이터 처리방법인 리스트 프로세싱입니다.  클리프 쇼를 포함하여 이들 세 명의 연구원은 컴퓨터에서 논리 이론가를 구현하기 위해 프로그래밍 언어인 IPL(어셈블리 언어 스타일의 프로그래밍 언어, Information Processing Language)을 개발했습니다. 이 프로그래밍 언어는 나중에 AI 연구원들에 의해 종종 사용하는 중요한 언어인 존 메카시(John McCarthy)의 Lisp 프로그래밍 언어의 기반이 될 동일한 형태의 기호 목록 처리를 사용했습니다.

 

허버트 사이먼은  1956년 1월 대학원 수업에서, 자신이 앨런 뉴얼과 함께 사고하는 머신(Thinking Machine)을  발명했다고 말했습니다. 이는 철학적 관점에서 논리 이론가를 시스템이 기호와 휴리스틱으로 인간 사고의 모델을 흉내 내는 것으로 볼 수 있다는 측면을 강조한 것입니다.

해당 논문에서의 추론의 특성과 학습 프로세스의 설명 

---

이 논리 이론가가 좀 더 발전하여, 나중에는 인간의 문제해결 과정을 모형화한 프로그램인  '일반문제해결자 (General Problem Solver, 1958)'로 나옵니다.

앨런 뉴얼은 인공지능과 인지심리학의 기초를 쌓은 공헌을 인정받아 허버트 사이먼과 함께 1975년에 튜링상을 받았습니다. 앨런 뉴얼과 허버트 사이먼은 지속적인 파트너십을 맺었습니다. 그들은 Carnegie Mellon University에 인공 지능 실험실을 설립하고 50년대 후반과 60년대에 걸쳐 일련의 중요한 프로그램과 이론적 통찰력을 제공했습니다.

문제를 해결하기 위해 기호와 휴리스틱을 이용했고, 이를 통해 기계가 마음을 반영하는 인간 사고의 모델이라는 것을 증명하고자 했던 분들이 바로 앨런 뉴얼과 허버트 사이먼이였습니다.

 

"물리적 심볼 시스템은 일반적인 지능적 행동에 필요하고 충분한 수단을 가지고 있습니다.(A physical symbol system has the necessary and sufficient means for general intelligent action.)"
- Allen Newell and Herbert A. Simon -

논리 이론가 만평