Mistral Leanstral 1.5, Rust 버그 11개를 잡은 Lean 4 모델

AI 요약

• 무슨 일: Mistral AI가 2026년 7월 2일 Leanstral 1.5를 공개했습니다.
  • Lean 4 형식 증명 모델로, 공식 발표는 119B 총 파라미터와 6B 활성 파라미터, Apache-2.0 라이선스를 제시합니다.
• 벤치마크: miniF2F 100%, PutnamBench 587/672, FATE-H 87%와 FATE-X 34%가 발표 수치입니다.
• 코드 영향: Rust 57개 저장소에서 위반 속성 47개를 표시했고, 이 중 실제 버그 11개를 찾았다고 Mistral은 설명합니다.
• 주의점: HN 토론에서는 대표 버그 예시가 일반적인 속성 기반 테스트로도 잡힐 수 있다는 반론이 나왔습니다.

Mistral AI가 2026년 7월 2일 Leanstral 1.5를 공개했습니다. 발표의 표면은 Lean 4용 형식 증명 모델입니다. 하지만 개발자 관점에서 더 눈에 띄는 대목은 수학 벤치마크보다 Rust 코드에서 실제 버그 11개를 찾았다는 주장입니다. Mistral은 57개 오픈소스 저장소를 대상으로 Rust 코드를 Lean으로 옮기고, 모델이 속성을 추론한 뒤 증명 또는 반증을 시도했다고 설명합니다.

이 뉴스는 범용 코딩 에이전트 릴리스와 다릅니다. 최근 devlery가 다룬 CodeRabbit Quiet 리뷰 프로필은 AI 리뷰 댓글을 사람이 읽을 수 있게 배치하는 문제였습니다. Google ADK Go 2.0은 에이전트 실행 순서와 사람 승인을 그래프로 묶는 문제였습니다. Leanstral 1.5는 그보다 좁습니다. 코드가 어떤 속성을 만족한다는 사실을 기계가 검사 가능한 증명으로 남길 수 있는가를 묻습니다.

출처 기반 생성 이미지입니다. 기준 사실은 Mistral의 2026년 7월 2일 공식 발표와 모델 카드에 둡니다.

Lean 4 증명을 코딩 에이전트 작업으로 바꿉니다

Leanstral 1.5의 대상은 일반 자연어 질의응답이 아닙니다. Mistral의 모델 카드는 이 모델을 Lean 4 형식 증명 엔지니어링과 자동 형식화를 위해 최적화한 모델로 설명합니다. 모델 카드에는 2026년 6월 30일 Labs v1.5, labs-leanstral-1-5, 문맥 256k, 가격 0달러, 119B 총 파라미터와 6.5B 활성 파라미터가 표시됩니다. 공식 발표문은 활성 파라미터를 6B로 적었습니다.

Mistral은 훈련 과정을 세 단계로 나눕니다. 중간 학습, 지도 미세조정, CISPO 강화학습입니다. 강화학습 환경은 두 종류입니다. 첫 번째는 멀티턴 정리 증명 환경입니다. 모델이 정리 명제를 받고 증명을 제출하면 Lean 컴파일러가 오류를 돌려주고, 모델은 그 피드백으로 증명을 고칩니다. 두 번째는 코드 에이전트 환경입니다. 모델이 파일시스템에서 파일을 고치고, bash 명령을 실행하고, Lean 언어 서버에서 목표와 타입 정보를 확인합니다.

이 구조가 코딩 에이전트 독자에게 의미 있는 이유는 작업 단위가 달라지기 때문입니다. 일반 코딩 에이전트는 테스트를 추가하거나 실패한 테스트를 고칩니다. Leanstral 1.5는 테스트가 아니라 증명 의무를 작업 항목으로 받습니다. 정리가 참이라는 증명을 만들고, 컴파일러가 받아들일 때까지 고치며, 필요하면 보조 정리와 파일 편집까지 수행합니다. 이는 PR 작성보다 느리고 좁은 작업이지만, 성공하면 결과물이 "그럴듯한 설명"이 아니라 Lean이 검사한 증명으로 남습니다.

수치는 크지만 조건을 같이 봐야 합니다

