기술 요약: Eigenius: 인식론적 층위화 및 기관 매개 추론을 갖춘 타입형 지식 그래프 DBMS

1. 문제 정의

모델 컨텍스트 프로토콜(MCP)을 활용하여 연구 루프를 구동하는 자율적 "AI 과학자"의 등장은 현재의 과학 데이터 인프라가 가진 결정적인 한계를 드러냈다. 기존 시스템은 일시적인 스크립트와 서사적 산문(narrative prose)에 의존하며, 이는 인간에게는 수동 감사가 가능할지라도 자율적 에이전트에게는 불충분한, 취약한 파이프라인을 생성한다. 자율적 에이전트에게는 암호학적으로 안전하고 완전히 보행 가능한(walkable) 증명 체인이 필요하기 때문이다.

Pharos 프로젝트(2008)와 같은 이전의 기계 감사 가능 과학 구현 시도들은 연합 아키텍처(federated architecture)에 의존했기 때문에 확장하는 데 실패했다. Pharos는 SQL Server, DataNet, HOL 정리 증명기(theorem provers)와 같은 이질적인 하위 시스템들을 불투명한 커스텀 브릿지로 엮어냈다. 이러한 접근 방식은 통일된 커널이 결여되어 다음과 같은 문제를 야기했다:

• 온톨로지 파편화: 스키마와 인스턴스 데이터가 서로 다른 범주에 존재함.
• 구조적 불변성 결여: 시스템 간 변환이 일시적이며 형식적으로 검증되지 않음.
• 폴리스토어(Polystore) 병목 현상: $N$개의 시스템을 통합하기 위해 $O(N^2)$의 쌍방향 어댑터가 필요함.
• 추론 통합 불능: 경험적 정당화 논리와 형식적 수학 증명이 공유 타입 시스템 없이 별도의 엔진에서 처리됨.

핵심 과제는 "무엇을 알고 있는가, 그리고 그 근거(warranty)는 무엇인가?"라는 감사 질문을 사후적으로 재구성하는 속성이 아니라, 데이터 모델 자체의 구조적 불변량으로 취급하는 데이터베이스 아키텍처를 구축하는 것이다.

2. 방법론 및 아키텍처

Eigenius는 통일된 수학적 커널을 기반으로 구축된 오픈 소스 타입형 지식 그래프 DBMS이다. 이는 연합 스택을 대체하여 타입 시스템, 저장 엔진, 그리고 통합 프로토콜을 긴밀하게 결합하는 단일 아키텍처를 제공한다.

핵심 기둥

1. 의존 타입 이론 (EigenTT): 커널은 핵심부에 직조된 의존 타입 이론(CIC 계열)을 사용한다. 스키마와 데이터는 통합되어 있으며, 클래스를 선언하는 것은 곧 리소스를 확정(committing)하는 것과 같다. 커밋의 단위는 **레이어(layer)**로, 부모 포인터를 가진 불변의 리소스 세트이다. 레이어의 정체성은 정형화된 CBOR의 SHA-256을 통한 콘텐츠 주소 지정(content-addressed) 방식을 따르며, 이는 그래프 이력에 대한 머클 약속(Merkle commitment)을 형성한다.
2. 인식론적 층위화 (Epistemic Stratification): 모든 리소스는 커밋 시점에 강제되는 엄격한 인식론적 상태를 보유한다. 시스템은 다음을 구분한다:
   • 선언됨 (Declared): 증거 없는 권위 (정형성 검사 완료).
   • 관찰됨 (Observed): 외부 출처와 함께 기록됨.
   • 유도됨 (Derived): 타입된 계산에 의해 생성됨.
   • 검증됨 (Verified): 정식으로 재검증된 증명 항(proof term)을 보유함.
     이 층위화는 정당화 논리(justification logic)에 기반하며, 과학적 주장이 프로버(prover)에 의해 해소될 수 없는 관찰과 관습에 의존한다는 점을 인정하여 모든 근거(warrant)를 사실적(factive)으로 간주하지 않는다.
3. 기관 매개 추론 (Institution-Mediated Reasoning): 외부 추론기(ODE 솔버, 정리 증명기)를 통합하기 위해, Eigenius는 **Goguen 및 Burstall 기관(institutions)**을 강력한 타입형 저장 프로시저의 일반화로서 채택한다.
   • 코모피즘 (Comorphisms): 시스템 간 변환은 엔진 내부에서 네이티브로 실행되는 강력한 타입형 ETL 파이프라인인 코모피즘으로 모델링된다.
   • 커밋 시점 검사: 변환 $m: S \to T$가 페이로드 타입과 일치하지 않으면 스키마 위반처럼 거부된다. 즉, 변환은 커밋 시점에 정적으로 검사된다.
   • 구체화 (Materialization): 전통적인 연합 데이터베이스에서 변환이 일시적인 것과 달리, Eigenius는 코모피즘의 출력을 콘텐츠 주소 지정된 내구적인 리소스로서 그래프에 직접 구체화한다.

형식 검증 통합

순수 수학을 다루기 위해, Eigenius는 IPC 오버헤드 없이 불투명한 증명 페이로드를 검증하는 문제를 해결한다:

