배경 및 맥락
formal verification은 컴파일이나 테스트보다 강한 보증을 제공하지만, 실제 산업 현장에서는 Lean, Coq, Isabelle 같은 도구를 다룰 수 있는 전문가가 부족하고 proof 작성 비용이 높아 적용 범위가 제한됐다. 최근 AI coding agent가 파일 편집, 빌드, 테스트, 오류 수정 루프를 수행하기 시작하면서, theorem prover도 장기 agent workflow의 한 대상이 되고 있다.
Mistral의 Leanstral 1.5는 이 흐름을 formal mathematics에서 code verification으로 확장한 사례다. 기존 캐시에 있던 OlmoLogic이 Prolog verifier 기반 RLVR로 symbolic reasoning을 끌어올린 접근이었다면, Leanstral 1.5는 Lean 4 ecosystem과 실제 repository proof engineering을 직접 겨냥한다.
핵심 내용
Leanstral 1.5는 Apache-2.0 라이선스로 공개된 119B total, 6B active parameter 모델이다. Mistral은 mid-training, supervised fine-tuning, CISPO 기반 reinforcement learning을 거쳤고, multiturn theorem proving 환경과 code-agent 환경을 모두 사용했다고 설명한다.
평가에서는 miniF2F validation/test를 100%로 포화했고, PutnamBench 672문제 중 587문제를 해결했다. FATE-H는 87%, FATE-X는 34%를 기록했으며, PutnamBench에서 4M token budget까지 올릴수록 성능이 단조 증가하는 강한 test-time scaling을 보였다. FLTEval pass@8은 43.2로, Mistral은 Opus 4.6의 39.6보다 높고 비용은 약 1/7이라고 주장한다.
코드 검증 사례도 중요하다. Mistral은 Aeneas로 Rust 코드를 Lean으로 변환하고, Leanstral이 correctness property를 추론한 뒤 증명 또는 반례 증명을 시도하는 파이프라인을 테스트했다. 57개 저장소에서 47개 violated property를 표시했고, 이 중 11개가 실제 버그였으며 5개는 GitHub에 미보고된 버그였다고 밝혔다.
경쟁 구도 / 비교
일반 coding benchmark는 agent가 코드를 작성하고 테스트를 통과하는지 본다. Leanstral 1.5는 한 단계 더 강한 조건인 formal property proof를 목표로 한다. 이는 fuzzing이나 unit test가 놓치기 쉬운 정수 overflow, 불변식 위반, 경계 조건을 잡는 데 유리하다.
동시에 formal verifier 기반 AI는 범용 assistant와 다르게 운영해야 한다. property가 잘못되면 잘못된 목표를 증명할 수 있고, proof가 실패했다고 코드가 틀렸다는 뜻도 아니다. 따라서 GitHub Copilot이나 Claude Code 같은 범용 coding agent와 경쟁한다기보다, 안전성과 정확성이 중요한 코드 영역에서 보조 검증 레이어로 자리 잡을 가능성이 높다.
의미
AI가 개발 생산성 도구에서 correctness 도구로 확장되는 흐름이 뚜렷해지고 있다. 특히 open-weight 모델이 특정 verifier와 결합해 좁지만 강한 능력을 확보하면, 엔터프라이즈는 frontier closed model만 기다리지 않고 domain-specific 검증 에이전트를 자체 워크플로에 붙일 수 있다.
실무적으로는 전체 코드베이스 formal verification을 바로 목표로 삼기보다, 핵심 자료구조, parser, serialization, crypto-adjacent utility, payment calculation처럼 invariant가 명확한 영역부터 시작하는 것이 맞다. CI에는 proof 결과를 blocking gate로 두기보다 reviewer attention signal로 먼저 도입하고, 사람이 확인한 property만 점진적으로 강화하는 운영 모델이 필요하다.