공식 발표의 첫 숫자는 miniF2F 100%입니다. miniF2F는 초등 문제부터 IMO 수준 문제까지 포함하는 형식 수학 벤치마크입니다. Mistral은 검증 세트와 테스트 세트 모두에서 100%를 달성했다고 적었습니다. PutnamBench에서는 672개 문제 중 587개를 해결했습니다. FATE-H는 87%, FATE-X는 34%로 표시됩니다. FLTEval에서는 pass@1이 28.9, pass@8이 43.2로 올랐고, Opus 4.6의 pass@8 39.6보다 높으며 비용은 7분의 1 수준이라고 설명합니다.

PutnamBench 비용 비교도 눈에 띕니다. Mistral은 Leanstral 1.5가 문제당 약 4달러로 Seed-Prover 1.5 high보다 7문제를 더 풀었다고 설명합니다. Seed-Prover 1.5 high는 문제당 10 H20-days 예산을 쓰며 비용이 300달러 이상으로 추정된다고 덧붙입니다. 다만 더 높은 순위의 일부 증명기는 자연어 증명 가이드를 받거나, Aleph Prover처럼 문제당 54달러에서 68달러가 드는 다른 조건에서 동작한다고 선을 긋습니다.

가장 실무적인 수치는 긴 추론 예산에서 나옵니다. Mistral은 PutnamBench에서 시도당 토큰 예산을 50k, 200k, 1M, 4M으로 늘리자 해결 문제가 44, 244, 493, 587로 늘었다고 적었습니다. 이는 모델이 긴 증명에서 멈추지 않고 파일을 고치고 추론을 이어 갈 때 성능이 올라간다는 주장입니다. 같은 발표에는 AVL 트리 삽입과 삭제의 O(log n) 시간 복잡도 증명을 270만 토큰과 22번의 문맥 압축으로 수행했다는 사례도 들어 있습니다.

Rust 버그 11개의 경로

Mistral의 코드 검증 실험은 Aeneas를 출발점으로 삼습니다. Aeneas는 Rust 코드를 Lean으로 변환합니다. 그 다음 Leanstral은 코드에서 사용자의 의도를 추론해 정합성 속성을 만듭니다. 모델은 각 속성을 네 번 증명하려고 시도합니다. 모두 실패하면 반대로 그 속성의 부정을 네 번 증명하려고 합니다. 이 과정을 거쳐 Mistral은 57개 저장소에서 47개 위반 속성을 표시했고, 그중 11개가 실제 버그였으며 5개는 GitHub에 이전 보고가 없었다고 밝혔습니다.

공식 발표는 datrs/varinteger 라이브러리의 zigzag decoding sign 함수 사례를 듭니다. 입력이 Std.U64.MAX일 때 (value + 1) 표현식이 오버플로하고, 디버그 모드에서는 크래시가 나며 릴리스 모드에서는 조용한 데이터 손상이 일어날 수 있다는 설명입니다. 이 지점에서 발표문은 이런 엣지 케이스를 일반 테스트와 퍼징이 놓치기 쉽다고 주장합니다.

그 문장은 그대로 받아들이기 어렵습니다. Hacker News 토론에서는 이 예시가 속성 기반 테스트로 쉽게 잡힐 수 있는 경계값 아니냐는 반론이 나왔습니다. 한 사용자는 proptest로 간단한 왕복 테스트를 만들면 1초 안에 실패를 재현할 수 있다고 적었습니다. 또 다른 사용자는 이 라이브러리가 작고 오래 손대지 않은 코드라서, 대표 성공 사례로 보기에는 조심해야 한다고 지적했습니다. 따라서 이 사례의 강점은 "퍼징이 절대 못 잡는 버그"가 아니라 명세를 만들고 증명 시도까지 자동으로 묶은 경로에 있습니다.

테스트 생성과 증명 작성은 다른 제품입니다

AI 코딩 도구는 이미 테스트 생성에 익숙합니다. 모델에게 "이 함수의 엣지 케이스 테스트를 추가해줘"라고 요청하면 Jest, Pytest, Go test, Rust test를 쉽게 작성합니다. 이 방식은 빠르고 이해하기 쉽습니다. 실패하면 개발자가 로그를 보고 고칩니다. 하지만 테스트는 입력 표본을 확인합니다. 정리 증명은 특정 명제가 조건 아래에서 항상 성립한다는 것을 검사합니다. 두 방식은 서로 대체재라기보다 비용과 확실성이 다른 검증 도구입니다.

