AI 코딩 도구의 경쟁 축이 바뀌고 있습니다. 이제 핵심 질문은 “코드를 얼마나 잘 생성하나”를 넘어 “그 코드가 정말 맞다는 근거를 만들 수 있나”로 이동하고 있습니다. Mistral AI가 공개한 Leanstral 1.5는 바로 이 지점, 즉 Lean 4 기반 형식 검증과 증명 자동화에 초점을 맞춘 오픈소스 모델입니다.
Leanstral 1.5는 무엇인가
Leanstral 1.5는 Lean 4를 위한 형식 증명 엔지니어링 모델입니다. Lean 4는 수학 정리와 증명을 컴퓨터가 검증할 수 있도록 표현하는 증명 보조 시스템이며, 수학 증명을 위해 개발된 프로그래밍 언어 Lean을 활용합니다.
따라서 Leanstral 1.5는 일반 챗봇처럼 넓은 대화를 처리하기보다, 정리 증명, 자동 형식화, 코드 속성 검증 같은 좁고 까다로운 작업에 맞춰진 모델입니다.1 쉽게 말해 “그럴듯한 답”을 내는 AI가 아니라, 검증 가능한 증명과 코드의 성질을 다루는 AI에 가깝습니다.
아키텍처도 이 목적에 맞춰 설계됐습니다. Leanstral 1.5는 전문가 혼합, 즉 MoE 구조를 사용합니다. 전체 매개변수는 119B이지만 입력 토큰마다 128개 전문가 중 4개만 활성화합니다. Mistral은 약 6B 활성 매개변수를 제시했고, TestingCatalog은 Mistral 문서 기준 6.5B 활성 매개변수로 설명했습니다.12 큰 모델의 지식을 활용하면서도 매번 전체 모델을 쓰지 않는 방식입니다.
왜 중요한가: 성능보다 접근성
Mistral에 따르면 Leanstral 1.5는 miniF2F 벤치마크에서 100%를 기록했고, PutnamBench에서는 672개 문제 중 587개를 풀었습니다.2 수학 증명 벤치마크 기준으로 강한 성능을 보인 셈입니다.
하지만 이 모델의 더 큰 의미는 점수만이 아닙니다. Leanstral 1.5는 Apache 2.0 라이선스의 무료 오픈소스 모델이며, Hugging Face와 무료 API를 통해 제공됩니다.23 형식 검증과 증명 자동화가 일부 연구실이나 대형 조직만의 실험이 아니라, 더 많은 개발자와 연구자가 직접 다뤄볼 수 있는 영역으로 내려왔다는 점이 중요합니다.
또 하나의 실용적 특징은 긴 컨텍스트입니다. Leanstral 1.5는 최대 256k 토큰 컨텍스트 윈도를 지원하고, 텍스트와 이미지 입력을 받을 수 있으며 출력은 텍스트로 제공합니다.3 긴 증명 파일, 복잡한 라이브러리, 여러 파일에 걸친 코드 속성을 다뤄야 하는 증명 엔지니어링에서는 이 조건이 실제 사용성을 좌우할 수 있습니다.
형식 검증은 테스트와 무엇이 다른가
Leanstral 1.5를 이해하려면 “AI가 코드를 대신 써준다”는 관점에서 한 걸음 벗어나야 합니다. 이 모델의 핵심은 코드 생성보다 코드의 성질을 증명하는 데 있습니다.
테스트는 특정 입력을 넣고 기대한 출력이 나오는지 확인합니다. 반면 형식 검증은 코드가 만족해야 할 조건을 논리적으로 증명하려고 합니다. 예를 들어 특정 함수가 항상 경계 조건을 지키는지, 오버플로가 발생하지 않는지, 어떤 불변 조건이 유지되는지를 증명 대상으로 삼을 수 있습니다.
Mistral은 Rust 코드를 Lean으로 변환하는 파이프라인에서 57개 저장소를 시험했고, 11개 실제 버그를 찾았으며 그중 5개는 이전에 보고되지 않았다고 밝혔습니다.2 이는 Leanstral 1.5가 단순한 수학 문제 풀이 모델을 넘어, 코드 검증 워크플로에도 연결될 수 있음을 보여줍니다.
물론 즉시 모든 코드베이스에 적용할 수 있다는 뜻은 아닙니다. 실제 사용에는 언어 변환, 검증할 속성 정의, 기존 코드와의 통합, 오탐 처리 같은 장벽이 남아 있습니다. 그럼에도 방향은 분명합니다. AI 개발 도구는 점점 “코드를 생성하는 도구”에서 “코드가 맞다는 근거를 만드는 도구”로 확장되고 있습니다.
어떻게 바라봐야 하나
Leanstral 1.5를 당장 일반 개발자의 일상 코딩 도구로 보기에는 이릅니다. Lean 4와 형식 검증 자체가 아직 진입 장벽이 있는 영역이기 때문입니다. 그러나 고신뢰 시스템을 다루는 팀에게는 관찰할 가치가 큽니다.
특히 암호 라이브러리, 금융 시스템, 인프라 소프트웨어, 안전성이 중요한 코드처럼 “대부분 맞다”가 아니라 “틀리면 안 된다”에 가까운 영역에서는 형식 검증의 가치가 큽니다. Leanstral 1.5는 이런 작업을 더 저렴하고 공개된 방식으로 실험할 수 있게 만든 모델입니다.
결론
Leanstral 1.5의 의미는 벤치마크 성과에만 있지 않습니다. 핵심은 Lean 4 기반 형식 검증 모델을 오픈소스로 공개하고, Hugging Face와 무료 API를 통해 접근 가능하게 만들었다는 점입니다.
AI가 코드를 더 많이, 더 빠르게 쓰는 시대에는 그 코드가 맞다는 근거를 어떻게 확보할지가 더 중요해집니다. Leanstral 1.5는 그 질문에 대한 현재의 중요한 시도입니다. 앞으로의 AI 개발 도구 경쟁은 코드 작성 능력뿐 아니라, 코드의 정확성을 증명하고 검증 가능한 신뢰를 제공하는 능력에서 갈릴 수 있습니다.
1Mistral releases Leanstral 1.5 open model for proof engineering
이 노트는 보도·비평·교육·연구 목적으로 작성되었습니다. 저작권 문의가 있으시면 에서 알려주세요.