Inference-Time Diversity in RL-Trained Lean Theorem Provers: A Diagnostic Study

Motivation

• Known: RL post-training은 base model 대비 출력 분포의 다양성을 좁히는 대신 best-of-N 성능을 향상시키는 경향이 있으며(entropy collapse), 최근 연구들은 RLVR(RL with verifiable rewards)이 base model의 추론 지원 범위(reasoning support)를 실제로 확장하는지에 대해 문자열 매칭/유닛 테스트 검증 기반의 수학·코딩 벤치마크에서 의문을 제기해왔다.
• Gap: 기존 연구는 문자열 매칭이나 유닛 테스트로 검증되는 도메인에서 RLVR의 mode collapse를 다루었을 뿐, Lean kernel이 정확하게 증명을 검증하는 exact-verifier 도메인에서의 inference-time collapse는 다루지 않았고, SFT-trained 모델을 대조군으로 포함한 비교도 부재했다.
• Why: RL-trained theorem prover들이 대규모 샘플링 예산을 투입해도 추가 이득을 얻지 못하는 현상은 형식 증명 자동화의 스케일링 전략에 근본적 한계를 시사하며, 저비용의 구조적 개입만으로 이를 보완할 수 있다면 모델 크기나 학습 연산량을 늘리는 것과는 독립적인 실용적 대안을 제공한다.
• Approach: DeepSeek-Prover-V1.5-RL을 중심으로 i.i.d. 샘플링과 15개의 tactic skeleton을 8개의 goal-hint와 교차한 고정 스케줄(structured mode)을 비교하고, paraphrase 및 irrelevant comment를 포함한 통제된 diversity ablation과 base-vs-RL, RL-vs-SFT 교차 모델 비교를 통해 현상의 원인을 구조적으로 분리했다.

Achievement

Figure 1. A-RL i.i.d. sampling flatlines at 42/244 from k=32 on-

1. i.i.d. 샘플링 정체 진단: miniF2F-test에서 V1.5-RL이 k=32에서 k=64로 예산을 두 배 늘려도 42/244로 동일하여 추가로 해결된 정리가 전혀 없음을 확인했다.
2. 구조적 개입의 효과 입증: 15개 tactic skeleton 고정 스케줄이 k=16에서 +45% 상대적 개선(55 vs. 38, mean Δ=+12.3±4.2, n=3 seeds 전부 부호 유지)을 달성하며 정체를 돌파함을 보였다.
3. 프롬프트 다양성 교란요인 배제: skeleton은 효과가 있으나 paraphrase는 baseline과 동일하고 irrelevant comment는 오히려 성능을 저하시켜, 이득이 단순 프롬프트 다양성이 아닌 구조적 내용에서 온다는 것을 입증했다.
4. 난이도 계층화를 통한 국소화: leave-one-out 형식화-난이도 계층화로 세 가지 perturbation 간 구조적-내용 그라디언트를 밝히고, 구조적 이득이 쉬운/사소한 난이도 버킷에 집중됨을 보였다.
5. RL 특이성 확립: V1.5-Base는 개입 여부와 무관하게 정리를 하나도 증명하지 못해 RL이 증명 능력을 생성하는 동시에 붕괴시키는 단계임을 규명했고, DeepSeek-Prover-V2-7B(RL)는 집계 성능은 평평하지만 i.i.d. baseline이 도달 못하는 +3개의 frontier 정리를 추가로 해결한 반면, SFT-trained Goedel-Prover는 −10.0±4.4개(n=3, 모든 seed에서 부호 유지)로 오히려 손실을 보여 현상이 RL 특유임을 확인했다.

How

Figure 2. Structural-content gradient at k=16: C2 < A-RL = C1

• 구조화된 질의를 (정리 문, tactic skeleton) 쌍으로 정의하고, 15개 Lean tactic skeleton과 8개 goal-hint comment를 교차한 15×8=120 결정론적 그리드를 구성, k∈{16,32,64}로 첫 k개 그리드 엔트리를 샘플링
• Sample mode(A)는 프롬프트를 고정하고 seed를 변화, Structured mode(B)는 seed를 고정하고 스케줄에 따라 프롬프트를 변화시켜 동일한 LLM-call 예산 하에서 두 다양성 소스를 apples-to-apples 비교
• C1(paraphrase): 16개의 의미적으로 동등한 재서술을 Lean comment로 주입(tactic prefix 없음), C2(comment): 16개의 내용 없는 Lean comment를 prepend하여 구조적 내용과 단순 다양성을 분리하는 ablation 수행
• V1.5-RL과 V1.5-Base의 within-architecture 대조, 그리고 DeepSeek-Prover-V2-7B(RL)와 Goedel-Prover-SFT의 cross-model 대조를 통해 RL-specificity 검증
• Lean 4.9.0-rc1과 Mathlib commit 7fa489a5을 고정하여 최신 toolchain의 강력한 내장 tactic solver(simp, aesop, nlinarith)로 인한 교란 요인을 제거, temperature 0.6, top-p 0.95로 디코딩하고 lake env lean --json 기반 120초 타임아웃으로 검증

Originality

• i.i.d. 샘플링 정체(plateau)와 구조화된 tactic skeleton 개입 간의 명확한 대비를 통해 RL-trained Lean prover의 mode collapse를 최초로 체계적으로 진단
• paraphrase와 irrelevant comment를 포함한 통제된 diversity ablation 설계로 "프롬프트 다양성" 자체와 "구조적 내용"을 명확히 분리한 실험적 기여
• non-RL base 변형이 공개된 유일한 RL-trained Lean prover(V1.5)를 활용한 within-architecture 대조 실험으로 RL이 증명 능력의 생성과 붕괴의 원천임을 동시에 규명한 설계
• SFT-trained 모델(Goedel-Prover)을 대조군으로 명시적으로 포함해 RL-specificity를 cross-model 수준에서 검증한 최초의 시도로 보임

Limitation & Further Study

• 실험이 주로 miniF2F-test라는 단일 벤치마크와 소수의 7B급 모델(V1.5, V2, Goedel-Prover)에 국한되어 있어 더 큰 모델이나 다른 벤치마크로의 일반화 가능성이 검증되지 않음
• tactic skeleton 15개와 goal-hint 8개의 선택이 수작업(hand-selected)에 기반하고 있어 스케줄 설계 자체의 최적성이나 다른 도메인·언어(Lean 외 Coq, Isabelle 등)로의 이식성에 대한 논의가 부족함
• 구조화된 스케줄이 결정론적이라는 특성 상, 향후 연구에서는 skeleton 선택을 적응적(adaptive)으로 만들거나 tree search와 결합하는 방향, 그리고 RL 학습 자체를 mode collapse에 강건하도록 개선하는 방향이 필요함
• pass@k 개선의 절대적 크기가 여전히 작아(k=16에서 55/244 수준) 실용적 정리 증명 시스템으로서의 성능 향상 폭이 제한적임

Evaluation

총평: RL-trained Lean prover의 inference-time mode collapse를 명확한 실험 설계와 통제된 ablation으로 진단하고, 저비용의 구조적 개입이 이를 완화할 수 있음을 설득력 있게 보인 견실한 진단 연구이나, 벤치마크와 모델 규모의 제한성으로 일반화에는 추가 검증이 필요하다.