미스트랄, Lean 증명 특화 모델 ‘Leanstral 1.5’ 공개

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로 올라감

학습 방식은 ‘컴파일러 피드백 받는 증명 에이전트’에 가까움

• 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에 보고되지 않은 버그였음

---

기술 맥락

• Leanstral 1.5의 선택은 일반 코딩 모델을 억지로 증명에 쓰는 게 아니라, Lean 컴파일러 피드백을 학습 루프 안에 넣는 방식이에요. 증명은 자연어 답변처럼 그럴듯하면 되는 게 아니라 컴파일되어야 하니까, 실패 신호가 아주 명확하거든요.

• 멀티턴 증명 환경과 코드 에이전트 환경을 같이 쓴 이유도 여기에 있어요. 짧은 정리만 푸는 모델은 벤치마크에는 좋아 보여도 실제 저장소에서는 파일 구조, 보조 정리, 타입 오류, 기존 코드 스타일을 다뤄야 하거든요.

• 비용 비교가 중요한 이유는 형식 검증이 원래 비싼 작업이기 때문이에요. PutnamBench에서 문제당 약 4달러 수준으로 높은 성능을 냈다는 주장은, 증명 자동화가 연구 데모를 넘어 실무 파이프라인에 들어갈 가능성을 보여줘요.

• Rust 버그 탐지 사례는 특히 개발자에게 와닿아요. 테스트와 퍼징이 놓칠 수 있는 오버플로우·엣지 케이스를, 코드에서 속성을 만들고 증명 실패를 추적하는 방식으로 찾았기 때문이에요.