Faults in Our Formal Benchmarking: Dataset Defects and Evaluation Failures in Lean Theorem Proving

Motivation

• Known: Lean 커널은 주어진 proof artifact가 formal statement를 증명함을 수학적으로 확실히 보장하며, 이 때문에 커널 검증을 통과한 벤치마크 결과는 통상 신뢰할 만한 것으로 간주되어 왔다.
• Gap: 그러나 커널 검증은 formal statement가 원래의 informal problem을 충실히 인코딩했는지, 평가 하네스가 trivial하거나 adversarial한 해법에 강건한지는 전혀 보장하지 않으며, 이로 인한 fidelity 결함과 evaluation loophole이 벤치마크 신뢰성을 훼손할 수 있다는 점이 충분히 다뤄지지 않았다.
• Why: LLM 기반 theorem proving 시스템(DeepSeek-Prover V2, Goedel Prover 2, Kimina Prover 등)의 성능 비교와 발전 방향이 이러한 벤치마크 점수에 의존하고 있으므로, 벤치마크 자체의 결함은 보고된 능력 향상이 실제 능력 향상인지 여부를 왜곡할 수 있어 매우 중요한 문제이다.
• Approach: 저자들은 formal benchmarking 파이프라인을 5단계(informal problem, formalization, model/prover, Lean kernel, reported metric)로 분해하여 커널이 실제로 보장하는 trust boundary가 어디인지 규명하고, corpus 규모의 static checker와 LLM 기반 semantic-audit prompt를 결합해 다섯 개 주요 Lean 벤치마크와 그 fork들을 감사한다.

Achievement

1. 대규모 결함 발견: 13개 벤치마크 변형(약 10,000개 문제)에 대해 corpus-wide static checker를 실행하여 4,833건의 findings를 도출했고, 이 중 398건은 반례, 공허 정리(vacuous theorem), 불건전 공리(unsound axiom) 등 기계적으로 인증 가능한 결함이었다.
2. 결함 분류체계(fault taxonomy) 제안: fidelity issues(specification/formalization/domain/Lean encoding), evaluation loopholes(robustness), maintenance decay로 구성된 taxonomy를 제시하고 각 범주가 요구하는 서로 다른 교정 방식을 명확히 했다.
3. 평가 점수에 대한 실증적 영향 분석: 92개 문제로 구성된 labeled challenge set과 corrected subset을 통해 결함이 보고된 prover 점수를 부풀리거나(inflate) 낮출(deflate) 수 있음을 실증했다.
4. 자동화 도구 및 릴리즈 표준 공개: Lean 4 metaprogram 기반 static checker와 recall-oriented semantic-audit prompt, 수정된 dataset snapshot을 공개하여 향후 formal math dataset 제작과 평가의 재현성·신뢰성을 높이는 표준을 제안했다.

How

• Lean 4 metaprogram으로 구현된 static checker를 13개 벤치마크 변형 전체(~10,000 문제)에 적용해 결함을 스캔
• 발견된 결함 중 기계적으로 검증 가능한 것(반례 존재, vacuous theorem, unsound axiom 등)에 대해 machine-checkable certificate 부여
• static analysis로 판별 불가능한 semantic mismatch(예: informal problem과의 불일치)를 탐지하기 위해 92개 문제로 구성된 labeled challenge set에 LLM 기반 recall-oriented semantic-audit prompt 적용
• fidelity issues(specification/formalization/domain & definition/Lean encoding), evaluation loopholes(proof acceptance robustness), maintenance issues(버전 드리프트, mathlib 변화)로 구성된 fault taxonomy(Table 2) 구축
• 결함이 수정된 corrected subset에서 기존 prover 점수와 비교하여 결함이 점수에 미치는 영향(inflate/deflate) 측정
• 대표 사례(missing hypothesis, incomplete translation, wrong domain/type, version/definition drift, incorrect source statement 등)를 Figure 2-5로 구체적으로 제시

Originality

• 기존 연구들이 개별 문제 오류를 산발적으로 지적한 것과 달리, formal benchmarking 파이프라인 전체를 5단계로 분해하여 Lean 커널의 trust boundary가 실제로 어디까지인지 최초로 명확히 개념화함
• corpus-scale static checker와 LLM 기반 semantic audit을 결합한 하이브리드 감사 방법론을 제시하여, 기계적으로 결정 가능한 결함과 그렇지 않은 semantic mismatch를 분리해서 다룸
• fidelity issues, evaluation loopholes, maintenance decay라는 3분류 체계와 이에 대응하는 서로 다른 교정 방식(review vs. static analysis vs. harness 강화 vs. version pinning)을 명시적으로 매칭한 실행 가능한(actionable) taxonomy 제안
• 단순 결함 발견에 그치지 않고 결함 수정이 실제 보고된 prover 점수에 미치는 정량적 영향까지 실증한 점

Limitation & Further Study

• 감사 대상이 miniF2F, ProofNet, FormalMath, CombiBench, ProverBench 등 5개 벤치마크와 그 fork에 국한되어 있어, Lean 생태계 밖(Isabelle, Coq 등) 및 더 광범위한 벤치마크로의 일반화 가능성은 검증되지 않음
• semantic mismatch 탐지에 사용된 LLM 기반 audit prompt는 92개 문제라는 비교적 작은 labeled challenge set에서만 검증되어, 대규모 자동 semantic audit의 recall/precision에 대한 엄밀한 정량적 평가가 제한적일 수 있음
• 정적 분석 checker가 탐지할 수 없는 미묘한 fidelity issue(예: 문제 의도의 뉘앙스 손실)는 여전히 수작업 검토에 의존하며, 향후 이러한 semantic audit의 자동화 수준을 높이는 후속 연구가 필요함
• mathlib과 Lean 버전이 지속적으로 진화함에 따라 maintenance decay 문제는 일회성 감사로 완전히 해결되지 않으므로, 지속적인 버전 고정 및 능동적 stewardship 체계의 실질적 운영 방안에 대한 추가 검토가 필요함

Evaluation

총평: LLM 기반 theorem proving 커뮤니티가 당연시해온 "커널 검증 = 벤치마크 신뢰성"이라는 가정을 정면으로 반박하며, 대규모 실증 감사와 실행 가능한 taxonomy로 문제의 심각성과 해법을 동시에 제시한 시의적절하고 중요한 연구이다.