When Many Answers Are Valid, Voting Fails: Symbolic Verification for Best-of-K Causal Reasoning in LLMs

기술 요약: 다수의 정답이 유효할 때, 투표는 실패한다

문제 정의
Self-Consistency와 같은 현재의 LLM 추론 시점 스케일링(inference-time scaling) 방법들은 샘플링된 추론 궤적(reasoning traces) 중 가장 빈번하게 등장하는 답이 가장 신뢰할 수 있다는 가정에 의존한다. 이러한 접근 방식은 인과 추론 작업에서 여러 개의 서로 다른 출력이 모두 완전히 정답일 수 있는 경우(예: Pearl의 백도어 기준을 만족하는 서로 다른 유효한 조정 집합들)에 실패한다. 이러한 "다중 만족(many-satisfier)" 시나리오에서는, 유효한 확률 질량(probability mass)이 여러 개의 정답 문자열로 파편화되는 반면, 하나의 부적절한 답이 단순히 가장 흔한 오류라는 이유만으로 투표에서 우위를 점할 수 있다. 결과적으로, 정확한 단순 다수결 투표(exact plurality voting)는 샘플링된 궤적의 대다수가 유효한 추론을 포함하고 있음에도 불구하고 부적절한 답을 선택할 수 있으며, 이는 일관성 없고 잘못된 선택으로 이어진다.

방법론: CALVER
저자들은 참조 정답(reference answer)을 참조하지 않고 $K$개의 샘플링된 궤적 풀에서 최적의 후보를 선택하도록 설계된 학습 불필요(training-free) 심볼릭 검증기인 CALVER(Causal Axiom-Level VERification)를 소개한다.

• 궤적 계약(Trace Contract): CALVER는 모델이 다음의 유형화된 6개 슬롯 스키마에 따라 추론을 출력하도록 요구한다: (1) 그래프, (2) 쿼리, (3) 전략, (4) 도출 기록, (5) 계산된 결과, (6) 정답.
• 심볼릭 검증: CALVER는 정답 빈도를 집계하는 대신, 각 궤적을 실행 가능한 인과적 명세(causal specification)에 대해 결정론적으로 점수를 매긴다. 검증기는 6가지 체크를 수행한다:
  1. 그래프 파싱: 그래프 구조(DAG 또는 ADMG)를 검증한다.
  2. 쿼리 바인딩: 쿼리 변수가 문제와 일치하는지 확인한다.
  3. 전략 유효성: 제안된 집합이 그래픽 기준(예: d-separation, m-separation, backdoor adjustment, intervention reachability)을 만족하는지 확인한다.
  4. 도출 기록: 추론 단계의 구문 및 출처(provenance)를 검증한다.
  5. 계산된 결과: 수치적 일관성을 보장하기 위해 함수(예: 평균 처치 효과, ATE)를 독립적으로 재계산한다.
  6. 정답 일관성: 최종 정답이 계산된 결과와 일치하는지 확인한다.
• 선택 규칙: 선택기는 가장 높은 점수(최대 배포 점수 6점)를 가진 궤적을 선택한다. 동점인 경우 가장 먼저 나온 궤적을 선택한다.
• 모드: CALVER는 두 가지 모드로 작동한다:
  • Supplied-Graph(제공된 그래프): 소스 그래프가 제공되며, 궤적은 이를 기준으로 점수가 매겨진다.
  • Constructed-Graph(구성된 그래프): 모델이 텍스트로부터 그래프를 추출해야 하며, 궤적은 모델이 재구성한 자신의 그래프를 기준으로 점수가 매겨지되, 최종 등급은 숨겨진 소스 그래프를 사용하여 판정된다.

주요 기여

1. 정식화: 본 논문은 다중 정답 상황에서의 best-of-$K$ 선택을 결정 가능한 유효성 클래스(decidable validity class)에 대한 집계로 정식화한다. CALVER는 이를 DAG 및 ADMG에 대한 6개 구성 요소의 그래프 의존적 궤적 점수로 구현한다.
2. 이론:
   • 엄격한 ATE 인증 적합성(Strict ATE Certificate Soundness): 저자들은 특정 가드(treatment exclusion 및 decision margin)를 만족하는 최대 점수 궤적이 평균 처치 효과(ATE) 쿼리에 대한 올바른 임계값 결정을 보장함을 증명한다.
   • 유효성 파편화 정리(Validity Fragmentation Theorem): 유효한 확률 질량이 여러 유효한 답으로 나뉘어 있을 때, 정확한 단순 다수결이 어떻게 일관성을 잃을 수 있는지(단일 부적절한 답이 약간 더 높은 개별 질량을 가짐으로써 승리할 수 있음)를 증명한다.
