Mistral Leanstral 1.5 — Lean 4 정형 검증으로 오픈소스 Rust 버그를 잡는 방법

핵심 요약

Mistral AI가 Leanstral 1.5를 Apache 2.0 라이선스로 공개했다(〈Mistral AI〉 2026.07.02). 119B 총 파라미터·6B active(MoE) 모델로, Lean 4 기반 정형 검증(formal verification)·증명 엔지니어링에 특화됐다. 벤치마크에서 miniF2F 포화, PutnamBench 587/672 해결을 보고했으며, 57개 오픈소스 Rust 저장소 자동 스캔에서 11건의 실제 버그(그중 5건은 GitHub 미보고)를 찾아냈다(〈Mistral AI〉 2026.07.02). 개발자는 Hugging Face 가중치와 무료 API(leanstral-1-5) 로 실험할 수 있다.

무슨 일이 있었나

모델 스펙 (〈Mistral AI〉 2026.07.02)

• 라이선스: Apache 2.0 (상업·자체 호스팅 가능)
• 아키텍처: MoE, 6B active / 119B total
• 컨텍스트: 장기 증명 시 220만+ 토큰 처리 사례 보고 (AVL 트리 시간복잡도 증명)
• 배포: Hugging Face, Mistral Vibe, Labs API

성능 하이라이트

| 벤치마크 | 결과 |

| --- | --- |

| miniF2F | 100% (검증·테스트 세트) |

| PutnamBench | 587/672 |

| FATE-H | 87% |

| FATE-X | 34% |

코드 검증 파이프라인 (〈Mistral AI〉 2026.07.02)

1. Aeneas: Rust 코드 → Lean으로 변환

2. Leanstral 1.5: 코드에서 정확성 속성(property) 추론

3. 증명 시도(각 4회) 실패 시 부정 명제 증명 시도

4. 57개 저장소 스캔 → 47개 위반 속성 → 11개 실제 버그 확인

대표 버그 사례: datrs/varinteger

• zigzag decode sign 함수에서 Std.U64.MAX 입력 시 (value + 1) 정수 overflow
• debug에서는 크래시, release에서는 조용한 데이터 손상
• 전통 퍼징·단위 테스트로는 발견이 어려운 경계값 버그

시장의 해석

"증명 가능한 코드"의 실용화

정형 검증은 오랫동안 학술·핵심 인프라에 머물렀다. Leanstral 1.5는 LLM + 자동화 파이프라인으로 오픈소스 일반 라이브러리까지 범위를 넓혔다. 다만 57개 중 11버그(약 19%) 는 인간 검토·오탐 필터가 여전히 필요함을 보여 준다.

비용 구조

일부 분석에 따르면 PutnamBench 수준 문제를 경쟁 모델 대비 약 1/75 비용으로 처리했다는 주장이 있다(〈TPS Report〉 2026.07). 6B active로 고난도 추론을 노리는 MoE 효율 사례로 읽힌다.

고유 인사이트: Leanstral의 가치는 "수학 문제 풀이" 가 아니라 CI 파이프라인에 넣을 수 있는 검증 단계에 있다. 예를 들어 금융·암호·직렬화 crate는 PR마다 Aeneas+Leanstral 스캔을 돌려 overflow·불변식 위반을 차단하는 게이트로 쓸 수 있다. 다만 false positive 47→11 필터링 비용을 팀 SLA에 반드시 포함해야 한다.

체크포인트와 리스크

• 체크포인트
• Labs API retirement 일정(2026.09.30 예정, 〈Testing Catalog〉)
• OpenATP 등 도구 체인 Leanstral 1.5 포인터 업데이트
• Rust→Lean 변환 실패 케이스·unsupported construct 목록
• Mistral Vibe에서의 증명 디버깅 UX

• 리스크 요인
• 오탐·미탐 — 프로덕션 단독 의존 불가
• 256k 컨텍스트 한도 vs 초장기 증명 컴팩션 이슈
• API 무료 기간 종료 후 비용 급증

마무리

Leanstral 1.5는 "AI가 코드를 짠다" 논쟁 옆에 "AI가 코드를 증명한다" 축을 추가했다. Rust·시스템 프로그래밍을 다룬다면, 작은 crate 하나로 Aeneas+Leanstral 파이프라인을 돌려보는 것이 가장 빠른 학습 경로다. Apache 2.0이므로 사내 PoC 장벽도 낮다. 다만 자동 증명 ≠ 배포 승인 — 최종 판단은 여전히 엔지니어·리뷰에 남는다.

참고 자료

• Leanstral 1.5: Proof Abundance for All - Mistral AI (2026-07-02)
• Mistral releases Leanstral 1.5 model for proof engineering - Testing Catalog (2026-07)