기술 요약: Pythagoras-Prover

문제 정의

현대의 Lean 정리 증명기(theorem provers)들은 강력한 성능을 달anim했으나, 종종 방대한 양의 훈련 및 추론 컴퓨팅에 의존하며, 수백억 개의 파라미터를 가진 프런티어 규모의 모델이나 광범위한 탐색, 자기 수정, 대규모 샘플링 예산과 같은 계산 집약적인 추론 절차를 필요로 한다. 이러한 의존성은 검증된 증명 데이터의 희소성과 정형 증명 탐색을 위한 긴 추론 트레이스(reasoning traces)로 인해 초감독 미세 조정(SFT) 및 샘플링 비용을 높게 만든다. 결과적으로, 소규모 오픈 소스 증명기와 거대 모델 사이에는 상당한 격차가 존재하며, 이는 막대한 컴퓨팅 자원이 없는 연구자와 실무자들의 접근성을 제한한다.

방법론

저자들은 Pythagoras-Prover라는 컴퓨팅 효율적인 오픈 소스 Lean 4 정리 증명기 제품군을 소개한다. 이 접근 방식은 원시 모델 규모보다는 단계적이고 컴퓨팅을 아끼는(compute-frugal) 데이터 파이프라인과 훈련 전략에 의존한다.

1. 데이터 구축 및 커리큘럼 학습

훈련 코퍼스는 세 가지 난이도 티어(Easy, Medium, Hard)로 구성되며, 모든 단계는 정식성을 보장하기 위해 Lean 타입 체커(type-checker)에 의해 제어된다:

• Easy 및 Medium 티어: "Theorem Prover as a Judge"에서 영감을 얻은 3단계 파이프라인을 통해 생성된다. DART-Math-Hard, DeepScaleR, OpenR1-Math와 같은 데이터셋의 자연어 문제들이 Lean 문장으로 자동 형식화(autoformalized)된다. 실패한 증명은 분석되며, 특정 오류 범주(예: 태틱 실패, 타입 불일치)를 타겟팅하는 루브릭 가이드 기반 증류(rubric-guided distillation) 프로세스를 통해 단순화된 합성 변형들을 생성한다. 이 과정은 자동 형식화 성공률을 상대적으로 30% 향상시킨다.
• Hard 티어: Big-Math-RL-Verified의 경시 수준 문제들(Olympiads, AIME, AMC)에서 가져온다. 쉬운 티어들과 달리, 이들은 강화 학습을 위한 난이도를 유지하기 위해 단순화되지 않는다.
• 커리큘럼 SFT: 모델은 난이도 순서(Easy $\to$ Medium $\to$ Hard)에 따른 커리큘럼을 사용하여 훈련되며, 파라미터 효율성을 유지하기 위해 LoRA(Low-Rank Adaptation)를 사용한다. SFT 과정 중에는 8k-토큰 컨텍스트 예산을 관리하기 위해 **동적 증명 추론 필터링 스킴(dynamic proof-reasoning filtering scheme)**이 적용된다: 만약 추론 체인과 증명의 합이 제한을 초과하면 추론 부분은 버리고 증명은 유지하며, 증명 단독으로도 제한을 초과하면 해당 인스턴스를 폐기한다.

2. 확장된 Lean 형식화 (ALF) 및 자기 증류 (Self-Distillation)

Lean 검증 처리량(throughput)의 병목 현상을 극복하기 위해, 저자들은 **확장된 Lean 형식화 (Augmented Lean Formalisation, ALF)**를 도입한다.

• 메커니즘: ALF는 검증된 시드 인스턴스에 다섯 가지 구조적 변이 연산자(단순화, 일반화, 보조 정리 제안, 증명 단계 분해, 재구성)를 적용한다.
• 효율성: 모든 변이된 인스턴스를 Lean으로 검증하는 것은 계산적으로 불가능하므로, ALF는 경량화된 **문장 정렬 체크(statement-alignment check)**를 사용한다. 이는 생성된 증명이 변이된 문장을 참조하는지 확인하여, 전체 컴파일 없이도 구조적 유효성을 보장한다.
• 자기 증류: 포스트-RL 모델은 이러한 변이된 문장들에 대한 증명을 생성한다. 이 과정은 매 인스턴스마다 검증을 수행하지 않고도 코퍼스를 약 2.5배(약 200만 개 인스턴스로) 확장한다. 이 확장된 코퍼스는 지속적인 SFT 및 확산 기반 증명기(diffusion-based prover)를 훈련하는 데 사용된다.

3. 모델 아키텍처

이 제품군은 두 가지 생성 패러다임을 아우른다:

• 자기회귀 증명기 (Autoregressive Provers): 위 파이프라인으로 훈련된 4B 및 32B 파라미터 모델.
• 확산 기반 증명기 (Diffusion-Based Prover): Pythagoras-Prover-Diffusion-4B로, Lean을 위한 최초의 개념 증명 단계인 확산 기반 정리 증명기이다. 이는 **태틱 기반 마스킹(tactic-based masking)**을 활용하며, 여기서 전체 Lean 태틱(tactic)은 개별 토큰이 아닌 하나의 단위로서 마스킹되고 디노이징(denoising)된다. 이는 디노이징 목적 함수를 이산적 추론 단계와 일치시킨다.

4. 강화 학습 (RL)

