FormInv: A Measurement Protocol for Semantic Invariance in Mathematical Reasoning Benchmarks

Motivation

• Known: 기존 수학 추론 벤치마크(GSM8K, MATH, MathBench 등)는 canonical formulation에 대한 정확도만을 측정하며, MathCheck·GSM-Plus·PutnamGAP 등 일부는 paraphrase 기반 견고성을 도입했지만 paraphrase의 논리적 동등성을 검증하는 절차(logical-equivalence check, cross-model unanimity)는 부재했다.
• Gap: Paraphrase 품질이 검증되지 않아 의미적으로 잘못된 paraphrase가 벤치마크 순위를 왜곡할 수 있으며, 기존의 raw consistency(SCR, VOV 등) 지표는 accuracy를 k개의 paraphrase에 걸쳐 compounding한 기계적 효과와 뒤섞여 있어 모델의 진짜 formulation brittleness를 difficulty와 분리하지 못한다.
• Why: 모델의 실제 수학적 이해 능력을 평가하려면 canonical accuracy만으로는 부족하며, 동일한 정답을 내는 이론(theorem)에 대해서도 표현 방식에 따라 답이 뒤집히는 현상(brittleness)을 분리해서 측정해야 신뢰할 수 있는 모델 랭킹과 벤치마크 설계가 가능하기 때문이다.
• Approach: Lean4로 검증된 Mathlib4 정리들을 canonical statement로 삼고, CAS 및 전문가 검증을 거친 8개 paraphrase family를 구성한 뒤, cross-model unanimity 기반 audit과 difficulty-controlled 지표인 CIR·SCR(및 per-theorem Cochran's Q 검정)을 통해 9개 모델의 semantic invariance를 측정한다.

Achievement

Figure 1. Per-family failure rates across three representative models (3-model shared evaluation). F5 (connective variat

1. Paraphrase 오류 자동 검출: cross-model unanimity(≥3/4 또는 ≥6/9 모델 일치)를 이용해 MathCheck에서 4개(3.1%)의 의미적으로 잘못된 paraphrase를 10달러 이하 비용으로 검출했고, 이를 제거하면 GPT-4o의 순위가 2위에서 4위로 하락하는 등 랭킹이 크게 변화함을 보였다.
2. CIR(Conditional Inconsistency Rate) 제안: 모든 모델이 canonical form에서 정답을 맞춘 정리들만 대상으로 조건화하여 accuracy confound를 제거한 지표를 제시했고, Claude Haiku 4.5(41.9%)와 DeepSeek V3(4.7%) 사이 37%p 격차를 발견했으며, CIR이 accuracy와 anti-correlated(ρ=-0.57~-0.59)함을 독립적인 두 데이터셋에서 재현했다.
3. No-Free-Benchmark corollary 증명: 어떤 모델도 모든 paraphrase family에서 우세하지 않으므로, 벤치마크가 포함하는 family 선택이 곧 모델 랭킹을 암묵적으로 결정한다는 명제를 제시했다.
4. FormInv 벤치마크와 FormInvSelector 구축: 103개 Lean4 검증 정리, 8개 paraphrase family, 760개(및 811개 harder track) 항목으로 구성된 데모 벤치마크를 만들고, 목표 task의 family 프로파일에 따라 최적 모델을 추천하는 FormInvSelector 유틸리티를 제공했다.

How

Figure 1. Per-family failure rates across three representative models (3-model shared evaluation). F5 (connective variat

• MathCheck 등 기존 벤치마크에 대해 cross-model unanimity 기반 audit(≥3/4 또는 ≥6/9 모델이 canonical은 맞히고 paraphrase는 틀리는 경우 flag)을 적용해 mislabeled paraphrase를 탐지
• 103개(및 확장 셋) Lean4-verified Mathlib4 정리를 canonical statement로 사용하고, CAS 및 전문가 검증을 거친 8개 paraphrase family(comparison-order, definition-by-expansion, connective-variation 등)를 생성
• 각 모델의 canonical-correctness로 조건화하여 CIR을 계산(난이도 통제), SCR(원시 일치율)과 함께 산출
• per-theorem Cochran's Q 검정으로 within-theorem failure clustering이 독립성 가정 하의 null보다 유의하게 높은지 검증(p<0.01, 8개 중 6개 모델)
• Spearman 상관분석으로 CIR과 canonical accuracy 간 관계(및 raw consistency와의 대비)를 분석하고, 독립적인 103개 정리 세트로 재현성 검증
• FormInvSelector로 모델별 per-family failure profile을 집계해 목표 task에 맞는 모델 추천

Originality

• 심리측정학의 Differential Item Functioning(DIF) 개념과 Doob의 L2 조건부 기대값 정리, measurement invariance theory를 형식 수학 추론 벤치마크 평가에 처음으로 도입
• 기존의 unconditional consistency 지표(VOV, XParaCon, CheckList INV, MathCheck robustness)가 accuracy compounding 효과와 혼재되어 있음을 명확히 지적하고, 이를 분리하는 difficulty-controlled 지표(CIR)를 제안
• 단일 모델 평가로는 발견할 수 없는 paraphrase 오류를 cross-model unanimity로 자동 검출하는 저비용(10달러 이하) audit 프로토콜을 실제 공개 벤치마크(MathCheck)에 적용해 재랭킹까지 실증
• "No-Free-Benchmark" corollary라는 새로운 이론적 명제를 통해 paraphrase family 선택이 벤치마크의 암묵적 모델 랭킹을 결정한다는 점을 정식화

Limitation & Further Study

• 데모 벤치마크의 규모가 103~366개 정리 수준으로 상대적으로 작아, 더 넓은 수학 영역·다양한 정리 유형에 대한 일반화 가능성은 추가 검증이 필요함
• paraphrase family가 8개로 제한되어 있어, 저자들이 다루지 않은 다른 유형의 semantic-preserving transformation에서도 유사한 CIR anti-correlation이 유지되는지는 불명확함
• cross-model unanimity 기반 audit은 여전히 다수 모델의 공통 편향(shared blind spot)에는 취약할 수 있어, 완전한 equivalence oracle의 대체재로 보기엔 한계가 있음
• Lean4 검증 및 CAS/전문가 검증에 의존하므로, 형식화가 어려운 자연어 중심 수학 문제로의 확장성에 대한 논의가 부족함
• 후속 연구로는 더 큰 규모의 정리 집합과 더 다양한 도메인(대수, 조합론 등)에 대한 CIR 검증, 그리고 audit 프로토콜의 완전 자동화 및 비용 절감이 필요함

Evaluation

총평: 단순 accuracy 기반 평가의 사각지대를 정량적으로 드러내고 이를 측정하는 재사용 가능한 프로토콜과 지표(CIR)를 제시한 점에서 벤치마크 평가 방법론에 실질적 기여를 하는 논문이며, 실제 공개 벤치마크에 적용해 재랭킹까지 보인 실증력이 인상적이다.