본 논문은 대규모 언어 모델(LLM)을 이용한 자동 추론의 민주화 가능성에 주목하면서, LLM이 생성하는 형식적 사양의 신뢰성 문제를 다룹니다. LLM의 확률적 특성과 형식적 검증의 결정론적 요구사항 간의 차이를 해소하기 위해, LLM이 생성한 형식적 산출물의 오류 모드와 불확실성 정량화(UQ)를 종합적으로 조사합니다. 5개의 최첨단 LLM을 체계적으로 평가하여, SMT 기반 자동 형식화의 정확도에 대한 도메인 특이적 영향(논리적 작업에서는 +34.8%, 사실적 작업에서는 -44.5%)을 밝히고, 토큰 확률의 엔트로피와 같은 기존 UQ 기법이 이러한 오류를 식별하지 못함을 보여줍니다. LLM 출력을 모델링하기 위한 확률적 맥락 자유 문법(PCFG) 프레임워크를 제시하여, 불확실성 분류 체계를 개선합니다. 불확실성 신호는 작업에 따라 다름을 발견하고 (예: 논리의 경우 문법 엔트로피, AUROC>0.93), 이러한 신호의 경량 융합을 통해 선택적 검증을 가능하게 하여 최소한의 기권으로 오류를 획기적으로 줄이고(14-100%), LLM 기반 형식화를 신뢰할 수 있는 엔지니어링 분야로 전환합니다.
