Leanstral 1.5: Proof Abundance for All
Summary
미스트랄 AI가 Lean 4 언어를 활용한 공식 검증 및 수학적 증명 성능을 대폭 향상시킨 오픈소스 모델 Leanstral 1.5를 출시했습니다.
Key Points
- Leanstral 1.5는 총 119B 파라미터 중 6B 활성 파라미터를 사용하는 Apache-2.0 라이선스의 무료 오픈소스 모델이다.
- 중간 훈련, 지도 파인튜닝(SFT), CISPO 기반 강화학습(RL)의 3단계 과정을 거쳐 훈련되었으며 다중 턴 및 코드 에이전트 환경을 활용했다.
- 실제 오픈소스 저장소 검증 과정에서 기존에 발견되지 않았던 오류 5개를 찾아내며 실무 적용 가능성을 입증했다
Notable Quotes & Details
Notable Data / Quotes
- 119B total and only 6B active parameters
- 587/672 PutnamBench
- FATE-H (87%)
- FATE-X (34%)
- 5 previously unknown bugs across 57 repositories
Intended Audience
공식 검증(Formal Verification) 연구원, 수학적 증명 및 소프트웨어 신뢰성 공학 분야의 개발자