Delta1 with LLM: symbolic and neural integration for credible and explainable reasoning

이 논문은 논리적 엄밀성과 LLM 의 해석 가능성을 결합하여, FTSC 기반의 결정적 정립 생성기 Delta1 과 LLM 을 통합함으로써 의료 및 규제 분야에서 신뢰할 수 있고 설명 가능한 추론을 가능하게 하는 신경-상징적 프레임워크를 제안합니다.

핵심

이 논문은 **"로봇이 논리적으로 완벽하게 생각하면서도, 인간이 이해할 수 있는 말로 설명해 주는 새로운 방법"**을 소개합니다.

기존의 인공지능 (AI) 은 두 가지 큰 문제가 있었습니다.

1. 논리 AI: 수학처럼 정확하지만, 왜 그런 결론이 나왔는지 설명을 못 합니다. (흑색 상자)
2. 언어 AI (LLM): 사람처럼 말은 잘하지만, 논리적으로 틀린 말을 할 수 있습니다. (할루시네이션)

이 논문은 이 두 가지를 합쳐서 **"논리적으로 틀릴 수 없는 AI"**를 만들었습니다. 이름은 ∆1-LLM입니다.

이 복잡한 기술을 일상적인 비유로 쉽게 설명해 드릴게요.

---

🏗️ 비유: "완벽한 건축가 (∆1)"와 "재미있는 해설가 (LLM)"

이 시스템은 두 명의 전문가가 팀을 이루어 일합니다.

1. 건축가 ∆1 (수학자 역할)

• 역할: 이 친구는 완벽한 논리를 담당합니다.
• 비유: imagine you are building a house. Imagine you are a master architect who only uses perfectly cut bricks.
  • 이 건축가는 "이 벽돌을 쌓으면 집이 무너진다"는 것을 수학적으로 100% 증명할 수 있습니다.
  • 그는 실수를 하지 않으며, "왜 무너지는지"에 대한 **정확한 설계도 (증명 과정)**를 가지고 있습니다.
  • 하지만 이 건축가는 말을 못 합니다. 그는 "여기서 무너집니다"라고만 표시할 뿐, "왜 무너지는지"를 사람처럼 설명해 주지는 못합니다.

2. 해설가 LLM (작가 역할)

• 역할: 이 친구는 설명을 담당합니다.
• 비유: 건축가가 "여기서 무너집니다"라고 표시한 설계도를 받아, 재미있는 이야기꾼이 됩니다.
  • "아! 이 벽돌이 너무 무거워서 아래 기둥이 버티지 못했네요. 그래서 2 층이 무너진 거예요!"라고 사람이 이해하기 쉬운 언어로 설명해 줍니다.
  • 하지만 이 해설가 혼자라면 "아마도 무너졌을 거예요"라고 추측만 할 수 있습니다.

🤝 팀워크: "∆1 + LLM"

이 두 명이 만나면 어떤 일이 일어날까요?

1. **건축가 (∆1)**가 "이 규칙들을 모두 적용하면 모순이 생겨서 시스템이 붕괴됩니다"라고 수학적으로 증명합니다. (이때부터 틀릴 수 없음이 보장됩니다.)
2. **해설가 (LLM)**가 그 증명 결과를 받아, **"왜 모순이 생겼는지"**를 의사, 변호사, 혹은 일반인이 이해할 수 있는 말로 풀어냅니다.
   • 예: "환자가 감염되면 항생제를 써야 하는데, 동시에 고열이 나면 항생제를 쓰면 안 된다는 규칙이 있어서 충돌이 일어났습니다. 그래서 치료 계획을 수정해야 합니다."

이것이 바로 **"구축을 통한 설명 (Explainability by Construction)"**입니다. 설명이 나중에 덧붙여지는 게 아니라, 논리 자체가 설명 가능한 형태로 만들어지는 것입니다.

---

🏥 실제 사례로 이해하기

이 시스템이 실제로 어떻게 쓰이는지 세 가지 예를 들어볼게요.

