LiveKnowledge: 검증 가능한 지식 엔지니어링

LiveKnowledge는 비정형 텍스트와 구조화되고 검증 가능한 지식 사이의 루프를 완성하는 CLI 도구입니다. 이 도구는 대규모 언어 모델 (LLM)과 Answer Set Programming (via Clingo)을 결합하여, 진화하는 지식 베이스 내에서 사실을 추출, 검증 및 질의합니다. 이 포스트에서는 v2.1 아키텍처 — 즉, 이것이 무엇을 하는지, 왜 작동하는지, 그리고 더 넓은 뉴로-심볼릭 (neuro-symbolic) 환경에서 어디에 위치하는지를 다룹니다.

문제점

대부분의 지식 도구는 지식을 데이터베이스 내의 벡터로 취급합니다. 이를 검색할 수는 있지만, _검증_할 수는 없습니다. 만약 두 사실이 서로 모순된다면, 벡터 저장소는 이를 알려주지 않습니다. RAG (Retrieval-Augmented Generation) 파이프라인은 검색된 문서에 기반하여 생성을 수행할 수 있지만, 검색된 사실들이 일관된 논리 이론을 형성하는지 알 방법이 없습니다.

LiveKnowledge는 지식을 논리 프로그램 (logic programs) — 즉, 솔버 (solver)가 일관성을 검증할 수 있는 ASP 사실과 규칙 — 으로 취급합니다. 모든 통합 과정은 **병합 일관성 체크 (merged-coherence check)**를 거칩니다. Clingo는 결합된 KB (지식 베이스) + 후보 프로그램을 해결합니다. 만약 만족 불가능 (unsatisfiable)하다면, 해당 후보는 모순된 것으로 간주되어 거부됩니다. 이것이 핵심 불변량입니다: 어떠한 모순도 지식 베이스에 들어올 수 없습니다.

아키텍처: LLM-Modulo 프레임워크

이 아키텍처는 문헌에서 LLM-Modulo 프레임워크 [1][2]라고 부르는 방식을 따릅니다. LLM이 후보 지식(또는 후보 답변)을 제안하지만, 별도의 검증 가능한 모듈 — 여기서는 Clingo — 이 냉혹한 수학적 문지기 역할을 합니다. 솔버가 모순을 발견하면 후보는 거부되며, LLM은 이를 수정해야 합니다.

이는 반례 유도 귀납적 합성 (Counterexample-Guided Inductive Synthesis, CEGIS) [3]의 직접적인 응용입니다. 솔버는 반례 (병합된 프로그램의 만족 불가능한 핵심 부분)를 생성하고, LLM은 해당 실패 추적 (failure trace)을 가추적 수정 (abductive revision)을 위한 신호로 사용합니다. 시스템은 단순히 수락하거나 거부하는 것에 그치지 않고, 왜 그런지를 설명하고 다시 작성합니다.

                       answer_question flow

      question ──► generate (LLM) ──► verify (LLM) ──► D ──►
...

상세 루프

Ask (질문) — 지식 베이스(KB)를 대상으로 질문을 던집니다. LLM은 사실에 근거하여 답변을 제안합니다.
Verify (검증) — 답변을 KB와 대조하여 검증합니다 (텍스트 답변의 경우 LLM 기반, 지식 일관성의 경우 Clingo 기반).
Abduce & Revise (가추 및 수정) — 검증에 실패하면, abductive_revisor가 실패 원인에 대한 가설과 복구 계획을 생성한 후 후보 답변을 다시 작성합니다. 이는 실제 작동하는 CEGIS (Counterexample-Guided Inductive Synthesis) [3] 과정입니다.
Gap report (공백 보고) — 확정된 답변의 근거(rationale)에는 KB에 누락된 특정 술어 시그니처(predicate signatures, 예: profit/2, demand_cycle/1)가 나열됩니다. 이러한 휴리스틱 형태의 가추적 지식 유도(abductive knowledge induction)는 Learning from Answer Sets (LAS) [4]와 관련이 있습니다. 즉, 시스템이 논리 이론을 완성하기 위해 무엇이 누락되었는지를 식별하는 것입니다.
Learn (학습) — 소스 텍스트가 LLM에 입력되며, LLM은 정확히 누락된 술어들을 타겟팅하여 사실(facts)을 추출합니다. 공백 보고(gap report)는 **우선순위 신호(prioritisation signal)**이지 엄격한 제약 조건이 아닙니다. LLM은 여전히 소스 텍스트에 근거(grounded)를 두어야 합니다.
Verify coherence (일관성 검증) — Clingo가 병합된 프로그램 (KB ⊕ 후보)을 확인합니다. 만약 충족 불가능(unsatisfiable)하다면 후보는 거부됩니다.
Resolve (해결) — 결정론적 스캔(deterministic scan)을 통해 타겟 술어들이 이제 올바른 아리티(arity)를 가지고 KB에 존재하는지 확인합니다.

