▲

Leanstral: 신뢰할 수 있는 코드 및 형식 증명 엔지니어링을 위한 오픈소스 에이전트

 (mistral.ai)
1P by GN⁺ 13시간전 | ★ favorite | 댓글 1개
  • Lean 4용으로 설계된 최초의 오픈소스 코드 에이전트로, 형식 증명(formal proof) 을 자동화해 인간 검증 부담을 줄이는 것을 목표로 함
  • Apache 2.0 라이선스로 모델 가중치를 공개하고, Mistral Vibe 환경과 무료 API 엔드포인트를 통해 즉시 사용 가능
  • 6B 활성 파라미터의 희소 아키텍처를 사용해 효율성과 비용 절감을 달성하며, lean-lsp-mcp와 같은 MCP 통합을 지원
  • FLTEval 벤치마크에서 Qwen3.5, GLM5, Kimi-K2.5 등 대형 오픈소스 모델보다 높은 점수를 기록하고, Claude Sonnet 대비 15배 이상 저렴한 비용으로 유사 성능을 보임
  • 형식 증명 자동화와 코드 신뢰성 향상을 결합한 새로운 접근으로, 연구 수학과 미션 크리티컬 소프트웨어 개발 모두에 활용 가능성 제시

Leanstral 개요

  • Leanstral은 Lean 4를 위한 최초의 오픈소스 코드 에이전트로, 형식 증명 보조기(proof assistant) 환경에서 작동
    • Lean 4는 복잡한 수학적 객체(예: perfectoid 공간)와 소프트웨어 명세를 표현할 수 있음
    • 기존 증명 시스템이 일반 모델 래퍼나 단일 문제에 집중하는 것과 달리, Leanstral은 현실적 형식 저장소(formal repositories) 에서 효율적으로 작동하도록 훈련됨
  • 6B 활성 파라미터를 가진 희소(sparse) 아키텍처를 채택해, 병렬 추론(parallel inference) 과 Lean의 검증 기능을 결합
  • MCP 통합 지원을 통해 lean-lsp-mcp와 같은 자주 사용되는 프로토콜과 호환

공개 및 접근성

  • Apache 2.0 라이선스로 모델 가중치를 공개하고, Mistral Vibe 내 에이전트 모드로 제공
  • 무료 API 엔드포인트(labs-leanstral-2603) 를 통해 누구나 접근 가능하며, 사용자 피드백을 수집해 차기 모델 개선에 활용 예정
  • 기술 보고서와 평가 도구 FLTEval을 함께 공개해, 기존 수학 중심 평가를 넘어 실제 증명 엔지니어링 성능을 측정

성능 평가 (Evaluation)

  • FLT 프로젝트의 Pull Request 단위로 모든 형식 증명 및 새로운 수학 개념 정의를 완료하는 능력을 기준으로 평가
  • 비교 대상: Claude Opus 4.6, Sonnet 4.6, Haiku 4.5, Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B, GLM5 744B-A40B

Leanstral vs. 오픈소스 모델

  • Leanstral-120B-A6B는 GLM5(16.6점), Kimi-K2.5(20.1점)보다 높은 26.3점(pass@2) 을 기록
  • Qwen3.5가 4회 실행(pass@4)에서 25.4점을 얻은 반면, Leanstral은 절반의 실행으로 더 높은 점수 달성
  • 동일 비용 수준에서 29.3점(pass@4) 까지 선형적으로 확장

Leanstral vs. Claude 제품군

  • Sonnet 대비 2.6점 우위(26.3점 vs 23.7점) 를 보이며, 실행 비용은 $36 vs $549로 15배 이상 저렴
  • pass@16 기준으로 31.9점을 기록해 Sonnet보다 8점 높음
  • 최고 성능의 Claude Opus 4.6은 39.6점을 기록했으나, 비용이 $1,650으로 Leanstral 대비 92배 높음
  • 모든 벤치마크는 Mistral Vibe 환경에서 수정 없이 수행
