핵심 요약
- 모델 사양: Leanstral 1.5는 총 119B, 활성 6.5B 파라미터의 MoE 구조와 256k 컨텍스트 길이를 갖춘 Lean 4 특화 모델로 명시되어 있다
- 가격 정책: Mistral 공식 문서상 가격 항목이 $0로 표기되어 있으며, 실험과 평가 목적의 무료 접근이 강조된 것으로 기술되어 있다
- API 호환성: Chat Completions, 함수 호출, 에이전트, 구조화 출력, OCR, 문서 QnA, FIM, 임베딩, 모더레이션, 오디오, 배치 처리까지 광범위하게 지원
Leanstral 1.5는 닫힌 상용 모델 중심이던 형식 증명 도구 시장에 무료 학술 채널을 제공한다는 점에서 오픈수학·연구 인프라 확장에 의미 있는 변화로 읽힌다.
Mistral이 Lean 4 형식 증명 환경에 특화된 신규 모델 Leanstral 1.5(식별자 labs-leanstral-1-5)를 공식 문서에 등재했다. Geeknews 토픽(Leanstral 1.5) 기준 등록 시점은 2026-07-01T18:34:57+00:00 이며 Labs v1.5 모델군으로 분류된다. 자동 정리 증명과 자동 형식화를 겨냥한 이번 공개는, 그동안 상용 API 중심으로 전개되던 형식 증명 보조 영역에 무료 대체재를 제시한 첫 사례로 주목받는다.
Leanstral 1.5 개요 및 출시 배경
Leanstral 1.5는 Mistral이 자체 Labs 라인업에서 공개한 Lean 4 전용 보조 모델이다. Lean 4는 수학적 정리를 코드로 표현해 컴퓨터가 엄밀하게 검증하도록 돕는 형식 증명 언어로, AI 기반 보조 도구의 수요가 꾸준히 늘고 있다. Mistral 측은 이 모델이 정리 증명 자동화(theorem proving automation)와 자동 형식화(auto-formalization)에 초점을 두고 있다고 소개하고 있다.
형식 증명 자동화 워크플로
기존 Lean 4 보조 도구는 전형적으로 수학적 명제를 입력하면 캐스케이드 검색과 휴리스틱 결합으로 증명 시퀀스를 생성해 검증 엔진에 위임하는 흐름을 따른다. Leanstral 1.5는 LLM 단계에서 명제 해석과 증명 초안을 담당하는 구간을 대체하며, Lean 신택스에 가까운 출력과 자동 정리 증명(automatic theorem proving) 친화적 응답을 지향하는 것으로 소개된다.
오픈소스 AI 및 학술 커뮤니티 파급 효과
가격 항목이 $0로 명시된 무료 접근은 대학 연구실과 개인 학습자에게 비용 부담을 크게 낮춰준다. Mistral 공식 문서(Mistral Docs)에 따르면 이 모델은 평가와 연구 목적의 무료 사용이 강조되며, 오픈소스 AI 생태계에서 형식 증명 데이터셋 구축과 재현 가능 실험을 촉진할 것으로 보인다.
모델 아키텍처와 핵심 사양
공개된 사양을 핵심 수치 위주로 정리하면 다음과 같다.
- 모델 식별자: labs-leanstral-1-5 (Labs v1.5 계열)
- 파라미터 구조: 총 119B, 활성 6.5B의 전문가 혼합(MoE) 구성
- 컨텍스트 길이: 256k 토큰
- 목표 작업: Lean 4 형식 증명, 자동 정리 증명, 자동 형식화
MoE 구조는 활성화 파라미터를 억제하면서도 거대한 지식 용량을 확보하는 전형적인 스케일링 전략으로, 256k의 긴 컨텍스트는 긴 증명 스크립트나 다중 명제 일괄 처리에 유리하게 작용할 것으로 분석된다.
가격 정책과 접근 전략
Mistral 문서상 Leanstral 1.5는 가격 항목이 $0로 표기되어 있으며, 평가 및 연구 목적의 무료 접근을 강조한 가격으로 안내된다. Lean 4 보조 도구가 가진 시장 특성은 다름 아닌 다음과 같다.
- 대부분의 사용자가 학술 연구자 혹은 취미 개발자라는 점
- 장기적인 데이터 확보와 커뮤니티 확보가 모델 품질 향상의 핵심이라는 점
- 상용 모델의 경우 평가 비용이 결과 재현의 큰 장벽이라는 점
이런 점을 고려하면 무료 공개는 단가 경쟁이라기보다, 데이터 피드백 루프와 학술 커뮤니티 내 점유율 확보를 위한 전략적 선택으로 읽힌다.
Mistral API 통합 범위
Leanstral 1.5는 Mistral의 광범위한 엔드포인트와 호환된다. 호환 범위는 다음과 같이 정리된다.
| 엔드포인트 | 활용 의도 |
|---|---|
| Chat Completions | 대화형 증명 보조 세션 |
| 함수 호출 및 에이전트 | Lean 도구 체인 자동 호출 |
| 구조화 출력 | Lean 신택스 형태 응답 보장 |
| OCR / 문서 QnA | 논문 스캔본에서 명제 추출 |
| FIM / 임베딩 | 증명 라인 단위 채우기 및 검색 |
| 모더레이션 / 오디오 / 배치 | 안전 필터, 음성 입력, 대량 평가 |
OCR과 문서 QnA가 함께 노출된다는 점은, LaTeX 원고나 스캔 PDF에서 명제를 자동 추출해 Lean 4로 옮기는 파이프라인을 손쉽게 구성할 수 있음을 시사한다.
활용 시나리오와 전망
실질적으로 강점이 살아날 시나리오는 다음과 같이 정리된다.
- 학술 논문 보조: 256k 컨텍스트로 긴 증명본을 한 번에 입력해 부분 격차(gap) 후보를 도출
- 교육 환경: 학생이 작성한 증명 스텁을 입력으로 받아 오류 지점과 수정 제안을 즉각 피드백
- 데이터셋 구축: 자연어 명제와 Lean 4 증명 쌍을 대량 생성해 공개 벤치마크 확장
- 에이전트 파이프라인: 함수 호출과 구조화 출력을 활용해 Lean 컴파일러 호출·결과 해석을 자동화
다만 이 모델의 실질 성능이 일반 범용 모델 대비 어느 정도 우위를 제공하는지에 대한 벤치는 아직 제한적이며, Lean 4 도구 생태계와 결합한 종합 평가가 축적되어야 할 것으로 보인다. 그럼에도 무료 채널을 통한 접근성 확보는 해당 영역의 진입 비용을 급격히 낮추는 사건이라는 점에서 충분한 의의가 있다.
정리 포인트
- 사양 포인트: 119B MoE / 6.5B 활성 / 256k 컨텍스트, Labs v1.5 계열의 Lean 4 특화 모델
- 정책 포인트: 가격 항목이 $0로 표기된 무료 접근은 학술과 평가 목적의 확장 노선
- 생태계 포인트: OCR, FIM, 함수 호출, 구조화 출력 등 광범위한 API 호환으로 도구 체인 통합이 용이
- 관전 포인트: 무료 모델의 성능 검증과 오픈소스 데이터셋으로의 환원 여부가 향후 핵심 변수가 될 것