---
title: "미스트랄, 리언4 증명 자동화 모델 ‘린스트랄 1.5’ 공개"
published: 2026-06-30T20:44:56.000Z
canonical: https://jeff.news/article/4497
---
# 미스트랄, 리언4 증명 자동화 모델 ‘린스트랄 1.5’ 공개

미스트랄 문서에 리언4 형식 증명 공학에 최적화된 린스트랄 1.5 모델 카드가 올라왔다. 모델은 자동 정리 증명과 자동 형식화에 맞춰졌고, 전체 1190억 파라미터 중 65억 파라미터가 활성화되는 구조이며 25만6000 토큰 컨텍스트를 제공한다.

- 미스트랄이 린스트랄 1.5(Leanstral 1.5) 모델 카드를 공개함
  - 리언4(Lean 4) 형식 증명 공학에 최적화된 모델
  - 자동 정리 증명(automated theorem proving)과 자동 형식화(autoformalization)를 겨냥함

- 스펙은 짧지만 꽤 특화돼 있음
  - 전체 파라미터는 1190억 개
  - 실제 활성 파라미터는 65억 개
  - 컨텍스트 길이는 25만6000 토큰
  - 문서상 가격은 0달러로 표시됨

- 중요한 건 이 모델이 범용 코딩 모델이 아니라는 점임
  - 목표가 파이썬 함수 하나 짜주는 게 아니라, 리언4에서 증명을 만들고 정리하는 쪽에 있음
  - 자연어 명세를 형식 언어로 옮기는 자동 형식화까지 명시돼 있어서, 수학·검증·고신뢰 소프트웨어 쪽에 더 가까움

- 개발자 입장에선 아직 당장 주류 워크플로는 아니지만 방향성은 의미 있음
  - 테스트는 예시를 확인하는 도구고, 형식 증명은 성질 자체를 증명하는 쪽임
  - 금융, 컴파일러, 암호, 안전성 높은 시스템처럼 “틀리면 큰일 나는” 영역에선 이런 모델이 보조 도구로 커질 가능성이 있음

- 다만 원문이 모델 카드 수준이라 실제 벤치마크나 사용 사례는 거의 없음
  - 성능 수치, 비교 대상, 실패 케이스가 빠져 있어서 모델의 실전 가치는 추가 자료를 봐야 판단 가능함

## 핵심 포인트

- 린스트랄 1.5는 리언4 형식 증명 공학용 모델
- 자동 정리 증명과 자동 형식화에 최적화
- 전체 1190억 파라미터, 활성 65억 파라미터, 컨텍스트 25만6000 토큰

## 인사이트

본문은 짧지만 타깃은 꽤 선명하다. 일반 코딩 모델이 아니라 형식 검증과 증명 자동화 쪽으로 모델이 세분화되는 흐름이라, 안전성이 중요한 코드베이스를 다루는 팀은 눈여겨볼 만함.