Leanstral 1.5는 증명 작성의 진입 장벽을 낮추는 사용 경로까지 함께 냈습니다. Hugging Face 모델 페이지는 Mistral Vibe 안에서 vibe --agent lean을 실행하는 경로를 안내합니다. 선택적으로 Lean LSP MCP를 붙이는 설정도 함께 제시합니다. 로컬 배포도 열어 두었습니다. vLLM 서버에서 mistralai/Leanstral-1.5-119B-A6B를 띄우고 OpenAI 호환 클라이언트로 호출하는 예시가 들어 있습니다. 권장 vllm 버전은 0.24.0 이상입니다.

개발팀이 여기서 바로 얻는 결론은 "모든 Rust 라이브러리를 Lean으로 검증하자"가 아닙니다. 오히려 반대입니다. 형식 검증은 명세가 틀리면 아무 의미가 없습니다. Lean이 검사한 증명은 기계적으로 맞을 수 있지만, 그 명제가 실제 요구사항을 포괄하지 않으면 제품 안전과는 멀어집니다. 따라서 Leanstral 같은 모델은 테스트를 대체하는 자동 버튼보다, 명세 작성과 증명 디버깅을 도와주는 전문 에이전트에 가깝습니다.

Mistral의 좁은 모델 전략과 맞닿아 있습니다

Mistral은 최근 넓은 범용 챗봇 경쟁만 고집하지 않았습니다. devlery가 다룬 Mistral 커넥터 제어 GA는 MCP 권한과 커넥터 운영을 제품화한 사례였습니다. Mistral의 Emmi AI 인수는 산업 엔지니어링과 물리 시뮬레이션 쪽으로 내려가는 선택이었습니다. Leanstral 1.5도 같은 결을 가집니다. 작은 활성 파라미터와 좁은 작업 범위로 특정 기술 병목을 공략합니다.

HN의 긍정 반응도 이 지점에 몰렸습니다. 한 사용자는 Mistral이 대형 모델과 정면 경쟁하기 어렵다는 비판은 타당하지만, OCR과 파일 분석 같은 특정 능력을 저렴한 비용에 제공하는 전략을 봐야 한다고 썼습니다. 다른 사용자는 Mistral이 예전만큼 오픈 가중치를 많이 내지는 않는다고 아쉬움을 남겼지만, 작은 특화 모델과 도구가 Opus 같은 최전선 모델을 모든 작업에 쓰는 것보다 효율적일 수 있다고 봤습니다.

이 전략은 장점과 약점이 분명합니다. 장점은 비용과 배포 자유도입니다. Leanstral 1.5는 Apache-2.0 가중치와 무료 API 엔드포인트를 제시합니다. 약점은 시장 크기와 통합 난도입니다. 형식 검증을 실제 제품 개발에 쓰는 팀은 많지 않습니다. Lean 4, 명세, 증명 실패 해석, 기존 CI 연결을 모두 이해해야 합니다. Mistral이 모델을 공개했다고 해서 대다수 개발팀의 검증 습관이 곧바로 바뀌지는 않습니다.

Lean 4 선택에도 반론이 있습니다

HN 토론에서는 Lean 4를 소프트웨어 검증 전면에 세우는 선택에도 질문이 나왔습니다. 한 사용자는 이 영역이 Isabelle/HOL이나 TLA+ 쪽이라고 생각했다며, 여러 증명 도구를 함께 쓰도록 학습한 모델을 기대했다고 적었습니다. 답변자는 Lean이 소프트웨어 검증에서는 Isabelle, Rocq, Agda보다 채택이 적었던 것이 맞지만, 범용 함수형 프로그래밍 언어로서 추진력을 얻고 있다고 설명했습니다. 또 요구사항과 명세 정렬에는 Dafny나 F* 같은 접근이 더 실용적일 수 있다는 의견도 덧붙였습니다.

이 반론은 도구 선택의 실제 기준을 짚습니다. 형식 검증 도구의 선택은 모델 점수만으로 정해지지 않습니다. 조직이 이미 쓰는 언어, 검증하려는 속성, 팀의 수학 배경, 라이브러리 생태계, CI 통합, 리뷰 문화가 모두 들어갑니다. Leanstral 1.5가 Lean 4에서 강하다고 해서 TLA+ 명세, Dafny 계약, F* 검증, Coq/Rocq 생태계를 곧바로 대체하지 않습니다. Mistral의 발표는 Lean 4 쪽에 강한 신규 모델을 더했지만, 소프트웨어 검증 도구 논쟁을 끝낸 것은 아닙니다.

