기술 요약: 증거 기반 검증된 에이전트 추론 (EG-VAR)

문제 정의

대규모 언어 모델(LLM)은 추론 과정에서 경험적 사실을 환각(hallucination)하는 경우가 빈번하며, 이는 데이터를 조작하거나 검색된 증거와 상충하는 오래된 파라미터 사전 지식(parametric priors)에 의존하기 때문에 발생한다. 도구 증강 추론(RAG)은 모델이 외부 소스를 참조할 수 있게 해주지만, **검증 가능한 경험적 주장(verifiable empirical claims)**을 보장하지는 못한다. 기존 방식들은 다음과 같은 두 가지 구조적 실패를 겪는다:

1. 입증되지 않은 출력(Unattested Outputs): 수용된 출력이 반드시 입증된 증거로부터 유래했다는 보장이 없다. 모델은 자신의 내부 사전 지식과 충돌하는 검색된 데이터를 무시할 수 있다(확증 편향).
2. 검증되지 않은 연역(Unverified Deductions): 수용된 연역이 형식적 정밀 검토를 견뎌내지 못할 수 있다. 모델은 부적절한 논리 단계를 수행하거나 도구의 출력을 오해할 수 있다.

심볼릭 사실 검증기나 LLM 기반 정리 증명기(theorem provers)와 같은 기존 솔루션들은 외부 근거가 부족하거나(수학 전용 증명기), 구조적으로 근거 없는 주장의 부재를 보장할 수 없는 학습된 구성 요소에 의존한다는 한계가 있다.

방법론: EG-VAR 아키텍처

본 논문은 도구 입증(tool-attestation)과 증명 보조 도구(Lean 4)를 통합하여 경험적 추론을 통제 가능하게 설계된 4계층 아키텍처인 **EG-VAR (Evidence-Grounded Verified Agentic Reasoning)**를 제시한다. 이 시스템은 LLM을 엄격하게 정의된 신뢰 원장(trust ledger) 내의 신뢰할 수 없는 구성 요소로 취급한다.

4계층 스택

1. L1: 도구 계층 (신뢰 가능, 결정론적): 결정론적 런타임이 외부 소스(예: 테이블 셀 조회, 집계)에 대한 쿼리를 실행한다. 이는 쿼리, 소스 식별자, 결과를 기록한 런타임 증인(witness)인 Attested T 페이로드를 생성한다. 오직 런타임만이 이러한 증인을 생성할 수 있다.
2. L2: 소스별 형식화 (오프라인 감사): "큐레이터(curator)"는 각 데이터 소스에 대한 **리프트 카탈로그(lift catalog)**를 정의한다. 이는 L1 저장소 사실(예: "행 $r$, 열 $c$의 셀 값은 $v$이다")을 L2 세계 온톨로지 사실(예: HasProperty, ArgmaxWhere)로 매핑한다. 이러한 리프트는 한 번 감사된 후 공리(axioms)로 임포트된다.
3. L3: Lean 4 커널 (신뢰 가능, 형식적): 커널은 Evidence Verified 주장을 발행하는 유일한 권위자이다. 커널은 단일 발행 규칙인 **mkVerified**를 강제하며, 이 규칙은 런타임으로부터의 Attested T 가설을 요구한다. 커널은 모든 증명 단계를 타입 체크하며, 단계가 실패할 경우 해당 주장은 거부된다.
4. L4: 솔버 LLM (신뢰할 수 없음, 확률적): LLM은 타입이 지정된 목표(typed goal)를 전달받고 증명 택틱(proof tactics)을 제안한다. LLM은 런타임에 의해 도입된 Attested T 항들을 소비할 수는 있지만, 이를 직접 합성할 수는 없다. 만약 커널이 택틱을 거부하면, 시스템은 반복하거나 기권(abstain)한다.

핵심 메커니즘

• mkVerified 규칙: Evidence Verified를 위한 유일한 생성자는 Attested T 증인을 필요로 한다. 이는 검증된 출력이 반드시 대응하는 도구 호출 없이 존재할 수 없음을 보장한다(정리 3.1).
• 종속 합 증인(Dependent Sum Witnesses): 주장들은 종속 합($\Sigma$)으로 프레임화된다. "어떤 엔티티가 속성 $P$를 가지는가?"라는 질문에 대해, 목표는 $\Sigma (e : \text{String}) (v : \text{Value}), \text{Evidence Verified}(\dots)$가 된다. 표면적인 답은 커널에 의해 체크된 증명에서 추출된 증인이다.
• 정직한 기권(Honest Abstention): 만약 커널이 (리프트 누락, 잘못된 택틱, 또는 입증 부족으로 인해) 증명을 거부하면, 시스템은 추측하는 대신 재현 가능한 감사 추적(audit trail)과 함께 ABSTAIN을 출력한다.
• 등급 규율(Grade Discipline): 증거는 명시적인 등급(VERIFIED, SUPPORTED, PLAUSIBLE, SPECULATIVE)을 가진다. 시스템은 "업캐스트 금지(no-upcast)" 규칙을 강제한다: 결론은 자신의 가장 약한 전제보다 높은 등급을 가질 수 없다.

