미스트랄, 수학 증명·코드 검증용 오픈소스 모델 ‘린스트랄 1.5’ 공개

• 미스트랄이 수학 증명과 코드 검증에 특화한 오픈소스 AI 모델 ‘린스트랄 1.5’를 공개함

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

• 구조는 전문가 혼합(MoE)이라 덩치는 큰데, 실제 계산은 꽤 아껴 쓰는 타입임

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

• 학습도 그냥 수학 데이터 때려 넣은 수준이 아니라, Lean 컴파일러 피드백을 루프 안에 넣은 게 포인트임

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

• 벤치마크 숫자는 꽤 세게 나옴

  • 정형 수학 벤치마크 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 쪽으로 옮긴 뒤 속성 위반을 찾는 흐름은, 장기적으로 테스트와 퍼징의 빈틈을 보완할 수 있는 방식이에요.