ProofGate: A Reproducible Audit of Faithfulness, Alignment, and Vacuity in State-of-the-Art Lean Theorem Provers

Motivation

• Known: Lean 4 커널이 승인한 증명은 검증 가능한 증거로 간주되어 왔고, DeepSeek-Prover-V2, Kimina-Prover-72B, Goedel-Prover-V2 등 최근 시스템들은 miniF2F·PutnamBench에서 88~99%대의 높은 pass rate를 보고해 왔다.
• Gap: implicit sorry, statement misformalization, informal-formal misalignment 등 여러 독립 관찰들이 존재함에도, 이들을 통합적으로 점검하는 재현 가능한 감사 도구나 표준화된 보고 프로토콜이 없어 보고된 pass rate가 실제로 무엇을 의미하는지 검증되지 않은 채 받아들여지고 있다.
• Why: 단일 실패 검증(예: sorry 은닉, 커널 신뢰 기반 확장, 통계-자연어 불일치, 문제 공허성)이 있어도 보고된 결과 전체가 unaudited claim이 될 수 있으므로, formal mathematical reasoning의 진전을 정확히 측정하려면 faithfulness·alignment·vacuity를 분리해 검증할 표준 계측 도구가 AI-for-Math 커뮤니티에 필수적이다.
• Approach: kernel-level axiom inspection, banned-tactic linter, negation-counterexample probe, FormalAlign 방식의 alignment score라는 네 가지 직교적 검사를 결합해 단일 무차원 지표 Faithful-Pass(및 커널 전용 변형 Kernel-Faithful-Pass)를 산출하는 Python 패키지 ProofGate를 구축하고, 이를 DeepSeek-Prover-V2, Kimina-Prover-72B, Goedel-Prover-V2의 모든 공개 증명 아티팩트에 적용한다.

Achievement

1. 통합 분류체계 제시: 현재 pass-rate 지표가 혼동하는 faithfulness, alignment, vacuity라는 세 실패 모드를 명확히 구분하는 taxonomy를 제안했다.
2. 오픈소스 감사 파이프라인 ProofGate 공개: 네 가지 직교 검사를 통합해 Faithful-Pass와 Kernel-Faithful-Pass라는 단일 지표를 산출하는 Python 패키지를 배포했으며, 각 검사를 lean4checker, Comparator, Plausible 같은 기존 도구로 대체 가능한 백엔드로 설계했다.
3. 합성 코퍼스 검증: 각 항목에 정답 판정이 수작업으로 부여된 10개 adversarial 코퍼스에서 파이프라인이 10개 모두 일치하는 것으로 검증했다.
4. SOTA 3개 시스템 전수 감사: 총 879개 공개 증명에 대한 정적 감사와, DeepSeek·Kimina의 635개 증명 전체에 대한 pinned mathlib 기준 전체 kernel-level 감사, τ=0.40(사전 등록)에서의 SBERT 기반 alignment 감사를 수행했다.
5. 주요 실증 발견: (i) 커널 감사 결과 Kernel-Faithful-Pass_T1=100%로 sorry나 추가 axiom이 전혀 없음을 확인했으나 T0 기준에서는 Kimina 11개 증명이 native_decide를 사용해 예외임을 밝혔고, (ii) DeepSeek miniF2F-test에서 SBERT 기반 오정렬률 15.2%가 ReForm의 전문가 주석 비율과 1.2%p 이내로 근접함을 보였으며, (iii) Goedel-Prover-V2의 miniF2F "공개 증명"이 실제로는 sorry placeholder만 있는 벤치마크 입력 문장에 불과함을 논문이 명시하지 않은 채 밝혀냈다.

How

• Check 1 (kernel-level axiom inspection): 각 prover의 고정된(pinned) mathlib revision에 대해 커널 레벨에서 axiom base와 sorryAx 존재 여부를 검사하고, 엄격한 신뢰 기반 T0와 native_decide 등을 허용하는 확장된 T1을 구분해 평가
• Check 2 (banned-tactic linter): 소스 레벨에서 금지된 tactic(예: sorry로 이어질 수 있는 permissive tactic) 사용 여부를 정적으로 검출
• Check 3 (negation-counterexample probe): 명제의 부정에 대한 반례 탐색을 통해 vacuous(공허한) 문제 여부를 판별
• Check 4 (FormalAlign-style alignment score): SBERT 기반 임베딩 유사도로 자연어 진술과 formal statement 간 의미적 정렬도를 사전 등록된 threshold τ=0.40 기준으로 측정하고 τ∈[0.30,0.50] 구간에서 민감도 분석 수행
• 이상의 네 검사를 통합해 단일 dimensionless metric Faithful-Pass 및 Kernel-Faithful-Pass 산출
• DeepSeek-Prover-V2(635개), Kimina-Prover-72B(197개), Goedel-Prover-V2 등 공개된 모든 증명 아티팩트(총 879개 정적 감사)에 파이프라인 적용

Originality

• 기존에 개별적으로 존재하던 lean4checker, Comparator, Plausible 같은 Lean 생태계 도구들의 기능을 하나의 통합 감사 파이프라인으로 결합하고 substitutable backend 구조로 설계한 점
• faithfulness, alignment, vacuity라는 서로 혼동되어 온 세 현상을 명시적으로 분리하는 taxonomy와 이를 정량화하는 단일 무차원 지표 Faithful-Pass를 제안한 점
• 특정 시스템의 우열을 가리려는 목적이 아니라, 커뮤니티 전체가 사용할 재현 가능한 measurement instrument와 보고 프로토콜을 제공하려 한 연구 목적의 프레이밍
• 세 SOTA 시스템의 공개 아티팩트 전수(635개 kernel-level 전체 감사 포함)에 대한 실증적 감사를 수행해, Goedel-Prover-V2의 "증명"이 실제로는 sorry placeholder뿐이라는, 해당 논문이 명시하지 않은 사실을 발견한 점

Limitation & Further Study

• Check 2(banned-tactic linter)는 소스 레벨 검사이므로 선언된 theorem signature가 벤치마크 기대치와 다른 유형의 unfaithfulness는 현재 포착하지 못하며, 저자들도 Comparator를 향후 후속 도구로 제안함
• Check 3(vacuity probe)은 고정된 소수 tactic만 사용하는 작은 probe로, Plausible 같은 무작위 반례 탐색 도구보다 검출력이 떨어짐
• SBERT 기반 alignment score는 threshold τ 설정에 민감하며 전문가 주석과 완전히 일치하지는 않음(1.2%p 차이는 남아 있음)
• 감사 대상이 3개 시스템의 공개 아티팩트에 국한되어 있어 일반화 가능성에는 한계가 있고, PutnamBench 등 다른 벤치마크로의 전체 확장은 향후 과제로 남아 있음
• 후속 연구로 Comparator, Plausible을 실제 백엔드로 통합하고, miniF2F·PutnamBench 유지관리자 및 향후 prover 논문 저자들이 채택할 표준 보고 프로토콜 확산이 필요함

Evaluation

총평: 보고된 pass rate 뒤에 숨겨진 여러 실패 모드를 체계적으로 분리하고 실제 공개 아티팩트를 전수 감사해 구체적이고 반박하기 어려운 실증적 문제(특히 Goedel-Prover-V2 사례)를 드러낸 점에서 AI-for-Math 커뮤니티에 실질적 기여를 하는 연구이며, 각 개별 검사 기법 자체의 참신성보다는 통합과 실증적 적용의 가치가 크다.