Grammars of formal uncertainty: When to trust llms in automated reasoning tasks

Motivation

• Known: LLM은 형식명세(formal artifacts) 생성에 뛰어난 성능을 보이며, 형식방법의 대중화 가능성을 제시함. 기존 불확실성 정량화(UQ) 기법으로는 토큰 확률의 엔트로피 등이 존재.
• Gap: LLM은 본질적으로 확률적이나 형식검증은 결정론적 보증을 요구하는 근본적 인식론적 간극(epistemological gap)이 존재. SMT 기반 자동형식화(autoformalization)의 효과가 작업별로 극단적으로 다르며(+34.8% from -44.5%), 기존 UQ 기법들이 형식산출물의 오류를 식별하지 못함.
• Why: 형식검증이 안전-임계 시스템으로 제한되는 핵심 이유는 전문성 필요 및 노동 비용. LLM의 불확실성을 신뢰할 수 있는 방식으로 활용하면 형식방법을 민주화할 수 있음.
• Approach: LLM 출력의 확률분포를 PCFG로 모델링하고, 이로부터 도출된 25개 불확실성 메트릭을 작업별로 융합하여 선택적 검증을 수행.

Achievement

그림 1: '수학이나 물리를 공부하고 열심히 일하는 모든 사람은 성공할 것이다'라는 명제에 대한 LLM 생성 논리적 변형, 측정된 PCFG 규칙 빈도, 계산된 확률분포. 실제 데이터 사용, 합성 데이터 없음.

1. 실증적 실패모드 분석: 5개 최신 LLM을 4개 형식추론 데이터셋으로 평가하여 SMT 기반 자동형식화의 도메인 특이성을 정량화. ProofWriter에서 +34.8% 정확도 향상, FOLIO에서 -44.5% 저하. 기존 UQ 기법(토큰 확률 엔트로피)이 이러한 오류를 포착하지 못함을 증명.
2. PCFG 기반 확률 프레임워크: 측정 가능한 확률공간(Σ*, F)을 정의하고, LLM이 유도하는 확률측도(probability measure) µ_{T,θ,SMT}를 SMT-LIB v2 문법 기반 PCFG로 근사. 최대우도추정(MLE)과 Lidstone 평활화(smoothing)를 통해 규칙 확률을 추정하며, 커버리지 보증 정리(Coverage Guarantee Theorem 1)로 샘플 크기의 필요성을 이론화.
3. 세분화된 불확실성 분류법: 기존 epistemic/aleatoric 이분법을 넘어 4개 범주(epistemic-knowledge, epistemic-procedural, recursive-complexity, capacity-limited)로 확장한 정제된 분류체계 제시. 25개 메트릭 개발 및 평가 완료.
4. 작업 종속적 신호 식별 및 선택적 검증: 불확실성 신호가 작업에 따라 달라짐을 입증 (예: 논리 작업에서 문법 엔트로피 AUROC > 0.93). 경량의 모델-불가지론적(model-agnostic) 신호 융합으로 개별 메트릭 성능 초과. 최소 기각(minimal abstention)으로 오류율 14-100% 감소.

How

이론적 기초

• 확률공간 정형화: 문자 집합 Σ에 대해 모든 유한 문자열의 집합 Σ을 측정가능 공간 (Σ, F)으로 정의 (F는 실린더 집합 σ-대수)
• LLM 확률측도: 작업 T와 파라미터 θ에 대해 LLM이 유도하는 조건부 측도 µ_{T,θ,SMT} = µ_{T,θ}(A∩L_{SMT})/µ_{T,θ}(L_{SMT}) 정의

PCFG 근사 방법

