기술 요약: ForEx – 논리적 오류 탐지를 위한 설명 가능한 추론용 형식 검증 프레임워크

1. 문제 정의

대규모 언어 모델(LLM)의 논리적 오류 탐지 평가는 주로 예측 정확도(레이블 정답 여부)에 의존한다. 그러나 이러한 접근 방식은 모델이 제공한 추론이 실제로 예측된 레이블을 뒷받ing하는지를 검증하지 못한다. 올바른 예측은 진정한 논리적 도출이 아닌 표면적인 상관관계에서 비롯될 수 있으며, 반대로 잘못된 예측은 특정 해석하에서는 형식적으로 타당하지만 인간의 주석(annotation)과는 다른 추론 과정을 동반할 수 있다.

또한, 기존의 기호적 접근 방식(예: NL2FOL)은 일반적으로 입력된 논증의 만족 가능성을 확인하기 위해 입력 인자를 형식화할 뿐, 모델이 생성한 추론 과정을 형식화하지는 않는다. 더불어, 표준적인 주석 관행은 해석적 변이를 단일한 "골드(gold)" 레이블로 압축하여, 논증에 대한 타당한 대안적 해석을 가릴 위험이 있다. 즉, 예측된 레이벨, 생성된 설명, 그리고 그 설명의 형식적 도출 가능성을 공동으로 분석하는 프레임워크가 부족한 실정이다.

2. 방법론: ForEx 프레임워크

저자들은 ForEx(Formal Verification for Explainable Reasoning)를 제안한다. 이 프레임워크는 LLM이 생성한 자연어 설명을 Lean4(형식 증명 보조 도구)로 변환하여, 변환된 근거가 인코딩된 전제 하에서 도출 가능한지를 검증한다. 워크플로우는 다음 세 단계로 구성된다:

A. 추론 후보 생성

"Reasoner" 모델은 입력 문장을 전달받아 최대 $k$개의 후보를 생성한다. 각 후보는 $(f_i, a_i, s_i)$를 포함하는 튜플이다:

• $f_i$: 예측된 논리적 오류 유형.
• $a_i$: 자연어 설명(근거).
• $s_i$: 설명을 형식화한 Lean4 구조.

"Modifier"는 $s_i$를 초기 Lean4 코드로 변환한다.

B. 실행 피드백 및 Lean4 검증

이 단계는 생성된 Lean4 코드가 컴파일되도록 반복적인 수정 루프를 사용한다:

1. 컴파일 시도: "Executor"는 Lean4 코드를 컴파일하려고 시도한다.
2. 피드백 루프: 컴파일에 실패하면(상태 F), Executor는 에러 메시지와 원래의 설명 $a_i$를 전달받아 코드를 수정한다.
3. 제약 조건: 의미적 왜곡(semantic drift)을 방지하기 위해 수정은 원래의 설명과 초기 코드 내로 엄격히 제한된다. Executor는 새로운 논리적 내용을 도입할 수 없다.
4. 종료: 루프는 코드가 성공적으로 컴파일될 때(상태 T) 또는 최대 수정 횟수($iter_{max}$)에 도달할 때까지 계속된다.

C. 레이블 일관성 평가

프레임워크는 레이블 정답 여부와 형식 검증 상태를 분리하기 위해 LLM Argument Verification Matrix를 도입한다. 이 매트릭스는 두 축을 기준으로 출력을 네 가지 사분면으로 분류한다:

1. Lean4 검증: 통과(컴파일 성공) vs 실패(컴파일 실패).
2. 레이블 일관성: 일치(예측이 인간 주석과 동일) vs 불일치.

네 가지 결과 카테고리는 다음과 같다:

• Compilable-Correct (CC): 통과 및 일치.
• Compilable-Alternative (CA): 통과 및 불일치 (인간의 주석과 다른 레이블을 지지하는 형식적으로 유효한 추론 과정을 나타냄).
• Uncompilable-Correct (UC): 실패 및 일치.
• Uncompilable-Incorrect (UI): 실패 및 불일치.

D. 합의 기반 주석 파이프라인 (Consensus-Guided Annotation Pipeline)

주석의 모호성을 해결하기 위해 저자들은 다음의 파이프라인을 제안한다:

1. 모델과 인간의 주석을 오류 카테고리에 대한 멀티-핫 벡터(multi-hot vectors)로 표현한다.
2. PCA(주성분 분석)와 마할라노비스 거리(Mahalanobis distance)를 사용하여 이상치 모델을 식별하고 필터링한다.
3. 잽커 거리(Jaccard distance)를 계산하여 "고합의(high-consensus)" 문장(낮은 불일치)을 식별한다.
4. 적어도 50%의 잔류 모델이 형식 검증 하에서 특정 레이블을 할당하는 경우, 고합의 문장에 대해 주석을 확장한다.

3. 주요 기여

