미스트랄, Lean 4 정리증명 오픈모델 Leanstral 1.5 공개 (Apache-2.0)

핵심 요약

미스트랄이 7월 2일 형식 검증 언어 Lean 4용 오픈웨이트 모델 Leanstral 1.5를 Apache 2.0 라이선스로 공개했다. 119B 파라미터 MoE(활성 6.5B)에 256k 토큰 컨텍스트를 갖췄고, 수학 증명 벤치마크 PutnamBench 672문제 중 587개를 풀었다.

1. 사양과 성능

2. 제공과 라이선스

• Hugging Face 공개 + 무료 API(Mistral Labs 티어 $0)
• Apache 2.0 — 상업적 사용·수정 자유
• 57개 저장소 테스트에서 기존에 알려지지 않은 버그 5개 발견

3. 왜 Lean 4인가

Lean 4는 수학·소프트웨어를 기계가 검증 가능한 형식으로 증명하는 언어다. LLM이 "그럴듯한" 답을 넘어 형식적으로 옳음이 검증된 증명·코드를 생성하도록 돕는 것이 핵심 가치로, 환각을 원천 차단하는 방향이다.

자주 묻는 질문

정리증명 모델이 일반 개발에 어떤 의미가 있나요?

형식 검증은 금융·항공·암호처럼 오류가 치명적인 영역에서 코드의 정확성을 수학적으로 보장합니다. LLM이 이 과정을 자동화하면, 검증 비용이 높아 미뤄지던 안전성 증명을 더 널리 적용할 수 있게 됩니다.

Apache 2.0 오픈웨이트라는 게 왜 중요한가요?

가중치를 내려받아 자체 인프라에서 돌리고 상업적으로 활용·수정할 수 있다는 뜻입니다. 폐쇄 API에 종속되지 않고 온프레미스로 민감 데이터를 다룰 수 있어, 연구·기업 도입 문턱이 크게 낮아집니다.