1. 병원에서의 진단 (의료)

• 상황: "감염되면 백혈구가 높고, 백혈구가 높으면 열이 나며, 감염과 열이 동시에 있으면 항생제를 써야 한다"는 규칙이 있습니다.
• 문제: 그런데 환자가 "감염"은 있는데 "열"은 없는데도 "항생제"를 써야 한다는 모순이 생길 수 있습니다.
• ∆1-LLM 의 역할:
  • ∆1: "이 규칙들을 모두 적용하면 수학적으로 '모순'이 발생합니다. 항생제 사용이 불가능합니다." (논리적 증명)
  • LLM: "아! 감염이 있다고 해서 무조건 항생제를 쓰면 안 되네요. 열이 나야 한다는 조건이 빠졌어요. 진단 기준을 더 명확히 해야 합니다." (실제 해결책 제시)

2. 회사 규정 (준수 관리)

• 상황: "비밀 유지 (Privacy)"를 지키려면 "데이터 공유 (Share)"를 못 하고, "투명성 (Transparency)"을 지키려면 "데이터 공유"를 해야 합니다.
• 문제: 두 가지 규정을 동시에 지키려고 하면 회사가 망합니다.
• ∆1-LLM 의 역할:
  • ∆1: "이 두 규칙은 동시에 성립할 수 없습니다. (수학적 증명)"
  • LLM: "비밀 유지와 투명한 공유는 서로 충돌합니다. 어느 한쪽의 범위를 줄이거나, 익명 처리를 도입해야 합니다."

3. 계약서 검토 (법률)

• 상황: "공급자가 독점 계약을 맺으면 (Exclusive), 지체 없이 물건을 보내야 하고 (Timely), 지연 시 벌금이 붙는데 (Penalty), 구매자가 아무 이유 없이 계약을 끊을 수 있다 (Termination)"는 조항이 있습니다.
• 문제: 독점 계약인데 아무 이유나 끊을 수 있다면, 공급자는 손해를 봅니다.
• ∆1-LLM 의 역할:
  • ∆1: "이 조항들은 논리적으로 충돌합니다."
  • LLM: "독점 계약을 맺었는데 구매자가 마음대로 계약을 끊을 수 있다면, 공급자는 손해를 봅니다. 계약 해지 조건을 명확히 하거나, 위약금을 조정해야 합니다."

---

💡 왜 이것이 중요한가요?

기존의 AI 는 "이게 맞을 것 같아"라고 추측만 했습니다. 하지만 이 ∆1-LLM은 다음과 같은 장점이 있습니다.

1. 틀릴 수 없음: 논리적으로 증명된 결과이므로, 거짓말이나 헛소리를 하지 않습니다.
2. 이해하기 쉬움: 복잡한 수학 증명 대신, "왜 그런지"를 사람처럼 설명해 줍니다.
3. 해결책 제시: 단순히 "틀렸습니다"라고 말하는 게 아니라, "어떻게 고쳐야 하는지" 구체적인 조언을 줍니다.

🚀 결론

이 논문은 **"인공지능이 이제부터 수학적 정확성을 유지하면서도, 인간과 대화할 수 있는 진정한 파트너가 되었다"**는 것을 보여줍니다.

마치 완벽한 논리를 가진 천재 건축가가 재미있는 해설가와 손을 잡아서, 어떤 건물이 왜 무너지는지, 그리고 어떻게 고쳐야 안전한지를 누구나 이해할 수 있게 설명해 주는 것과 같습니다. 이는 의료, 법률, 금융처럼 실수가 치명적인 분야에서 AI 를 안전하게 쓸 수 있는 길을 열어줍니다.

기술 요약

1. 문제 정의 (Problem)

최근 신경 - 심볼릭 (Neuro-symbolic) 추론 분야에서는 형식적 논리의 엄밀함과 대규모 언어 모델 (LLM) 의 해석 가능성 (Interpretability) 을 통합할 수 있는 프레임워크에 대한 요구가 증가하고 있습니다.

