ChatGPT에 코드짜기나 코드 오류 찾기 등 다양한 기능이 있다는 건 알고 있었는데, 논리식 증명도 하는 줄은 처음 알았네요. (P→Q)&(Q→P)와 (P&Q)∨(~P&~Q)가 논리적 동치라는 걸 ChatGPT한테 증명해 달라고 했더니, 우선 진리표를 그려서 증명하더라고요.
그 다음은 자연연역을 사용해서 그걸 다시 증명하라고 했더니 이렇게 나오네요.
다른 자연연역 스타일로는 증명을 못하냐고 물어보았더니, 논리학 입문 교재에서 흔히 나오는 피치 스타일의 자연연역을 제시하네요.
아주 신통방통한 게 마음에 듭니다!
음... 그런데 ChatGPT를 완전히 신뢰하기는 어렵겠네요. 성능을 시험해 보려고 ~(~A ∨ ~B)가 (A ∧ ~B)로 되어야 한다고 헛소리를 해봤더니, 그걸 덥썩 받아들이네요... 너가 왜 사과하는 거니...
ChatGPT 완전 구라쟁이에요. 믿을 수 없는 놈입니다. 예를 들어, 어떤 주제 던져주고 그 주제에 해당하는 가장 많이 인용되는 논문들 10개 알려주라고 하면 막 있는 것처럼 떠들어대는데 찾아보면 없는 애들이 대부분이더라구요.
심지어 없는 논문 요약해보라고 하면 해줍니다. -_-; 나중에 이걸 주제로 논문을 써볼까해요. Lying of AI? 라는 가제로 AI가 거짓말을 할 수 있다는 주장을 검토해볼까 해요. 미디어에서는 AI가 일종의 환영Hallucination을 본다고 ㅋㅋㅋ 말하기도 하더라구요
더 잘 알고 계시겠지만 chatGPT는 기호 조작에 기반한 인공지능와 비교하면 상당히 다른 방식으로 구성된 인공지능으로 알고 있습니다. 매우 복잡한 수학 문제를 던져줄 경우, 틀리는 경우도 왕왕 있다고 합니다. 그래서 사용자의 검토가 필수적입니다.(수 많은 자료가 있지만, 다음을 참조: https://www.wsj.com/articles/ai-bot-chatgpt-needs-some-help-with-math-assignments-11675390552) 몇몇 수학자들 인터뷰를 봤는데, chatGPT를 쓰기보다는 자기들이 평소에 쓰던 단순한 계산기를 쓸거라 하더군요. 논리학에서도 상황이 비슷할 것이라 추측이 됩니다. 그래서 chatGPT에게 시켜서 푼 논리학 문제의 풀이가 옳고 그른지는 반드시 검토해야겠죠. 그럴려면, 형식 논리학을 잘 숙지하고 있어야 겠죠. 그런데 형식 논리학을 숙지하는데 있어서, 모님이 지금 모 단체에서 하는 논리학 강의를 잘 수강하는 것이 큰 도움이 될거라 사료되네요??
활용 방법론을 생각해보면, chatGPT에게 어떤 문제를 풀게하고, 학생들에게 그 문제 풀이가 맞는지 틀린지 검토하는 것을 맡겨도 재미있을 것 같습니다. 문제 풀기를 대행하기보다는, 아마 이런 오류 찾아내는 과정이 훨씬 더 공부가 될지도 모릅니다.
뱀발입니다만, 수학 문제 풀이에서의 chatGPT3.5(녹색 마크의 무료 버전)의 신뢰성에 대한 문제제기가 많았는데, 유료 사용자만 접근 가능한 GPT4 기반의 chatCPT에서는 이런 문제가 많이 수정되었는지 모르겠네요. (신뢰성을 높인다고 했는데, 한달에 20달러를 내고 사용 해봐야 진짜 높아졌는지 알겠죠?)
사실, 글을 올리고 나서 자연연역으로 증명한 걸 살펴봤는데, 저로서는 좀 이해하기 어려운 과정들을 제시하고 있어서, 제가 놓친 게 있는지, ChatGPT가 잘못한 건지 고민 중이었어요. 진리표로는 증명을 잘 해서 자연연역도 맞을 거라고 생각하고 올렸는데, 좀 이상하더라고요. 가령, 피치 형식으로 증명한 것 중, 2에서 P&Q를 가정한 다음에 5에서 2를 다시 반복하는 불필요한 작업을 하고 있는데데, 이후에 살펴보면서 '이게 도대체 뭐지?'하고 생각했어요.
증명을 꼼꼼하게 살펴보니, 자연연역 증명에서는 확실하게 틀린 부분들이 있네요. 전건부정의 오류를 후건부정이라고 하니 말이에요. 그밖에도 가정에 들어갔다가 나오는 과정도 (머리가 복잡해서 솔직히 다 따져보지는 못하겠지만) 굉장히 미심쩍고요. ChatGPT의 자연연역 증명을 믿었다가는 큰일나겠습니다;;
저놈의 ChatGPT 자연연역이 자꾸 신경쓰여서 제가 직접 증명해 봤네요. 그동안 (P → Q) & (Q → P) ≡ (P & Q) ∨ (~P & ~Q)를 진리표로만 확인하고서 굳이 자연연역으로 증명해 본 적은 없었는데, 이번 기회에 해봤습니다. (제가 직접 증명하기 귀찮아서 ChatGPT한테 시켜본 건데, ChatGPT가 맞는지 확인하려니 역설적이게도 결국 직접 증명해야 하네요.)
(1) ((P → Q) & (Q → P)) → ((P & Q) ∨ (~P & ~Q))
- (P → Q) & (Q → P) ..... 전제 / (P & Q) ∨ (~P & ~Q)
- ~((P & Q) ∨ (~P & ~Q)) ..... 가정 / 모순
- ~(P & Q) & ~(~P & ~Q) ..... 2, 드모르간 규칙
- (~P ∨ ~Q) & ~(~P & ~Q) ..... 3, 드모르간 규칙
- (~P ∨ ~Q) & (P ∨ Q) ..... 4, 드모르간 규칙
- P ∨ Q ..... 5, 단순화
- P → Q ..... 1, 단순화
- Q → P ..... 1, 단순화
- P → P ..... 7-8, 가언삼단논법
- P ..... 6, 8, 9, 단순양도논법
- ~P ∨ ~Q ..... 5, 단순화
- ~Q → ~P ..... 7, 자리뒤집기(대우)
- ~P → ~Q ..... 8, 자리뒤집기(대우)
- ~P → ~P ..... 12-13, 가언삼단논법
- ~P ..... 11, 12, 14, 단순양도논법
- P & ~P ..... 10, 15, 연언화
- ~((P & Q) ∨ (~P & ~Q)) → (P & ~P) ..... 2-16, 가정 나오기(간접증명법)
- (P & Q) ∨ (~P & ~Q) ..... 17, 귀류법
(2) ((P & Q) ∨ (~P & ~Q)) → ((P → Q) & (Q → P))
- (P & Q) ∨ (~P & ~Q) ..... 전제 / (P → Q) & (Q → P)
- P & Q ..... 가정 / (P → Q) & (Q → P)
- Q ..... 2, 단순화
- Q ∨ ~P ..... 3, 선언지첨가법
- ~Q → ~P ..... 4, 조건화
- P → Q ..... 5, 자리뒤집기(대우)
- P ..... 2, 단순화
- P ∨ ~Q ..... 7, 선언지첨가법
- ~P → ~Q ..... 8, 조건화
- Q → P ..... 9, 자리뒤집기(대우)
- (P → Q) & (Q → P) ..... 6, 10 연언화
- (P & Q) → ((P → Q) & (Q → P)) ..... 2-11, 가정 나오기(조건 증명법)
- ~P & ~Q ..... 가정 / (P → Q) & (Q → P)
- ~P ..... 13, 단순화
- ~P ∨ Q ..... 14, 선언지첨가법
- P → Q ..... 15, 조건화
- ~Q ..... 13, 단순화
- ~Q ∨ P ..... 17, 선언지첨가법
- Q → P ..... 18, 조건화
- (P → Q) & (Q → P) ..... 16, 20, 연언화
- (~P & ~Q) → (P → Q) & (Q → P) ..... 가정 나오기(조건증명법)
- (P → Q) & (Q → P) ..... 1, 12, 21, 단순양도논법
생각했던 것보다 증명이 훨씬 기네요. 여기 사용된 규칙은 김광수의 『논리와 비판적 사고』에 근거한 것입니다(잡념과 공상 : 네이버 블로그 과 잡념과 공상 : 네이버 블로그 참고). 처음에는 인터넷에 있는 Proof Checker로 증명 과정을 하나하나 검사해 보려고 했는데, 긴 증명을 저에게는 다소 낯선 표기법에 맞추어 입력하는 게 너무 복잡해서 그냥 가장 익숙한 방식을 택했습니다. 혹시 증명에서 잘못된 부분을 발견하신 분들은 꼭 알려주세요.
제가 간단한 논리학 퍼즐을 낼 때에는 제대로 답을 못 했는데 (정답은 '그렇다') 복잡한 연역 시스템은 잘 다루는 게 신기하네요. 확실히 기계라 그런지 논리학의 semantics보다 syntax에 더 강한가 봅니다.
한 때 기호논리학 기계 출신으로서 (1)번 10과 11로 선언지 제거하면 ~Q 나오고 modus tollens로 7이랑 였으면 ~P 그럼 다시 10이랑 연언하면 모순 도출된다는 게 보이네요. 근데 드모르간을 저렇게 하나씩 해야해요? 아니면 먼저 연언지 단순화해서 드모르간 해야하는 건가요? 10년 낡은 기계라 기억이 잘 안나네요.
LLM은 언어생성모델이기 때문에 입력 값에 대해 확률적으로 가장 괜찮다고 생각하는 단어나 어절을 출력하는 모델입니다. 인간이 대화를 하면서 항상 정확성과 논리적 일관성을 구구절절 따지지 않습니다. 그런다면 인생이 피곤해지겠죠. 마찬가지로 Chat GPT같은 LLM도 학습된 데이터를 통해 언어를 구사하기 때문에 완전 구라다라고 단정짓긴 어렵습니다. 다만 신뢰성이나 정확성(ex. 논문 출처, 산수)이 고도로 요구되는 경우는 hollucination이 발생할 수 밖에 없습니다. 관련된 연구들도 Chat GPT 나오고 나서 폭발적으로 증가하는 추세입니다.
(1)
오, 퍼즐이 재미있네요. Bennett이 결혼하였을 경우와 결혼하지 않았을 경우 둘 다를 따져 봐야 하는 거네요! 결혼하였다면, 결혼한 Bennett이 결혼하지 않은 Chalotte을 보고 있는 거고, 결혼하지 않았다면, 결혼한 Alice가 결혼하지 않은 Bennett을 보고 있는 거군요. 인터넷을 찾고서야 왜 답이 '그렇다'가 되어야 하는지 이해했습니다ㅠㅠ
(2)
복잡한 연역 시스템도 잘 못 다루는 것 같아요. 진리표도 잘 썼고, 많은 사람들이 코딩도 잘 한다고 했으니, 자연연역은 당연히 맞겠지 생각하고 검토 없이 이 글을 올렸는데, 증명한 걸 뜯어보니 굉장히 이상하네요. 가령,
- From P → Q and ~P, derive ~Q using modus tollens.
라든가,
- From Q → P and ~Q, derive ~P using modus tollens.
라는 부분은 확실하게 틀렸네요. 또 그 아래 피치 스타일 증명에서도 2-5까지의 쓸데 없는 과정을 왜 하는 건지, 애초에 1이 (P→Q) & (Q → P)인데 왜 6에서 (~P & ~Q)를 가정한 다음 11에서 (P→Q) & (Q → P)을 도출하는 건지 등등, 저로서는 이해할 수 없는 무의미한 연역들이 계속 이어져요.
특히, 증명의 부분들 각각을 보면 얼핏 과정이 타당해 보이는데, 전체적으로 보면 도대체 무엇을 위해 각각의 논리식을 도출한 건지 의미를 알 수가 없네요. (제가 ChatGPT의 심오하고 치밀한 뜻을 이해하지 못한 것일지 모르겠지만, 적어도 제가 증명할 때 사용한 방식과 비교해 보면 도대체 의미를 알 수 없는 과정들이 너무 많네요.)
(3)
오, 조언해주신대로 하면 증명 과정이 더 단축되네요! 다만, 제가 약간 '균형충'이라 (1)의 6-10까지와 11-15까지가 구조적으로 정확히 대응하는 게 만족스러웠는데, 단축된 증명에서는 11 이후로 구조적 균형(?)이 깨져서 아쉽네요.
(4)
굳이 저렇게 하나하나 드모르간을 적용하지는 않아도 되는 걸로 알고 있어요. 교재마다 좀 더 간소화해서 드모르간을 적용하기도 하고, 하나씩 단계별로 적용하기도 해요. 그런데 인터넷에 있는 Fitch Proof Constructor는 드모르간의 종류를 4가지로 구분해서 하나씩만 적용하도록 되어 있더라고요. 그래서 저도 나누어 보았어요.
배중률을 갖다 치우라는 GPT의 계시인가요 ㄷㄷㄷ
그렇다고 하더라구요. 사실 ChatGPT에게 직접 물어보면 그렇게 설명해주더군요. ㅎㅎ 먼저 해당 지문의 토픽에서 많이 사용되는 단어들의 빈도들을 분석해서 한 단어 바로 다음 단어에 어떤 것이 더 '자연스레' 붙는지를 따지는 모델이니까요. 신뢰성이나 정확성과 관련해서 제기되는 문제에 대해서 이미 여러 사람들이 '인용을 붙여야 된다'거나 '자료를 묻는 질문에는 제한적인 언어모델을 적용해야한다'는 등의 제안을 했고, 이를 바탕으로 얼마전에 나온 Bing의 채팅에는 인용 기능이 붙어 있더군요. 하지만 Bing 채팅 기능을 통해 얻는 글이 ChatGPT의 수려한 영어(?)에 비하면 만족스럽지는 않더라구요. 전 이게 재밌는 지점이었어요. 말투와 수사만으로 그 말의 내용에 설득력이 더해진다는 것 말입니다. 빙 챗도 가끔 거짓된 정보를 말하긴 하는데, 챗 지피티는 거짓된 정보를 말할 때 아주 '감쪽같이' 하는 것 같다는 것이죠.
