An Auditable Harness for AI-Assisted Lean Formalization: Pilot Logs from Finite Differential Privacy

Motivation

• Known: Lean 4와 Mathlib는 커널 검증을 통한 강력한 정확성 오라클을 제공하며, 언어모델을 활용한 tactic 제안·증명 탐색·autoformalization 연구가 miniF2F, ProofNet 등 벤치마크에서 활발히 이루어지고 있다.
• Gap: 그러나 프롬프트, 원본 출력, 컴파일 로그, 정리 진술이 함께 공개되지 않아 AI-assisted formal mathematics의 workflow 주장들을 재현하고 검증하기 어려우며, 특히 컴파일 성공만으로는 모델이 목표를 약화시키거나 로컬 정의를 변경해 트리비얼하게 통과시키는 실패 모드를 감지할 수 없다는 방법론적 공백이 있다.
• Why: AI가 정리를 "증명했다"는 주장이 컴파일 성공만으로 액면 그대로 받아들여지는 관행은 sorry/axiom 같은 escape hatch나 진술 왜곡 같은 숨은 실패를 못 보이게 하므로, 재현 가능하고 감사 가능한 로깅 스키마는 향후 AI-for-math 연구의 신뢰성 있는 비교와 허위 능력 주장 제거에 필수적이다.
• Approach: 각 시도에 대해 prompt SHA-256, 원문 또는 상태태그 트랜스크립트, 추출된 Lean 파일, lake env lean 컴파일 로그, escape-hatch 스캔, 진술/컨텍스트 감사를 모두 기록하는 고정 파이프라인을 설계하고, 이를 gpt-5.4/gpt-5.5 두 모델과 6개 finite-DP 정리, 셀당 2회 시행으로 총 24회 시도에 적용했다.

Achievement

1. 높은 컴파일 성공률과 완전한 진술 보존: 24회 시도 중 21회(87.5%, Wilson 95% CI 69.0-95.7%)가 컴파일에 성공했고, 24/24 모두 할당된 정리 진술과 로컬 Lean 컨텍스트를 그대로 보존했으며 escape hatch 사용은 전무했다.
2. 실패 모드의 세밀한 분류: 3건의 실패를 hallucinated lemma(존재하지 않는 Mathlib 상수 참조) 1건과 tactic-script 오류 2건으로 명확히 구분해 기록했다.
3. 재현 가능한 로깅 스키마와 감사 도구 제공: task_id, prompt_sha256, compile_log_path, first_error_message 등을 포함한 JSON 스키마와 audit_statement_matches.py라는 구문 감사 스크립트를 공개해 다른 연구가 채택 가능한 실무적 산출물을 제공했다.

How

• finite pure DP의 6개 정리(난이도별 easy~hard)를 태스크로 선정하고, 고정된 프롬프트 템플릿(toolchain 고정, escape hatch 금지, task body 축자 삽입)을 모든 태스크에 동일 적용
• Codex CLI를 통해 gpt-5.4, gpt-5.5 두 모델을 호출, (task, model)당 2회씩 총 24회 시행하고 CLI 커맨드라인과 종료 코드까지 기록
• 모델 출력에서 단일 fenced lean 블록을 추출해 고정 경로에 저장 후 lake env lean으로 독립 검증, stdout/stderr를 그대로 저장
• 컴파일 성공(exit code 0)과 별개로 sorry/admit/axiom/unsafe 존재 여부를 스캔하는 escape-hatch 검사를 병행
• audit_statement_matches.py로 정리 이름/시그니처 일치 여부와 로컬 정의(Kernel, PureDP, Stochastic 등) 변경 여부를 검사
• compile-fail-tactic, compile-fail-unknown-lemma, compile-fail-typeclass, cheated 등 고정된 실패 분류 체계(taxonomy)를 적용
• 각 시도를 task_id, model, trial, prompt_sha256, outcome, elapsed_seconds 등을 포함한 JSON 레코드로 로깅하고, 로컬 경로 노출 등의 이유로 16건은 원문 트랜스크립트 공개, 8건은 보류(withheld) 처리

Originality

• 기존 AI-for-math 연구들이 pass rate 같은 집계 지표만 보고하는 것과 달리, 프롬프트 해시부터 컴파일 로그, 진술/컨텍스트 감사까지 전 과정을 아우르는 end-to-end 감사 파이프라인을 처음으로 체계화함
• 컴파일 성공만으로는 포착되지 않는 "약화된 정리 증명" 실패 모드를 명시적으로 겨냥한 구문적 진술/컨텍스트 감사(audit_statement_matches.py)를 설계·구현함
• 모델 평가가 아닌 하네스 설계/감사 방법론 자체를 기여로 명확히 프레이밍하여, 오염(contamination) 가능성과 소규모 표본의 한계를 스스로 명시하는 겸손하고 투명한 보고 방식을 채택함

Limitation & Further Study

• 시행 수가 24회로 매우 작아 Wilson 신뢰구간이 넓으며, task별 pass rate(n=4)에 대한 통계적 결론은 사실상 불가능함
• 6개 태스크가 공개된 Mathlib 및 DP 교재와 겹칠 가능성이 높아 사전학습 데이터 오염(contamination) 문제가 결과 해석을 제한함
• gpt-5 계열 한 모델군만 다루어 모델 간 비교나 일반화 가능성이 없으며, 저자도 이를 모델 간 헤드투헤드 비교로 제시하지 않겠다고 명시함
• 하네스가 single-shot 방식으로 설계되어 반복적 수정(iterative repair), 검색 보강, tactic-level 상호작용, rollback을 포함한 proof search는 다루지 않아 실제 활용되는 다양한 AI-assisted 워크플로우를 포괄하지 못함
• 후속 연구에서는 더 많은 모델군, 더 많은 태스크, contamination을 통제한 novel 태스크, 그리고 iterative repair를 포함하는 확장된 로깅 스키마 적용이 필요함

Evaluation

총평: 모델 성능 주장이 아닌 재현 가능한 감사 인프라 자체를 기여로 삼은 겸손하고 방법론적으로 견고한 파일럿 연구로, 규모는 작지만 AI-assisted formal mathematics 커뮤니티가 채택할 만한 실용적인 로깅/감사 템플릿을 제공한다.