VOUCH for Mathematical Reasoning: Counterfactual Contracts Cure the Self-Verification Pathology

Motivation

• Known: chain-of-thought 수학 문제에서 self-consistency(Wang et al., 2023)나 same-family LLM-as-judge처럼 단일 모델이 자신의 반사실적 예측(counterfactual prediction)에 대한 commitment를 걸고 이를 검증하는 self-verification 방식이 별도의 오라클이나 실행 환경 없이 사용 가능하여 널리 쓰이고 있다.
• Gap: 이러한 single-side self-verification은 고정된 결정론적 디코딩 정책(rule ra)을 쓰는 self-coherent reasoner의 경우, commitment와 실제 post-intervention 예측이 구성상 항상 일치하게 되어 CCself(a;ι)=1이 성립하므로, 정답인지 여부와 무관하게 검증 이벤트가 항상 통과된다는 구조적 결함(unsoundness)이 이론적으로도 실증적으로도 검증되지 않은 채 방치되어 있었다.
• Why: 이 문제는 self-consistency, self-refine, same-family LLM-as-judge 등 현재 널리 쓰이는 multi-agent 검증 및 arbitration 프로토콜 전반에 구조적으로 내재된 취약점이며, adversarial 상황에서 confidently wrong solver를 careful solver와 구분하지 못해 verifier의 신뢰도 자체를 근본적으로 훼손할 수 있으므로 수학 추론뿐 아니라 LLM 기반 자기검증 체계 전반의 설계에 중요한 함의를 갖는다.
• Approach: Proposition 2.1을 통해 single-side counterfactual verification의 불건전성을 형식적으로 증명하고, 세 개의 수학 벤치마크에서 adversarial-prompt regime을 통해 그 병리(pathology)를 실증한 뒤, proposer가 자기 자신뿐 아니라 두 번째 에이전트의 post-intervention 예측까지 commit해야 하는 dual-side counterfactual contract를 제안하여 이를 완화한다.

Achievement

Figure 2. Per-cell relative reduction in hurt | acted-on-wrong mov-

1. 이론적 증명(Proposition 2.1): 고정 결정론적 디코딩 정책 하에서 self-form counterfactual consistency CCself(a;ι)가 정답 여부와 무관하게 항상 1이 됨을 증명하여 self-consistency 및 same-family LLM-as-judge 설정 모두에 적용되는 구조적 결함을 formalize했다.
2. 실증적 병리 재현: GSM8K, MATH-algebra, SVAMP 세 벤치마크의 clean/adversarial 6개 cell 전반에서 정확도는 최대 28pp 하락하는 동시에 self-verification rate는 최대 11.6pp 상승하는 일관된 cross-cell signature를 확인했다.
3. Dual-side contract 및 수렴 정리: cross-form counterfactual consistency(CCcross)에 기반한 dual-side VOUCH 프로토콜을 설계하고, hurt:caught ratio를 평균 46%(cell별 27%~68%) 감소시켰으며 모든 cell에서 95% bootstrap CI가 0보다 엄격히 크다는 것을 보였고, 세 가지 전제조건(C1~C3) 하의 장기 weight-convergence theorem(Theorem 3.5)도 제시했다.
4. 베이스라인 대비 구조적 원인 확인: 동일 계열 LLM-as-judge(Llama-3.1-8B)와 self-consistency(k=5) 베이스라인 모두 동일한 self-coherent pathology를 그대로 물려받음을 head-to-head 비교로 확인하여, 문제가 sampling이나 arbitration 방식이 아니라 구조 자체에 기인함을 입증했다.

How

Figure 3. Three-rate decomposition on all math and code cells. The dual-side construction lifts the catch rate (top) on

• Proposition 2.1: fixed deterministic rule ra, intervention ι, fa=ra, commitment ˆy′a(ι(x))=ra(ι(x))를 가정하고 verification event가 확률 1로 성립함을 수학적으로 증명
• Table 1: GSM8K(n=500), MATH-alg(n=300), SVAMP(n=300)에서 clean vs adversarial system prompt(rushed-engineer 디코딩 정책 유도)를 비교하여 accuracy와 verify rate 측정
• Dual-side 프로토콜: proposal(반대측 예측 ˆy′a,b 포함) → acceptance(기본 수락) → verification(S, C indicator 계산) → outcome(S=C=1일 때만 검증 통과, multiplicative weight update m(S,C))의 4단계 구조 설계
• Intervention menu I(숫자 변경, 절 제거, 무관한 방해 요소 추가, paraphrase, 문제 교체)에 대해 informativeness I(ι)를 정의하고 offline ranking으로 top-3를 선택하는 VOUCH-Adaptive 변형 구성
• hurt:caught ratio, bootstrap CI, 세 가지 rate(three-rate decomposition) 등을 이용해 6개 math cell 전체에서 정량적으로 평가하고 Llama-3.1-8B same-family judge, self-consistency k=5와 비교

Originality

• 기존에 암묵적으로 사용되던 self-verification 방식(self-consistency, same-family LLM-as-judge)의 근본적 불건전성을 tautology 형태의 형식적 증명(Proposition 2.1)으로 최초로 명시화했다는 점이 독창적이다.
• 단순히 경험적 실패를 보고하는 데 그치지 않고, cross-form counterfactual consistency라는 새로운 정의와 dual-side contract, 그리고 명시적 전제조건 하의 장기 수렴 정리(Theorem 3.5)까지 이론-실증을 결합한 완결적 해결책을 제시했다.
• intervention informativeness I(ι)라는 개념을 도입해 어떤 반사실적 개입이 진단적으로 유효한지 정량화하고 adaptive 변형으로 이어지는 설계적 통찰을 제공했다.

Limitation & Further Study

• 실험이 GSM8K, MATH-algebra, SVAMP 등 상대적으로 단순한 산술/대수 문제에 국한되어 있어, 복잡한 다단계 증명이나 code reasoning 등 다른 도메인으로의 일반화 가능성은 추가 검증이 필요하다.
• adversarial regime이 통제된 system prompt로 인위적으로 유도된 것이라 실제 배포 환경에서 발생하는 자연스러운 confidently-wrong 행동 패턴을 충분히 반영하는지 불분명하다.
• weight update의 네 가지 multiplier 값(1.20, 0.90, 0.95, 0.50)이 hyperparameter로 설정되어 있고 정성적 순서만 이론적으로 보장되므로, 실제 성능이 이 값들의 구체적 선택에 얼마나 민감한지에 대한 sensitivity 분석이 제한적이다.
• dual-side 프로토콜이 두 에이전트 간 disagreement가 존재하는 경우에만 적용 가능하여, 두 에이전트가 동일하게 잘못된 방향으로 self-coherent한 경우(공유된 bias)에는 여전히 취약할 수 있다.

Evaluation

총평: Self-verification의 구조적 결함을 형식적 증명과 실증으로 명확히 드러내고 이를 해결하는 dual-side contract를 제안한 점에서 이론적 엄밀성과 실용적 기여를 모두 갖춘 우수한 연구이나, 검증 범위가 비교적 단순한 수학 벤치마크에 국한되어 있어 폭넓은 일반화 검증이 후속 과제로 남는다.