Gap Lifecycle: 휴리스틱에서 해결까지

공백 보고(gap report)는 답변 흐름(answer flow)과 학습 흐름(learning flow) 사이의 가교 역할을 합니다. 이는 세 가지 해석 계층을 거칩니다:

계층	의미	신뢰도
Answer gap signal (답변 공백 신호)	"KB에 X가 있다면 이 답변이 개선될 것입니다"	휴리스틱, LLM 기반
...

The Hermeneutic Review (해석학적 검토)

모든 공백 타겟이 정확한 것은 아닙니다. LLM이 술어 이름을 환각(hallucinate)할 수도 있고, 소스 텍스트가 실제로는 profit/3(더 풍부한 스키마)를 지원함에도 불구하고 공백 보고가 profit/2를 요구할 수도 있습니다. v2.1에서는 target_review.drop을 통해 인간의 검토가 노출됩니다. 이는 사람이 "이 타겟은 틀렸으므로 해결 과정에서 제외하라"고 말할 수 있게 해주는 간단한 JSON 필드입니다.

저는 이것을 **해석학적 루프 (Hermeneutic Loop)**라고 부릅니다. Clingo는 profit/3이 지식 베이스 (KB)의 나머지 부분과 수학적으로 일치하는지 검증할 수 있지만, profit/3이 특정 비즈니스 도메인에 타당한지는 오직 인간만이 알 수 있습니다. Dreyfus가 주장했듯이 [5], 기계는 인간이 현실 세계의 추론에 가져오는 체화된 맥락적 이해 (embodied, contextual understanding)가 부족합니다. target_review 메커니즘은 LiveKnowledge의 'Live'가 실현되는 지점입니다. 즉, 기계는 구문 (syntax)을 처리하고, 인간은 의미 (meaning)를 제공합니다.

해결의 세 가지 상태

해결 검사 (resolution check)는 모든 타겟 술어 (target predicate)에 대해 세 가지 결과를 생성합니다:

상태	CLI 출력	의미
정확한 일치 발견	`recipe/2 — resolved`	술어가 KB에 정확한 인자 수 (arity)로 존재함
...

스키마 진화로서의 인자 수 드리프트 (Arity-Drift)

이 시스템에서 나타나는 가장 흥미로운 창발적 특성 중 하나는 **인자 수 드리프트 탐지 (arity-drift detection)**입니다. 해결 검사가 profit/3을 발견했지만 갭 (gap)에서 요구한 것이 profit/2인 경우, 시스템은 이를 묵인하거나 거부하는 대신 불일치를 보고합니다.

