Papers·1주 전
Pythagoras-Prover: 4B 모델로 DeepSeek-Prover-V2-671B 능가, Lean 정리 증명의 효율성 혁신
Pythagoras-LM 팀이 공개한 Pythagoras-Prover는 4B 파라미터로 MiniF2F-Test pass@32에서 86.1%를 기록, DeepSeek-Prover-V2-671B(82.4%)를 167배 적은 파라미터로 능가했습니다. 32B 모델은 93.0%로 오픈소스 SOTA를 달성하고 PutnamBench 672문제 중 93문제를 해결했습니다. 핵심은 커리큘럼 SFT, 동적 증명 추론 필터링, Augmented Lean Formalisation(ALF) 데이터 증강으로, 학습 및 추론 비용을 대폭 줄였습니다. 단, MiniF2F-ALF 변형 벤치마크에서는 모든 모델의 정확도가 하락해 데이터 오염에 취약할 수 있습니다.
Pythagoras-LM 팀이 실용적인 컴퓨팅 예산에 맞춘 Lean 정리 증명기 제품군을 공개했습니다. 4B 및 32B autoregressive 모델과 최초의 diffusion 기반 증명기(4B)를 포함하며, 학습 효율성을 크게 개선했습니다.
핵심 결론
- 성능 — Pythagoras-Prover-4B는 MiniF2F-Test pass@32에서 86.1%로 DeepSeek-Prover-V2-671B(82.4%)를 능가, 32B는 93.0%로 오픈소스 SOTA.
- PutnamBench — 32B 모델이 672문제 중 93문제 해결, 기존 오픈소스 대비 큰 폭 개선.
- 확장성 — 4B 모델이 671B 모델보다 167배 적은 파라미터로 더 높은 성능을 달성한 점이 주목할 만합니다.
방법
- 커리큘럼 SFT — Lean 검증 코퍼스를 easy/medium/hard로 계층화해 점진적으로 학습, 모델이 짧고 단순한 증명에서 길고 어려운 증명으로 발전.
- 동적 필터링 — SFT 중 정보성 있는 증명 추적을 유지하면서 각 인스턴스를 8k 토큰 컨텍스트 예산 내로 제한.
- ALF — Augmented Lean Formalisation: 검증된 문제를 변형한 formal statement variants를 self-distillation으로 생성, 추가 학습 신호 확보. 모든 변형을 형식 검증하지 않아도 됩니다.
- Diffusion 증명기 — 4B diffusion 모델은 추론 시 반복적으로 증명을 정제, autoregressive 모델과 다른 접근법을 제공합니다.
한계·조건
- 데이터 오염 — MiniF2F-ALF 변형 벤치마크에서 모든 모델의 정확도가 하락, ALF가 데이터 오염에 취약할 수 있음을 시사.
- 컴퓨팅 — 학습 및 추론 비용이 낮지만, diffusion 모델의 반복 정제 과정은 여전히 추가 연산이 필요합니다.
- 공개 — 모델과 MiniF2F-ALF 벤치마크가 공개되었습니다.
편집자 한 줄
4B 모델이 671B를 능가한 점은 인상적이지만, ALF 변형 벤치마크에서의 성능 하락은 실제 일반화 능력에 대한 의문을 남깁니다.
- #lean
- #theorem-proving
- #pythagoras-lm
- #curriculum-learning
- #diffusion
Pythagoras-LM