Leanstral 1.5: 미스트랄, Lean 4 증명 생성 모델을 아파치 2.0으로 공개

미스트랄 AI는 공식 블로그(mistral.ai/news/leanstral-1-5/)를 통해 2026년 7월 2일 Leanstral 1.5를 공개한다고 알렸다. 이 모델은 총 1190억 개 매개변수 중 약 60억 개만 활성화되는 희소 구조로 만들어졌으며 아파치 2.0 라이선스로 배포된다. 가중치는 허깅페이스에서 받을 수 있고, 미스트랄은 “labs-leanstral-1-5”라는 무료 API 엔드포인트도 함께 제공한다. 이 엔드포인트는 2026년 9월 30일 종료될 예정이다.

형식 검증이란 프로그램이 명세대로 동작한다는 사실을 수학적으로 증명하는 일이다. 지금까지는 항공전자, 철도, 암호처럼 실패가 치명적인 영역에만 머물러 있었다. 그런 증명을 손으로 쓰는 데 사람의 노동이 워낙 많이 들기 때문이다.

미스트랄은 miniF2F 벤치마크를 "포화시켰다"고 밝혔다. 검증 세트와 테스트 세트 모두에서 100%를 기록했다는 것이다. 이는 그 벤치마크가 더 이상 모델 사이의 차이를 가려내지 못한다는 뜻이지, Leanstral이 어떤 정리든 증명한다는 뜻은 아니다. 또한 이 모델은 PutnamBench의 672문제 중 587문제를 풀었고 FATE‑H(87%)와 FATE‑X(34%)에서 최고 수준에 도달했다고 한다. 짚어둘 점이 있다. 이 수치들은 오직 공식 발표에서 나온 것이며 아직 독립적인 연구로 확인되지 않았다.

미스트랄은 — TestingCatalog가 전한 내용이다 — 러스트 코드 검증 파이프라인에 붙여 오픈소스 저장소 57곳에 적용한 결과, 모델이 47건의 위반을 지적했고 그중 11건이 실제 버그, 5건은 깃허브에 한 번도 보고된 적 없는 것이었다고 밝혔다. 회사가 든 사례 가운데 하나는 datrs/varinteger 라이브러리의 지그재그 디코딩에 쓰이는 부호 함수의 오버플로다. 디버그 모드에서는 크래시를, 릴리스 빌드에서는 조용한 데이터 손상을 일으킬 수 있다. 이 역시 관리자들이 해당 보고를 받아들였는지는 아직 공개되지 않았다.

형식 검증 모델이 개방형 라이선스로 나온 것은, 그동안 고신뢰 산업에만 갇혀 있던 자동 검증 기술이 더 넓게 쓰이기 위한 중요한 한 걸음이다. 아파치 2.0이라는 말은 누구든 가중치를 내려받아 그 수치를 직접 시험해볼 수 있다는 뜻이기도 하다. 숫자가 버티는지는 그렇게 해서 알게 된다.