이것은 버그가 아니라, 일종의 술어 발명 (predicate invention) [6]입니다. 이익을 범위(

벡터 저장소 (Vector stores)는 단조적 (monotonic)입니다. 즉, 더 많은 문서를 추가할수록 검색 시스템이 찾을 수 있는 범위가 확장될 뿐입니다. 하지만 지식은 **비단조적 (non-monotonic)**입니다. 새로운 사실이 기존의 결론을 무효화할 수 있기 때문입니다. 만약 이전에 신뢰했던 공급업체가 신뢰할 수 없다는 사실을 알게 된다면, "그들이 저렴하므로 그들에게서 구매하라"는 추론은 단순히 상충하는 증거 아래 묻히는 것이 아니라 철회 (retract)되어야 합니다.

답집합 솔버 (answer set solver)인 Clingo는 부정-실패-로서의-부정 (negation-as-failure) 및 **강한 부정 (strong negation)**을 통해 비단조적 추론 (non-monotonic reasoning)을 기본적으로 지원합니다. LiveKnowledge의 추가 전용 (additive-only) v2.1은 아직 이를 완전히 활용하지는 못하며 — 모순이 발생하면 철회 대신 거부 (rejection)가 발생합니다 — 하지만 솔버는 이를 위해 설계되었습니다. 지식 베이스 (KB) 구조는 비단조적 업데이트를 수용할 준비가 되어 있습니다. 모든 통합 (integration)은 새로운 불변 스냅샷 (immutable snapshot)을 생성하므로, 이전 스냅샷을 로드함으로써 변경 사항을 언제든지 되돌릴 수 있습니다.

이론 수정 (theory revision) [7]에 관한 문헌들은 원시 데이터로부터의 귀추적 지식 유도 (abductive knowledge induction)가 바로 이러한 능력, 즉 새로운 데이터가 이전의 결론과 모순될 때 논리적 이론을 수정할 수 있는 능력을 필요로 한다는 것을 보여줍니다. 이것이 v2.2의 목표이며, 아키텍처는 이를 위해 설계되었습니다.

문헌과의 매핑 방식

LiveKnowledge v2.1은 여러 연구 흐름의 교차점에 위치합니다:

LLM-Modulo Framework [1][2] — LLM이 제안하고, 솔버(solver)가 검증합니다. 우리의 abductive_revisor는 솔버의 실패 추적(failure traces)을 수정 신호로 사용하는 CEGIS [3]의 직접적인 구현입니다.
Learning from Answer Sets (LAS) [4] — 갭 리포트(gap report)는 가추적 지식 유도(abductive knowledge induction)의 휴리스틱한 형태로, 논리 이론을 완성하는 데 필요한 누락된 술어(predicate)를 식별합니다.
Abductive Knowledge Induction [7] — 결합된 generate→verify→abduce→revise 루프는 Meta-Interpretive Learning 프레임워크를 반영하며, 여기서 LLM은 학습된 메타 인터프리터(meta-interpreter) 역할을 수행합니다.
Predicate Invention [6] — 인자 수 드리프트(arity-drift) 탐지는 LLM이 갭 리포트에서 예상한 것보다 더 풍부한 술어 스키마(predicate schema)를 발명한 사례를 드러냅니다.
Multi-Shot ASP Solving [8] — 이 아키텍처는 향후 버전에서 스트리밍 및 상태 유지 추론(stateful reasoning)을 위해 Clingo의 멀티샷(multi-shot) 모드를 채택하도록 설계되었습니다.

향후 단계 (LiveKnowledge v2.2+)

v2.1은 가산적(additive)이고 얕은 해상도(shallow-resolution)를 가진 아키텍처입니다. 다음과 같은 몇 가지 유예된 기능들이 계획되어 있습니다:

의미론적 갭-완전성 (Semantic Gap-Completeness)

현재는 술어 이름과 인자 수(arity)가 확장된 지식 베이스(KB)의 어디에서든 나타나면 갭이 "닫힌" 것으로 간주합니다. 향후 버전에서는 **예시-인스턴스 임계값(example-instance thresholds)**을 평가하고, **최소 모델(minimal models)**을 검토하며, 원래 질문에 자동으로 다시 답변하여 갭이 실제로 해결되었음을 증명할 것입니다.

비단조적 철회 (Non-Monotonic Retractions)

가산적 방식만 사용하는 것은 안전한 시작이지만, 실제 지식은 진화합니다. 향후 작업에서는 최소 불만족 코어(minimal unsatisfiable core) 분석을 통한 **이론 수정(theory revision)**을 구현하여, 지식 그래프의 나머지 부분을 손상시키지 않으면서 오래된 ASP 파편을 안전하게 삭제하거나 덮어쓸 것입니다 [7].

멀티샷 상태 유지 추론 (Multi-Shot Stateful Reasoning)

현재는 모든 성공적인 통합이 이전 스냅샷을 덮어씁니다. 실시간 스트리밍 에이전트를 위해, 시스템은 Clingo의 멀티샷 솔빙(multi-shot solving) [8]을 채택하여, 전체 KB를 다시 그라운딩(re-grounding)하지 않고도 #program 시나리오를 동적으로 주입하고 전환할 수 있는 지속적이고 상태가 유지되는 추론 스트림을 유지할 것입니다.

시리즈의 첫 번째 파트입니다. 곧 파트 2가 공개될 예정입니다 — 의미론적 간극 완결성 (semantic gap-completeness), 비단조적 철회 (non-monotonic retractions), 그리고 멀티샷 추론 (multi-shot reasoning)을 다룹니다.

참고 문헌

[1] S. Shetye. "An LLM-Modulo Framework for Automated PDDL Domain Model Generation." 석사 학위 논문, Universität Stuttgart. PDF

[2] A. Ishay, J. Lee. "LLMs as ASP Programmers: Self-Correction Enables Task-Agnostic Nonmonotonic Reasoning." arXiv:2604.27960

[3] P. Orvalho, M. Janota, V. Manquinho. "Counterexample Guided Program Repair Using Zero-Shot Learning and MaxSAT-based Fault Localization." AAAI 2025. PDF

[4] M. Borroto, K. Gallagher, A. Ielo, I. Kareem, F. Ricca, A. Russo. "Question Answering with LLMs and Learning from Answer Sets." arXiv:2509.16590

[5] H. Dreyfus. What Computers Still Can't Do: A Critique of Artificial Reason. MIT Press, 1992.

[6] S. Dumančić, W. Meert, H. Blockeel. "Theory Reconstruction: A Representation Learning View on Predicate Invention." arXiv:1606.08660

[7] W-Z. Dai, S.H. Muggleton. "Abductive Knowledge Induction From Raw Data." PDF

[8] M. Gebser, R. Kaminski, B. Kaufmann, T. Schaub. "Multi-shot ASP solving with Clingo." Theory and Practice of Logic Programming, 2019. arXiv:1705.09811

시리즈의 첫 번째 파트입니다. 곧 파트 2가 공개될 예정입니다 — 의미론적 간극 완결성 (semantic gap-completeness), 비단조적 철회 (non-monotonic retractions), 그리고 멀티샷 추론 (multi-shot reasoning)을 다룹니다. dev.to에서 저를 팔로우하거나 adamrybinski.com을 방문해 주세요.