수학 증명을 100% 채운 모델이, 실제 코드 버그도 찾아냈다
벤치마크에서 100점을 받는 모델은 많아졌지만, 그 실력을 실제 코드의 숨은 버그를 찾는 데 그대로 써먹은 사례는 흔치 않아요. 7월 2일 Mistral AI가 공개한 Leanstral 1.5가 그 드문 사례예요. 어려운 증명 벤치마크를 포화시킨 동시에, 57개의 실제 오픈소스 저장소에서 아무도 몰랐던 버그 5건을 찾아냈거든요.
핵심 요약
- Mistral AI가 Lean 4(정리 증명기) 기반 증명 엔지니어링에 특화된 코드 에이전트 모델 Leanstral 1.5를 공개했어요.
- 아키텍처는 MoE로, 총 119B 파라미터 중 토큰당 4개 전문가만 활성화돼요(활성 파라미터는 자료마다 6B 또는 6.5B로 표기돼요).
- 어려운 수학 증명 벤치마크 miniF2F에서 검증·테스트 세트 모두 100%를 기록해 벤치마크를 포화시켰어요.
- 57개 오픈소스 저장소를 검사해 47개의 속성 위반을 찾아냈고, 그중 11개가 실제 버그였으며 5개는 GitHub에 보고된 적 없는 버그였어요.
- 가중치는 Apache-2.0 라이선스로 공개됐고, 무료 API로도 제공돼요.
The Model That Saturated a Math Benchmark Also Found Real Bugs in Production Code
Plenty of models now score 100% on some benchmark. Far fewer turn that same capability loose on real code and actually find bugs nobody knew about. Mistral AI’s Leanstral 1.5, released July 2, is one of those rare cases — it saturated a hard proof benchmark and, in the same release, flagged five previously unreported bugs across 57 real repositories.
TL;DR
- Mistral AI released Leanstral 1.5, a code agent model specialized in proof engineering built on Lean 4, a proof assistant.
- It’s a mixture-of-experts architecture: 119B total parameters, with only 4 experts active per token (reported as either 6B or 6.5B active, depending on the source).
- It saturated miniF2F, a hard formal-math benchmark, hitting 100% on both the validation and test sets.
- Across 57 tested open-source repositories, it flagged 47 violated properties, 11 of which were genuine bugs — 5 previously unreported on GitHub.
- Weights are released under Apache 2.0, with a free API also available.
구조화 분석
이 모델은 정확히 무엇을 하는 모델인가
Leanstral 1.5는 Lean 4라는 정리 증명기(proof assistant)를 다루는 코드 에이전트 모델이에요. 정리 증명기는 수학 명제나 소프트웨어의 속성(예: 이 함수는 항상 이런 조건을 만족한다)을 형식 언어로 표현하고, 그게 실제로 참인지 기계가 검증 가능한 방식으로 증명해주는 도구예요. Mistral은 이 작업을 “증명 엔지니어링(proof engineering)“이라 부르고, Leanstral을 여기에 최적화했어요. 자동 정리 증명과 자동 형식화(자연어로 된 명제를 형식 언어로 옮기는 작업) 모두를 다뤄요.
아키텍처는 128개 전문가 중 토큰마다 4개만 활성화하는 MoE(mixture-of-experts) 구조예요. 총 파라미터는 119B이고, 실제로 계산에 쓰이는 활성 파라미터는 약 6B(Hugging Face 모델명 기준)에서 6.5B(공식 서술 기준) 사이로 표기가 조금씩 달라요. 컨텍스트 윈도우는 25만6천 토큰으로, 긴 증명 과정을 다루기에 충분한 길이예요.
어떻게 훈련시켰나
훈련은 세 단계를 거쳤어요. 먼저 중간 훈련(mid-training)으로 기초 능력을 다지고, 그다음 지도학습 미세조정(SFT)으로 Lean 4 증명을 실제로 작성하는 능력을 훈련했어요. 마지막으로 CISPO라는 방식의 강화학습을 두 가지 환경에서 진행했는데, 하나는 여러 차례 대화를 주고받으며 정리를 증명하거나 반박하는 환경이고, 다른 하나는 파일을 직접 편집하고 bash 명령을 실행하고 Lean 언어 서버를 쓸 수 있는 코드 에이전트 환경이에요. 증명을 이론적으로만 다루는 게 아니라, 실제 개발 도구를 쓰면서 훈련시켰다는 뜻이에요.
miniF2F를 100% 채웠다는 것의 의미
miniF2F는 초급 문제부터 국제수학올림피아드(IMO) 수준까지 걸쳐 있는, 대수·조합론·정수론에 걸친 다양한 증명 능력을 시험하는 크로스시스템 벤치마크예요. Leanstral 1.5는 검증 세트와 테스트 세트 모두에서 100%를 기록하며 이 벤치마크를 포화시켰다고 밝혔어요. 이전 최고 점수가 정확히 몇 점이었는지는 공개된 자료에 나와 있지 않지만, 포화(saturate)라는 표현 자체가 이 벤치마크로는 더 이상 모델 간 실력 차이를 가늠하기 어려워졌다는 뜻이에요.
다른 지표들도 함께 공개됐어요. 672개 문제로 구성된 PutnamBench에서는 587문제, 약 87%를 풀었고요. FATE-H와 FATE-X에서는 각각 87%, 34%로 해당 시점 최고 성능을 기록했다고 해요. FLTEval에서는 Pass@1 기준 28.9%(이전 21.9%에서 상승), Pass@8 기준 43.2%(이전 31.9%에서 상승)를 기록했는데, 비교 대상으로 언급된 Opus 4.6의 FLTEval Pass@1이 39.6%였다는 점도 함께 공개됐어요.
진짜 코드에서 찾아낸 버그들
이 릴리스에서 가장 실용적인 대목은 벤치마크 바깥, 실제 오픈소스 코드에 적용해본 결과예요. 57개 저장소를 대상으로 테스트한 결과 47개의 속성 위반이 감지됐고, 그중 11개가 실제 버그로 확인됐으며, 이 중 5개는 GitHub에 한 번도 보고된 적 없는 버그였어요. 구체적으로 공개된 사례는 하나예요. datrs/varinteger라는 저장소의 지그재그 디코딩용 부호 함수에서, Std.U64.MAX 값이 입력되면 (value + 1) 연산에서 오버플로우가 발생하는 버그였어요. 디버그 모드에서는 크래시가 나지만, 릴리스 모드에서는 크래시 없이 조용히 데이터가 손상되는 무음 데이터 손상(silent data corruption)을 일으키는 버그였고요. 나머지 4건의 구체적인 저장소명과 내용은 공개되지 않았어요.
별도로 공개된 사례로, 실제 구현체의 AVL 트리(자가 균형 이진 탐색 트리)에 대해 삽입·삭제 연산이 O(log n) 시간 복잡도를 만족한다는 걸 완전히 증명한 사례도 있어요. 이건 버그를 찾은 게 아니라 정리를 증명한 사례인데, 트리의 재귀 구조를 그대로 반영하는 구조적 귀납, 모나드 기반 시간 추적, 재균형 경로에 대한 전수 케이스 분석이 모두 필요한 작업이었다고 해요. 270만 토큰과 22번의 압축(compaction)을 거쳐 완전하고 검증된 증명을 만들어냈다고 Mistral은 설명했어요.
공개 범위
가중치는 Apache-2.0 라이선스로 공개돼 Hugging Face(mistralai/Leanstral-1.5-119B-A6B)에서 받을 수 있고, API도 무료로 제공돼요. Mistral의 코딩 환경인 Mistral Vibe에서 쓰는 걸 권장하고 있고요.
왜 중요한가
형식 검증은 그동안 “이론적으로는 완벽하지만 실무에 쓰기엔 너무 느리고 어렵다”는 평가를 받아온 영역이에요. 사람이 직접 증명을 작성하려면 전문 지식과 오랜 시간이 필요했거든요. 이번 발표가 흥미로운 건, 벤치마크 포화라는 숫자놀음에서 그치지 않고 실제 오픈소스 코드에서 그동안 아무도 몰랐던 버그를 찾아냈다는 실증 사례를 함께 내놨다는 점이에요. 형식 검증 AI가 연구실 밖에서도 쓸모를 증명한 셈이에요.
이건 코드 품질 관리의 방식을 바꿀 수 있는 신호이기도 해요. 테스트 코드로 몇 가지 케이스만 확인하던 방식에서, 함수가 어떤 조건에서도 항상 성립해야 하는 속성 자체를 수학적으로 증명하는 방식으로 한 걸음 나아갈 수 있다는 가능성을 보여줬거든요.
핵심 통찰
이 릴리스가 보여주는 건, 벤치마크에서의 완벽한 점수와 실전에서의 유용성이 항상 같이 가는 건 아니지만, 이번만큼은 둘이 같은 능력에서 나왔다는 거예요. miniF2F를 풀어내는 데 쓰인 바로 그 증명 능력이, 실제 코드의 숨은 결함을 짚어내는 데도 그대로 통했다는 뜻이니까요.
증명 벤치마크를 100% 채운 능력이, 실제 프로덕션 코드에서 아무도 모르던 버그 5개를 찾아내는 능력과 같은 것이었어요.
이 지점에서 형식 검증 AI가 다음으로 갈 방향도 짐작할 수 있어요. 단발성 벤치마크 경쟁을 넘어, CI 파이프라인이나 코드 리뷰 과정에 상시로 들어가 속성 위반을 자동으로 잡아내는 도구로요.
My Take
저는 이 발표에서 버그 헌팅 사례가 벤치마크 점수보다 훨씬 인상 깊었어요. 100% 포화라는 숫자는 사실 체감하기 어렵지만, “GitHub에 보고된 적 없는 실제 버그 5개”는 바로 이해가 되는 결과거든요. AI 모델의 성능을 볼 때 벤치마크 순위표보다 이런 실전 적용 사례를 먼저 찾아보는 습관이 실제 유용성을 가늠하는 데 더 도움이 돼요.
다만 형식 검증은 아직 진입 장벽이 있는 영역이에요. Lean 4로 속성을 정의하고 증명 대상을 세팅하는 과정 자체가 일반적인 단위 테스트보다 손이 많이 가거든요. 그래도 오픈소스 가중치와 무료 API로 공개됐다는 점에서, 관심 있다면 자신이 자주 쓰는 라이브러리의 핵심 함수 하나를 골라 Leanstral로 속성 검증을 시도해보는 것도 형식 검증이 실무에 어디까지 쓰일 수 있는지 감을 잡는 좋은 방법이 될 것 같아요.
Deep Dive
What this model is actually built to do
Leanstral 1.5 is a code agent model built around Lean 4, a proof assistant — a tool that lets you express mathematical statements or software properties (say, “this function always satisfies this condition”) in a formal language and mechanically verify whether they’re true. Mistral calls this work “proof engineering,” and Leanstral is optimized for it, covering both automated theorem proving and autoformalization (translating natural-language statements into formal ones).
The architecture is a mixture-of-experts model activating 4 of 128 experts per token. Total parameters sit at 119B, with active parameters reported as roughly 6B (per the Hugging Face model name) to 6.5B (per the official description) depending on the source. The context window is 256,000 tokens — enough room for long proof chains.
How it was trained
Training ran through three stages: mid-training to build foundational capability, then supervised fine-tuning (SFT) to develop actual Lean 4 proof-writing skill, and finally CISPO-based reinforcement learning across two environments — a multi-turn theorem proving/refutation environment, and a code agent environment where the model could edit files, run bash commands, and use the Lean language server directly. Proof-writing wasn’t trained as an abstract exercise; it was trained using actual development tooling.
What saturating miniF2F actually means
miniF2F is a cross-system benchmark for formal mathematics spanning elementary problems up to IMO-level challenges, testing proof ability across algebra, combinatorics, and number theory. Leanstral 1.5 reportedly saturates it, hitting 100% on both the validation and test sets. The exact prior state-of-the-art score isn’t specified in available materials, but the word “saturate” itself signals this benchmark can no longer meaningfully distinguish between models’ proof ability.
Other reported numbers: 587 of 672 problems (about 87%) on PutnamBench; state-of-the-art scores of 87% on FATE-H and 34% on FATE-X; and on FLTEval, Pass@1 of 28.9% (up from 21.9%) and Pass@8 of 43.2% (up from 31.9%) — with Opus 4.6’s FLTEval Pass@1 cited at 39.6% for comparison.
Bugs found in real code
The most practically interesting part of this release sits outside the benchmarks entirely. Across 57 tested repositories, the model flagged 47 violated properties, 11 of which turned out to be genuine bugs — 5 of them previously unreported on GitHub. One case is described in detail: a sign function for zigzag decoding in datrs/varinteger, where feeding in Std.U64.MAX triggers an overflow in a (value + 1) operation — crashing in debug mode, but silently corrupting data in release mode. The other four bugs aren’t named or detailed in available materials.
A separate case involves proving, not finding a bug: Leanstral proved complete time-complexity guarantees for a real AVL tree (self-balancing binary search tree) implementation, confirming that insertion and deletion are O(log n). That required structural induction mirroring the tree’s recursive structure, careful monadic time tracking, and exhaustive case analysis across rebalancing paths — reportedly taking over 2.7 million tokens and 22 compactions to produce a complete, verified proof.
What’s public
Weights are open under Apache 2.0 and available on Hugging Face (mistralai/Leanstral-1.5-119B-A6B), with a free API also offered — recommended for use inside Mistral’s coding environment, Mistral Vibe.
Why It Matters
Formal verification has long carried a reputation as theoretically airtight but too slow and specialized for practical use — writing proofs by hand takes real expertise and real time. What makes this release notable is that it doesn’t stop at a benchmark-saturation headline; it pairs that with concrete evidence of finding bugs nobody knew existed in real open-source code. That’s formal verification AI proving its usefulness outside the lab.
It’s also a signal for how code quality assurance might change. Instead of checking a handful of test cases, there’s a real path toward mathematically proving that a function’s properties hold under every possible condition.
Key Insight
What this release shows is that a perfect benchmark score and real-world usefulness don’t always travel together — but this time, they came from the same underlying capability. The exact proof-writing skill that saturated miniF2F was the same skill that surfaced hidden defects in real code.
The capability that saturated a proof benchmark at 100% was the same capability that found five bugs nobody knew existed in production code.
That also hints at where formal-verification AI goes next — past one-off benchmark competitions, toward becoming a standing tool inside CI pipelines or code review, automatically catching property violations as they’re introduced.
My Take
The bug-hunting result landed harder for me than the benchmark score. A 100% saturation number is genuinely hard to feel in your gut, but “five real bugs nobody had reported on GitHub” is immediately legible. When judging an AI model’s real capability, checking for concrete applied results like this is more useful than scanning a leaderboard first.
Formal verification still has a real barrier to entry — defining properties in Lean 4 and setting up what to prove takes noticeably more effort than writing a standard unit test. But with open weights and a free API, a reasonable way to build intuition for how far this actually reaches in practice is picking one core function from a library you use often and trying property verification on it with Leanstral.