Leanstral 1.5: 모두를 위한 증명 풍요

• 형식 검증을 실제 개발 작업에 더 가깝게 쓰려는 흐름 속에서, Mistral AI가 Lean 4용 Apache-2.0 모델 Leanstral 1.5를 공개함
• 모델은 119B 총 파라미터 중 6B만 활성화하며, 중간 학습·지도 미세조정·CISPO 강화학습을 거쳐 증명 작성과 코드 저장소 작업을 함께 학습함
• miniF2F 100%, PutnamBench 587/672, FATE-H 87%, FATE-X 34%를 기록해 수학 증명 벤치마크와 실제 증명 엔지니어링 평가에서 강한 성능을 보임
• 실제 코드 검증에서는 AVL 트리의 O(log n) 시간 복잡도 증명과 Rust-to-Lean 파이프라인을 통해 57개 저장소에서 11개 실제 버그를 찾아냄
• 가중치와 leanstral-1-5 무료 API가 공개되어, 정리 증명·증명 디버깅·저장소 기여 같은 실용적 증명 엔지니어링에 바로 적용 가능함

Leanstral 1.5의 공개와 모델 특성

• Leanstral 1.5는 Lean 4에서 증명 엔지니어링을 수행하도록 만든 모델임
• 라이선스는 Apache-2.0이며, 모델 규모는 총 119B 파라미터와 6B 활성 파라미터임
• 형식 검증 성능을 끌어올려 수학 벤치마크뿐 아니라 실제 코드 속성 검증에도 활용할 수 있음
• miniF2F를 포화하고, PutnamBench 672문제 중 587문제를 해결했으며, FATE-H 87%, FATE-X 34%를 달성함

증명 피드백을 학습한 3단계 훈련

• 학습은 중간 학습, 지도 미세조정, CISPO 기반 강화학습의 3단계로 구성됨
• 강화학습에는 두 가지 환경이 쓰임
  • 멀티턴 환경: 모델이 정리 명제를 받아 증명하거나 반증하고, Lean 컴파일러 피드백을 바탕으로 증명을 반복 수정함
  • 증명이 컴파일되면 성공하며, 그렇지 않으면 문제를 풀거나 예산을 소진할 때까지 루프가 이어짐
  • 코드 에이전트 환경: 원시 파일시스템에서 개발자처럼 파일을 편집하고, bash 명령을 실행하며, Lean language server로 목표·오류·타입 정보를 실시간 확인함
• 코드 에이전트 환경은 저장소 안의 부분 증명 완성, 보조정리 작성, 여러 차례의 컨텍스트 압축 이후에도 작업을 지속하는 긴 작업을 다룸
• 최종 정답성은 대상 정리 목록을 기준으로 Mistral의 SafeVerify 포크에서 검증됨

수학·증명 엔지니어링 벤치마크

• 평가에는 miniF2F, PutnamBench, FATE-H/FATE-X, FLTEval이 사용됨
  • miniF2F는 초등 문제부터 IMO 수준 문제까지 포함하는 형식 수학 벤치마크임
  • PutnamBench는 Putnam Mathematical Competition의 672개 문제로 구성됨
  • FATE-H와 FATE-X는 각각 대학원·박사 수준의 추상대수 벤치마크임
  • FLTEval은 Fermat’s Last Theorem 저장소의 실제 풀 리퀘스트를 기반으로 증명 엔지니어링 난도를 평가함
• miniF2F에서는 검증 세트와 테스트 세트 모두에서 100% 를 달성함
• PutnamBench와 FATE-H/X에서는 자연어 증명 가이드 없이 Goedel-Architect, Seed-Prover 1.5 high, AxProverBase와 비교됨
• FATE-H/X 성능: {b:87,34}
• FATE-H는 87%, FATE-X는 34% 로 새로운 최고 성능을 달성함
• PutnamBench에서는 Seed-Prover 1.5 high보다 7문제를 더 풀었고, 문제당 비용은 약 4달러 수준임
  • Seed-Prover의 high 설정은 문제당 10 H20-days 예산을 쓰며 비용이 300달러 이상으로 추정됨
  • 더 높은 순위의 일부 증명기는 자연어 증명 가이드를 받거나, Aleph Prover처럼 문제당 54~68달러가 드는 다른 조건에서 동작함

