# Leanstral: 신뢰할 수 있는 코드 및 형식 증명 엔지니어링을 위한 오픈소스 에이전트

> Clean Markdown view of GeekNews topic #27586. Use the original source for factual precision when an external source URL is present.

## Metadata

- GeekNews HTML: [https://news.hada.io/topic?id=27586](https://news.hada.io/topic?id=27586)
- GeekNews Markdown: [https://news.hada.io/topic/27586.md](https://news.hada.io/topic/27586.md)
- Type: GN+
- Author: [neo](https://news.hada.io/@neo)
- Published: 2026-03-17T15:33:13+09:00
- Updated: 2026-03-17T15:33:13+09:00
- Original source: [mistral.ai](https://mistral.ai/news/leanstral)
- Points: 1
- Comments: 1

## Topic Body

- **Lean 4**용으로 설계된 최초의 오픈소스 코드 에이전트로, **형식 증명(formal proof)** 을 자동화해 인간 검증 부담을 줄이는 것을 목표로 함  
- **Apache 2.0 라이선스**로 모델 가중치를 공개하고, **Mistral Vibe** 환경과 **무료 API 엔드포인트**를 통해 즉시 사용 가능  
- **6B 활성 파라미터**의 희소 아키텍처를 사용해 효율성과 비용 절감을 달성하며, **lean-lsp-mcp**와 같은 MCP 통합을 지원  
- **FLTEval 벤치마크**에서 Qwen3.5, GLM5, Kimi-K2.5 등 대형 오픈소스 모델보다 높은 점수를 기록하고, **Claude Sonnet** 대비 15배 이상 저렴한 비용으로 유사 성능을 보임  
- **형식 증명 자동화와 코드 신뢰성 향상**을 결합한 새로운 접근으로, 연구 수학과 미션 크리티컬 소프트웨어 개발 모두에 활용 가능성 제시  

---

### Leanstral 개요
- Leanstral은 **Lean 4**를 위한 최초의 오픈소스 코드 에이전트로, **형식 증명 보조기(proof assistant)** 환경에서 작동  
  - Lean 4는 복잡한 수학적 객체(예: perfectoid 공간)와 소프트웨어 명세를 표현할 수 있음  
  - 기존 증명 시스템이 일반 모델 래퍼나 단일 문제에 집중하는 것과 달리, Leanstral은 **현실적 형식 저장소(formal repositories)** 에서 효율적으로 작동하도록 훈련됨  
- **6B 활성 파라미터**를 가진 희소(sparse) 아키텍처를 채택해, **병렬 추론(parallel inference)** 과 Lean의 검증 기능을 결합  
- **MCP 통합 지원**을 통해 lean-lsp-mcp와 같은 자주 사용되는 프로토콜과 호환  

### 공개 및 접근성
- **Apache 2.0 라이선스**로 모델 가중치를 공개하고, **Mistral Vibe** 내 에이전트 모드로 제공  
- **무료 API 엔드포인트(`labs-leanstral-2603`)** 를 통해 누구나 접근 가능하며, 사용자 피드백을 수집해 차기 모델 개선에 활용 예정  
- **기술 보고서**와 **평가 도구 FLTEval**을 함께 공개해, 기존 수학 중심 평가를 넘어 실제 증명 엔지니어링 성능을 측정  

### 성능 평가 (Evaluation)
- **FLT 프로젝트의 Pull Request 단위**로 모든 형식 증명 및 새로운 수학 개념 정의를 완료하는 능력을 기준으로 평가  
- 비교 대상: Claude Opus 4.6, Sonnet 4.6, Haiku 4.5, Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B, GLM5 744B-A40B  

#### Leanstral vs. 오픈소스 모델
- **Leanstral-120B-A6B**는 GLM5(16.6점), Kimi-K2.5(20.1점)보다 높은 **26.3점(pass@2)** 을 기록  
- Qwen3.5가 4회 실행(pass@4)에서 25.4점을 얻은 반면, Leanstral은 절반의 실행으로 더 높은 점수 달성  
- 동일 비용 수준에서 **29.3점(pass@4)** 까지 선형적으로 확장  

#### Leanstral vs. Claude 제품군
- **Sonnet 대비 2.6점 우위(26.3점 vs 23.7점)** 를 보이며, 실행 비용은 **$36 vs $549**로 15배 이상 저렴  
- **pass@16** 기준으로 31.9점을 기록해 Sonnet보다 8점 높음  
- 최고 성능의 **Claude Opus 4.6**은 39.6점을 기록했으나, 비용이 **$1,650**으로 Leanstral 대비 **92배** 높음  
- 모든 벤치마크는 **Mistral Vibe** 환경에서 수정 없이 수행  

| 모델 | 비용($) | 점수 |
| --- | --- | --- |
| Haiku | 184 | 23.0 |
| Sonnet | 549 | 23.7 |
| Opus | 1,650 | 39.6 |
| Leanstral | 18 | 21.9 |
| Leanstral pass@2 | 36 | 26.3 |
| Leanstral pass@4 | 72 | 29.3 |
| Leanstral pass@8 | 145 | 31.0 |
| Leanstral pass@16 | 290 | 31.9 |

### 사례 연구 (Case Studies)

#### Lean 버전 변경 대응
- **Lean 4.29.0-rc6**에서 발생한 타입 별칭 관련 오류를 다룬 StackExchange 질문을 입력  
- Leanstral은 문제 환경을 재현하고, **정의적 동등성(definitional equality)** 문제를 정확히 진단  
- `def` 대신 `abbrev`를 사용하도록 제안해, **rw 전술(tactic)** 이 다시 정상 작동하도록 수정  
- 문제 원인과 해결 이유를 사용자에게 명확히 설명  

#### 프로그램 추론 및 변환
- **Rocq**의 프로그램 정의를 **Lean**으로 변환하고, 사용자 정의 표기법까지 구현  
- 예시로 `plus2` 명령이 변수 X에 2를 더하는 동작을 수행함을 증명  
- 주어진 Rocq 명세만으로 Lean에서 **정리(theorem)** 를 완성하고 증명 수행  

### 사용 방법
- **Mistral Vibe 통합**: `/leanstall` 명령으로 즉시 사용 가능  
- **Labs API**: 무료 또는 저비용으로 접근 가능  
- **모델 다운로드**: Apache 2.0 라이선스로 직접 실행 가능  

### 의의
- Leanstral은 **코드 생성과 형식 증명 자동화**를 결합한 최초의 오픈소스 시도  
- **연구 수학, 검증 가능한 소프트웨어 개발, 고신뢰 시스템 설계** 등에서 활용 가능성 제시  
- **비용 효율성과 개방성**을 동시에 확보한 새로운 코드 검증 인프라로 평가됨

## Comments



### Comment 53222

- Author: neo
- Created: 2026-03-17T15:33:13+09:00
- Points: 1

###### [Hacker News 의견들](https://news.ycombinator.com/item?id=47404796) 
- 사람들이 이제 **에이전트가 원하는 동작을 명세하고**, 그 명세에 맞춰 코드를 작성할 수 있다는 패턴을 인식하기 시작한 게 흥미로움  
  TDD나 검증 도구 등 어떤 방식을 쓰든, 시간이 지나면 이런 검증 스위트가 “어떻게 동작해야 하는가”를 보여주는 실행 가능한 **문서 저장소**로 쌓이게 됨  
  이런 접근은 단순한 마크다운 스펙보다 훨씬 강력함. 의도가 아니라 **세부 동작**을 코드로 담기 때문임  
  소프트웨어가 복잡해질수록 “그건 Jim한테 물어봐” 식의 구두 전승은 한계가 있음
  - 차이가 크지 않다고 느낌. 코드도 결국 .md 파일에 적을 정보의 다른 표현일 뿐임  
    세밀함과 맥락이 해상도 변화 속에서 사라짐  
    TDD나 검증 중심 개발엔 동의하지만, 그걸 코드로 쓰는 게 최종 목표는 아님  
    이미 수백만 줄의 테스트가 존재하니, 그걸 **기반으로 발전**시키는 게 현실적임
  - AI가 등장하면서 비로소 **TDD가 꿈꾸던 현실**이 가능해졌다고 생각함
  - 이런 접근이 흥미롭지만, 블로그 글이 헷갈렸음  
    Lean이 실제로 어떤 도움을 주는지 궁금함.  
    예를 들어 Lean으로 상태 머신을 증명하고, 그걸 Dart로 옮기는 식인가?  
    Lean을 잘 몰라서 이게 현실적인 접근인지 감이 안 옴

- 최근 Jack Clark(Anthropic 공동창업자)과 Ezra Klein의 팟캐스트에서도 언급됐듯, **모델 정렬(alignment)** 은 상대적이며 다양성이 중요하다는 논의가 많음  
  Mistral의 모델이 다른 최전선 모델에 비해 뒤처진다는 의견도 있지만, 다양한 정렬 기법과 회사를 실험하는 게 생태계에 중요함
  - 결국 **시간이 해결**해줄 것이라 생각함

- 실제 성공 사례가 Simon Willison의 [Red Green TDD](https://simonwillison.net/guides/agentic-engineering-patterns/red-green-tdd/)를 떠올리게 함  
  Leanstral이 실패 환경을 재현하는 테스트 코드를 만들고, **정의적 동등성(definitional equality)** 문제를 찾아낸 과정이 인상적이었음
  - 에이전트가 스스로 테스트를 작성한다면, 코드와 테스트를 따로 작성할 때보다 **정확성 보장**이 더 높아질까 궁금함
  - TDD는 결국 **프롬프트 엔지니어링**과 같다고 생각함. 에이전트에게 명확한 목표를 주는 과정이니까

- 이 모델이 특정 작업에 맞게 훈련되었지만 **Opus보다 성능이 낮음**  
  Opus는 6배 비싸지만, 그만한 가치가 있어 보임
  - 아이디어는 좋지만, 결국 **품질이 신뢰보다 우선**임  
    자본이 적은 유럽 스타트업이 이런 틈새를 노리는 건 이해되지만, 큰 수익으로 이어지긴 어려울 듯함
  - 벤치마크 신뢰도는 애매하지만, pass@2나 pass@3 결과를 보면 인상이 달라짐  
    Codex 같은 모델과 비교하는 게 더 흥미로울 것 같음
  - 모델이 **오픈소스**라서 로컬에서 실행 가능함. 그게 꽤 중요한 포인트 아닌가?

- “신뢰할 수 있는 코드”라는 컨셉이 마음에 듦  
  하지만 비교 기준이 헷갈림. Haiku보다 싸다고 강조하지만, Haiku 자체가 이 작업에 약하고 Leanstral은 그보다 더 약함  
  정확성이 목표라면 “싸지만 별로”가 왜 중요한지 모르겠음  
  그래도 Opus도 완벽하지 않으니, 규모를 키우면 더 나은 결과를 낼 수도 있을 듯함
  - 그래프를 보면 pass 수를 늘릴수록 성능이 좋아짐  
    2회에서는 Haiku와 Sonnet보다 낫고, 16회에서는 Opus에 근접하면서도 **비용 효율**이 높음
  - 사실 간단함 — 프롬프트에 **“신뢰할 수 있는 출력만”** 요청하면 됨

- Lean을 모르는 입장에서, 이게 직접적인 가치가 있는지 궁금함  
  Go 같은 언어 코드에 자동으로 증명을 붙여주는 건가, 아니면 단순히 **오픈 모델의 다양성**을 응원하면 되는 건가?
  - 아마도 에이전트가 Lean4 명세를 생성하고, 그 명세를 기준으로 소프트웨어를 평가하는 구조일 것임  
    하지만 결국 Lean4 명세 자체가 **소프트웨어 아티팩트**가 됨  
    그렇다면 그 명세가 올바른지 검증하는 문제로 다시 돌아감 — 결국 **인간 검토**가 필요함

- 몇 주 전부터 이런 흐름을 예상했는데, 실제로 맞아 기쁨임  
  LLM 시대에는 코드의 인간 친화성보다 **증명 가능성과 토큰 효율성**이 더 중요해질 것 같음  
  Lean과 Rust를 결합해, “증명된 코드만 컴파일되는” 세상이 올 수도 있음  
  관련 논의는 [이전 댓글](https://news.ycombinator.com/item?id=47192116)에 정리했음
  - 다만 어떤 증명 시스템도 “옳은 증명”을 보장하지는 않음  
    단지 **논리적으로 유효(valid)** 함을 보장할 뿐임  
    증명이 무엇을 증명하는지 완전히 이해하는 건, 프로그램을 이해하는 것만큼 어렵지만, 그 과정에서 사고가 깊어지는 이점이 있음

- “오픈소스”를 말만이 아니라 실제로 **Apache-2.0 라이선스 가중치**로 공개한 점이 반가움
  - 하지만 커뮤니티 기준으로 보면, 모델을 재현할 수 없으면 “**open weights**”일 뿐 “open source”는 아님

- [Mistral 공식 뉴스](https://mistral.ai/news/leanstral)에 따르면  
  Claude Opus는 비용 1,650달러에 점수 39.6,  
  Leanstral pass@8은 145달러에 31.0, pass@16은 290달러에 31.9로,  
  **비용 대비 성능 효율**이 꽤 높음