Mistral, 형식 검증 특화 AI 모델 Leanstral 1.5 공개

Mistral AI 공식 발표에 따르면 회사는 Lean 4 기반 형식 증명과 코드 검증에 특화한 AI 모델 Leanstral 1.5를 공개했다. Mistral은 새 모델을 Apache 2.0 라이선스로 제공하며, Hugging Face 모델 가중치와 무료 API 엔드포인트를 함께 열었다고 밝혔다.

Leanstral 1.5는 전체 1190억 매개변수 가운데 60억 개 활성 매개변수를 사용하는 구조로 소개됐다. Mistral은 이 모델이 수학 정리 증명과 실제 코드 검증을 모두 겨냥한다고 설명했다. 형식 증명은 자연어 답변과 달리 Lean 컴파일러가 증명의 유효성을 확인할 수 있어, AI 추론 결과를 검증 가능한 산출물로 연결하려는 연구와 개발 흐름에서 주목받고 있다.

회사는 Leanstral 1.5가 miniF2F 검증·테스트 세트를 모두 해결했고, PutnamBench 672문제 가운데 587문제를 풀었다고 밝혔다. 또 추상대수 벤치마크인 FATE-H와 FATE-X에서 각각 87%, 34% 성능을 기록했다고 설명했다. 다만 이 수치는 Mistral이 공개한 평가 조건에 따른 결과이므로, 실제 활용 판단에는 제3자 재현과 비용·시간 조건 비교가 함께 필요하다.

훈련 과정은 중간 학습, 지도 미세조정, 강화학습으로 구성됐다. Mistral은 모델이 theorem statement를 받아 증명이나 반례를 시도하고, Lean 컴파일러 피드백을 통해 반복적으로 수정하는 환경에서 학습했다고 설명했다. 또 코드 에이전트 환경에서는 파일을 수정하고 명령을 실행하며 Lean 언어 서버의 목표와 오류 정보를 읽는 방식으로 긴 증명 작업을 수행하도록 훈련했다.

실제 코드 검증 사례도 제시됐다. Mistral은 Rust 코드를 Lean으로 번역하는 Aeneas와 Leanstral을 결합해 57개 오픈소스 저장소를 시험했고, 이 과정에서 47개 위반 속성을 표시했으며 그중 11개가 실제 버그로 이어졌다고 밝혔다. 회사는 이 가운데 5건은 GitHub에 이전에 보고되지 않은 버그였다고 설명했다.

이번 공개는 AI 모델 경쟁이 일반 대화와 코드 생성에서 검증 가능한 추론으로 넓어지고 있음을 보여준다. 특히 형식 검증 분야는 개발자가 작성한 코드가 특정 성질을 만족하는지 수학적으로 확인하는 영역이다. Leanstral 1.5가 실무 개발 과정에 널리 쓰이려면 모델 성능뿐 아니라 Lean 기반 검증 워크플로, 기존 테스트·정적 분석 도구와의 결합, 평가 결과의 독립 검증이 함께 따라야 한다.

출처: Mistral AI https://mistral.ai/news/leanstral-1-5/ · Hugging Face https://huggingface.co/mistralai/Leanstral-1.5-119B-A6B · Mistral Docs https://docs.mistral.ai/models/model-cards/leanstral-1-5