모델 비용($) 점수
Haiku 184 23.0
Sonnet 549 23.7
Opus 1,650 39.6
Leanstral 18 21.9
Leanstral pass@2 36 26.3
Leanstral pass@4 72 29.3
Leanstral pass@8 145 31.0
Leanstral pass@16 290 31.9

사례 연구 (Case Studies)

Lean 버전 변경 대응

  • Lean 4.29.0-rc6에서 발생한 타입 별칭 관련 오류를 다룬 StackExchange 질문을 입력
  • Leanstral은 문제 환경을 재현하고, 정의적 동등성(definitional equality) 문제를 정확히 진단
  • def 대신 abbrev를 사용하도록 제안해, rw 전술(tactic) 이 다시 정상 작동하도록 수정
  • 문제 원인과 해결 이유를 사용자에게 명확히 설명

프로그램 추론 및 변환

  • Rocq의 프로그램 정의를 Lean으로 변환하고, 사용자 정의 표기법까지 구현
  • 예시로 plus2 명령이 변수 X에 2를 더하는 동작을 수행함을 증명
  • 주어진 Rocq 명세만으로 Lean에서 정리(theorem) 를 완성하고 증명 수행

사용 방법

  • Mistral Vibe 통합: /leanstall 명령으로 즉시 사용 가능
  • Labs API: 무료 또는 저비용으로 접근 가능
  • 모델 다운로드: Apache 2.0 라이선스로 직접 실행 가능

의의

  • Leanstral은 코드 생성과 형식 증명 자동화를 결합한 최초의 오픈소스 시도
  • 연구 수학, 검증 가능한 소프트웨어 개발, 고신뢰 시스템 설계 등에서 활용 가능성 제시
  • 비용 효율성과 개방성을 동시에 확보한 새로운 코드 검증 인프라로 평가됨