• 상반된 한계: 심볼릭 접근법 (자동 증명기 등) 은 증명 가능한 건전성 (Soundness) 과 투명한 추론 구조를 제공하지만, 언어적 표현력이 부족합니다. 반면, 신경 모델 (LLM) 은 유창성과 적응성을 가지지만, 추론의 정확성에 대한 보장이 없으며 확률적 (Stochastic) 성격을 띠어 검증이 어렵습니다.
• 기존 기술의 부족: 기존 자동 증명기 (ATP) 는 증명 경로를 생성하지만 불투명하며, LLM 기반 추론은 오류 가능성이 있습니다. 또한, 기존 신경 - 심볼릭 시스템은 대부분 근사적 추론에 그치거나, 형식적 건전성을 보장하지 못합니다.
• 핵심 과제: 논리적 타당성과 자연어 설명이 설계 단계에서 공존하며, 기계가 검증 가능하고 인간이 이해할 수 있는 추론 시스템을 구축하는 것입니다.

2. 방법론 (Methodology)

이 논문은 **∆1 (Automated Theorem Generator)**과 LLM을 결합한 엔드 - 투 - 엔드 (End-to-End) 파이프라인을 제안합니다. 이 시스템은 "구축에 의한 설명 가능성 (Explainability-by-construction)"을 핵심 원칙으로 합니다.

A. 아키텍처 개요

1. 전단 (Front-end) LLM: 자연어 입력 (규칙, 정책, 계약서 등) 을 받아 TPTP 스타일의 논리 술어 (Atomic Predicates) 집합 $L = \{x_1, ..., x_n\}$으로 변환합니다.
2. ∆1 (Theorem Generator):
   • FTSC (Full Triangular Standard Contradiction): 논리 술어 집합을 기반으로 '완전 삼각형 표준 모순 (FTSC)' 구조를 구성합니다.
   • 결정적 생성: 검색 (Search) 이나 확률적 가이드 없이, 다항 시간 ($O(n^3)$) 내에 $n!$개의 비중복적이고 최소 불만족 (Minimal Unsatisfiable, MUS) 클라우즈 집합을 결정적으로 생성합니다.
   • 정리 생성: 각 정리 (Theorem) 는 $S \setminus \{C\} \vdash \neg C$ 형태로, 하나의 절 (Clause) 을 제거하면 만족 가능해지지만 제거된 절은 나머지 절들에 의해 반증됨을 의미합니다. 이는 논리적 건전성과 최소성을 보장합니다.
   • 증명 경로 (Proof Trace): 각 정리에 대해 명시적인 유도 시퀀스를 생성하여 추론 과정을 투명하게 기록합니다.
3. 후단 (Back-end) LLM:
   • ∆1 이 생성한 증명 경로와 정리를 자연어 설명으로 변환합니다.
   • 맥락적 중요도나 새로움에 따라 정리를 순위 매기고, 구체적인 문제 해결 방안 (Remediation) 을 제안합니다.

B. 핵심 논리 (FTSC)

∆1 은 입력된 $n$개의 서로 다른 술어 $x_1, ..., x_n$에 대해 다음과 같은 FTSC 구조를 정의합니다:

• $D_1 = x_1$
• $D_2 = x_2 \lor \neg x_1$
• ...
• $D_n = x_n \lor \neg x_1 \lor \dots \lor \neg x_{n-1}$
• $D_{n+1} = \neg x_1 \lor \neg x_2 \lor \dots \lor \neg x_n$

이 집합은 본질적으로 불만족스럽습니다. ∆1 은 이 집합에서 하나의 절 $C$를 제거했을 때 나머지 절들이 $C$를 반증한다는 정리를 생성하며, 이는 모든 가능한 논리적 충돌 패턴을 체계적으로 포착합니다.

3. 주요 기여 (Key Contributions)

