괴델을 들먹이며 강한 인공 지능이 불가능하다고 주장한 학자들

 

괴델의 불완전성의 정리(Gödel's incompleteness theorem, 1931)를 들먹이며 강한 인공 지능(strong AI)이 불가능하다고 주장하는 학자들이 여러 명 있었다. 강한 인공 지능을 정의하는 방식에는 여러 가지가 있지만, 쉽게 말하자면 시각과 청각도, 언어 인식도, 물리학 연구도, 소설 창작도, 음악 작곡도, 도덕 철학 연구도 인간만큼 잘 하는 인공 지능이다.

 

비슷한 류의 논거를 괴델의 증명이 발표되기도 전에 Post가 제시했다고 한다:

 

Absolutely Unsolvable Problems and Relatively Undecidable Propositions: Account of an Anticipation, Emil L. Post, 1921.

 

LucasPenrose가 제시했던 논거들이 가장 유명한 것 같다. 이 두 명은 괴델의 정리를 명시적으로 언급한다:

 

Minds, Machines and Gödel, John R. Lucas, 1959.

『황제의 새마음(The Emperor's New Mind: Concerning Computers, Minds, and the Laws of Physics)Roger Penrose, 1989(영어판).

Shadows of the Mind: A Search for the Missing Science of Consciousness, Roger Penrose, 1994.

 

Jerry Fodor는 『The Mind Doesnt Work That Way: The Scope and Limits of Computational Psychology(2000)』에서 기계가 인간을 결코 온전하게 흉내 낼 수 없다고 이야기하는데 괴델에 대해 깊이 이야기하는 것 같지는 않지만 LucasPenrose와 비슷한 이야기를 하는 것 같다.

 

Douglas R. Hofstadter는 『괴델, 에셔, 바흐: 영원한 황금 노끈(Gödel, Escher, Bach: An Eternal Golden Braid, 1979)』의 471~477쪽과 577~578쪽에서 Lucas의 주장을 반박한다(영어판 쪽수임).

 

Penrose에 대한 반박과 재반박에는 다음과 같은 것들이 있다:

 

Penrose is Wrong, Drew McDermott, http://www.calculemus.org/MathUniversalis/NS/10/09mcdermott.html

Minds, Machines, And Mathematics: A Review of Shadows of the Mind by Roger Penrose, David J. Chalmers, http://www.calculemus.org/MathUniversalis/NS/10/03chalmers.html

A Refutation of Penrose's Gödelian Case Against Artifcial Intelligence, Selmer Bringsjord & Hong Xiao, http://www.rpi.edu/~faheyj2/SB/SELPAP/PENROSE/pen.sel8.pdf

Penroses Gödelian argument, Solomon Feferman, http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.130.7027&rep=rep1&type=pdf

Beyond the Doubting of a Shadow: A Reply to Commentaries on Shadows of the Mind, Roger Penrose, http://www.calculemus.org/MathUniversalis/NS/10/01penrose.html

 

Pinker는 「So How Does the Mind Work?」에서 Fodor의 주장을 반박했다.

http://pinker.wjh.harvard.edu/articles/papers/So_How_Does_The_Mind_Work.pdf

 

 

 

 

 

괴델의 불완전성의 정리

 

괴델의 불완전성의 정리에 따르면 수학 명제들 중에 참임을 증명할 수 있는 명제도 있고, 거짓임을 증명할 수 있는 명제도 있지만, 참인데도 참이라는 것을 증명할 수 없는 명제도 있다. 참인 명제인데도 증명할 수가 없는 경우가 있다는 것은 당대의 많은 수학자들에게 커다란 충격을 안겨 주었다고 한다. 증명이 어려운 것이 아니라 아예 근본적으로 증명이 불가능한 것이다.

 

괴델의 불완전성의 정리를 온전히 이해하는 것은 수학을 전공하지 않은 사람에게는 거의 불가능에 가까울 정도로 어렵다. 그나마 증명 과정을 상세히 따라가면서도 상당히 쉽게 설명한 책이 있긴 하다. 하지만 괴델의 논문에 비해 쉬울 뿐이다. 그리고 엄밀한 증명(watertight proof) 과정을 보기 위해서는 괴델의 논문을 직접 읽어야 할 것이다.

 

『괴델, 에셔, 바흐: 영원한 황금 노끈(Gödel, Escher, Bach: An Eternal Golden Braid), Douglas R. Hofstadter, 1979, 1999(20주년 기념판).

『괴델의 증명(Gödel's Proof), Ernest Nagel, James Roy Newman, Douglas Hofstadter, 1958, 2002(개정판).

 

나는 이 두 권 중에 『Gödel, Escher, Bach』를 읽어 보았다. 이 책은 괴델의 정리의 증명 과정을 상세히 추적할 뿐 아니라 여러 가지로 읽어 볼 만한 책이다. 에셔의 모순적인 그림과 바흐의 음악도 소개하고 있으며, 마음과 인공 지능에 대해서 여러 가지를 다룬다. 또한 나는 이 책만큼 기발한 말장난이 많이 있는 책을 본 적이 없다.

 

하지만 한국어판 번역은 엉망이다. 나는 이 책의 번역을 비판한 적이 있다.

http://cafe.daum.net/Psychoanalyse/82Xi/22

 

나는 괴델의 정리를 들먹이며 강한 인공 지능이 불가능하다는 주장에 동의하지 않는다. 하지만 그렇다고 내가 그런 주장을 완벽하게 반박할 수 있을지도 의문이다. 괴델의 정리 자체가 너무 복잡하고 헷갈리기 때문에 온전히 이해하기 힘들다. 따라서 그것을 응용한 LucasPenrose의 논거를 반박하는 것도 상당히 어려울 가능성이 크다.

 

나는 괴델의 정리를 제대로 이해하기 위해 엄청난 시간을 투자할 생각이 없다. 그래서 그냥 내가 할 수 있는 만큼만 생각해 보고 이야기하려고 한다. 이것이 이 글과 이 글의 업그레이드판의 한계일 것이다.

 

 

 

 

 

참임을 증명하려고만 하는 컴퓨터

 

수학 명제를 증명하도록 하는 프로그램을 만드는 것은 어떤 의미에서는 참 쉽다. 프로그램을 돌릴 시간만 충분하다면 컴퓨터는 수학자가 증명할 수 있는 어떤 정리도 증명할 수 있다. 이것은 시간만 충분하다면 바둑의 신을 프로그래밍할 수 있는 것과 마찬가지다.

 

바둑에서 경우의 수는 361!(361*360*359*……*3*2*1)을 넘지 않을 것이다. 그 경우의 수를 몽땅 고려하면 완벽한 수를 둘 수 있다. 물론 361!이라는 수는 천문학적으로 크다라는 말도 어울리지 않을 정도로 상상을 초월할 정도로 큰 숫자다. 10!은 컴퓨터에게 그리 큰 수가 아니고 어쩌면 미래에는 20!까지 감당할 수 있을지 모르지만 361!은 절대 아니다.

 

수학의 증명 과정은 어떤 의미에서는 문자열에 불과하다. 따라서 길이가 1인 문자열의 모든 조합을 따져보고, 길이가 2인 문자열의 모든 조합을 따져보고, 길이가 3인 문자열의 모든 조합을 따져보는 식으로 계속 진행하다 보면 결국 참임을 증명할 수 있는 명제의 증명 과정에 이를 것이다. 물론 시간을 무한대에 가깝게 요구하는 프로그램은 실생활에서는 별로 쓸모가 없지만 여기에서는 원리적인 문제를 따지려고 하는 것이다.

 

어쨌든 위에서 소개한 프로그램을 만들었다고 하자. 이 프로그램에 거짓임이 이미 증명된 수학 명제를 증명하라고 요구했을 때 무슨 일이 벌어질까? 이 프로그램은 영원히 멈추지 않을 것이다. 왜냐하면 그 명제가 참임을 증명하려고만 끝없이 노력할 것이기 때문이다. 이 프로그램은 이 명제는 참이니까 증명할 수 있을 거야라는 강박관념에 사로잡힌 것이다.

 

실제로 비슷한 일이 수학계에서 벌어졌다. 에우클레이데스(Εκλείδης, Euclid, 유클리드)의 평행선 공리가 공리라고 보기에는 찜찜하다고 생각한 수학자들은 무려 2천년 동안이나 다른 공리들로부터 시작하여 평행선 공리가 참임을 증명하려고 했다.

 

아마추어 수학자들 중에는 컴퍼스와 자만 이용해서 각을 삼등분할 수 있는 방법을 찾아내려고 애쓰는 사람들도 많이 있다고 한다. 이미 불가능하다는 것이 증명되었는데도 말이다.

 

 

 

 

 

참과 거짓의 양방향으로 증명하려고 하는 컴퓨터

 

수학 명제들 중에는 거짓도 있다는 것을 고려하면 좀 더 나은 프로그램을 만들 수 있다. 이 프로그램은 위에서 소개한 것과 비슷하다. 하지만 한 가지 차이가 있다. 위에서는 문자열의 크기를 늘리면서 참임을 증명하려고만 하지만 이 프로그램은 참임을 증명하려고 시도하기도 하고 거짓임을 증명하려고 시도하기도 한다. 참이든 거짓이든 증명이 나오면 그 문자열(증명 과정)을 출력한다.

 

이 프로그램은 위에서 소개한 프로그램보다 훨씬 강력하다. 위에서 소개한 프로그램에 거짓 명제를 입력하면 끝없이 무모한 시도를 한다. 반면 이 프로그램은 참임을 증명할 수 있는 명제를 입력해도 증명 과정을 출력하고 거짓임을 증명할 수 있는 명제를 입력해도 증명 과정을 출력한다. 물론 경우에 따라서 시간이 너무 많이 걸려서 우주가 망한 다음에나 결과를 출력하겠지만 말이다.

 

하지만 이 프로그램에도 일종의 강박관념이 있다. 이 강박관념은 모든 제대로 된 수학 명제는 참이거나 거짓이기 때문에 참임을 증명할 수 있거나 거짓임을 증명할 수 있다는 생각으로 괴델의 정리가 발표되기 전까지는 많은 수학자들이 믿고 있었다. 따라서 참임을 증명할 수도 없고 거짓임을 증명할 수도 없는 명제를 입력하면 이 프로그램은 무한히 멈추지 않을 것이다.

 

괴델의 정리를 들먹이며 강한 인공 지능이 불가능하다고 보는 사람들은 이런 프로그램을 염두에 두고 있는 것 같다.

 

 

 

 

 

괴델의 정리를 고려한 프로그램

 

현대 수학자들은 제대로 된 수학 명제라 할지라도 증명도 반증도 할 수 없는 경우가 있다는 것을 잘 안다. 이 지식을 이용해서 프로그램을 개량할 수 있다.

 

이 프로그램은 문자열의 크기를 하나씩 늘려가면서 세 가지를 고려한다. 첫째, 그 문자열이 해당 명제가 참임을 증명하는 과정인지 따진다. 둘째, 그 문자열이 해당 명제가 거짓임을 증명하는 과정인지 따진다. 셋째, 그 문자열이 해당 명제가 참임을 증명할 수도 거짓임을 증명할 수도 없다는 것을 증명하는 과정인지 따진다. 셋 중 하나임이 확인된다면 그것을 출력한다.

 

참임을 증명할 수도 없고 거짓임을 증명할 수도 없는 명제의 경우 물론 컴퓨터는 그 명제가 참임을 증명할 수도 없고 거짓임을 증명할 수도 없다. 하지만 이 경우 사람도 그 명제가 참임을 증명할 수도 없고 거짓임을 증명할 수도 없다.

 

만약 사람이 어떤 명제가 참임을 증명할 수도 없고 거짓임을 증명할 수도 없다는 것을 증명할 수 있다면 컴퓨터가 그것을 하지 못하리라는 근본적인 이유는 없어 보인다. 물론 위에서 만든 무지막지한 프로그램의 경우에는 무한대에 가까운 시간이 걸릴지도 모른다. 하지만 지금 여기에서는 근본적인 가능성을 우선 따져보고 싶다. 그리고 프로그램을 아무리 개량해도 인간만큼 빠르게 그런 증명을 찾아낼 수는 없을 것이라는 점을 보장하는 근본적인 이유는 없어 보인다.

 

 

 

 

 

2010-05-15