1. ForEx 프레임워크: LLM이 생성한 설명을 Lean4로 변환하여, 단순한 입력 인자가 아닌 형식화된 추론 체인을 기계적으로 검사할 수 있게 하는 새로운 시스템을 제공한다.
2. LLM Argument Verification Matrix: 레이블 일관성과 형식 검증 상태를 분리하는 지표를 통해, 기존 인간 주석과 상충하면서도 형식적으로 도출 가능한 추론을 제공하는 사례("Compilable-Alternative" 카테고리)를 드러낸다.
3. Consensus-Guided Annotation Pipeline: 인간의 기준, 다중 LLM 합의, 형식 검증을 결합하여 주석 분석 및 보수적인 레이블 확장을 지원하며, 주석의 불일치를 노이즈가 아닌 해석적 변이의 신호로 취급한다.

4. 실험 결과

프레임워크는 LOGIC-Climate 데이터셋(1,074개 인스턴스, 13개 오류 카테고리)을 대상으로 평가되었으며, 10% 샘플링된 부분 집합과 15개의 서로 다른 Reasoner 모델(사고형 및 비사고형 변체 포함)을 사용하였다.

• 컴파일 성공률: Lean4 컴파일 통과율은 4회의 수정 반복 후 초기 **36.70%**에서 **98.65%**로 증가했다. 대부분의 이득은 첫 번째 반복 후에 발생했다.
• 검증 vs 레이블 일치:
  • **Compilable-Correct (CC) + Compilable-Alternative (CA)**의 결합 비율은 일관되게 높았으며, 대부분의 모델에서 **90%**를 초과했다(최고 97.59%). 이는 대다수의 LLM 출력이 검증을 통과하는 형식적 추론 체인으로 변환될 수 있음을 나타낸다.
  • 그러나 인간의 레이벨과 일치하는 CC 비율은 상위 모델들 사이에서 약 17%에서 23% 사이로 현저히 낮았다.
  • CA 비율이 지배적이었으며, 이는 많은 형식적으로 검증된 추론 체인이 인간의 주석과 다른 레이블을 지지하고 있음을 시사한다.
• 오류 분석:
  • Uncompilable-Correct (UC) 비율은 매우 낮았으며(<2%), 이는 이 환경에서 올바른 레이블이 검증 가능한 추론 체인 없이 발생하는 경우가 드물다는 것을 의미한다.
  • Uncompilable-Incorrect (UI) 실패는 주로 "오류 없음(No Fallacy, NF)" 예측 때문이었으며, 이는 고립된 단일 문장 입력의 맥락 부족으로 인해 발생했을 가능성이 있다.
• 주석 확장: 합의 기반 파이프라인은 고합의 문장들을 식별했다. 확장된 주석은 원래의 인간 주석에 대해 **0.77의 재현율(recall)**을 달성하였으며, 원래 레이블의 대부분을 보존하면서도 형식적으로 지지되는 대안들을 추가하였다.

5. 의의 및 주장

본 논문은 ForEx가 LLM 평가를 단순한 레이블 정답 여부를 넘어 형식화된 추론 체인의 기계 검증 가능한 분석으로 이동시킨다고 주장한다.

• 체계적 간극: 결과는 형식적 도출 가능성과 레이벨 일치 사이의 체계적인 간극을 드러낸다. "Compilable-Alternative" 출력의 높은 빈도는 기존의 인간 주석이 입력 논증에 대한 타당한 해석을 충분히 포착하지 못하거나, 모델이 다른 가정 하에서 올려히 추론하고 있을 가능성을 시사한다.
• 예측을 넘어: 본 프레임워크는 모델이 "골드" 레이벨과 다르더라도 형식적으로 유효한(인코딩된 전제 하에서 도출 가능한) 추론 체인을 제공할 수 있음을 입증한다. 이러한 구별은 표준적인 예측 기반 지표에서는 보이지 않는 부분이다.
• 주석의 유용성: ForEx는 검증 도구일 뿐만 아니라 다운스트림 주석 분석을 위한 메커니즘으로 제시된다. 이는 골드 레이벨이 불충분하거나 여러 유효한 해석이 존재하는 경우를 식별하여, 합의 기반의 대안 레이블로 주석을 확장하는 데 도움을 준다.

저자들은 Lean4를 통한 형식 검증이 인코딩된 전제 하에서의 도출 가능성을 인증하는 것이지, 원래의 자연어 문장과의 의미적 일치(semantic alignment)를 보장하는 것은 아니라는 점을 언급하며 신중한 태도를 유지한다. 자연어는 완전히 명시된 의미론적 토대를 갖추지 못하므로, 형식화 자체가 불완전할 경우 형식적 결과가 모델의 능력을 과장할 수 있음을 인정한다. 향-후 연구로는 더 풍부한 논증 구조와 맥락 정보를 통합하여 검증 결과와 의미적 정확성 사이의 정렬을 개선하는 것이 제안되었다.