긴 추론 예산에서의 확장성과 FLTEval

• Leanstral 1.5는 PutnamBench에서 토큰 예산을 늘릴수록 Pass@8 성능이 부드럽고 단조롭게 상승함
• 시도당 토큰 예산을 25k에서 4M까지 높인 실험에서 해결 문제 수는 다음처럼 증가함
  • 50k 토큰: 44문제
  • 200k 토큰: 244문제
  • 1M 토큰: 493문제
  • 4M 토큰: 587문제
• 긴 증명에서 중단하지 않고 수백만 토큰에 걸쳐 추론·파일 편집·수정을 계속하는 동작이 성능 향상으로 이어짐
• FLTEval도 완전히 오픈소스로 공개됨
• FLTEval에서 Leanstral 1.5는 pass@1을 21.9에서 28.9로, pass@8을 31.9에서 43.2로 끌어올림
• pass@8 43.2는 Opus 4.6의 39.6을 넘는 수치이며, 비용은 7분의 1 수준임
• 오픈소스 모델 중 3~10배 큰 모델들보다도 앞선 성능을 보임

실제 코드 검증 사례

• AVL 트리 시간 복잡도 증명

  • AVL 트리는 삽입과 삭제 중 재균형을 통해 O(log n) 높이를 유지하는 자기 균형 이진 탐색 트리임
  • Leanstral 1.5는 실제 구현에 대해 삽입과 삭제가 O(log n)임을 검증함
  • 이 작업에는 트리 재귀 구조를 반영하는 구조적 귀납법, 모나드 기반 시간 추적 처리, 재균형 경로에 대한 전수 사례 분석이 필요했음
  • 증명은 270만 개 이상의 토큰과 22번의 컨텍스트 압축을 거쳐 진행됨
  • Leanstral은 TimeM 모나드의 각 계층을 체계적으로 펼쳐 제어 흐름과 섞인 계산을 드러냄
  • 삽입에 대해 높이 단위당 48스텝과 상수항에 가까운 경계를 세우고, 높이와 트리 크기를 로그 관계로 연결함

• Rust 코드에서 버그 찾기

  • 버그 탐지 실험은 Aeneas가 Rust 코드를 Lean으로 변환하고, Leanstral이 코드에서 사용자 의도를 추론해 정합성 속성을 생성하는 파이프라인으로 구성됨
  • Leanstral은 각 속성을 4번 시도해 증명하고, 모두 실패하면 그 부정을 다시 4번 시도해 증명함
  • 57개 저장소에서 47개 위반 속성이 표시됐고, 이 중 11개가 실제 버그를 가리킴
  • 실제 버그 중 5개는 GitHub에 이전에 보고되지 않았던 버그임
  • datrs/varinteger 라이브러리의 zigzag decoding sign 함수에서 한 사례가 발견됨
  • 입력이 Std.U64.MAX일 때 (value + 1) 표현식이 오버플로함
  • 디버그 모드에서는 크래시가 발생하고, 릴리스 모드에서는 조용한 데이터 손상이 발생함
  • 이 엣지 케이스는 일반적인 테스트와 퍼징이 놓치기 쉬운 사례임

배포와 사용 방법

• 가중치는 Hugging Face에 공개됨
• 무료 API 엔드포인트는 모델 카드에서 leanstral-1-5 이름으로 제공됨
• 사용 환경으로는 Mistral Vibe가 권장됨
• 시작 절차는 Mistral Vibe 설정, Leanstral 1.5 설치, 에이전트 실행, 선택적 Lean LSP MCP 설치, 증명 작업 시작 순서임
• Lean LSP MCP는 ~/.vibe/config.toml에 추가해 설치하는 방식이 권장됨
• 기존 MCP 서버가 없으면 mcp_servers = []를 제거해야 할 수 있음
• Leanstral은 정리 해결, 증명 디버깅, 저장소 기여 작업에 사용할 수 있음