Mistral AI가 7월 4일 Lean 4 프로그래밍 언어 기반 형식 검증 모델 Leanstral 1.5를 Apache 2.0 라이선스로 공개했다. Lean 4는 수학 증명과 소프트웨어 정확성을 형식적으로 검증하는 언어다.
수학 벤치마크 성능은 다음과 같다.
▼ Leanstral 1.5 주요 벤치마크 결과
| 벤치마크 | 설명 | 점수 |
|---|---|---|
| miniF2F | 고등~수학 올림피아드 수준 형식 수학 | 100% |
| PutnamBench | 퍼트넘 수학 대회 672문제 | 587문제 해결 |
| FATE-H | 군론·환론 등 석사 수준 대수학 | 87% |
| FATE-X | 박사 수준 대수학 | 34% |
PutnamBench와 FATE-H, FATE-X에서 오픈소스 모델 중 1위다. PutnamBench에서만 비공개 모델 Aleph Prover가 앞선다.
수학 훈련에 집중했지만 코드 검증에서도 성과를 냈다. 57개 오픈소스 저장소를 직접 스캔해 이전까지 알려지지 않은 버그 5건을 찾아냈다. 그 중 하나는 Rust 라이브러리 varinteger의 오버플로 버그다.
학습 방식은 중간 학습(mid-training), 지도 미세조정(supervised fine-tuning), 강화학습을 순차적으로 적용했다. 모델은 Hugging Face와 Mistral 무료 API를 통해 이용할 수 있다.
국내 소프트웨어 개발 현장에서 형식 검증은 아직 도입 사례가 드물다. Leanstral 1.5는 Apache 2.0 라이선스라 상업적 활용도 가능해, 금융·항공·자동차 등 안전 중요 시스템을 다루는 국내 개발팀의 오픈소스 품질 관리 도구로 검토 대상이 될 수 있다.
