# Leanstral 1.5: 모두를 위한 증명 풍요 > Clean Markdown view of GeekNews topic #31124. Use the original source for factual precision when an external source URL is present. ## Metadata - GeekNews HTML: [https://news.hada.io/topic?id=31124](https://news.hada.io/topic?id=31124) - GeekNews Markdown: [https://news.hada.io/topic/31124.md](https://news.hada.io/topic/31124.md) - Type: GN+ - Author: [neo](https://news.hada.io/@neo) - Published: 2026-07-05T01:44:33+09:00 - Updated: 2026-07-05T01:44:33+09:00 - Original source: [mistral.ai](https://mistral.ai/news/leanstral-1-5/) - Points: 1 - Comments: 1 ## Topic Body - 형식 검증을 실제 개발 작업에 더 가깝게 쓰려는 흐름 속에서, Mistral AI가 **Lean 4**용 Apache-2.0 모델 **Leanstral 1.5**를 공개함 - 모델은 119B 총 파라미터 중 6B만 활성화하며, 중간 학습·지도 미세조정·CISPO 강화학습을 거쳐 증명 작성과 코드 저장소 작업을 함께 학습함 - miniF2F 100%, PutnamBench 587/672, FATE-H 87%, FATE-X 34%를 기록해 수학 증명 벤치마크와 실제 증명 엔지니어링 평가에서 강한 성능을 보임 - 실제 코드 검증에서는 AVL 트리의 **O(log n)** 시간 복잡도 증명과 Rust-to-Lean 파이프라인을 통해 57개 저장소에서 11개 실제 버그를 찾아냄 - 가중치와 `leanstral-1-5` 무료 API가 공개되어, 정리 증명·증명 디버깅·저장소 기여 같은 **실용적 증명 엔지니어링**에 바로 적용 가능함 --- ### Leanstral 1.5의 공개와 모델 특성 - **Leanstral 1.5**는 [Lean 4](https://leanprover.github.io/)에서 증명 엔지니어링을 수행하도록 만든 모델임 - 라이선스는 **Apache-2.0**이며, 모델 규모는 총 119B 파라미터와 6B 활성 파라미터임 - 형식 검증 성능을 끌어올려 수학 벤치마크뿐 아니라 실제 코드 속성 검증에도 활용할 수 있음 - miniF2F를 포화하고, PutnamBench 672문제 중 587문제를 해결했으며, FATE-H 87%, FATE-X 34%를 달성함 ### 증명 피드백을 학습한 3단계 훈련 - 학습은 **중간 학습**, 지도 미세조정, CISPO 기반 강화학습의 3단계로 구성됨 - 강화학습에는 두 가지 환경이 쓰임 - **멀티턴 환경**: 모델이 정리 명제를 받아 증명하거나 반증하고, Lean 컴파일러 피드백을 바탕으로 증명을 반복 수정함 - 증명이 컴파일되면 성공하며, 그렇지 않으면 문제를 풀거나 예산을 소진할 때까지 루프가 이어짐 - **코드 에이전트 환경**: 원시 파일시스템에서 개발자처럼 파일을 편집하고, bash 명령을 실행하며, Lean language server로 목표·오류·타입 정보를 실시간 확인함 - 코드 에이전트 환경은 저장소 안의 부분 증명 완성, 보조정리 작성, 여러 차례의 컨텍스트 압축 이후에도 작업을 지속하는 긴 작업을 다룸 - 최종 정답성은 대상 정리 목록을 기준으로 [Mistral의 SafeVerify 포크](https://github.com/mistralai/LeanstralSafeVerify)에서 검증됨 ### 수학·증명 엔지니어링 벤치마크 - 평가에는 **miniF2F**, PutnamBench, FATE-H/FATE-X, FLTEval이 사용됨 - miniF2F는 초등 문제부터 IMO 수준 문제까지 포함하는 형식 수학 벤치마크임 - PutnamBench는 Putnam Mathematical Competition의 672개 문제로 구성됨 - FATE-H와 FATE-X는 각각 대학원·박사 수준의 추상대수 벤치마크임 - FLTEval은 Fermat’s Last Theorem 저장소의 실제 풀 리퀘스트를 기반으로 증명 엔지니어링 난도를 평가함 - miniF2F에서는 검증 세트와 테스트 세트 모두에서 **100%** 를 달성함 - PutnamBench와 FATE-H/X에서는 자연어 증명 가이드 없이 Goedel-Architect, Seed-Prover 1.5 high, AxProverBase와 비교됨 - FATE-H/X 성능: {b:87,34} - FATE-H는 **87%**, FATE-X는 **34%** 로 새로운 최고 성능을 달성함 - PutnamBench에서는 Seed-Prover 1.5 high보다 7문제를 더 풀었고, 문제당 비용은 약 **4달러** 수준임 - Seed-Prover의 high 설정은 문제당 10 H20-days 예산을 쓰며 비용이 300달러 이상으로 추정됨 - 더 높은 순위의 일부 증명기는 자연어 증명 가이드를 받거나, Aleph Prover처럼 문제당 54~68달러가 드는 다른 조건에서 동작함 ### 긴 추론 예산에서의 확장성과 FLTEval - Leanstral 1.5는 PutnamBench에서 토큰 예산을 늘릴수록 **Pass@8 성능**이 부드럽고 단조롭게 상승함 - 시도당 토큰 예산을 25k에서 4M까지 높인 실험에서 해결 문제 수는 다음처럼 증가함 - 50k 토큰: 44문제 - 200k 토큰: 244문제 - 1M 토큰: 493문제 - 4M 토큰: 587문제 - 긴 증명에서 중단하지 않고 수백만 토큰에 걸쳐 추론·파일 편집·수정을 계속하는 동작이 성능 향상으로 이어짐 - [FLTEval](https://github.com/mistralai/FLTEval)도 완전히 오픈소스로 공개됨 - FLTEval에서 Leanstral 1.5는 pass@1을 21.9에서 **28.9**로, pass@8을 31.9에서 **43.2**로 끌어올림 - pass@8 43.2는 Opus 4.6의 39.6을 넘는 수치이며, 비용은 7분의 1 수준임 - 오픈소스 모델 중 3~10배 큰 모델들보다도 앞선 성능을 보임 ### 실제 코드 검증 사례 - ## AVL 트리 시간 복잡도 증명 - AVL 트리는 삽입과 삭제 중 재균형을 통해 **O(log n)** 높이를 유지하는 자기 균형 이진 탐색 트리임 - Leanstral 1.5는 실제 구현에 대해 삽입과 삭제가 O(log n)임을 검증함 - 이 작업에는 트리 재귀 구조를 반영하는 구조적 귀납법, 모나드 기반 시간 추적 처리, 재균형 경로에 대한 전수 사례 분석이 필요했음 - 증명은 270만 개 이상의 토큰과 **22번의 컨텍스트 압축**을 거쳐 진행됨 - Leanstral은 TimeM 모나드의 각 계층을 체계적으로 펼쳐 제어 흐름과 섞인 계산을 드러냄 - 삽입에 대해 높이 단위당 48스텝과 상수항에 가까운 경계를 세우고, 높이와 트리 크기를 로그 관계로 연결함 - ## Rust 코드에서 버그 찾기 - 버그 탐지 실험은 **Aeneas**가 Rust 코드를 Lean으로 변환하고, Leanstral이 코드에서 사용자 의도를 추론해 정합성 속성을 생성하는 파이프라인으로 구성됨 - Leanstral은 각 속성을 4번 시도해 증명하고, 모두 실패하면 그 부정을 다시 4번 시도해 증명함 - 57개 저장소에서 47개 위반 속성이 표시됐고, 이 중 **11개가 실제 버그**를 가리킴 - 실제 버그 중 5개는 GitHub에 이전에 보고되지 않았던 버그임 - [datrs/varinteger](https://github.com/datrs/varinteger) 라이브러리의 zigzag decoding sign 함수에서 한 사례가 발견됨 - 입력이 `Std.U64.MAX`일 때 `(value + 1)` 표현식이 오버플로함 - 디버그 모드에서는 크래시가 발생하고, 릴리스 모드에서는 조용한 데이터 손상이 발생함 - 이 엣지 케이스는 일반적인 테스트와 퍼징이 놓치기 쉬운 사례임 ### 배포와 사용 방법 - 가중치는 [Hugging Face](https://huggingface.co/mistralai/Leanstral-1.5-119B-A6B)에 공개됨 - 무료 API 엔드포인트는 [모델 카드](https://docs.mistral.ai/models/model-cards/leanstral-1-5)에서 `leanstral-1-5` 이름으로 제공됨 - 사용 환경으로는 **Mistral Vibe**가 권장됨 - 시작 절차는 Mistral Vibe 설정, Leanstral 1.5 설치, 에이전트 실행, 선택적 Lean LSP MCP 설치, 증명 작업 시작 순서임 - [Lean LSP MCP](https://github.com/oOo0oOo/lean-lsp-mcp)는 `~/.vibe/config.toml`에 추가해 설치하는 방식이 권장됨 - 기존 MCP 서버가 없으면 `mcp_servers = []`를 제거해야 할 수 있음 - Leanstral은 정리 해결, 증명 디버깅, 저장소 기여 작업에 사용할 수 있음 ## Comments ### Comment 61264 - Author: neo - Created: 2026-07-05T01:44:34+09:00 - Points: 1 ###### [Hacker News 의견들](https://news.ycombinator.com/item?id=48780801) - Mistral이 대형 모델과 경쟁하기 어렵다는 비판은 타당하지만, 실제로는 **작은 모델에서 특정 기능을 고품질로 제공**하는 데 집중하고 있다고 봄 OCR이나 파일 분석 같은 작업에 Mistral을 쓰는데, 계정에 100달러를 넣어두면 요청량 걱정 없이 1년은 돌아감 비용이 극히 작아서, Opus 4.8과 경쟁하지 못하더라도 충분히 가치가 있음 - OCR에서는 실제로 얼마나 경쟁력이 있는지 궁금함 **저렴한 가격에 괜찮은 품질**은, 나중에 실수를 줄이기 위해 10배 가격을 내고 최고 품질을 쓰는 것보다 더 틈새시장처럼 보임 - 유럽 바보들은 돈을 최대한 버는 최적화가 아니라 **좋은 제품을 만드는 최적화**를 하고 있네 /s - “연 100달러 이하로 1년치 문서 처리”가 생각만큼 훌륭한지는 잘 모르겠음. 적어도 **유럽 경쟁력** 관점에서는 Mistral이 매출 상한을 너무 낮게 잡는 셈임 OCR은 이미 범용재에 가깝고, 오픈소스 모델이나 AWS 같은 곳에서도 기본으로 제공함 게다가 연 100달러 가격표로는 충성도를 만들기 어렵고, 전환 비용도 없어서 더 낮은 가격이 나오면 고객은 바로 떠날 수 있음 쉽게 복제되는 저가 도구에 고객 락인이 없다면 사업이라기보다 기능에 가까움 구매자 입장에서는 좋겠지만, 유럽 기업이 장기적으로 세계 경쟁사와 제품 역량으로 경쟁하길 원한다면 나쁜 전략으로 보임 - 작업 자체는 좋지만, **버그 발견 예시**가 이상하게 느껴졌음 zigzag 디코딩의 sign 함수에서 `Std.U64.MAX` 입력 시 `(value + 1)`이 오버플로되어 디버그 모드에서는 크래시, 릴리스 모드에서는 조용한 손상이 난다고 했는데, 이걸 테스트가 “보통 놓치는” 경계 조건이라고 부를 수 있는지 모르겠음 나쁜 테스트라면 놓치겠지만, 신중한 사람이나 기계학습 기반 코딩 시스템은 “극단값을 테스트해야겠다”를 꽤 잘함. 특히 사용자 입력을 파싱하는 코드라면 더 그렇다 더 흥미로운 버그도 찾았지만 빠르게 설명하기 어려워서 이 예시를 든 건지 궁금함 - 특히 “퍼징도 놓친다”는 부분이 이상함. 내가 본 **퍼징**은 일반적으로 경계값을 의도적으로 탐색함 이런 인코딩 라이브러리라면 괜찮은 코드의 기본 기대치가 퍼징이고, 거의 확실히 몇 초 안에 잡혔을 것 같음 실제로 `proptest`로 아주 간단한 왕복 테스트를 만들었더니 1초도 안 돼 수십 개 실패와 아래 결과가 나왔음: `thread 'signed_round_trip' (50528) panicked at tests/test.rs:72:1:` `Test failed: attempt to multiply with overflow.` `minimal failing input: value = 4611686018427387904` `successes: 2` `local rejects: 0` `global rejects: 0` - “보통 놓친다”고 하긴 어렵겠지만, 실제로 존재했으니 **가끔은 놓치는 버그**이긴 함 Lean을 쓰면 어떤 예시를 테스트해야 할지 영리하게 고를 필요가 줄어든다는 장점은 드러남 - 이건 기본적인 **품질 보증**임. 테스트가 이런 걸 놓친다면 우리가 보통 기대하는 것보다 훨씬 쓸모가 제한적일 것임 저자들의 배경이 궁금해짐 - 이건 그냥 쓰레기 홍보임 1980년쯤 발명된 모든 **속성 기반 테스트** 시스템은 경계값을 탐색함 C와 C++의 의미론, 또는 그 부재 때문에 실제 테스트가 어려울 수는 있음. 컴파일러가 정의되지 않은 동작으로 이어지는 모든 입력에 대해 “테스트 통과”라고 해도 허용되기 때문임 - 글 중간에 여러 최전선급 LLM과 비교가 나오는데, 전부 반년 전 모델들임 “우리 새 모델이 **3세대 전 중국 모델들**보다 낫다”는 식이라 꽤 웃겼음 - 이건 **60억 매개변수 모델**이라 완전히 다른 급임. 오히려 “최전선급 소형 언어 모델”이 더 기대됨 - 동의하지만, **오픈 가중치**이고 비교적 작다는 것만으로도 헤드라인감임. 이 모델은 꽤 잘 돌아감 - 그 라이브러리는 [https://github.com/datrs/varinteger]()임 논문이 공개되기 일주일 전에 같은 문제가 이미 이 저장소에 올라와 있어서 아마 맞는 것 같음: [https://github.com/datrs/varinteger/issues/8]() 이 사람이 Leanstral 직원인지, 아니면 Leanstral이 이 이슈를 그냥 가져온 건지는 모르겠음 이 라이브러리는 작고, 테스트가 놀랄 만큼 부실하며, 8년 동안 거의 손대지 않은 상태임: [https://github.com/datrs/varinteger/blob/master/tests/test.r...]() 다운로드는 하루 약 1천 건 정도라 낮은 편으로 보임: [https://crates.io/crates/varinteger]() 그래서 유일한 예시로 내세울 만큼 대단한 성공이라고 보기는 어려움. 자동 탐지가 유용한 건 맞지만, 이 하위 분야에서는 주목할 만한 성과인지 잘 모르겠음 증명 작성 LLM은 써본 적 없지만, 학습 데이터가 부족한 편이라 일반 코딩 모델보다 거칠어도 놀랍지는 않음 참고로 [https://crates.io/crates/varinteger]()에는 [https://github.com/mafintosh/varinteger-rs]()로 표시되지만, 이 주소가 [https://github.com/datrs/varinteger]()로 리다이렉트되므로 겉보기와 달리 같은 라이브러리로 보임 - **증명**의 문제는 가치를 전달하기가 가끔 어렵다는 데 있음 핵심은 버그를 찾는 게 아니라, 특정 종류의 버그가 특정 가정 아래 없다는 것을 증명하는 것임 하지만 이 이야기는 팔기 어려워서 마케팅은 자주 “이 버그를 찾았다” 쪽으로 흘러감 - Lean을 전혀 모르는 사람에게도 유용할 수 있을까? 작업 중인 소프트웨어를 검증하고 싶은데 **형식 검증** 경험이 없음 명세, 코드, 그리고 제한된 학습 시간만으로도 쓸 만한 결과를 얻을 수 있을지 궁금함 - 증명하려는 부분 자체는 이해해야 하지만, 전체 증명 과정을 다 이해할 필요는 없음 수학이라기보다 **Haskell 타입**을 읽는 것에 더 가깝고, 어휘만 수학에서 많이 빌려온 느낌임 - 글의 “Bug Discovery: Finding Hidden Flaws” 절을 읽어보면, Rust 코드만 가지고 시작해서 오픈소스 Rust에서 문제를 찾는 데 모델을 쓴 것으로 보임 애플리케이션 검증을 위한 **Lean 코드**를 작성하도록 대화하며 도움받을 수도 있겠지만, 확실하진 않음 - 최소한 코드에 대해 어떤 정리를 증명하고 싶은지, 그리고 그걸 Lean에서 어떻게 표현할지는 이해해야 함 그렇지 않으면 출력을 검증할 수 없음 기계적으로는 올바르다고 검사된 어떤 명제를 증명했을 수 있지만, 그 명제가 무슨 뜻인지, 실제로 검증하려는 내용을 포괄하는지 모르면 의미가 없음 - Lean4를 전혀 모르는 상태에서 약 6개월 만에 대부분의 코딩을 Lean4로 하는 수준까지 왔고, 이 과정은 **AI 보조** 덕분에 크게 빨라졌음 모델들이 Lean4에 얼마나 일관되게 유창한지 놀라울 정도임. 최전선급 모델뿐 아니라 작은 로컬 모델도 마찬가지였고, LLM이 Lean4를 그냥 잘 이해하는 것 같음 아직 Lean4 전문가라고 부르기엔 갈 길이 남았지만, 이제 유용한 프로그램을 만드는 데 보조가 꼭 필요하진 않음 지식이 거의 없는 상태에서도 완전히 이해하지 못한 부분을 신뢰할 수 있다는 점은 학습 속도를 크게 끌어올림. 불완전한 지식으로도 의존 가능한 프로그램을 얻는 게 실용적이고 동기부여도 됨 중간 증명 단계 전체가 아니라, 자신의 공리와 명제 표면을 설명하는 언어 부분에 의해 한계가 정해지는 느낌임. 시간이 지나 더 많은 것을 하려면 더 많이 이해해야 하지만, 어떤 의미에서는 N+1 수준에서 안전하게 작업할 수 있음 Lean4는 정리 증명 역할과 별개로도 즐거운 프로그래밍 언어이고, 속도도 놀랍게 빠름 `io_uring`에 붙여서 쓰고 있는데, 많은 경우 C++/libuv나 Rust/Tokio보다 훨씬 빠름 가끔 p99.99 지연 시간 같은 데서 큰 꼬리가 보이면 숫자를 고정 폭으로 바꾸는 식의 튜닝이 필요하지만, C++와 Rust도 튜닝은 해야 함 - Lean 4를 형식 검증용으로 밀고 있는 점이 흥미로움 이 영역은 **Isabelle/HOL**과 TLA+ 쪽이라고 생각했음 적어도 세 가지 모두를 쓰도록 학습한 모델을 기대했을 것 같음. 선형대수의 전방향 유도에는 Isabelle/Isar도 더 나아 보이는데, 누가 설명해줄 수 있을까? - Lean은 Isabelle이나 예전 Coq인 **Rocq**에 비해 소프트웨어 검증에서 채택이 적었던 게 맞음 이 분야에서는 Agda조차 더 많이 쓰인 편임 다만 Lean은 현재 대안으로 상당한 추진력을 얻고 있고, 특히 범용 함수형 프로그래밍 언어로서의 능력이 큼 개인적으로는 요구사항과 명세를 맞추기 쉬운 Hoare 논리나 분리 논리 기반 접근이 더 실용적이라고 봄. Dafny와 F*가 마음에 듦 - Twitter 발표에서 개발자들이 **Le Chaton Fat**을 슬쩍 언급하는 게 재미있었음 그들이 실제로 Le Chaton Fat에 관여했는지와 무관하게, 진짜 “새로운 대형 범용” 모델이 곧 나올 것 같음 미디어 소동 이후에도 직접 언급했으니 기대됨. 이름은 “Large 4”보다 더 창의적이면 좋겠음 - 최신 OpenATP에서 **Leanstral 1.5**를 써볼 수 있음 OpenATP는 에이전트형 자동 정리 증명기를 위한 오픈소스 Python 패키지이자 CLI이며, Docker에서 로컬로 실행하거나 Modal 샌드박스에서 원격 실행하는 방식을 기본 지원함 GitHub: [https://github.com/henryrobbins/open-atp]() Docs: [https://open-atp.henryrobbins.com]()