Leanstral 1.5는 Mistral AI가 공개한 Lean 4 형식 증명(formal proof) 및 코드 검증 특화 오픈소스 모델이다. Apache-2.0 라이선스로 공개됐으며, 119B 총 파라미터 중 토큰당 약 6B대 파라미터만 활성화되는 MoE 구조를 사용한다.
핵심 특징
| 항목 | 내용 |
|---|---|
| 목적 | Lean 4 증명 작성, proof engineering, 코드 속성 검증 |
| 구조 | 119B total, 약 6.5B active per token MoE |
| 컨텍스트 | 최대 256k, 200k 이하 권장 |
| 입력 | 텍스트와 이미지 입력, 텍스트 출력 |
| 라이선스 | Apache-2.0 |
| 사용 경로 | Hugging Face weights, 무료 Mistral API, Mistral Vibe |
성능 포인트
Mistral 발표 기준 Leanstral 1.5는 miniF2F 검증·테스트 세트를 100% 해결하고, PutnamBench 672문제 중 587문제를 해결한다. FATE-H와 FATE-X에서는 각각 87%, 34% 성과를 제시한다.
특히 중요한 점은 test-time scaling이다. 토큰 예산을 늘릴수록 PutnamBench 해결 수가 증가하며, 긴 증명 작업에서 context compaction을 거치며 계속 전진하는 에이전트형 proof engineering 능력을 보인다.
코드 검증 사례
Leanstral 1.5는 수학 증명뿐 아니라 실제 코드 검증에도 적용됐다. Mistral은 Aeneas로 Rust 코드를 Lean으로 변환하고, Leanstral이 코드 의도를 추론해 correctness property를 만들고 증명하는 파이프라인을 실험했다.
57개 오픈소스 저장소 테스트에서 47개 violated property를 찾았고, 이 중 11개가 실제 버그로 이어졌으며 5개는 GitHub에 이전 보고가 없던 버그였다고 설명한다. 예시로 datrs/varinteger의 zigzag decoding overflow 버그가 언급된다.
사용 시작
Mistral은 Mistral Vibe에서 Lean agent로 사용하는 경로를 권장한다.
uv tool install mistral-vibe
uv tool update mistral-vibe
vibe --setupVibe 안에서 Leanstral을 설치한 뒤:
/leanstall
exitLean 프로젝트 디렉터리에서 실행한다.
vibe --agent lean누구에게 유용한가
- Lean 4로 수학 증명이나 정형 명세를 작성하는 연구자
- Rust 등 시스템 코드의 속성 검증을 실험하는 엔지니어
- proof assistant와 AI 에이전트를 결합하려는 팀
- closed model 의존도를 줄이고 싶은 형식검증 워크플로 사용자
관련 문서
- Mistral Vibe — Mistral의 CLI 코딩 어시스턴트
- ai-agent-evaluation — 에이전트 평가와 벤치마크 설계
- qwen — 오픈소스 대형 언어 모델 생태계
- llm-fine-tuning — SFT·RL·PEFT를 포함한 LLM 파인튜닝 개요
참고 자료
- Leanstral 1.5: Proof Abundance for All — Mistral AI (2026-07-02)
- mistralai/Leanstral-1.5-119B-A6B — Hugging Face 모델 카드
- Mistral’s open-source Leanstral 1.5 aces formal math benchmarks and catches real bugs in code — The Decoder (2026-07-04)