3. 실험: 다양한 모델 제품군(Qwen, Mistral), 그래프 제품군(CLEAR, bnlearn), 그리고 설정(제공된 그래프, 텍스트-투-그래프 구축, 논리 퍼즐)에 걸친 광범위한 평가를 수행한다.

결과

• 베이스라인 대비 우월성: 다수의 정답이 존재하는 CLEAR clean-core 벤치마크(126개 문제)에서, CALVER는 **42.1%**의 정확도를 달exp성하여 정확한 단순 다수결(~30.9%), 집합 인식 메도이드(set-aware medoid), 모델 확신도(model confidence), 학습된 보상 모델(Skywork Reward V2), 그리고 LLM 심사위원(72B 파라미터까지 확장된 경우 포함)을 크게 상회하였다.
• $K$에 따른 스케일링: 샘플링 예산($K$)이 증가함에 따라 CALVER와 다수결 간의 성능 격차가 벌어진다. 다수결의 성능은 정체되는 반면, CALVER는 계속해서 개선되어 $K=32$에서 **57.9%**에 도달한다.
• 그래프 복구에 대한 강건성: 텍스트-투-그래프 설정에서 정확한 그래프 복구율이 낮을 때(예: 자연스러운 서사 수준에서 34%)에도, CALVER는 다수결보다 17.6 퍼센트 포인트 더 높은 성능을 보인다. 이는 글로벌 그래프 구조가 불완전하게 재구성되더라도, 쿼리 국소적 관계가 보존된다면 후보별 검증이 성공할 수 있음을 입증한다.
• 일반화: CALVER는 독립적인 벤치마크(bnlearn, CausalGraph2LLM), 서로 다른 모델 제품군, 그리고 검증 술어(verification predicate)가 적응된 비인과적 도메인(Knights and Knaves 논리 퍼즐)으로 전이된다.
• 효율성: 심볼릭 검증은 생성 비용 대비 최소한의 오버헤드(7%)만을 추가하며, 단일 CPU 스레드에서 각 궤적을 18ms 내에 점수화한다.

의의 및 주장
본 논문은 CALVER가 다수의 유효한 답이 존재하는 체제에서 표면적 빈도나 학습된 선호도 모델보다 더 강력한 선택 신호를 제공한다고 주장한다. 저자들은 다음을 확립한다:

• 투표의 실패: 유효한 답이 투표를 파편화할 때, 인과 추론에서 정확한 단순 다수결은 근본적으로 결함이 있다.
• 실행 가능한 유효성: (심볼릭 체크를 통한) 태스크 정의 유효성 클래스의 충족 여부를 기반으로 집계하는 것이 정답 문자열 빈도에 기반하여 집계하는 것보다 더 신뢰할 수 있다.
• 체제 경계(Regime Bound): 이 방법은 많은 답이 유효하고 단일 추출물을 신뢰할 수 없는 "중간 체제"에서 가장 효과적이다. 답이 거의 유일하다면 표준 투표가 충분하며, 텍스트-투-그래프 추출이 매우 신뢰할 수 있다면 하나의 그래프를 추출하여 직접 푸는 것이 더 우수하다.
• 독립성: 선택 메커니즘은 학습된 휴리스틱이 아니라 실행 가능한 술어(인과적 공리 또는 논리 규칙)에 의존하므로, 다양한 모델 아키텍처와 학습 목적 함수에 대해 강건하다.

저자들은 CALVER가 실제 세계의 인과 그래프에 대한 과학적 진리를 결정한다고 주장하는 것이 아니라, 제공된 구조나 텍스트가 주어졌을 때 가장 형식적으로 유효한 추론 궤적을 선택하는 것이라고 강조한다. 이 방법의 이점은 후보의 추론에 대해 유효성 체크를 실행할 수 있는 능력에 엄격하게 결부되어 있다.