Mistral은 Lean4의 첫 번째 오픈 소스 코드 에이전트인 Leanstral을 출시했습니다. Leanstral은 코드를 생성하고 동시에 형식적 증명을 출력합니다.

1M AI 뉴스 에 따르면, 미스트랄 AI는 오늘 정형 검증 도구인 Lean 4를 위해 특별히 설계된 최초의 오픈 소스 코드 에이전트인 Leanstral을 출시했습니다. AI 코드 생성의 핵심 병목 현상은 사람의 검토인데, Leanstral은 코드를 생성하는 동시에 Lean 4에서 자동으로 검증할 수 있는 정형 증명을 출력함으로써 이 단계를 우회합니다. 이 모델은 총 1200억 개의 파라미터와 60억 개의 활성화 파라미터를 가진 희소 MoE 아키텍처를 사용하며, Apache 2.0 라이선스 하에 오픈 소스로 제공되고, lean-lsp-mcp에 특화된 학습 최적화 기능을 갖추고 있습니다. 미스트랄 바이브(`/leanstall` 명령어)에서 별도의 설정 없이 바로 시작하거나, 무료 API 엔드포인트 `labs-leanstral-2603`을 통해 호출할 수 있으며, 다운로드한 가중치를 자체 배포할 수 있습니다.

Mistral은 Lean 4 커뮤니티의 페르마의 마지막 정리 형식화 프로젝트를 테스트베드로 사용하는 새로운 평가 벤치마크인 FLTEval을 발표했습니다. 비용 비교: Leanstral pass@2는 36달러에 26.3점을 기록하여 549달러의 Claude Sonnet 4.6(23.7점)을 앞섰습니다. pass@16은 290달러에 31.9점을 기록하여 Sonnet보다 8점 높았으며, Claude Opus 4.6은 39.6점을 달성하기 위해 1,650달러가 필요합니다. 오픈 소스 모델 중 Qwen3.5-397B-A17B는 25.4점을 달성하기 위해 4번의 실행이 필요하며, 이는 Leanstral pass@2보다 낮은 점수입니다.