프랑스 AI 기업 미스트랄이 4일(현지시간) 수학 정리 증명에 특화한 코드 에이전트 모델 ‘린스트랄 1.5(Leanstral 1.5)’를 아파치 2.0 오픈소스 라이선스로 공개했다. 정리 증명 언어 린4(Lean 4)를 다루도록 설계된 이 모델은 이전 버전인 린스트랄-2603을 개선한 것으로, 미스트랄 스몰4 계열에 속한다. 회사는 무료 API 엔드포인트도 함께 열었다.
린스트랄 1.5는 전체 1190억 개 매개변수 중 토큰당 65억 개만 활성화하는 전문가 혼합(MoE) 구조를 쓴다. 128개의 전문가 서브네트워크 가운데 4개만 매 토큰마다 호출돼 연산량을 낮추면서도 전체 용량은 크게 유지하는 방식이다. 컨텍스트 길이는 25만6000토큰이며 텍스트와 이미지를 함께 입력받아 텍스트로 답을 낸다. 훈련은 중간훈련, 지도 미세조정, CISPO 기반 강화학습 순으로 3단계에 걸쳐 이뤄졌으며, 정리 증명 여러 차례 시도와 실제 파일시스템에서 코드를 수정하는 두 가지 강화학습 환경이 모델의 행동 방식을 다듬었다고 미스트랄은 설명했다.
성능 면에서 미스트랄은 린스트랄 1.5가 수학 벤치마크 미니F2F의 검증·테스트 세트 모두에서 100%를 기록해 사실상 포화 상태에 도달했다고 밝혔다. 대학수학경시대회 문제 모음인 퍼트넘벤치에서는 672개 문제 중 587개를 풀었으며, 문제당 비용은 약 4달러 수준이라고 회사는 설명했다. 이는 경쟁 모델인 시드-프루버 1.5의 고성능 설정(문제당 300달러 이상 추정)보다 훨씬 저렴한 수준이다. 페르마의 마지막 정리 저장소의 실제 풀 리퀘스트로 구성된 FLTEval 벤치마크에서는 8회 시도 기준 정답률(pass@8)이 43.2%로, 앤트로픽 클로드 오퍼스 4.6의 39.6%를 앞섰다고 미스트랄은 주장했다.
미스트랄은 두 가지 사례 연구도 공개했다. 하나는 실제 AVL 트리(자가 균형 이진 탐색 트리) 구현의 시간 복잡도가 O(log n)임을 구조적 귀납법으로 증명한 사례이며, 다른 하나는 러스트(Rust) 코드를 린4로 자동 번역해 검증하는 파이프라인을 57개 오픈소스 저장소에 적용한 사례다. 이 과정에서 11건의 실제 버그가 발견됐고 이 중 5건은 깃허브에 보고된 적이 없던 문제였다고 회사는 밝혔다. 개발팀은 미스트랄의 CLI 도구 ‘바이브(Vibe)’나 자체 서버 구축용 오픈소스 추론 엔진 vLLM을 통해 린스트랄 1.5를 바로 사용해볼 수 있다.
