Mistral AI, Lean 4용 형식 검증 모델 「Leanstral 1.5」 공개

Mistral AI는 Lean 4에서의 형식 검증을 지원하는 Apache-2.0 라이선스 모델 「Leanstral 1.5」를 공개했다. 총 파라미터 119B, 활성 파라미터 6B 규모이며, miniF2F를 포화시키고 PutnamBench에서는 672문제 중 587문제를 풀었다. FATE-H에서 87%, FATE-X에서 34%를 기록해 새로운 state-of-the-art를 달성했으며, Hugging Face와 무료 API를 통해 이용할 수 있다.