▲
GN⁺ 13시간전  [-]
Hacker News 의견들

  • 사람들이 이제 에이전트가 원하는 동작을 명세하고, 그 명세에 맞춰 코드를 작성할 수 있다는 패턴을 인식하기 시작한 게 흥미로움
    TDD나 검증 도구 등 어떤 방식을 쓰든, 시간이 지나면 이런 검증 스위트가 “어떻게 동작해야 하는가”를 보여주는 실행 가능한 문서 저장소로 쌓이게 됨
    이런 접근은 단순한 마크다운 스펙보다 훨씬 강력함. 의도가 아니라 세부 동작을 코드로 담기 때문임
    소프트웨어가 복잡해질수록 “그건 Jim한테 물어봐” 식의 구두 전승은 한계가 있음

    • 차이가 크지 않다고 느낌. 코드도 결국 .md 파일에 적을 정보의 다른 표현일 뿐임
      세밀함과 맥락이 해상도 변화 속에서 사라짐
      TDD나 검증 중심 개발엔 동의하지만, 그걸 코드로 쓰는 게 최종 목표는 아님
      이미 수백만 줄의 테스트가 존재하니, 그걸 기반으로 발전시키는 게 현실적임
    • AI가 등장하면서 비로소 TDD가 꿈꾸던 현실이 가능해졌다고 생각함
    • 이런 접근이 흥미롭지만, 블로그 글이 헷갈렸음
      Lean이 실제로 어떤 도움을 주는지 궁금함.
      예를 들어 Lean으로 상태 머신을 증명하고, 그걸 Dart로 옮기는 식인가?
      Lean을 잘 몰라서 이게 현실적인 접근인지 감이 안 옴

  • 최근 Jack Clark(Anthropic 공동창업자)과 Ezra Klein의 팟캐스트에서도 언급됐듯, 모델 정렬(alignment) 은 상대적이며 다양성이 중요하다는 논의가 많음
    Mistral의 모델이 다른 최전선 모델에 비해 뒤처진다는 의견도 있지만, 다양한 정렬 기법과 회사를 실험하는 게 생태계에 중요함

    • 결국 시간이 해결해줄 것이라 생각함

  • 실제 성공 사례가 Simon Willison의 Red Green TDD를 떠올리게 함
    Leanstral이 실패 환경을 재현하는 테스트 코드를 만들고, 정의적 동등성(definitional equality) 문제를 찾아낸 과정이 인상적이었음

    • 에이전트가 스스로 테스트를 작성한다면, 코드와 테스트를 따로 작성할 때보다 정확성 보장이 더 높아질까 궁금함
    • TDD는 결국 프롬프트 엔지니어링과 같다고 생각함. 에이전트에게 명확한 목표를 주는 과정이니까

  • 이 모델이 특정 작업에 맞게 훈련되었지만 Opus보다 성능이 낮음
    Opus는 6배 비싸지만, 그만한 가치가 있어 보임

    • 아이디어는 좋지만, 결국 품질이 신뢰보다 우선임
      자본이 적은 유럽 스타트업이 이런 틈새를 노리는 건 이해되지만, 큰 수익으로 이어지긴 어려울 듯함
    • 벤치마크 신뢰도는 애매하지만, pass@2나 pass@3 결과를 보면 인상이 달라짐
      Codex 같은 모델과 비교하는 게 더 흥미로울 것 같음
    • 모델이 오픈소스라서 로컬에서 실행 가능함. 그게 꽤 중요한 포인트 아닌가?

  • “신뢰할 수 있는 코드”라는 컨셉이 마음에 듦
    하지만 비교 기준이 헷갈림. Haiku보다 싸다고 강조하지만, Haiku 자체가 이 작업에 약하고 Leanstral은 그보다 더 약함
    정확성이 목표라면 “싸지만 별로”가 왜 중요한지 모르겠음
    그래도 Opus도 완벽하지 않으니, 규모를 키우면 더 나은 결과를 낼 수도 있을 듯함

    • 그래프를 보면 pass 수를 늘릴수록 성능이 좋아짐
      2회에서는 Haiku와 Sonnet보다 낫고, 16회에서는 Opus에 근접하면서도 비용 효율이 높음
    • 사실 간단함 — 프롬프트에 “신뢰할 수 있는 출력만” 요청하면 됨

  • Lean을 모르는 입장에서, 이게 직접적인 가치가 있는지 궁금함
    Go 같은 언어 코드에 자동으로 증명을 붙여주는 건가, 아니면 단순히 오픈 모델의 다양성을 응원하면 되는 건가?

    • 아마도 에이전트가 Lean4 명세를 생성하고, 그 명세를 기준으로 소프트웨어를 평가하는 구조일 것임
      하지만 결국 Lean4 명세 자체가 소프트웨어 아티팩트가 됨
      그렇다면 그 명세가 올바른지 검증하는 문제로 다시 돌아감 — 결국 인간 검토가 필요함

  • 몇 주 전부터 이런 흐름을 예상했는데, 실제로 맞아 기쁨임
    LLM 시대에는 코드의 인간 친화성보다 증명 가능성과 토큰 효율성이 더 중요해질 것 같음
    Lean과 Rust를 결합해, “증명된 코드만 컴파일되는” 세상이 올 수도 있음
    관련 논의는 이전 댓글에 정리했음

    • 다만 어떤 증명 시스템도 “옳은 증명”을 보장하지는 않음
      단지 논리적으로 유효(valid) 함을 보장할 뿐임
      증명이 무엇을 증명하는지 완전히 이해하는 건, 프로그램을 이해하는 것만큼 어렵지만, 그 과정에서 사고가 깊어지는 이점이 있음

  • “오픈소스”를 말만이 아니라 실제로 Apache-2.0 라이선스 가중치로 공개한 점이 반가움

    • 하지만 커뮤니티 기준으로 보면, 모델을 재현할 수 없으면 “open weights”일 뿐 “open source”는 아님

  • Mistral 공식 뉴스에 따르면
    Claude Opus는 비용 1,650달러에 점수 39.6,
    Leanstral pass@8은 145달러에 31.0, pass@16은 290달러에 31.9로,
    비용 대비 성능 효율이 꽤 높음

답변달기