---
title: "미스트랄, 수학 증명·코드 검증용 오픈소스 모델 ‘린스트랄 1.5’ 공개"
published: 2026-07-04T08:05:02.731Z
canonical: https://jeff.news/article/4614
---
# 미스트랄, 수학 증명·코드 검증용 오픈소스 모델 ‘린스트랄 1.5’ 공개

미스트랄이 Lean 4 기반 수학 증명과 코드 검증에 특화한 오픈소스 모델 린스트랄 1.5를 공개했다. 1190억 파라미터 MoE 구조지만 실제 추론에는 약 65억 파라미터만 쓰고, 퍼트넘벤치 672문제 중 587개를 해결했다.

- 미스트랄이 수학 증명과 코드 검증에 특화한 오픈소스 AI 모델 ‘린스트랄 1.5’를 공개함
  - 기존 린스트랄-2603의 후속 모델이고, 미스트랄 스몰 4 계열을 기반으로 만들어짐
  - 목표가 꽤 명확함. 대규모 언어 모델(LLM)이 그럴듯한 답을 쓰는 게 아니라, Lean 4로 검증 가능한 수학 증명과 코드 논리를 만들어내는 쪽임

- 구조는 전문가 혼합(MoE)이라 덩치는 큰데, 실제 계산은 꽤 아껴 쓰는 타입임
  - 전체 파라미터는 1190억 개지만, 입력 토큰마다 128개 전문가 중 4개만 활성화함
  - 그래서 실제 연산에는 약 65억 파라미터만 쓰는 구조고, 미스트랄은 이걸 비용 효율의 핵심으로 밀고 있음
  - 컨텍스트는 최대 25만6000토큰까지 지원하고, 입력은 텍스트와 이미지를 받을 수 있음

- 학습도 그냥 수학 데이터 때려 넣은 수준이 아니라, Lean 컴파일러 피드백을 루프 안에 넣은 게 포인트임
  - 먼저 중간학습, 지도 미세조정(SFT), CISPO 기반 강화학습(RL)을 거침
  - 한 환경에서는 모델이 수학 정리를 증명하거나 반박하고, Lean 컴파일러가 내는 오류를 보고 다시 고치는 식으로 반복함
  - 다른 환경에서는 파일 시스템 안에서 파일을 수정하고 Bash 명령을 실행하고 Lean 언어 서버에서 목표, 오류, 타입 정보를 확인함. 거의 개발자처럼 증명 작업을 굴리는 셈임

> [!IMPORTANT]
> 퍼트넘벤치에서 672문제 중 587개를 해결했는데, 문제당 비용은 약 4달러로 제시됨. 경쟁 모델들이 수십 달러에서 300달러 이상을 쓰는 설정과 비교하면 꽤 센 주장임.

- 벤치마크 숫자는 꽤 세게 나옴
  - 정형 수학 벤치마크 miniF2F에서는 검증셋과 테스트셋 모두 100%를 기록함
  - 퍼트넘 수학경시대회 문제 기반 퍼트넘벤치에서는 672문제 중 587개를 해결함
  - 추상대수학 벤치마크 FATE-H와 FATE-X에서는 각각 87%, 34%로 새 최고 성능을 냈다고 함
  - 페르마의 마지막 정리 저장소의 풀리퀘스트 기반 FLTEval에서도 Pass@1은 21.9에서 28.9로, Pass@8은 31.9에서 43.2로 올라감

- 진짜 흥미로운 건 ‘더 오래 생각하면 더 잘 푼다’는 테스트 타임 스케일링이 꽤 선명하게 보였다는 점임
  - 퍼트넘벤치에서 5만 토큰 예산으로는 44문제를 풀었음
  - 20만 토큰에서는 244문제, 100만 토큰에서는 493문제까지 올라감
  - 400만 토큰까지 늘리자 587문제를 해결함. 어려운 증명 문제에서는 추론 예산이 곧 성능이라는 걸 숫자로 보여준 셈임

- 코드 검증 쪽에서도 그냥 데모가 아니라 실제 저장소를 건드린 사례가 나옴
  - 미스트랄은 Rust 코드를 Lean으로 변환하는 Aeneas와 결합해 57개 오픈소스 저장소를 분석함
  - 그 결과 47개의 속성 위반을 찾았고, 이 중 11건이 실제 버그로 확인됨
  - 5건은 기존에 깃허브에 보고되지 않았던 새 버그였다고 함

- 대표 사례는 Rust 라이브러리 datrs/varinteger의 Zigzag 디코딩 오버플로우임
  - 최대 64비트 정수 입력에서 `(value + 1)` 연산이 오버플로우를 일으키는 문제였음
  - 디버그 모드에서는 프로그램이 종료되고, 릴리스 모드에서는 데이터 손상으로 이어질 수 있는 버그였음
  - 기존 테스트나 퍼징으로는 잡기 어려웠던 케이스를 자동으로 찾았다는 게 미스트랄의 주장임

- 공개 방식도 꽤 공격적임. 허깅페이스에 오픈소스로 올라가고, 미스트랄의 AI 에이전트 CLI인 Mistral Vibe와 무료 API `leanstral-1-5`로 쓸 수 있음
  - 수학 연구자만이 아니라 정형 검증, 컴파일러, 보안, 고신뢰 시스템 쪽 개발자들이 바로 실험해볼 수 있는 포지션임
  - 특히 한국에서도 금융, 반도체, 임베디드, 보안처럼 “틀리면 큰일 나는 코드”를 다루는 팀은 관심 가질 만함

---
## 기술 맥락
- 린스트랄 1.5의 핵심 선택은 Lean 4를 모델의 작업 환경으로 삼은 거예요. 자연어 답변은 그럴듯해 보여도 맞는지 확인하기 어렵지만, Lean은 증명과 타입을 기계적으로 검증해주거든요.

- MoE 구조를 쓴 이유도 비용 때문이에요. 전체 모델은 1190억 파라미터 규모지만 매 토큰마다 일부 전문가만 켜면, 큰 모델의 전문성은 가져가면서 추론 비용은 낮출 수 있어요.

- 강화학습 환경을 파일 시스템과 Lean 언어 서버까지 확장한 것도 중요해요. 실제 증명 작업은 한 번에 답을 쓰는 문제가 아니라, 오류를 보고 파일을 고치고 보조 정리를 추가하는 반복 작업이기 때문이에요.

- Rust 검증 사례가 의미 있는 이유는 수학 벤치마크를 넘어 실제 코드베이스로 연결됐기 때문이에요. Aeneas로 Rust 코드를 Lean 쪽으로 옮긴 뒤 속성 위반을 찾는 흐름은, 장기적으로 테스트와 퍼징의 빈틈을 보완할 수 있는 방식이에요.

## 핵심 포인트

- 린스트랄 1.5는 Lean 4 증명 보조 시스템에 최적화된 AI 코드 에이전트다
- miniF2F 검증셋과 테스트셋에서 모두 100%를 기록했고 퍼트넘벤치에서는 587문제를 풀었다
- Rust 코드를 Lean으로 변환해 57개 오픈소스 저장소에서 47개 속성 위반을 찾았고, 11건은 실제 버그로 확인됐다

## 인사이트

LLM 경쟁이 ‘말 잘하는 모델’에서 ‘검증 가능한 정답을 만드는 모델’로 넘어가는 장면임. 특히 비용까지 낮췄다는 점 때문에 연구용 장난감이 아니라 실제 코드 검증 파이프라인 후보로 볼 만하다.