Mistral AI가 Lean 4 기반의 증명 특화 대규모 언어 모델 Leanstral 1.5를 Apache-2.0 라이선스로 공개했다. 미니F2F 100% 달성은 물론 실제 코드 저장소 57곳에서 11건의 버그를 형식적으로 잡아냈다는 점까지, 증명 모델이 연구실을 벗어나 개발现场에 투입될 수 있다는 신호다.
- Leanstral 1.5는 119B 총 파라미터 중 6B만 활성화하는 MoE 구조로, 3단계 학습 파이프라인을 거쳐 Apache-2.0로 공개됐다.
- miniF2F 100%, PutnamBench 87.3%, FATE-H 87%, FATE-X 34%를 기록해 학회 증명 벤치마크에서 최고 수준 점수를 받았다.
- Rust-to-Lean 파이프라인으로 57개 저장소를 검증해 11개의 실제 버그를 탐지, 증명 모델의 실무 적용 가능성을 입증했다.
증명 모델이 학술용을 넘어 코드 저장소 검증까지 영역을 확장하며 오픈소스 형식 검증 시대가 본격화되고 있다.
Leanstral 1.5 개요
Mistral AI의 첫 증명 특화 모델
Leanstral 1.5는 Mistral AI가 Lean 4 증명 언어를 위해 직접 학습한 첫 번째 전용 모델이다. 발표에 따르면 모델 이름은 Lean(증명 언어) + Mistral(기업명)의 합성어이며, Mistral AI 공식 홈페이지를 통해 가중치가 함께 배포된다. 이전까지 증명 모델 대부분이 비공개 연구였다는 점에서 이번 공개는 의미가 크다는 평가가 나온다.
119B/6B MoE 구조와 Apache-2.0 라이선스
총 119B 파라미터 가운데 실제 추론 시점에는 6B만 활성화되는 Mixture-of-Experts 구조다. 라이선스는 Apache-2.0로, 상업적 이용과 파생 모델 배포까지 허용한다. 동일 규모군의 경쟁 모델들이 비공개 가중치를 고수해온 것과 대비되는 선택으로, Mistral이 증명 분야에서도 오픈 전략을 이어가고 있음을 보여준다.
3단계 학습 파이프라인
수학 텍스트 기반 중간 학습
첫 단계에서는 일반 웹코퍼스 대신 수학 논문, 교과서, 보조정리 데이터베이스를 모아 중간 학습을 진행했다. 증명 모델의 품질이 사전학습 코퍼스의 수학 밀도에 크게 의존한다는 최근 연구 흐름을 그대로 따른 것으로 분석된다.
증명 트레이스 기반 SFT
두 번째 단계는 Supervised Fine-Tuning으로, Lean 4에서 성공한 증명 트레이스를 학습 데이터로 사용했다. 단순 문제-정답 쌍이 아니라 단계별 전술(tactic) 시퀀스를 그대로 모사하도록 구성한 점이 특징이다.
CISPO 기반 강화학습
세 번째 단계는 강화학습으로, 보상 신호는 증명 성공 여부만 사용했다. 발표문에 따르면 CISPO는 clipped importance sampling 계열의 RL 알고리즘으로 표기되며, 성공한 증명과 실패한 증명을 명시적으로 분리해 정책 업데이트를 안정화한다고 회사 측이 설명했다.
벤치마크 성능과 의미
miniF2F·PutnamBench 합성 증명 점수
| 벤치마크 | Leanstral 1.5 | 성격 |
|---|---|---|
| miniF2F | 100% | 합성 수학 올림피아드 |
| PutnamBench | 587/672 (87.3%) | 대학 수학 경시대회의 형식화 |
| FATE-H | 87% | 실제 Hacker 표준 라이브러리 검증 |
| FATE-X | 34% | 실제 외부 프로젝트 검증(Experiments) |
미니F2F 100% 달성은 해당 데이터셋이 사실상 포화 상태에 도달했음을 시사한다. PutnamBench 87.3%는 672문제 중 587문제를 해결했다는 의미로, 이전 최고 수준 모델들과 비교해도 상위권이라는 것이 회사 측의 주장이다.이다.
FATE-H·FATE-X 실제 증명 엔지니어링 점수
FATE-H와 FATE-X는 실제 코드 저장소에서 추출한 증명 과제다. FATE-H 87%는 Lean 표준 라이브러리 수준에서는 모델이 거의 풀어낼 수 있음을, FATE-X 34%는 외부 비표준 프로젝트에서는 난이도가 크게 뛰어오른다는 사실을 각각 보여준다.
합성-실제 격차가 시사하는 모델 한계
합성 벤치마크와 실제 프로젝트 점수 사이에는 여전히 상당한 격차가 존재한다. 이는 단순 점수 경쟁보다 도메인 일반화가 핵심 과제임을 시사한다는 해석이 관련 커뮤니티에서 나오고 있다.
코드 저장소 적용 사례
Rust-to-Lean 파이프라인 구조
Mistral은 Leanstral 1.5와 함께 Rust 코드를 Lean 4 정형 명세로 변환하는 파이프라인을 공개했다. 단계는 크게 Rust 파싱, 사양 추출, Lean 정형화, 자동 증명의 4단계로 구성된다. 기존 Coq용 도구들과 달리 Rust 생태계에 맞춘 것이 특징이다.
AVL 트리 O(log n) 증명 사례
공개 사례 중 대표적 예시는 AVL 트리의 균형 유지 조건이 회전 연산 후에도 유지된다는 점에 대한 O(log n) 시간 복잡도 증명이다. 발표에 따르면 사람이 수 시간 걸리는 보조정리 연결을 모델이 단독으로 완수했다고 회사 측은 소개했다.
57개 저장소 중 11개 버그 탐지 결과
다섯 개 카테고리 총 57개의 실제 오픈소스 Rust 저장소를 대상으로 평가를 진행했고, 11개 저장소에서 새로운 버그 또는 미묘한 불변식 위반이 발견됐다. 다만 회사는 구체적인 저장소 명단을 모두 공개하지는 않았다.
업계에 미치는 영향과 전망
증명 모델의 오픈소스 전환
증명 모델 분야는 학회 논문 형태로만 공유되는 폐쇄적 흐름이 강했다. Apache-2.0로 가중치가 풀린 만큼 대학 연구실뿐 아니라 보안과 금융처럼 검증 비용이 큰 산업에서도 자체 파인튜닝이 시도될 것으로 예상된다는 분석이 나온다.
엔터프라이즈 형식 검증 도입 가능성
형식 검증(Formal Verification)은 원래 수학 명제를 코드로 옮겨 결함이 논리적으로 불가능함을 보이는 기법이다. 증명 모델이 오픈소스로 제공됨에 따라 인증( certification) 이나 의료기기 같은 규제 산업에서도 도입 비용이 크게 내려갈 수 있을 것으로 보인다.
Mistral의 오픈 전략 강화
Mistral은 이전에도 라이트급 모델을 커뮤니티 우선으로 배포해왔다. 이번 증명 모델 공개로 오픈소스 LLM 라인업이 일반 chat 모델에서 수학·증명 영역까지 확장되었다는 점에서 회사의 오픈 전략이 일관되다는 평가다.
- 증명 모델은 학술용을 넘어 실제 코드 저장소 검증 단계로 영역을 넓혔으며, 결과적으로 57개 중 11개 저장소에서 실제 버그가 발견됐다.
- 합성 벤치마크와 실제 프로젝트 사이 점수 격차는 여전히 크므로 도메인 일반화 성능 향상이 향후 핵심 경쟁력이 될 가능성이 높다.
- Apache-2.0 기반 오픈 배포로 대학뿐 아니라 인증·보안 산업까지 형식 검증 도입 문턱이 낮아질 것으로 전망된다.
참고 출처: GeekNews 원문, Mistral AI 공식 발표