1. 신경 - 심볼릭 통합 파이프라인: ∆1 의 결정적 정리 생성 능력과 LLM 의 해석 능력을 결합하여, 형식적 건전성과 인간 수준의 해석 가능성을 동시에 달성하는 시스템을 구축했습니다.
2. 구축에 의한 설명 가능성 (Explainability-by-Construction): 기존 사후 (Post-hoc) 해석 방식과 달리, 논리 정리가 생성되는 과정 자체에서 투명하고 검증 가능한 증명 경로를 확보합니다. 모든 설명은 결정적 증명 트리에 기반합니다.
3. 이론적 및 실증적 검증: 의료, 규정 준수, 규제, 계약 분석 등 고위험 도메인에서 ∆1+LLM 이 최소 모순을 식별하고 실행 가능한 통찰을 제공함을 입증했습니다.
4. 최소 불만족 부분집합 (MUS) 의 생성적 접근: 기존 MUS 추출 알고리즘이 입력된 CNF 식을 분석하여 모순을 찾는 것과 달리, ∆1 은 모순을 '생성'함으로써 완전성과 해석 가능성을 보장합니다.

4. 결과 (Results)

논문은 의료, 규정 준수, 계약 관리 등 다양한 도메인에서 사례 연구를 수행했습니다.

• 의료 추론: "감염 -> 고 WBC -> 발열 -> 항생제 필요"와 같은 규칙 집합에서, ∆1 은 논리적 일관성을 해치는 최소 모순 (예: 발열과 감염이 동시에 존재할 때 항생제 필요성이 논리적으로 충돌하는지) 을 식별했습니다. LLM 은 이를 "임상적 맥락에서 과도한 제약"으로 해석하고, 항생제 처방 전 확인 테스트 추가 등의 구체적인 해결책을 제시했습니다.
• 규제 및 규정 준수 (GDPR, HIPAA 등): 서로 다른 관할권의 규정 (예: 데이터 이동성 vs 보관 제한) 간의 충돌을 식별하여, 어떤 조항이 최소 모순의 원인인지 LLM 을 통해 설명하고 수정안을 도출했습니다.
• 계약 관리: 계약 조항 간의 논리적 불일치 (예: 독점 공급과 무조건 해지 조항의 충돌) 를 사전에 발견하고, 조항 수정을 위한 구체적인 권고안을 생성했습니다.
• 성능: ∆1 은 $O(n^3)$ 시간 복잡도로 작동하며, 외부 SAT 솔버나 검증기 없이도 생성된 정리의 건전성을 보장합니다. 모든 출력은 재현 가능하며 결정적입니다.

5. 의의 및 중요성 (Significance)

• 신뢰할 수 있는 AI 의 기반: 기계가 검증 가능한 논리 (Symbolic) 와 인간이 이해할 수 있는 언어 (Neural) 를 결합함으로써, '검증 가능한 투명성'을 갖춘 신경 - 심볼릭 AI 의 새로운 패러다임을 제시합니다.
• 자동 증명에서 자동 이해로: 기존의 자동 증명 (Automated Theorem Proving) 이 단순히 참/거짓을 판별하는 것을 넘어, 자동화된 정리 이해 (Automated Theorem Understanding) 로의 전환을 가능하게 합니다.
• 실용적 가치: 의료, 법률, 금융 등 오류가 치명적인 분야에서 의사결정 지원 시스템으로 활용 가능하며, 규정 충돌을 사전에 탐지하고 수정하는 데 직접적으로 기여합니다.
• 미래 방향: 대칭성 깨기 (Symmetry-breaking) 최적화를 통한 확장성 개선, 강화 학습을 통한 정리 생성, 그리고 다중 에이전트 및 고차 추론으로의 확장을 통해 인간과 협력하는 자기 성찰적 (Self-reflective) 탐구 에이전트로 발전할 잠재력을 가집니다.

이 연구는 형식 논리의 엄밀함과 자연어의 유연성을 통합하여, 신뢰성 있고 설명 가능한 인공지능 시스템 구축을 위한 이론적, 실용적 토대를 마련했다는 점에서 중요한 의의를 가집니다.