기술적 요약: RL 기반 Lean 정리 증명기에서의 추론 시간 다양성

문제 제기

최근 신경망 기반 정리 증명기, 특히 강화 학습 (RL) 과 검증 가능한 보상 (RLVR) 으로 훈련된 모델들은 miniF2F 와 같은 형식 증명 벤치마크에서 강력한 성능을 발휘해 왔습니다. 지배적인 가정은 충분한 RL 훈련과 i.i.d. 샘플링을 통한 추론 시간 컴퓨팅 증가가 모델로 하여금 형식 증명에 필요한 구조적 사전 지식을 내재화할 수 있게 한다는 것입니다.

본 논문은 이러한 가정에 도전하며, RL 기반 Lean 증명기에서 추론 시간에 발생하는 모드 붕괴 (mode collapse) 현상을 진단합니다. 구체적으로 저자들은 샘플링 예산 ($k$) 을 늘리는 것이 예상보다 훨씬 일찍 체감 수익을 가져온다고 관찰합니다. DeepSeek-Prover-V1.5-RL 을 사용한 miniF2F-test 벤치마크에서, 샘플링 예산을 $k=32$에서 $k=64$로 두 배 늘려도 해결된 새로운 정리는 전혀 추가되지 않았습니다 (42/244 에 머무름). 모델은 좁은 범위의 증명 전략에 수렴하여 추가적인 확률적 샘플이 제공되더라도 대안을 탐색하지 못합니다.

방법론

본 연구는 DeepSeek-Prover-V1.5-RL 과 그 비-RL 베이스 변형을 사용한 통제된 진단 프레임워크를 적용하며, DeepSeek-Prover-V2-7B(RL) 및 Goedel-Prover(SFT 전용) 와의 교차 모델 비교를 병행합니다.

1. 스키레톤 스케줄 개입

플랫포밍이 컴퓨팅 부족이 아닌 구조적 다양성 부족 때문인지 테스트하기 위해, 저자들은 15 개의 전술 (tactic) 스키레톤으로 구성된 고정된 결정론적 스케줄을 도입합니다.

• 구조: 15 개의 수동 선정된 Lean 전술 스키레톤 (예: simp, intro, constructor, aesop) 과 8 개의 목표 힌트 코멘트 (자연어 제안) 를 결합한 $15 \times 8 = 120$ 그리드.
• 실행: 예산 $k$에 대해 모델은 이 그리드의 처음 $k$개 항목을 시도합니다. 이는 모델이 무작위 샘플링에 의존하는 대신 특정 전략적 시작점으로 증명을 시작하도록 강제합니다.
• 애블레이션 (Ablations): 개선의 원천을 분리하기 위해 저자들은 다음을 비교합니다:
  • B-RL (Skeleton): 구조화된 15 개 스키레톤 스케줄.
  • C1 (Paraphrase): 16 개의 의미상 동등한 지시문 재구성 (전술 구조 없음).
  • C2 (Irrelevant Comments): 16 개의 내용 없는 Lean 코멘트.
  • C3 (NL-only): 전술 접두사 없이 자연어 힌트만 사용하는 전용 조건.

2. 난이도 계층화

저자들은 leave-one-out 구성을 사용하여 실증적 형식화 난이도 점수 ($\sigma$) 를 정의합니다. 대상 정리에 대해, $\sigma$는 개입 없이 다른 베이스라인 모델들 (Goedel-Prover, V2-7B) 이 해결하는 정리의 수를 세는 것입니다. 이를 통해 정리를 Frontier(다른 모델이 해결하지 못함), Hard, Medium, Easy, Trivial 버킷으로 계층화합니다.

3. 직접적 분포 측정

행동적 플랫포밍을 넘어설 수 있도록, 저자들은 13,159 개의 확률적 샘플에 걸쳐 첫 번째 전술 헤드 (first-tactic head) 다양성을 분석합니다. 각 정리당 생성된 서로 다른 선두 전술 식별자 (예: have, rw, norm_num) 의 수를 세어 측정합니다.

주요 결과

1. 구조적 안내를 통한 플랫포밍 극복

