Leanstral: 신뢰할 수 있는 vibe-coding을 위한 오픈소스 기반

Leanstral은 Lean 4용 첫 오픈소스 코드 에이전트로, 고난도 수학과 미션 크리티컬 소프트웨어처럼 인간 검증 비용이 큰 영역에서 코드 생성과 형식 증명을 함께 수행하는 방향을 제시한다.

핵심은 6B active parameters를 가진 효율적인 sparse architecture다. Mistral AI는 이를 형식 증명 작업에 맞게 최적화했으며, Lean을 완전한 verifier로 활용하는 parallel inference 전략으로 성능과 비용 효율을 함께 노린다.

배포 범위도 넓다. Apache 2.0 라이선스의 weights를 공개했고, Mistral vibe의 agent mode와 무료 API endpoint, 향후 tech report와 새로운 평가 세트 FLTEval도 예고했다. 또한 MCP를 지원하며, 자주 쓰이는 lean-lsp-mcp에 맞춰 학습됐다고 밝혔다.

평가는 일반적인 competition math가 아니라 실제 proof engineering에 가까운 기준으로 진행했다. 각 PR에서 모든 formal proof를 완료하고 새 수학 개념을 정확히 정의하는지를 보는 방식이며, Claude Opus 4.6, Sonnet 4.6, Haiku 4.5와 오픈소스 모델들(Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B, GLM5 744B-A40B)과 비교했다.

비교 결과 Leanstral-120B-A6B는 훨씬 큰 오픈소스 모델들보다 효율적이었다. GLM5-744B-A40B와 Kimi-K2.5-1T-32B는 FLTEval 점수가 각각 약 16.6, 20.1 수준에 머문 반면, Qwen3.5-397B-A17B는 4 passes가 필요했지만 Leanstral은 더 적은 투자로 더 높은 점수를 냈다. pass@2에서는 26.3, pass@4에서는 29.3까지 올라갔다.

Claude 계열과의 비용 대비 성능 비교도 강조했다. Leanstral은 pass@2에서 26.3점으로 Sonnet의 23.7점을 넘기면서 비용은 $36에 그쳤고, pass@16에서는 31.9점을 기록했다. 반면 Claude Opus 4.6은 39.6점으로 품질 선두였지만, 실행 비용이 $1,650로 매우 높았다.

사례로는 두 가지를 제시했다.

• Lean 4 최신 버전에서 깨진 StackExchange 질문을 재현 환경까지 만들며 분석했고, def가 rw를 막는 이유를 definitional equality 관점에서 설명한 뒤 abbrev로 바꾸는 수정안을 제안했다.
• Rocq의 Imp 정의를 Lean으로 옮기고, 커스텀 notation까지 구현했으며, plus2 명령의 동작을 증명하는 예시도 보여줬다.

실사용 진입점도 바로 열어뒀다. Mistral Vibe에서는 /leanstall로 활성화할 수 있고, Shift+Tab으로 Leanstral을 선택하거나 vibe --agent lean을 사용할 수 있다. 또 labs-leanstral-2603 API endpoint와 Apache 2.0 weights도 제공해, 직접 실행 가능한 형식 검증형 코드 에이전트를 전면에 내세웠다.