Mistral AI, Leanstral 1.5 오픈소스 공개
원제: Leanstral 1.5: Proof abundance for all
왜 중요한가
6B 활성 파라미터의 경량 오픈소스 모델이 형식 검증 최고 성능을 달성, 학술·산업 분야의 소프트웨어 안전성 검증 접근성을 대폭 낮출 수 있다.
Mistral AI는 2026년 7월 2일, 형식 검증 특화 모델 Leanstral 1.5를 Apache-2.0 라이선스로 무료 공개했다. 총 파라미터 119B·활성 파라미터 6B 구성으로, miniF2F 포화 달성, PutnamBench 672문제 중 587문제 해결, FATE-H 87%·FATE-X 34%로 최고 성능을 기록했으며 오픈소스 저장소 57개에서 미발견 버그 5건을 발굴했다.
Mistral AI의 Leanstral 팀은 Lean 4 기반 증명 엔지니어링 모델 Leanstral 1.5를 2026년 7월 2일 공식 발표했다. 본 모델은 총 119B 파라미터이지만 추론 시 활성화되는 파라미터는 6B에 그쳐 효율적인 운용이 가능하다.
성능 면에서는 수학 올림피아드 수준의 형식 증명 벤치마크인 miniF2F를 포화(saturation) 달성하였고, 미국 Putnam 수학 경시대회 문제를 기반으로 한 PutnamBench에서 672문제 중 587문제를 해결했다. 또한 형식 검증 벤치마크 FATE-H에서 87%, FATE-X에서 34%를 기록하며 기존 최고 성능(state-of-the-art)을 갱신했다.
훈련 방식은 세 단계로 구성된다. 먼저 미드-트레이닝(mid-training)을 거친 뒤 지도 미세조정(SFT), 마지막으로 CISPO를 적용한 강화학습(RL)을 수행했다. RL 환경은 멀티턴 환경과 에이전틱(agentic) 환경 두 가지로 구성되며, 멀티턴 환경에서는 정리 문장이 주어지면 모델이 증명 또는 반증을 시도하고 Lean 컴파일러 피드백을 받는 방식으로 학습이 이루어진다.
실제 활용 측면에서는 공개된 오픈소스 저장소 57개를 대상으로 코드 속성 검증을 수행해 기존에 알려지지 않았던 버그 5건을 발굴했다. 이는 형식 검증이 실제 소프트웨어 개발 환경에서도 실용적으로 적용 가능함을 보여준다. 모델은 Hugging Face를 통해 다운로드할 수 있으며 무료 API도 제공된다.