728x90
반응형
최근 하버드의 CS50 AI 강의를 듣다가 흥미로운 장표를 발견했습니다. 겉보기에는 단순한 영어 문장 놀이처럼 보이지만, 사실 이 장표는 현대 자동 정리 증명(Automated Theorem Proving)과 지식 기반 에이전트(Knowledge-Based Agent)가 세상을 이해하는 가장 핵심적인 알고리즘, 바로 도출 규칙을 설명하고 있습니다.
오늘은 이 논리식이 왜 성립하는지, 그리고 우리 개발자들이 다루는 시스템 내부에서 이것이 어떻게 응용되는지 'Deep Dive' 해보겠습니다.
1. 문제의 정의 (Formal Definition)
사진 속 강사(Brian Yu)가 보여주는 예시는 다음과 같은 구조를 가지고 있습니다.
- (Ron is in the Great Hall) ∨ (Hermione is in the library)
- (Ron is not in the Great Hall) ∨ (Harry is sleeping)
- ∴ (Hermione is in the library) ∨ (Harry is sleeping)
이를 명제 논리(Propositional Logic)의 기호로 치환해 봅시다. (개발자에게는 자연어보다 변수가 편하니까요.)
- P: Ron is in the Great Hall
- Q: Hermione is in the library
- R: Harry is sleeping
이 식은 다음과 같은 CNF(Conjunctive Normal Form) 형태의 추론 규칙이 됩니다.
여기서 핵심은 P와 ￢P라는 상충되는 리터럴(Complementary Literals)이 존재한다는 점입니다. 이 둘은 논리적으로 공존할 수 없기에 서로 상쇄(Resolve)되고, 남은 리터럴들의 합집합(Q ∨ R)이 결론으로 도출됩니다.
2. 논리적 증명: 왜 이것이 참인가?
개발자 관점에서 디버깅하듯 케이스 분석(Case Analysis)을 해보면 이 규칙의 견고함을 알 수 있습니다.
P는 True 아니면 False, 두 가지 상태만 가질 수 있습니다.
Case 1: P가 True인 경우 (론이 연회장에 있다면)
두 번째 전제인 (￢P ∨ R)을 살펴봅시다.
- P가 True이므로 ￢P는 False가 됩니다.
- 이 전제(OR 연산)가 True가 되기 위해서는, 나머지 항인 R이 반드시 True여야 합니다.
- 결과적으로 (Q ∨ R)은 참이 됩니다.
Case 2: P가 False인 경우 (론이 연회장에 없다면)
첫 번째 전제인 (P ∨ Q)를 살펴봅시다.
- P가 False이므로, 이 전제가 True가 되기 위해서는 Q가 반드시 True여야 합니다.
- 결과적으로 (Q ∨ R)은 참이 됩니다.
결론: P의 진리값(State)이 무엇이든 간에, Q 혹은 R 둘 중 하나는 반드시 참이어야 합니다.
이것이 Resolution Rule이 Soundness(건전성)를 갖는 이유입니다.
3. Tech Insight: 이것이 왜 중요한가?
"그저 논리학 수업 내용 아닌가?"라고 생각할 수 있지만, 이 원리는 컴퓨터 과학, 특히 백엔드 로직과 AI 모델링 깊숙한 곳에 녹아 있습니다.
A. SAT Solver의 엔진
복잡한 의존성 관리 도구(npm, pip 등의 패키지 매니저)나 하드웨어 검증 시스템은 내부적으로 SAT Solver를 사용합니다. 수만 개의 제약 조건이 얽혀 있을 때, "이 조건을 만족하는 해가 존재하는가?"를 판단하기 위해 컴퓨터는 이 Resolution Rule을 반복적으로 수행하여 식을 간소화하거나 모순(Empty Clause)을 찾아냅니다.
B. 논리 프로그래밍 (Prolog)
지금은 많이 쓰이지 않지만, 규칙 기반 엔진이나 Prolog 같은 언어는 이 원리를 그대로 사용합니다. 특히 Horn Clause 형태의 데이터베이스에서 쿼리를 날릴 때, 추론 엔진은 이 도출 과정을 역방향 혹은 순방향으로 수행하여 답을 찾아냅니다.
C. 최적화와 컴파일러
컴파일러의 정적 분석(Static Analysis) 단계에서도 유사한 로직이 사용됩니다. 코드의 실행 경로(Control Flow) 중 논리적으로 도달 불가능한 코드(Dead Code)를 제거할 때, 컴파일러는 이러한 명제 논리적 추론을 통해 "이 조건에서는 저 블록이 절대 실행될 수 없음"을 증명해 냅니다.
4. 마치며
사진 속의 Make sure you convince yourself that you believe this conclusion.이라는 문구가 인상적입니다.
개발자인 우리에게는 이것이 단순한 믿음의 영역이 아닙니다. 상충되는 상태(P, ￢P)를 제거하여 시스템의 불확실성을 줄여나가는 알고리즘적 사고, 그것이 바로 코드로 논리를 구축하는 우리의 핵심 역량일 것입니다.
728x90
반응형