--- title: "미스트랄, Lean 증명 특화 모델 ‘Leanstral 1.5’ 공개" published: 2026-07-03T22:33:10.000Z canonical: https://jeff.news/article/4627 --- # 미스트랄, Lean 증명 특화 모델 ‘Leanstral 1.5’ 공개 미스트랄이 Lean 4 기반 증명·검증 작업에 특화된 Leanstral 1.5를 공개했다. 119B 전체 파라미터 중 6B만 활성화되는 구조로, miniF2F 100%, PutnamBench 587/672, FATE-H 87%, FATE-X 34% 같은 성적을 냈다. ## Lean 증명 특화 모델이 성능을 꽤 세게 끌어올림 - 미스트랄이 Lean 4 증명 엔지니어링용 모델 Leanstral 1.5를 공개함 - 라이선스는 Apache-2.0이고, 가중치는 Hugging Face에서 받을 수 있음 - 무료 API 엔드포인트 이름은 leanstral-1-5임 - 모델 크기는 전체 119B 파라미터지만 실제 활성 파라미터는 6B라고 밝힘 - 벤치마크 숫자가 꽤 공격적임 - miniF2F 검증·테스트 세트를 모두 100%로 포화시켰다고 함 - PutnamBench 672문제 중 587개를 풀었음 - FATE-H는 87%, FATE-X는 34%로 새 최고 성능을 냈다고 주장함 - FLTEval pass@1은 21.9에서 28.9로, pass@8은 31.9에서 43.2로 올라감 > [!IMPORTANT] > PutnamBench에서 Seed-Prover 1.5 high보다 7문제를 더 풀면서도 문제당 비용은 약 4달러라고 밝힘. Seed-Prover high는 문제당 10 H20-days 예산을 쓰는 설정이라, 추정 비용이 300달러 이상으로 언급됨. ## 학습 방식은 ‘컴파일러 피드백 받는 증명 에이전트’에 가까움 - Leanstral 1.5는 세 단계로 학습됨 - 미드 트레이닝, 지도 미세조정, CISPO 기반 강화학습을 거침 - 강화학습 환경은 크게 멀티턴 증명 환경과 코드 에이전트 환경으로 나뉨 - 멀티턴 환경에서는 모델이 정리를 증명하거나 반례를 찾아야 함 - 증명을 제출하면 Lean 컴파일러가 피드백을 줌 - 컴파일되면 성공이고, 실패하면 남은 예산 안에서 다시 고침 - 사람이 Lean으로 증명할 때 겪는 “오류 보고 고치기” 루프를 모델 학습에 직접 넣은 셈임 - 코드 에이전트 환경은 더 개발자스럽게 굴러감 - 모델이 실제 파일시스템에서 파일을 수정하고 bash 명령을 실행함 - Lean language server로 목표, 오류, 타입 정보를 확인함 - 부분 증명을 완성하거나 보조 정리를 만들고, 컨텍스트 압축을 여러 번 겪는 긴 작업까지 학습함 ## 테스트 타임 스케일링이 핵심 포인트임 - 토큰 예산을 늘릴수록 PutnamBench 성능이 부드럽게 올라갔다고 함 - 시도당 50k 토큰에서는 44문제 해결 - 200k 토큰에서는 244문제 해결 - 1M 토큰에서는 493문제 해결 - 4M 토큰에서는 587문제 해결 - 이게 중요한 이유는 모델이 긴 증명에서 쉽게 포기하지 않았다는 점임 - 증명이 길어져도 계속 추론하고 파일을 수정하고 다시 시도함 - AVL 트리 증명 사례는 270만 토큰 이상과 22번의 컨텍스트 압축을 거쳤다고 함 ## 실제 코드 검증에서도 버그를 잡았다고 함 - AVL 트리 구현의 시간 복잡도 보장을 증명한 사례가 나옴 - 삽입과 삭제가 O(log n)임을 완전한 검증 증명으로 연결함 - 삽입에 대해 높이 단위당 48스텝에 가까운 상한과 상수를 세움 - 트리 높이와 크기의 로그 관계까지 연결해 시간 복잡도를 닫음 - Rust 코드 버그 탐지 파이프라인도 흥미로움 - Aeneas가 Rust 코드를 Lean으로 변환함 - Leanstral이 코드 의도를 추론하고 정확성 속성을 생성함 - 각 속성을 네 번 증명해보고, 모두 실패하면 반대 명제를 네 번 증명해봄 - 57개 저장소에서 47개 위반 속성을 표시했고, 11개가 진짜 버그였으며 5개는 이전에 GitHub에 보고되지 않은 버그였음 > [!NOTE] > 예시로 나온 버그는 datrs/varinteger의 zigzag decoding sign 함수였음. Std.U64.MAX 입력에서 value + 1이 오버플로우해 디버그 모드에서는 크래시, 릴리스 모드에서는 조용한 데이터 손상을 만들 수 있었다고 함. --- ## 기술 맥락 - Leanstral 1.5의 선택은 일반 코딩 모델을 억지로 증명에 쓰는 게 아니라, Lean 컴파일러 피드백을 학습 루프 안에 넣는 방식이에요. 증명은 자연어 답변처럼 그럴듯하면 되는 게 아니라 컴파일되어야 하니까, 실패 신호가 아주 명확하거든요. - 멀티턴 증명 환경과 코드 에이전트 환경을 같이 쓴 이유도 여기에 있어요. 짧은 정리만 푸는 모델은 벤치마크에는 좋아 보여도 실제 저장소에서는 파일 구조, 보조 정리, 타입 오류, 기존 코드 스타일을 다뤄야 하거든요. - 비용 비교가 중요한 이유는 형식 검증이 원래 비싼 작업이기 때문이에요. PutnamBench에서 문제당 약 4달러 수준으로 높은 성능을 냈다는 주장은, 증명 자동화가 연구 데모를 넘어 실무 파이프라인에 들어갈 가능성을 보여줘요. - Rust 버그 탐지 사례는 특히 개발자에게 와닿아요. 테스트와 퍼징이 놓칠 수 있는 오버플로우·엣지 케이스를, 코드에서 속성을 만들고 증명 실패를 추적하는 방식으로 찾았기 때문이에요. ## 핵심 포인트 - Leanstral 1.5는 Apache-2.0 라이선스의 무료 모델이며 Hugging Face 가중치와 무료 API 엔드포인트로 제공됨 - 멀티턴 증명 환경과 코드 에이전트 환경에서 Lean 컴파일러 피드백을 받으며 증명을 반복하도록 학습됨 - 57개 오픈소스 저장소를 대상으로 47개 위반 속성을 찾았고, 그중 11개는 실제 버그였으며 5개는 GitHub에 보고되지 않았던 버그였음 ## 인사이트 LLM이 코드를 ‘그럴듯하게’ 쓰는 단계를 넘어, 형식 검증 도구와 붙어서 실제 버그를 찾는 방향으로 가고 있다는 신호가 꽤 강함. 아직 비용과 토큰 예산이 크지만, 검증 가능한 소프트웨어 개발 쪽에서는 무시하기 어려운 흐름임.