• 인 프로세스 검사 (In-Process Checking): 커널은 최소한의 Rust 텀 체커(nanoda_lib)를 바이너리에 직접 링크한다.
• 의존 쌍 (Dependent Pairs): 검증된 주장은 $(P, t)$ 형태의 의존 쌍으로 저장된다. 여기서 $P$는 명제(EigenTT 네이티브)이고, $t$는 불투명한 Lean 4 바이트이다.
• 바인딩 문제: 커밋 시, 커널은 세 부분의 검사를 수행한다: (1) 인 프로세스 체커를 통한 증명 유효성, (2) 미러 대응(Lean 상수를 체인 클래스 IRI에 매핑), (3) 앵커 일관성(소스 아카이브 해싱).

쿼리 언어 (EigenQL)

EigenQL은 집계 기능과 기관 설정을 위한 두 가지 특정 절을 갖춘 타입형 층위화 Datalog이다:

• FIBER: 쿼리 도중 외부 기관으로 실행을 디스패치한다.
• INTO: 외부 엔진의 응답을 이름이 지정된 IRI에 체인으로 고정(pin)하여 커밋 파이프라인을 트리거한다.

3. 주요 기여

본 논문은 네 가지 주요 기여를 설명한다:

• C1: 통합 데이터 모델: 경험적 정당화 논리와 형식적 수학 증명을 통합하는 자기 기술적 타입 그래프 모델. 인식론적 상태는 커밋 시 강제되는 구조적 베이스 클래스이다. 형식 검증은 불투명한 증명 페이로드를 스키마에 바인딩하는 임베디드 인 프로세스 텀 체커를 통해 처리된다.
• C2: 기관 통합 프로토콜: 기관을 강력한 타입형 일반화된 저장 프로시저로서 데이터베이스 세계에 도입하였다. 시스템 간 변환(코모피즘)은 커밋 시 정적으로 검사되며 내구적인 리소스로 구체화된다.
• C3: 폴리스토어 병목 현상 제거: 공유된 강력한 타입형 중간 표현(IR)을 그래프의 스키마로 직접 격상함으로써, 해당 IR을 공유하는 시스템 간의 코모피즘 변환은 순수 항등(identity)으로 축소되어 $O(N^2)$의 어댑터 비용을 제거한다.
• C4: 엔드 투 엔드 복제: 취약한 스크립트에서 벗어나, Chan 등의 WRN helicase 연구를 포함한 Nature 논문을 실체화된 증거 그래프로 재구성하여 전체 재계산 및 재인코딩을 수행하였다.

4. 결과 및 평가

RocksDB 저장소와 gRPC API를 사용하는 Rust 기반의 프로토타입은 마이크로 벤치마크와 매크로 평가를 통해 검증되었다.

• 마이크로 벤치마크 (데이터 주입): 시스템은 WordNet 및 UMLS 어휘(9.19M 체인 리소스)를 주입했다. 단일 코어에서 초당 약 5,200개의 검증된 리소스를 유지했다. 커밋 게이트가 주요 비용이며, 구조적 클래스 레이어는 ~28k/s, 엄격하게 타입 검사된 어휘 항목은 ~4k/s의 속도로 로드되었다.
• 매크로 평가 (Nature 연구 복제): 게놈 와이드 의존성 스크린, 실험실 검증 및 생체 내(in vivo) 모델을 포함한 고위급 연구를 재실행했다.
  • 일관성: 52개의 파생된 결론이 고정된 데이터로부터 모두 유지되었다.
  • 불일치 탐지: 재계산을 통해 논문의 서사와 데이터 사이의 네 가지 기계 검증된 불일치를 발견했다. 여기에는 수정된 표본 크기($n=54 \to 51$)와 정직한 p-값이 13 자릿수만큼 차이 나는 의사 복제(pseudoreplication) 오류가 포함된다.
  • 감사 가능성: 논문의 모든 분석 클래스는 라이브로 실행 가능하다; 가정들은 서사적 주의사항이 아닌 검사 가능한 리소스로 존재한다.

5. 의의 및 주장

본 논문은 Eigenius가 차세대 AI 주도 과학 연구를 지원하기 위한 필수적인 데이터베이스 커널을 제공한다고 주장한다. 그 의의는 다음과 같다:

1. 구조적 불변성: 데이터 출처와 인식론적 상태를 사후 재구성이 아닌 데이터 모델의 구조적 불변량으로 전환한다.
2. 에이전트 친화적 인프라: 자율적 에이전트가 과학적 추론을 위해 타입 검사와 테스트의 긴밀한 루프(즉, "컴파일러"와 "테스트 스위트")를 필요로 하는 "에이전트 역전(agent inversion)" 현상을 해결한다.
3. 통합된 인식론: 경험 과학을 위한 정당화 논리와 수학을 위한 형식 검증이라는 두 영역의 과학적 인식론을 단일 엔진 내에서 성공적으로 통합한다.
4. 검증 가능한 감사 체인: 감사자가 중간 미들웨어에 연락할 필요 없이 그래프만을 사용하여 판결로부터 원시 데이터와 증명 항까지의 전체 증명 경로를 다시 걸을 수 있는 "폐쇄형 감사 체인(closed audit chain)"을 가능하게 한다.

저자들은 무거운 네이티브 라이브러리를 지원하기 위해 컨테이너화된 서브스트레이트 대신 Wasm을 포기한 결정과, 검증기 및 코모피즘 타입 체커의 기계화가 여전히 필요하다는 한계를 인정한다. 궁극적인 목표는 AI 과학자가 인간의 개입 없이 과학적 그래프를 탐색, 변이 및 검증할 수 있도록 하는 것이다.