주요 기여

1. 근거의 구조적 보장: EG-VAR는 도구 입증을 타입된 공리로 결합하여 증명 보조 커널과 결합한 최초의 아키텍처이다. 이는 모든 VERIFIED 출력이 입증된 도구 호출에서 유래한다는 구조적 보장(정리 3.1)을 제공하며, LLM의 성능과 관계없이 근거 없는 환각을 제거한다.
2. 형식적 안전성 vs. 의미적 충실도: 본 논문은 형식적 안전성(증명이 커널에 의해 수용됨)과 의 의미적 충실도(형식화된 목표가 자연어 주장과 일치함)를 구분한다. EG-VAR는 전자를 구조적으로 보장하며, 후자는 형식화 파인튜닝을 통해 해결 가능한 정확도 목표로 취급한다.
3. 재현 가능한 감사 추적: 모든 검증된 주장에는 자립적인 Lean 증명 파일이 동반된다. 제3자는 LLM을 다시 실행하지 않고도 커널, 소스별 리프트, 도구 어댑터를 사용하여 오프라인에서 해당 주장을 다시 타입 체크할 수 있다.
4. 소스별 형식화 프로토콜: 본 논문은 데이터 소스를 동등한 신뢰 아티팩트로 취급하는 방법을 도입하며, 이는 클레임 측의 추론과 소스 측의 큐레이션을 분리하는 리프트 카탈로그(formalization)를 요구한다.

실험 결과

평가는 세 가지 티어에 걸친 TableBench(테이블 상의 수치 추론)에 집중한다:

• 티어 1 (골드-골 목표 벤치마크, $n=120$):

  • EG-VAR는 모호하지 않은 주장에 대해 **120/120 (100%)**를 달성하여, 골드 정답과 커널 체크된 증명을 일치시켰다.
  • 베이스라인(동일 모델, 도구는 있으나 커널 없음)은 95.0% (114/120)에서 정체되었다.
  • EG-VAR는 격차를 제로로 좁혔으며, 이는 커널 규율이 도구 출력의 올바른 구성을 강제함을 입증한다.

• 티어 1.5 (역사실적 스트레스 테스트, 5개 도메인 $\times$ 2개 모델):

  • 셀 값이 모델의 세계 지식 사전 지식과 모순되는 합성 테이블이 생성되었다(예: 특정 국가의 인구를 낮은 값으로 변경).
  • EG-VAR는 모든 도메인과 변화 폭에 대해 100% 소스 충실도를 유지했다.
  • 베이스라인(동일 도구 사용)은 80–90% (Sonnet) 및 50–80% (도구 미사용)로 떨어졌으며, 이는 EG-VAR가 모델이 검색된 증거를 무시하는 "사전 지식 덮어쓰기(prior-override)" 실패 모드를 구조적으로 방지함을 보여준다.

• 티어 2 (LLM 형식화 도구를 포함한 엔드 투 엔드, $n=120$):

  • LLM이 직접 형식적 목표를 제안하는 완전 자동화 설정(골드 픽스처 우회 제거)에서, 순수 형식화 에러율은 3.3% (Sonnet) 및 1.7% (Opus)였다.
  • 남은 불일치는 로그에 기록된 모호성(4.2%) 또는 벤치마크 아티팩트 이슈(1.7%)로 분류되었으며, 이는 모두 침묵하는 환각이 아닌 명시적이고 감사 가능한 형태였다.

의의 및 주장

본 논문은 EG-VAR를 고도의 신뢰가 요구되는 경험적 주장을 위한 기술적 거버넌스 인터페이스로 포지셔닝한다. 그 의의는 안전의 부담을 통계적 학습에서 아키텍처적 강제로 전환하는 데 있다:

• 근거 없는 출력의 제거: 구조적 보장은 "검증된 환각"(증거 없이 VERIFIED로 라벨링된 출력)이 시스템 위협 모델 하에서 불가능함을 보장한다.
• 측정 가능한 불확실성: 거절(abstention)을 학습된 행동이 아닌 커널 거부에 따른 구조적 결과로 만듦으로써, 시스템은 측정 가능한 "거절률"과 타입된 불확실성을 제공한다.
• 형식화 플라이휠(Formalization Flywheel): 저자들은 데이터 소스가 타입된 인터페이스(SQL, API, 지식 그래프)로 진화함에 따라, 형식화 부담이 재사용 가능한 인프라로 상쇄되어 검증당 비용을 줄일 것이라고 주장한다.
• 거버넌스 속성: 이 시스템은 세 가지 강제 가능한 속성을 가능하게 한다: (i) 재현 가능한 증명을 통한 모든 검증된 출력의 독립적 감사, (ii) 등급 규율을 통한 타입된 불확실성, (iii) 측정 가능한 시스템 속성으로서의 정직한 기권.

결론적으로, 의미적 형식화 오류(출시된 큐레이터 코퍼스를 통한 파인튜닝으로 해결 가능)는 여전히 존재하지만, **구조적 안전성 바닥(structural safety floor)**은 확립되었으며, 이는 경험적 추론에서 LLM 환각을 제거하는 길을 제시한다.