Most of a Formal Proof is Forced

Motivation

• Known: 기존 신경 정리 증명기(Yang et al., 2023; Xin et al., 2024)는 tactic string 등 surface syntax를 생성하고 Lean elaborator가 이를 Lean.Expr로 변환한 뒤 커널이 검증하는 파이프라인을 따르며, Kaplan et al. (2020)과 Hoffmann et al. (2022, Chinchilla)의 자연어 스케일링 법칙과 Hernandez et al. (2021)의 transfer scaling law가 이미 잘 정립되어 있다.
• Gap: Elaborator라는 학습 신호와 커널 채점 사이의 번역 계층이 존재하여 언어모델이 실제로 배우는 목표(surface syntax)와 최종 검증 대상(Lean.Expr) 간 괴리가 생기고, 이로 인해 "그럴듯해 보이지만 증명이 아닌" 결과물이 생성될 위험이 있으며, 정형 수학 코퍼스에서 자연어와 얼마나 다른 스케일링 거동을 보이는지, 그리고 그 엔트로피 구조가 탐색 전략에 어떤 함의를 갖는지는 규명되지 않았다.
• Why: Elaboration 계층을 제거하고 커널을 유일한 판정자로 삼음으로써 환각(hallucination)이 원천적으로 불가능한 이진 지표를 얻을 수 있으며, 엔트로피가 소수 결정점에 집중된다는 발견은 탐색 비용을 획기적으로 낮춰 SFT만으로도 경쟁력 있는 프루버를 만들 수 있는 실질적 경로를 제시하기 때문에 중요하다.
• Approach: 저자들은 Lean.Expr을 직접 생성하는 생성기를 학습시키고 Kernel Acceptance Rate(KAR)라는 이진·비환각적 지표로 채점하며, from-scratch 및 transfer 스케일링 스윕을 통해 손실 지수와 엔트로피 분포를 측정하고 이를 depth-first proof search에 활용한다.

Achievement

Figure 3. Test dataset cross-entropy against compute C = 6ND for the twelve sweep cells, log–log. Our test cross-entropy

1. Kernel Acceptance Rate(KAR) 지표 제안: 후보 항이 파싱되고 타입체크되며 커널이 추론한 타입이 목표 타입과 definitionally equal한지를 확인하는 이진·환각 불가능 지표를 정의하고, 실패를 parse err, type err, neq 세 범주로 분해했다.
2. 엔트로피 집중 현상 규명: 커널 기반 표면에서 다음 토큰이 목표 타입과 elaboration context에 의해 대부분 강제되며, 잔여 엔트로피가 소수의 진짜 결정점에 집중됨을 보였다(Figure 4).
3. 가파른 스케일링 지수 발견: from-scratch 및 transfer 스케일링 스윕에서 데이터·파라미터 축 모두에서 자연어 대비 3~4배 가파른 손실 지수를 확인했으며, 작은 비환원 바닥값(irreducible floor)이 존재하고 이 지수가 토큰화 방식에 대해 calibration-invariant함을 보였다(Figure 3).
4. 모델 크기의 중복성 발견: 30M 파라미터 이상에서는 모델 크기가 손실에 미치는 영향이 사라지고 손실이 오직 유효 데이터 양에 의해 결정됨을 실증했다.
5. 저비용 탐색 알고리즘 제시: 엔트로피 집중 구조를 활용해 발화된 스텝 경계마다 한 번의 모델 호출만 필요하고 그 사이는 무료 체인 롤아웃으로 처리하는 depth-first search 기법을 고안하고, SFT만으로 유의미한 실증 성능을 달성했다.

How