RL은 held-out 된 어려운 문제들에 대해 GRPO(Group Relative Policy Optimization)와 함께 전체 파라미터 미세 조정을 사용하여 수행된다. 보상은 이진(증명이 컴파일되고 문장과 일치함)이다. 저자들은 RL이 커리큘럼-SFT 모델에 비해 완만한 이득만을 제공한다는 점에 주목하며, 이는 고품질의 지도 학습 코퍼스가 이미 강력한 증명 탐색 행동을 내재화했음을 시사한다.

주요 기여

1. 컴퓨팅 효율적인 증명기: 강력한 정형 추론을 위해 반드시 프런티어 규모의 모델이 필요하다는 가설에 도전하는, Lean 제품군(4B, 32B, 4B 확산 모델)을 제공한다.
2. ALF 데이터 파이프라인: 경량화된 산술 체크를 사용하여 검증된 코퍼스를 약 2.5배 확장함으로써, 코퍼스 확장을 검증 처리량으로부터 분리하는 구조적 변이 스킴을 도입한다.
3. MiniF2F-ALF 벤치마크: MiniF2F-Test 세트에 ALF 변이를 적용하여 만든 오염 민감형 섭동(perturbation) 벤치마크이다. 이는 모델이 정확한 벤치마크 회상(recall)에 의존하는지, 아니면 전이 가능한 증명 행동을 보유하고 있는지를 평가하는 스트레스 테스트 역할을 한다.
4. 최초의 확산 정리 증명기: Lean을 위한 실행 가능한 확산 기반 증명기를 제시하며, 반복적 정제(iterative refinement)가 정형 증명을 위한 실행 가능한 디코딩 전략임을 입증한다(비록 현재의 컨텍스트 길이 제한은 존재하지만).

실험 결과

MiniF2F-Test, PutnamBench, MiniF2F-ALF에서 평가됨:

• MiniF2F-Test (Pass@32):
  • Pythagoras-Prover-4B는 **86.1%**를 달성하여, 약 167배 더 작음에도 불구하고 DeepSeek-Prover-V2-671B(82.4%)를 능가했다. 또한 Goedel-Prover-V2-8B(84.6%)와 Kimina-Prover-70B(84.0%)보다 높은 성능을 보였다.
  • Pythagoras-Prover-32B는 **89.8%**를 달성하여, 자기 수정(self-correction) 없이 평가된 모든 오픈 소스 증명기 중 선두를 차지했다.
• MiniF2F-Test (Pass@2048):
  • Pythagoras-Prover-32B는 **93.03%**에 도달하여, 자기 수정 없이 1/4의 샘플링 예산만으로 Goedel-Prover-V2-32B(Pass@8192에서 92.2%)를 앞지르며, 자기 수정이 없는 신경망 기반 Lean 증명기 중 새로운 SOTA를 기록했다.
• PutnamBench:
  • Pythagoras-Prover-32B는 Pass@2048에서 672개 문제 중 93개를 해결하여, 가장 강력한 오픈 소스 결과를 보여주었으며, 자기 수정을 포함한 Goedel-Prover-V2(Pass@184에서 86개)를 능가했다.
• MiniF2F-ALF (강건성):
  • 평가된 모든 모델은 이 섭동된 벤치마크에서 성능이 저하되었으며, 이는 높은 정확도가 원래 분할(split)에 대한 정확한 회상을 보장하지 않음을 확인시켜 준다.
  • Pythagoras-Prover-32B가 가장 강력한 성능(85.0%)을 유지했으며, Pythagoras-Prover-4B(83.2%)는 8배 더 큰 Goedel-Prover-V2-32B(83.6%)와 대등한 수준을 보이며 섭동 하에서도 적게 저하되었다.
• 확산 효율성:
  • Pythagoras-Prover-Diffusion-4B는 MiniF2F-Test에서 63.25%의 Pass@32를 달성했다. 자기회귀 대응 모델보다는 정확도가 낮지만, 2.58배 더 빠르게(10.56 vs 4.10 tokens/sec) 증명을 생성하여, 'GPU-초당 처리량' 관점에서 더 높은 효율을 제공한다.

의의 및 주장

본 논문은 강력한 Lean 정리 증명이 반드시 프런티어 규모의 모델에만 의존할 필요는 없다고 주장한다. 결과는 세심한 데이터 구축(커리큘럼 학습, ALF 증강, 자기 증류)과 효율적인 훈련 레시피(LoRA, 동적 필터링)가 모델 규모를 일부 대체할 수 있음을 보여준다.

특히 저자들은 다음을 강조한다:

• 효율성: Pythagoras-Prover-4B가 671B 파라미터 모델을 능가한다는 점은, 제안된 훈련 레시피가 수십억 규모의 베이스라인이 비실용적인 소규모 모델 환경으로 깔끔하게 전이될 수 있음을 시사한다.
• 강건성: 훈련 중 ALF 변이를 사용하는 것은 문장 수준의 섭동에 대한 강건성을 개선하며, 이는 MiniF2F-ALF에서 다른 베이스라인들에 비해 더 적은 성능 저하를 보임으로써 입증된다.
• 새로운 패러다임: 확산 기반 증명기의 도입은 정형 증명을 위한 반복적 정제의 초기 기준을 세우며, 증명기가 정확도뿐만 아니라 'GPU-초당 처리량 및 증명 수'로 비교될 수 있는 보완적인 방향을 제시한다.

저자들은 "컴퓨팅을 아끼는" 데이터 파이프라인이 이러한 결과의 주요 동력이며, 이를 통해 실제적인 컴퓨팅 예산 하에서도 최첨단 성능을 달성할 수 있었다고 결론짓는다.