• 베이스라인 붕괴: i.i.d. 샘플링을 사용하는 DeepSeek-Prover-V1.5-RL 은 $k=16$에서 38 개, $k=32$에서 42 개의 정리를 해결하며 $k=64$에서도 42 개에 머뭅니다.
• 스키레톤 유효성: 고정된 스키레톤 스케줄은 이 플랫포밍을 깨뜨려 $k=16$에서 55 개의 정리를 해결합니다 (상대적 개선 45%) 그리고 $k=64$까지 새로운 증명을 계속 찾아냅니다 (총 60 개).
• 애블레이션 발견:
  • 구조 vs 다양성: 지시문 재구성 (C1) 은 베이스라인과 동일한 pass@16(38/244) 을 보인 반면, 관련 없는 코멘트 (C2) 는 성능을 25/244 로 저하시킵니다. 이는 성취가 단순한 프롬프트 다양성이 아닌 구조적 안내에 의해 주도됨을 확인시켜 줍니다.
  • NL vs 전술: NL-only 조건 (C3) 은 48/244 를 해결하여 베이스라인과 전체 스키레톤 사이의 중간 값을 보입니다. 이는 자연어 힌트가 격차의 약 58% 를 회복시키는 반면, 문자 그대로의 전술 접두사가 나머지를 기여함을 나타냅니다.

2. 성취의 국소화

구조적 성취는 Easy 및 Trivial 버킷(다른 오픈소스 증명기로는 해결 가능하지만 V1.5-RL 의 i.i.d. 샘플링으로는 놓친 정리) 에 집중됩니다.

• 결합된 Easy+Trivial 열에서 스키레톤 개입은 +15의 순이익을 가져오는 반면, 재구성은 0 이고 관련 없는 코멘트는 -14 입니다.
• 어떤 교란도 "Frontier" 버킷 (어떤 베이스라인으로도 해결되지 않은 정리) 을 해제하지 못하여, 이 개입이 해결 가능한 알려진 문제들의 미탐색을 보완할 뿐 능력의 프론티어를 확장하지는 못함을 시사합니다.

3. 모드 붕괴의 RL 특이성

• 베이스 모델 대비: DeepSeek-Prover-V1.5-Base(비-RL) 는 i.i.d. 또는 스키레톤 조건 하에서 어떤 정리도 증명하지 못합니다. 이는 RL 이 증명 능력의 생성지이자 이후의 모드 붕괴의 발생지임을 확립합니다. 베이스 모델은 유효한 증명을 생성할 능력이 없으며, RL 단계는 그 능력을 생성하지만 이를 좁은 정책으로 붕괴시킵니다.
• 교차 모델 대비:
  • V2-7B (RL): 평탄한 집계 이익 (+1) 을 보이지만, 어떤 i.i.d. 베이스라인으로도 도달 불가능했던 +3 개의 Frontier 정리를 해제합니다.
  • Goedel-Prover (SFT): 스키레톤으로 음의 이익 (-10.0 $\pm$ 4.4) 을 보입니다. SFT 훈련 모델은 이미 광범위한 전술 스템을 탐색하는 것으로 보이며, 고정된 스키레톤 스케줄이 불필요하거나 제한적으로 작용합니다.

4. 붕괴의 직접적 증거

분포 분석에 따르면, 중앙값 정리는 64 개의 샘플에서 단 2 개의 서로 다른 첫 번째 전술 헤드만 받으며, 벤치마크의 49% 가 결정론적 단일 전략적 시작점을 받습니다. 관찰된 섀넌 엔트로피는 이론적 용량의 $\le 8\%$에 불과하여 심각한 모드 붕괴를 확인시켜 줍니다.

중요성 및 주장

본 논문은 "전술 스키레톤이 성능을 향상시킨다"는 서사를 **"RL 기반 증명기는 추론 시간에 전술 공간을 심각하게 미탐색한다"**는 서사로 재구성합니다.

• 이중 행위자로서의 RL: 저자들은 RL 이 이중적인 역할을 한다고 주장합니다. 즉, 베이스 모델이 전혀 없는 증명 능력을 생성하는 단계이면서 동시에 그 능력을 좁은 정책으로 붕괴시키는 단계라는 것입니다.
• 추론 시간 확장: 결과는 i.i.d. 샘플링을 통한 추론 컴퓨팅의 단순한 확장이 예상보다 훨씬 일찍 체감 수익을 가져온다고 시사합니다. 구조적 다양성 (프롬프트를 통한 증명 전략 변화) 은 확장을 위한 더 효율적인 축입니다.
• 시정 가능성: 모드 붕괴는 RL 기반 모델에 특이적입니다. SFT 기반 모델은 구조적 힌트를 통해 동일한 회복 가능한 붕괴를 보이지 않으며, 오히려 이로 인해 고통받습니다. 이는 향후 개입 (훈련 시간 엔트로피 정규화 또는 추론 시간 스키레톤 검색) 이 능력 생성과 다양성 유지 사이의 균형을 고려해야 함을 의미합니다.

본 연구는 "모드 붕괴"가 형식 검증 도메인에서 RL 파인튜닝 과정에 내재된 실제적이고 파이프라인에 의존적인 현상이며, 고정된 구조적 개입이 추가 훈련 없이도 잃어버린 탐색을 효과적으로 회복시킬 수 있음을 결론짓습니다.