• Lean 4 여덟 개 라이브러리(Mathlib HEAD, Init, Std, 컴파일러 내부, Batteries, Aesop, Lean Workbook, NuminaMath-Lean)에서 (type, value) 쌍 388,322개 선언을 추출하고 값이 있는 95,704개를 학습 풀로 사용
• Curry-Howard Correspondence에 따라 증명과 프로그램을 하나의 코퍼스로 통합하여 커널 기준 표면에서 인위적 경계를 학습하지 않도록 설계
• 값이 있는 Lean.Expr 트리를 pre-order depth-first walk로 선형화하여 arity가 고정된 constructor 시퀀스(토큰 스트림)로 변환(Figure 1)
• KAR(gθ; T)를 정의: 후보가 Lean.Meta.check를 통과하고 inferType 결과가 목표 타입과 isDefEq한지 확인하는 budget-k 지표
• Chinchilla 스타일 함수형(L(N,D)=E+A·N^-α+B·D^-β)과 Hernandez et al.의 transfer scaling law(DT=k·D^αT·N^βT)를 확장해 전이 데이터까지 흡수한 L(N,D)≈E+A·N^-α+B·(mw·D)^-β 식으로 from-scratch/transferred 12개 스윕에 대해 손실 지수 및 mw(warm-start 계급별 유효데이터 배율)를 적합
• 학습된 모델의 다음 토큰 조건부 분포 엔트로피를 위치별로 측정하여 결정점 희소성 확인
• 엔트로피 집중 구조를 활용한 depth-first proof search 구현: step boundary에서만 모델을 호출하고 그 사이는 강제된 토큰을 무료로 롤아웃

Originality

• Elaborator라는 중간 번역 계층을 제거하고 Lean.Expr(람다 계산 트리)을 직접 생성 대상으로 삼는 "substrate의 전환"이라는 관점 자체가 기존 tactic-string 기반 신경 정리 증명 연구와 근본적으로 다름
• 학습된 judge나 proof-state 재구성 없이 커널만을 유일한 판정 기준으로 삼아 환각이 구조적으로 불가능한 지표(KAR)를 설계
• 자연어 스케일링 법칙과 transfer scaling law를 정형 증명 코퍼스에 적용해 지수 비교를 최초로 시도하고, 토큰화 불변성(calibration-invariance)을 검증
• 엔트로피 집중 현상을 탐색 알고리즘 설계(무료 체인 롤아웃)에 직접 연결한 실용적 통찰

Limitation & Further Study

• 커널이 증명된 정리의 값(proof term)을 저장하지 않고 타입만 태그해 보관하기 때문에, 실제로 학습에 사용된 값 대부분(92,051개)은 정리 증명이 아니라 정의(definition) 본체이며 정리 증명은 3,653개에 불과해 코퍼스의 실질적 증명 다양성이 제한적일 수 있음(저자들도 이를 향후 수정할 한계로 인정)
• KAR 지표는 Type 대상에 대해서는 관대하여(any kernel-accepted inhabitant), 약한 목표 타입에 대해 퇴화된 항이 통과할 수 있는 gameable한 여지가 존재함
• 실험이 SFT만으로 진행되어 강화학습이나 self-play 등 후속 학습 기법과의 비교, 그리고 더 큰 스케일에서의 검증이 부족함
• 30M 이상에서 모델 크기가 중복된다는 결론이 특정 데이터 규모/도메인에 국한된 것인지, 더 큰 데이터셋에서도 유지되는지 추가 검증 필요
• Figure 발췌만으로는 실제 proof search의 성공률, 벤치마크(miniF2F 등) 대비 정량적 비교가 충분히 제시되지 않아 "경쟁력 있는 프루버로의 가능성"이라는 주장의 실증적 근거가 제한적임

Evaluation

총평: Elaborator를 제거하고 커널을 직접 판정자로 삼는 발상은 신선하고 이론적으로 탄탄하며, 스케일링 법칙과 엔트로피 집중이라는 두 축의 발견이 서로 잘 연결되어 탐색 알고리즘까지 이어지는 완결성 있는 워크숍 논문이나, 코퍼스의 증명-정의 불균형과 벤치마크 검증 부족이 아쉬운 한계로 남는다.