시그널-커버리지 매트릭스: 문장 자동 형식화(Statement Autoformalization)에서의 유형 및 의미론적 오류 계층화

LLM 자동 형식화(autoformalization)의 유형 정확도(type-correctness, TC%)는 2년 만에 $\sim$53%에서 $\sim$76%로 상승했지만, 이러한 스칼라(scalar) 값은 각 방법론이 어떤 오류를 해결하는지는 숨기고 있습니다. 우리는 Lean elaborator(통과/실패)와 의미론적 동등성 판단(동등/비동등)을 교차하여, 모든 출력을 네 가지 셀 중 하나로 분류하는 시그널-커버리지 매트릭스(signal-coverage matrix)를 제안합니다: 진정한 성공(true success, TS), 유형 전용(type-only, TO), 의미론 전용(semantic-only, SO), 또는 둘 다 실패(both fail, BF). Vanilla, Lean-Retry, Sample-Filter, 그리고 계층적 자동 형식화(Stratified Autoformalization, SAF)를 통해 DeepSeek V4-Pro 모델로 ProofNet# 및 MiniF2F-test를 테스트한 결과: (1) 세 가지 elab-feedback 방법론 전반에 걸쳐 +34에서 +36의 TS 이득은 $\sim$64%의 유형 계층(type-stratum) 회복을 의미하며, SO는 순수하게 정체되어 있습니다(기존 의미론적 오류의 87.5%를 구제했으나, 8개의 새로운 오류 생성). (2) 각 방법론의 TO-to-TS 비율은 23/61입니다 (Wilson 95% 신뢰 구간 [26.6%, 50.3%]). 이 계층 수준의 회복률은 홀드아웃(held-out) 방법론에 대한 $\Delta$TS를 2/186 이내로 예측하며, 6개의 (모델, 데이터셋) 셀 전체에서 $\Delta$TC를 Vanilla elab-fail 비율에 따라 선형적으로 나타냅니다 ($R^2=0.96$). (3) 두 판정관은 elab-feedback 출력에 대해 2637%p의 불일치를 보입니다 (Vanilla의 7%p 대비). 기호 판정관(symbolic-judge)의 위음성(false negatives) 중 3056%는 elaborator에 의해 강제된 재작성(rewrites)에서 기인합니다. 지속적인 잔여 오류는 두 개의 골드 형식화(gold-formalization) 오류로 감소합니다. TC%의 이득은 단순히 스칼라 값만으로 평가할 것이 아니라, 어떤 셀이 이동했는지에 따라 인정되어야 합니다.