Leanstral 1.5: Proof Abundance for All
Summary
미스트랄 AI가 형식 검증 및 수학적 증명 성능을 대폭 향상시키고 오픈소스로 공개한 Leanstral 1.5 모델에 대한 소개입니다.
Key Points
- Leanstral 1.5는 총 119B 파라미터 중 활성 파라미터가 6B인 오픈소스(Apache-2.0 라이선스) 모델로, 형식 검증 성능이 크게 업그레이드되었습니다.
- 중간 훈련(mid-training), 지도 미세조정(SFT), 그리고 CISPO 기반의 강화학습(RL) 3단계 프로세스를 거쳐 훈련되었습니다.
- 다중 턴 환경과 코드 에이전트 환경의 두 가지 강화학습 환경을 활용하여 실질적인 증명 엔지니어링 워크플로우를 학습했습니다.
Notable Quotes & Details
Notable Data / Quotes
- 6B active parameters
- PutnamBench 587/672
- FATE-H 87%
- FATE-X 34%
- 57 repositories tested, 5 previously unknown bugs
Intended Audience
AI 연구원, 수학자, 정형 검증(Formal Verification) 및 소프트웨어 엔지니어