형식적 불확실성의 문법: 자동화된 추론 작업에서 LLM을 신뢰할 시점

초록

대형 언어 모델(LLM)은 형식 명세를 생성함으로써 자동화된 추론의 민주화에 있어 상당한 가능성을 보여줍니다. 그러나 근본적인 긴장이 존재합니다: LLM은 확률적이지만, 형식 검증은 결정론적 보장을 요구합니다. 본 논문은 LLM이 생성한 형식적 산출물에서의 실패 모드와 불확실성 정량화(UQ)를 포괄적으로 조사함으로써 이러한 인식론적 간극을 해소합니다. 5개의 최첨단 LLM에 대한 체계적인 평가를 통해, 만족도 모듈로 이론(SMT) 기반 자동 형식화가 정확도에 미치는 도메인별 영향(+34.8%의 논리적 작업에서 -44.5%의 사실적 작업까지)을 밝혀냈으며, 토큰 확률의 엔트로피와 같은 기존의 UQ 기법이 이러한 오류를 식별하지 못함을 확인했습니다. 우리는 LLM 출력을 모델링하기 위해 확률적 문맥 자유 문법(PCFG) 프레임워크를 도입하여 정제된 불확실성 분류 체계를 제시합니다. 불확실성 신호는 작업에 따라 다르며(예: 논리 작업에서 문법 엔트로피, AUROC>0.93), 이러한 신호들의 경량 융합은 선택적 검증을 가능하게 하여 최소한의 기권으로 오류를 크게 줄이고(14-100%), LLM 기반 형식화를 신뢰할 수 있는 엔지니어링 분야로 전환합니다.

English

Large language models (LLMs) show remarkable promise for democratizing automated reasoning by generating formal specifications. However, a fundamental tension exists: LLMs are probabilistic, while formal verification demands deterministic guarantees. This paper addresses this epistemological gap by comprehensively investigating failure modes and uncertainty quantification (UQ) in LLM-generated formal artifacts. Our systematic evaluation of five frontier LLMs reveals Satisfiability Modulo Theories (SMT) based autoformalization's domain-specific impact on accuracy (from +34.8% on logical tasks to -44.5% on factual ones), with known UQ techniques like the entropy of token probabilities failing to identify these errors. We introduce a probabilistic context-free grammar (PCFG) framework to model LLM outputs, yielding a refined uncertainty taxonomy. We find uncertainty signals are task-dependent (e.g., grammar entropy for logic, AUROC>0.93). Finally, a lightweight fusion of these signals enables selective verification, drastically reducing errors (14-100%) with minimal abstention, transforming LLM-driven formalization into a reliable engineering discipline.

형식적 불확실성의 문법: 자동화된 추론 작업에서 LLM을 신뢰할 시점

Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Tasks

초록

Support