Pythagoras-Prover는 제한된 연산 예산에서도 작동하도록 설계된 오픈소스 Lean 정리 증명기 계열이다. 4B·32B 자기회귀 모델과 추론 시 증명을 반복 정제하는 4B 확산 기반 증명기(개념검증)를 포함한다. 검증된 증명 데이터가 희소한 문제를 풀기 위해, 쉬움·중간·어려움으로 계층화한 커리큘럼 SFT와 8k 토큰 내에서 유용한 증명 흔적을 보존하는 동적 필터링을 도입했고, 알려진 문제를 변형해 검증 코퍼스를 확장하는 'Augmented Lean Formalisation(ALF)'으로 표면 형태 의존을 줄였다. 결과적으로 4B 모델이 MiniF2F-Test pass@32에서 약 167배 큰 DeepSeek-Prover-V2-671B를 86.1% 대 82.4%로 능가했고, 32B는 93.0%로 오픈소스 최고 성능을 세우며 PutnamBench 672문제 중 93개를 풀었다.
- •제한된 연산 예산용 오픈소스 Lean 정리 증명기 계열 Pythagoras-Prover 공개
- •4B·32B 자기회귀 모델과 4B 확산 기반 증명기(개념검증) 포함
- •커리큘럼 SFT와 증명 코퍼스 확장 기법 ALF로 학습 효율·일반화 개선
- •4B 모델이 167배 큰 DeepSeek-Prover-V2-671B를 MiniF2F-Test에서 86.1% 대 82.4%로 능가
- •32B가 MiniF2F-Test 93.0% 오픈소스 SOTA 달성, PutnamBench 93/672 해결
Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation
- 1.컴퓨트 효율적 오픈소스 Lean 정리증명기 Pythagoras-Prover 패밀리 공개
- 2.4B·32B 자기회귀 모델과 첫 확산 기반 증명기(4B)를 제시
- 3.4B 모델이 167배 큰 DeepSeek-Prover-V2-671B를 MiniF2F서 능가(86.1 vs 82.4%)
- 4.증강 Lean 형식화(ALF)로 희소한 검증 코퍼스를 자기증류로 확장
왜 중요한가?
방대한 학습·추론 컴퓨트가 필요하던 형식 정리증명을 커리큘럼 SFT와 데이터 증강으로 소형 모델에서도 오픈소스 SOTA(32B 93.0%) 수준에 올려, 제한된 자원에서의 자동 정형증명 접근성을 크게 높인다.
현대 린(Lean) 정리 증명기의 높은 연산 비용과 희소한 검증 데이터 문제는 국내 고신뢰 시스템 개발 분야에서도 중요한 제약입니다. 'Pythagoras-Prover'는 증강된 린 형식화를 통해 효율적인 형식적 증명을 발전시키며, 국내 소프트웨어 검증 및 AI 기반 수리 추론 기술 발전에 기여하여 신뢰성 높은 시스템 구축을 지원할 것입니다.
본문 미리보기
arXiv:2606.12594v1 Announce Type: new Abstract: Modern Lean theorem provers achieve strong performance only with substantial training and inference compute, driven in part by scarce verified proof data and the long reasoning traces of formal proof search, making both supervised fine-tuning (SFT) and sampling expensive. We introduce Pythagoras-Prover, a compute-efficient open-source family of Lean theorem provers built for practical compute budgets. The family spans two generation paradigms: aut
전체 내용이 궁금하다면?
원문을 직접 읽어보세요
