Ground False: Dissecting Errors in Formal Mathematics Benchmarks

Motivation

• Known: ProofNet, PutnamBench, FATE 등 formal math 벤치마크들은 theorem proving과 autoformalization 모델 비교의 표준 척도로 널리 쓰여 왔으며, 이들의 released ground-truth formalization은 별도 검증 없이 그대로 신뢰되어 왔다.
• Gap: Theorem proving용 formalization은 정확성을 보증하는 formal proof 없이 배포되고, autoformalization의 informal source에 대한 faithfulness 판정은 벤치마크 저자 개인의 주관적 판단에만 의존하여 집단적 합의(collective consensus)가 부재하다는 근본적 검증 공백이 존재한다.
• Why: GT 오류는 theorem-proving 신호를 인위적으로 제한(cap)하고 equivalence 기반 autoformalization 지표에서 모델 간 성능 격차를 압축시키는 등, 벤치마크 평가 결과 자체를 예측 가능하지만 비대칭적인 방향으로 왜곡할 수 있어 커뮤니티가 신뢰하는 리더보드와 모델 비교의 타당성을 근본적으로 위협한다.
• Approach: Lean provability check, LLM faithfulness judge, human review를 결합한 semi-automated pipeline으로 ProofNet 367개 항목 전체를 3개 축(provability, logical strength, root cause)에 따라 감사하고, 동일 파이프라인을 6개 타 벤치마크에 적용해 오류율을 비교했다.

Achievement

Figure 3. Effect of wrong GTs on theorem-proving evaluation. “GT easier” over-estimates capability; “GT false” caps sign

1. 대규모 오류 발견: ProofNet 367개 항목 중 204개(56%)가 unfaithful이며 이 중 104개(28%)는 mathematically false임을 실증함.
2. 3축 taxonomy 구축: provability(참/거짓/불명), logical strength(stronger/weaker/incomparable/faithful), root cause(informal math 오독, missing premise, Mathlib 오독 등 9개 범주)로 오류를 체계적으로 분류함.
3. 평가 편향의 정량적 규명: false GT가 theorem-proving 신호를 cap하고, equivalence 기반 autoformalization 지표가 gap-compression 및 우연적 일치(coincidental agreement)로 인해 faithful 모델을 오히려 불리하게 만든다는 비대칭적 편향 메커니즘을 제시함.
4. ProofNet-Verified 공개: 367개 전 항목에 대한 per-item taxonomy label과 수정된 GT를 포함한 교정 벤치마크를 배포함.
5. 범용성 확인: PutnamBench, ProverBench, CombiBench, LeanCat, FATE family 등 6개 벤치마크에 동일 파이프라인을 적용해 unfaithful-GT 비율이 4.8%~60.0%로 한 자릿수 이상 차이 나며, 이는 큐레이션 과정(curatorial process)의 질에 좌우됨을 보임.

How

Figure 1. Misunderstanding of informal math. S1 is misread as a sphere in R, collapsing the domain to {−1, 1}.

• GT를 informal claim의 정답 formalization I에 대해 background theory T 하에서 논리적으로 동치(T ⊢ (G ↔ I))인지 여부로 faithfulness를 정의함
• Lean(Moura & Ullrich, 2021)을 이용해 formalized statement의 negation을 증명 시도함으로써 provability(참/거짓) 판정
• logical strength 축에서 G⇒I, I⇒G 함의 관계를 확인해 stronger/weaker/incomparable로 분류
• root cause 범주는 ProofNet 초기 판독에서 소수 범주를 시딩한 뒤, 전체 수작업 감사 과정에서 분할·병합·추가를 반복하며 안정화(iterative refinement)시킴
• LLM faithfulness judge와 human review를 결합한 semi-automated 파이프라인을 구성해 ProofNet 및 6개 타 벤치마크(PutnamBench, ProverBench, CombiBench, LeanCat, FATE family)에 적용

Originality

• Theorem proving과 autoformalization 두 태스크의 GT 신뢰성 문제를 동시에 다루며, 두 태스크에 미치는 편향 메커니즘을 각각 다르게(capping vs. gap-compression) 규명한 점이 독창적임
• provability, logical strength, root cause라는 직교하는 3축 taxonomy를 제시하여 단순 오류 분류를 넘어 원인-결과 매핑(root cause → logical strength → evaluative bias)까지 연결한 분석 틀을 구축함
• 단일 벤치마크 사례 연구에 그치지 않고 6개 이종 벤치마크에 동일 파이프라인을 적용해 실패 양상의 일반화 가능성과 절대적 품질 편차를 함께 보고한 점

Limitation & Further Study

• ProofNet-Verified 구축 과정에서 LLM faithfulness judge가 사용되는데, 이 judge 자체의 판단 오류나 편향이 최종 라벨의 신뢰성에 영향을 줄 수 있어 human review에 상당 부분 의존하는 구조적 한계가 있음
• provability 판정이 Lean에서 negation을 증명하지 못하는 경우 "Unknown"으로 남기 때문에, false임을 확정하지 못하는 항목들에 대한 처리 방식이 보수적일 수 있음
• 6개 타 벤치마크에 대한 감사가 ProofNet만큼 전수 조사인지, 또는 표본 조사인지 본문에서 명확히 드러나지 않아 오류율 비교의 엄밀성에 대한 추가 검증이 필요함
• 후속 연구로 다른 언어(Lean 외 Isabelle, Coq 등)나 더 넓은 범위의 자동화된 domain-specific 검증 도구를 결합해 human review 의존도를 낮추는 방향이 제안될 수 있음

Evaluation

총평: 공식 수학 벤치마크의 근본적 신뢰성 문제를 대규모 수작업 감사로 실증하고 이를 교정한 ProofNet-Verified와 일반화 가능한 taxonomy를 제공한 점에서 커뮤니티에 중요한 기여를 하는 연구이나, LLM judge 의존성과 타 벤치마크 감사의 엄밀성에 대한 추가 설명이 필요하다.