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

 (mistral.ai)
1P by GN⁺ | ★ favorite | 댓글 1개
  • 형식 검증을 실제 개발 작업에 더 가깝게 쓰려는 흐름 속에서, 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은 정리 해결, 증명 디버깅, 저장소 기여 작업에 사용할 수 있음

함께 보면 좋은 글 β

GN⁺   [-]
Hacker News 의견들

  • Mistral이 대형 모델과 경쟁하기 어렵다는 비판은 타당하지만, 실제로는 작은 모델에서 특정 기능을 고품질로 제공하는 데 집중하고 있다고 봄
    OCR이나 파일 분석 같은 작업에 Mistral을 쓰는데, 계정에 100달러를 넣어두면 요청량 걱정 없이 1년은 돌아감
    비용이 극히 작아서, Opus 4.8과 경쟁하지 못하더라도 충분히 가치가 있음

    • OCR에서는 실제로 얼마나 경쟁력이 있는지 궁금함
      저렴한 가격에 괜찮은 품질은, 나중에 실수를 줄이기 위해 10배 가격을 내고 최고 품질을 쓰는 것보다 더 틈새시장처럼 보임
    • 유럽 바보들은 돈을 최대한 버는 최적화가 아니라 좋은 제품을 만드는 최적화를 하고 있네 /s
    • “연 100달러 이하로 1년치 문서 처리”가 생각만큼 훌륭한지는 잘 모르겠음. 적어도 유럽 경쟁력 관점에서는 Mistral이 매출 상한을 너무 낮게 잡는 셈임
      OCR은 이미 범용재에 가깝고, 오픈소스 모델이나 AWS 같은 곳에서도 기본으로 제공함
      게다가 연 100달러 가격표로는 충성도를 만들기 어렵고, 전환 비용도 없어서 더 낮은 가격이 나오면 고객은 바로 떠날 수 있음
      쉽게 복제되는 저가 도구에 고객 락인이 없다면 사업이라기보다 기능에 가까움
      구매자 입장에서는 좋겠지만, 유럽 기업이 장기적으로 세계 경쟁사와 제품 역량으로 경쟁하길 원한다면 나쁜 전략으로 보임

  • 작업 자체는 좋지만, 버그 발견 예시가 이상하게 느껴졌음
    zigzag 디코딩의 sign 함수에서 Std.U64.MAX 입력 시 (value + 1)이 오버플로되어 디버그 모드에서는 크래시, 릴리스 모드에서는 조용한 손상이 난다고 했는데, 이걸 테스트가 “보통 놓치는” 경계 조건이라고 부를 수 있는지 모르겠음
    나쁜 테스트라면 놓치겠지만, 신중한 사람이나 기계학습 기반 코딩 시스템은 “극단값을 테스트해야겠다”를 꽤 잘함. 특히 사용자 입력을 파싱하는 코드라면 더 그렇다
    더 흥미로운 버그도 찾았지만 빠르게 설명하기 어려워서 이 예시를 든 건지 궁금함

    • 특히 “퍼징도 놓친다”는 부분이 이상함. 내가 본 퍼징은 일반적으로 경계값을 의도적으로 탐색함
      이런 인코딩 라이브러리라면 괜찮은 코드의 기본 기대치가 퍼징이고, 거의 확실히 몇 초 안에 잡혔을 것 같음
      실제로 proptest로 아주 간단한 왕복 테스트를 만들었더니 1초도 안 돼 수십 개 실패와 아래 결과가 나왔음:
      thread 'signed_round_trip' (50528) panicked at tests/test.rs:72:1:
      Test failed: attempt to multiply with overflow.
      minimal failing input: value = 4611686018427387904
      successes: 2
      local rejects: 0
      global rejects: 0
    • “보통 놓친다”고 하긴 어렵겠지만, 실제로 존재했으니 가끔은 놓치는 버그이긴 함
      Lean을 쓰면 어떤 예시를 테스트해야 할지 영리하게 고를 필요가 줄어든다는 장점은 드러남
    • 이건 기본적인 품질 보증임. 테스트가 이런 걸 놓친다면 우리가 보통 기대하는 것보다 훨씬 쓸모가 제한적일 것임
      저자들의 배경이 궁금해짐
    • 이건 그냥 쓰레기 홍보임
      1980년쯤 발명된 모든 속성 기반 테스트 시스템은 경계값을 탐색함
      C와 C++의 의미론, 또는 그 부재 때문에 실제 테스트가 어려울 수는 있음. 컴파일러가 정의되지 않은 동작으로 이어지는 모든 입력에 대해 “테스트 통과”라고 해도 허용되기 때문임

  • 글 중간에 여러 최전선급 LLM과 비교가 나오는데, 전부 반년 전 모델들임
    “우리 새 모델이 3세대 전 중국 모델들보다 낫다”는 식이라 꽤 웃겼음

    • 이건 60억 매개변수 모델이라 완전히 다른 급임. 오히려 “최전선급 소형 언어 모델”이 더 기대됨
    • 동의하지만, 오픈 가중치이고 비교적 작다는 것만으로도 헤드라인감임. 이 모델은 꽤 잘 돌아감

  • 그 라이브러리는 https://github.com/datrs/varinteger임
    논문이 공개되기 일주일 전에 같은 문제가 이미 이 저장소에 올라와 있어서 아마 맞는 것 같음: https://github.com/datrs/varinteger/issues/8
    이 사람이 Leanstral 직원인지, 아니면 Leanstral이 이 이슈를 그냥 가져온 건지는 모르겠음
    이 라이브러리는 작고, 테스트가 놀랄 만큼 부실하며, 8년 동안 거의 손대지 않은 상태임: https://github.com/datrs/varinteger/blob/master/tests/test.r...
    다운로드는 하루 약 1천 건 정도라 낮은 편으로 보임: https://crates.io/crates/varinteger
    그래서 유일한 예시로 내세울 만큼 대단한 성공이라고 보기는 어려움. 자동 탐지가 유용한 건 맞지만, 이 하위 분야에서는 주목할 만한 성과인지 잘 모르겠음
    증명 작성 LLM은 써본 적 없지만, 학습 데이터가 부족한 편이라 일반 코딩 모델보다 거칠어도 놀랍지는 않음
    참고로 https://crates.io/crates/varinteger에는 https://github.com/mafintosh/varinteger-rs로 표시되지만, 이 주소가 https://github.com/datrs/varinteger로 리다이렉트되므로 겉보기와 달리 같은 라이브러리로 보임

    • 증명의 문제는 가치를 전달하기가 가끔 어렵다는 데 있음
      핵심은 버그를 찾는 게 아니라, 특정 종류의 버그가 특정 가정 아래 없다는 것을 증명하는 것임
      하지만 이 이야기는 팔기 어려워서 마케팅은 자주 “이 버그를 찾았다” 쪽으로 흘러감

  • Lean을 전혀 모르는 사람에게도 유용할 수 있을까? 작업 중인 소프트웨어를 검증하고 싶은데 형식 검증 경험이 없음
    명세, 코드, 그리고 제한된 학습 시간만으로도 쓸 만한 결과를 얻을 수 있을지 궁금함

    • 증명하려는 부분 자체는 이해해야 하지만, 전체 증명 과정을 다 이해할 필요는 없음
      수학이라기보다 Haskell 타입을 읽는 것에 더 가깝고, 어휘만 수학에서 많이 빌려온 느낌임
    • 글의 “Bug Discovery: Finding Hidden Flaws” 절을 읽어보면, Rust 코드만 가지고 시작해서 오픈소스 Rust에서 문제를 찾는 데 모델을 쓴 것으로 보임
      애플리케이션 검증을 위한 Lean 코드를 작성하도록 대화하며 도움받을 수도 있겠지만, 확실하진 않음
    • 최소한 코드에 대해 어떤 정리를 증명하고 싶은지, 그리고 그걸 Lean에서 어떻게 표현할지는 이해해야 함
      그렇지 않으면 출력을 검증할 수 없음
      기계적으로는 올바르다고 검사된 어떤 명제를 증명했을 수 있지만, 그 명제가 무슨 뜻인지, 실제로 검증하려는 내용을 포괄하는지 모르면 의미가 없음
    • Lean4를 전혀 모르는 상태에서 약 6개월 만에 대부분의 코딩을 Lean4로 하는 수준까지 왔고, 이 과정은 AI 보조 덕분에 크게 빨라졌음
      모델들이 Lean4에 얼마나 일관되게 유창한지 놀라울 정도임. 최전선급 모델뿐 아니라 작은 로컬 모델도 마찬가지였고, LLM이 Lean4를 그냥 잘 이해하는 것 같음
      아직 Lean4 전문가라고 부르기엔 갈 길이 남았지만, 이제 유용한 프로그램을 만드는 데 보조가 꼭 필요하진 않음
      지식이 거의 없는 상태에서도 완전히 이해하지 못한 부분을 신뢰할 수 있다는 점은 학습 속도를 크게 끌어올림. 불완전한 지식으로도 의존 가능한 프로그램을 얻는 게 실용적이고 동기부여도 됨
      중간 증명 단계 전체가 아니라, 자신의 공리와 명제 표면을 설명하는 언어 부분에 의해 한계가 정해지는 느낌임. 시간이 지나 더 많은 것을 하려면 더 많이 이해해야 하지만, 어떤 의미에서는 N+1 수준에서 안전하게 작업할 수 있음
      Lean4는 정리 증명 역할과 별개로도 즐거운 프로그래밍 언어이고, 속도도 놀랍게 빠름
      io_uring에 붙여서 쓰고 있는데, 많은 경우 C++/libuv나 Rust/Tokio보다 훨씬 빠름
      가끔 p99.99 지연 시간 같은 데서 큰 꼬리가 보이면 숫자를 고정 폭으로 바꾸는 식의 튜닝이 필요하지만, C++와 Rust도 튜닝은 해야 함

  • Lean 4를 형식 검증용으로 밀고 있는 점이 흥미로움
    이 영역은 Isabelle/HOL과 TLA+ 쪽이라고 생각했음
    적어도 세 가지 모두를 쓰도록 학습한 모델을 기대했을 것 같음. 선형대수의 전방향 유도에는 Isabelle/Isar도 더 나아 보이는데, 누가 설명해줄 수 있을까?

    • Lean은 Isabelle이나 예전 Coq인 Rocq에 비해 소프트웨어 검증에서 채택이 적었던 게 맞음
      이 분야에서는 Agda조차 더 많이 쓰인 편임
      다만 Lean은 현재 대안으로 상당한 추진력을 얻고 있고, 특히 범용 함수형 프로그래밍 언어로서의 능력이 큼
      개인적으로는 요구사항과 명세를 맞추기 쉬운 Hoare 논리나 분리 논리 기반 접근이 더 실용적이라고 봄. Dafny와 F*가 마음에 듦

  • Twitter 발표에서 개발자들이 Le Chaton Fat을 슬쩍 언급하는 게 재미있었음
    그들이 실제로 Le Chaton Fat에 관여했는지와 무관하게, 진짜 “새로운 대형 범용” 모델이 곧 나올 것 같음
    미디어 소동 이후에도 직접 언급했으니 기대됨. 이름은 “Large 4”보다 더 창의적이면 좋겠음

  • 최신 OpenATP에서 Leanstral 1.5를 써볼 수 있음
    OpenATP는 에이전트형 자동 정리 증명기를 위한 오픈소스 Python 패키지이자 CLI이며, Docker에서 로컬로 실행하거나 Modal 샌드박스에서 원격 실행하는 방식을 기본 지원함
    GitHub: https://github.com/henryrobbins/open-atp
    Docs: https://open-atp.henryrobbins.com

답변달기