반대로 Lean 4에 관심 있는 개발자에게는 AI 보조가 학습 비용을 낮출 수 있습니다. HN의 한 사용자는 Lean 4를 전혀 모르는 상태에서 약 6개월 만에 대부분의 코딩을 Lean 4로 하는 수준까지 왔고, AI 보조가 이 과정을 크게 빠르게 했다고 적었습니다. 이 경험을 일반화할 수는 없지만, 증명 언어에서 모델 보조가 특히 강하게 느껴질 수 있는 이유는 있습니다. 컴파일러가 증명 실패 위치와 타입 정보를 정확히 돌려주기 때문입니다. 모델은 이 피드백을 받아 반복 수정할 수 있습니다.

개발팀이 지금 확인할 항목

첫째, 검증하려는 속성이 테스트로 충분한지부터 봐야 합니다. 경계값, 파싱 오류, 단순 불변식은 속성 기반 테스트와 퍼징이 더 빠르고 저렴할 수 있습니다. datrs/varinteger 반론은 이 기준을 확인하게 합니다. Leanstral 1.5가 가치 있는 자리는 테스트 케이스를 더 많이 만드는 것만으로 부족하고, 불변식과 증명 의무를 명시해야 하는 코드입니다. 암호, 파서, 상태 기계, 금융 계산, 동시성 자료구조가 후보가 될 수 있습니다.

둘째, 명세 작성 책임을 분리해야 합니다. 모델이 속성을 추론할 수 있어도, 그 속성이 제품 요구사항과 맞는지 판단하는 사람은 팀 안에 있어야 합니다. "이 함수는 항상 정렬된 리스트를 반환한다"와 "이 함수는 고객 결제 규칙을 만족한다"는 난도가 다릅니다. 전자는 코드 구조와 타입에서 추론할 수 있지만, 후자는 정책 문서와 비즈니스 예외를 알아야 합니다. 증명 모델은 명세 소유자를 없애지 않습니다.

셋째, 실행 비용과 시간을 제품 루프에 맞춰야 합니다. Mistral의 AVL 사례는 270만 토큰과 22번 문맥 압축을 썼습니다. 이는 자동완성이나 일반 코드 리뷰의 속도와 다릅니다. 야간 검증, 릴리스 전 고위험 모듈 검증, 보안 감사용 배치 작업에는 맞을 수 있습니다. 하지만 모든 PR마다 같은 수준의 증명을 요구하면 개발 속도가 막힐 수 있습니다.

넷째, 산출물 리뷰 방식을 정해야 합니다. Lean이 받아들인 증명은 신뢰할 수 있지만, 증명한 명제의 의미와 전제는 사람이 읽어야 합니다. PR에는 테스트 결과뿐 아니라 어떤 정리를 추가했는지, 어떤 전제를 두었는지, 어떤 파일을 신뢰 기반으로 삼았는지 표시해야 합니다. 증명 에이전트가 만든 diff는 코드 리뷰와 수학 리뷰를 동시에 요구합니다.

Leanstral 1.5는 개발자 도구 시장에서 화려한 데모보다 느린 질문을 던집니다. AI가 코드를 쓰는 일은 이미 익숙해졌습니다. 다음 질문은 AI가 쓴 코드나 사람이 쓴 코드에 대해 무엇이 항상 참인지 설명하고, 그 설명을 기계가 검사하게 만들 수 있는가입니다. Mistral의 발표는 그 질문에 대한 완성된 답은 아닙니다. 그러나 Rust 버그 탐지, FLTEval, 공개 가중치, Vibe와 Lean LSP MCP 경로를 한 번에 내놓으면서 증명 엔지니어링을 에이전트 워크플로 안으로 끌어왔습니다.

도입 판단은 냉정해야 합니다. 작은 라이브러리의 경계값 버그를 잡았다는 사례 하나로 기존 테스트 체계를 낮게 볼 수는 없습니다. Lean 4가 모든 팀의 검증 언어가 되는 것도 아닙니다. 그래도 Leanstral 1.5는 코딩 에이전트가 단순 구현과 리뷰 댓글을 넘어, 명세와 증명이라는 더 딱딱한 영역으로 들어가는 사례입니다. AI 개발팀이 이 발표에서 가져갈 메시지는 "테스트를 버리자"가 아니라 검증 작업의 단위를 테스트 케이스, 속성, 정리, 증명으로 나눠 보자입니다.