• 샘플 수집: 목표 LLM에서 N개의 SMT-LIB 프로그램 샘플 P_N = {P₁, ..., P_N} 생성
• 구문분석: SMT-LIB v2 문법 G_{SMT}으로 각 프로그램 구문분석, 적용된 규칙(production rules) 기록
• MLE 추정: 규칙 r = (A → β)의 상대빈도 p̂_MLE(r) = C(r)/C(A)로 계산 (C(r): 규칙 적용 횟수, C(A): LHS 비단말 총 적용 횟수)
• 평활화: Lidstone 평활화 p̂^(β_s)_N(r) = (C(r) + β_s)/(C(A) + β_s|R_A|)로 영(zero) 카운트 처리

메트릭 도출 (정적/동적)

• 정적 메트릭: 비단말 개수 |V_{SMT}|, 규칙 개수 |R_{SMT}|, 비단말당 평균 규칙, 최대 분기 인수(branching factor), 재귀 유형 감지
• 스펙트럼 성질: 평균 행렬 B의 스펙트럼 반경 ρ(B) = max{|λ| | det(B - λI) = 0} (ρ < 1: 유한 유도 길이, ρ ≥ 1: 구조 복잡도 높음)
• 정보이론 메트릭: 비단말별 Shannon 엔트로피 H(A) = -∑_{A→β∈R_A} p(A→β)log₂p(A→β), 문법 전체 엔트로피, KL 발산(KLD), 엔트로피 비율

선택적 검증 파이프라인

• 다중 불확실성 신호의 경량 융합(lightweight fusion)
• 임계값(threshold) 기반 신뢰도 추정 및 검증 대상 선택
• 형식 검증 엔진(SMT solver) 호출 최소화로 계산 효율성 확보

Originality

• 뉴로-심볼 시스템의 인식론적 갭 해결: LLM의 확률성과 형식방법의 결정론적 요구를 PCFG 기반 수학 프레임워크로 연결한 첫 시도
• 구조화된 불확실성 정량화: 단순 토큰 확률 엔트로피 대신 문맥자유문법 규칙 수준의 확률 분포를 체계적으로 모델링
• 세분화된 분류체계: epistemic-knowledge, epistemic-procedural, recursive-complexity, capacity-limited 4개 범주로 기존 이분법 확장
• 작업별 메트릭 최적성 발견: 동일한 메트릭이 작업마다 다른 성능을 보이며, 작업 인식형 신호 융합의 필요성을 실증적으로 입증
• 카버리지 보증 이론: 샘플링 기반 근사의 이론적 신뢰성을 정식화 (Theorem 1: 실패 확률의 상한 도출)

Limitation & Further Study

• PCFG 근사의 한계: 실제 LLM 분포 µ_{T,θ,SMT}와 PCFG 모델 µ_G의 괴리. KL 발산 최소화 보증 있으나, 문맥 의존성(context-dependency) 미포함 (Neural PCFG로 일부 완화 제시)
• 샘플 크기 의존성: 신뢰할 수 있는 PCFG 파라미터 추정에 필요한 최소 샘플 수 N에 대한 명시적 지침 부재. Coverage Guarantee는 상한만 제공.
• 평가 범위 제한: 4개 형식추론 데이터셋과 5개 LLM으로 평가했으나, 더 다양한 도메인(기하, 프로그램 검증 등)과 최신 모델(GPT-4o, Claude 3.5 등) 포함 필요
• 선택적 검증의 실제 비용 미계산: 기각 시 인간 검토 또는 대체 방법의 실제 비용 분석 부재. 오류 감소의 trade-off 정량화 부족
• 후속 연구 방향:
  • Neural PCFG 기반 문맥 의존 모델로 근사 정확도 향상
  • 다중 LLM 앙상블에서의 신호 융합 최적화
  • 형식증명(formal proofs), 프로그램 합성 등 다른 형식산출물로 확장
  • 모달리티 인식 아키텍처(modality-aware architectures) 설계로 신뢰성 강화

Evaluation

총평: 본 논문은 뉴로-심볼 시스템의 근본적인 인식론적 갭을 PCFG 기반 확률 프레임워크로 해결하려는 창의적 시도이며, 이론적 기초와 메트릭 설계가 우수하나, 실험 범위