AI 코딩 도구의 가장 큰 한계는 “그럴듯한 코드”와 “검증된 코드”가 다르다는 점입니다. Mistral AI가 공개한 Leanstral 1.5는 이 문제를 정면으로 다루는 Lean 4용 코드 에이전트 모델입니다.1 핵심은 더 빠른 코드 생성이 아니라, 수학 정리 증명과 코드 검증처럼 맞고 틀림을 엄밀하게 확인해야 하는 작업을 돕는 데 있습니다.
Leanstral 1.5는 무엇을 위한 모델인가
Lean 4는 수학 명제나 소프트웨어의 성질을 컴퓨터가 검증할 수 있는 형식으로 표현하는 도구입니다. 자연어로는 “명백하다”고 넘길 수 있는 부분도 Lean에서는 정의, 정리, 증명 단계로 정확히 적어야 합니다.
Leanstral 1.5의 최적화 대상은 자동 정리 증명과 자동 형식화입니다.2 자동 정리 증명은 Lean 안에서 증명 과정을 구성하는 일이고, 자동 형식화는 자연어 설명이나 명세를 Lean이 이해할 수 있는 정의와 정리로 바꾸는 작업입니다. 즉 Leanstral 1.5는 일반적인 코딩 보조 모델이라기보다, 형식 검증 환경에서 “증명 가능한 결과물”을 만드는 데 초점을 둔 모델로 보는 편이 정확합니다.
숫자가 보여주는 것은 벤치마크보다 작업 방식이다
Leanstral 1.5는 119B 규모의 mixture-of-experts 모델이며, 토큰당 6.5B 파라미터를 활성화합니다.2 전체 모델은 크지만 매 토큰마다 일부 전문가만 사용하는 구조입니다. 이 점은 긴 증명과 반복적인 수정 작업을 전제로 한 설계로 이해할 수 있습니다.
특히 컨텍스트 길이 256k 토큰은 중요합니다.2 Lean 작업에서는 단일 프롬프트로 답을 내는 것보다, 기존 증명 파일과 관련 라이브러리, 컴파일 오류, 이전 시도까지 함께 참고하며 고쳐 나가는 경우가 많습니다. 긴 문맥을 처리할 수 있다는 것은 단순히 많은 텍스트를 넣을 수 있다는 뜻이 아니라, 실제 Lean 프로젝트의 검증 루프에 더 가깝게 모델을 사용할 수 있다는 의미입니다.
Mistral은 Leanstral 1.5가 PutnamBench 672문제 중 587문제를 해결했다고 밝혔습니다.1 이 수치는 모델의 성능을 보여주는 지표이지만, 더 중요한 메시지는 형식 증명 영역에서도 전용 모델이 실용적인 수준으로 발전하고 있다는 점입니다.
사용 관점에서 봐야 할 포인트
Leanstral 1.5는 Apache-2.0 라이선스로 제공됩니다.1 문서상 Labs v1.5 모델로 표시되며, 제공 식별자는 labs-leanstral-1-5입니다.3 가격 항목은 $0로 표시되어 있습니다.3
API 사용 측면에서는 Chat Completions의 /v1/chat/completions 엔드포인트와 함께 사용할 수 있습니다.3 Function Calling은 /v1/chat/completions와 /v1/conversations를 지원하고, Agents & Conversations 기능은 /v1/agents와 /v1/conversations를 지원합니다.3
이 구성은 Leanstral 1.5를 단순 질의응답 모델로만 보기 어렵게 만듭니다. 실제 가치는 Lean 파일을 수정하고, 검증 결과나 오류 로그를 다시 받아, 다음 증명 시도를 이어가는 반복 작업에서 나옵니다. Lean 프로젝트 안에서 에이전트처럼 움직이며 형식 검증 루프를 보조하는 모델에 가깝습니다.
왜 중요한가
Leanstral 1.5의 의미는 “수학 문제를 많이 풀었다”에 그치지 않습니다. AI 코딩의 평가 기준이 코드 생성 속도에서 검증 가능한 정확성으로 이동하고 있음을 보여줍니다.
일반적인 소프트웨어 개발에서도 앞으로 중요한 질문은 “AI가 코드를 얼마나 빨리 쓰는가”보다 “그 코드가 어떤 방식으로 맞다는 것을 확인할 수 있는가”가 될 가능성이 큽니다. Leanstral 1.5는 그 방향을 Lean 4와 형식 증명이라는 구체적인 환경에서 보여주는 모델입니다.
1Leanstral 1.5: Proof Abundance for All
이 노트는 보도·비평·교육·연구 목적으로 작성되었습니다. 저작권 문의가 있으시면 에서 알려주세요.