LLM - Leanstral : Lean 4용 범용 코드 에이전트 모델 시리즈

https://mistral.ai/news/leanstral/

https://www.alphaxiv.org/abs/2608.leanstral

2026.8.6
[Leanstral]

본 논문에서는 총 1190억 개의 파라미터 중 60억 개만 활성 파라미터로 사용하는 Lean 4용 범용 코드 에이전트 모델 시리즈인 Leanstral을 소개합니다. Leanstral은 특화된 증명 프레임워크 대신 오픈 소스 Mistral Vibe 코드 에이전트 하네스 내에서 직접 작동하며, 컨텍스트 압축 외에는 테스트 시간 확장 방법을 사용하지 않고, 문제당 토큰 예산이 증가함에 따라 성능이 매끄럽게 확장됩니다. 이러한 규모에도 불구하고 Leanstral은 훨씬 더 크고 독점적인 시스템에 필적하는 결과를 보여줍니다. miniF2F에서 포화 상태를 달성하고, PutnamBench에서 672개 문제 중 587개를 해결하며, FATE-X에서 34%, FLTEval에서 43.2%라는 새로운 최고 성능을 달성했습니다. Leanstral은 경쟁 수학 분야를 넘어 대학원 수준의 수학, 수리 금융, 코드 검증 등 다양한 실제 저장소의 문제를 해결합니다. Leanstral을 기반으로 구축된 완전 자동화 파이프라인은 오픈 소스 소프트웨어에서 이전에 알려지지 않았던 버그를 발견했습니다. 이 보고서에서는 Leanstral의 학습 방법과 테스트 시 계산량에 따른 성능 확장성을 자세히 설명합니다. Leanstral 1.5는 Apache-2.0 라이선스로 오픈소스로 공개되어 있습니다.