Leanstral 1.5

 (docs.mistral.ai)
1P by GN⁺ | ★ favorite | 댓글 1개
  • Leanstral 1.5는 Lean 4 형식 증명 엔지니어링에 맞춘 업데이트 모델로, 자동 정리 증명과 자동 형식화를 겨냥함
  • 모델 규모는 총 119B 파라미터와 6.5B 활성 파라미터 구성이며, 긴 증명·문서 맥락 처리를 전제로 함
  • 제공 식별자는 labs-leanstral-1-5이고, 문서상 Labs v1.5 모델로 표시됨
  • 컨텍스트 길이는 256k, 가격 항목은 $0로 표시되어 실험·평가용 접근성을 강조함
  • Chat Completions, 함수 호출, 에이전트, 구조화 출력, OCR, 문서 QnA, FIM, 임베딩, 모더레이션, 오디오, 배치 처리 API와 함께 사용할 수 있음

Lean 4 형식 증명에 맞춘 모델

  • Leanstral 1.5는 Lean 4 형식 증명 엔지니어링 모델의 업데이트 버전임
  • 핵심 최적화 대상은 자동 정리 증명과 자동 형식화임
  • 모델 식별자는 labs-leanstral-1-5로 제공됨

모델 규모와 기본 속성

  • 파라미터 구성은 119B total parameters, 6.5B active로 표시됨
  • 컨텍스트 길이는 256k임
  • 가격 항목은 $0로 표시됨
  • 릴리스 구분은 Labs v1.5임

대화·에이전트·구조화 출력 API

문서 처리·코드 보완·임베딩

안전성·오디오·배치 처리

함께 보면 좋은 글 β

GN⁺   [-]
Hacker News 의견들

  • 궁금해서 가입하고, 계정에 돈을 넣고, 써보려 했더니 안 됨. Labs 모델이라길래 Labs를 켜려 했는데, 이번엔 알 수 없는 오류가 남. 안내대로 고객지원에 연락하려 했더니 고객지원은 없고, 대충 만든 FAQ만 있음
    FAQ는 바이브 코딩한 것처럼 보이고 검색도 형편없어서, 어떤 질의를 넣어도 전혀 관련 없는 답만 나옴. 그러다 깨달았음: AI가 고객지원을 잘한다면, 왜 AI 회사들은 자기 AI로 고객지원을 제공하지 않는 걸까?

    • 실제로 쓰긴 함. 예를 들면 Cursor가 있음. 예전 논의인 “Cursor IDE support hallucinates lockout policy, causes user cancellations”를 보면 됨[1]
      [1]: https://news.ycombinator.com/item?id=43683012
    • AI가 고객지원을 잘한다고 생각한 사람은 없었음. 싼 고객지원을 만들어줄 뿐이고, 이미 많은 회사는 고객지원 품질에 관심이 없어서 형편없는 지원을 제공해 왔기 때문에 비용을 더 줄일 수 있다는 점에 좋아하는 것임
      실제 문제를 고치는 데 돈을 써야 하는 게 짜증나는 회사 입장에서는 “좋은” 고객지원인 셈임
    • 이 댓글 보고 웃기면서도 울컥했음. 너무나 EU스럽다는 느낌. EU 기업 계약 하나 따내는 데 18개월이 걸렸고, 오늘 서명해서 돌려보냈더니 “죄송하지만 7월 말까지 휴가입니다...”라는 자동응답이 왔음
      지난 1년 동안 이 담당자와 연락하는 동안 받은 휴가 자동응답만 이번이 네 번째임
    • 이상하고 답답한데, 나는 결제 수단을 전혀 연결한 적이 없어도 이 모델을 무료로 사용할 수 있음
    • 이 사람들은 이메일에 답을 안 함. qwant도 마찬가지였음
      표본은 둘뿐이지만, 프랑스 회사들은 영어로 연락받는 걸 별로 안 좋아한다고 가정하게 됨

  • 약간 다른 얘기지만, EU가 실제 최첨단 LLM 시장에서 아무것도 갖고 있지 않다는 게 꽤 슬픔. 특히 최근 미국이 진짜 최첨단 모델 접근을 완전히 제한한 일을 생각하면 더 그렇다
    이게 순전히 자금과 인프라 부족 때문이었을까?

    • Mistral은 자신들이 싸우기로 한 영역에서는 대체로 이기고 있고, 지금은 그게 필요함
      EU 경제 전체가 최첨단 모델에 얼마나 기여할 수 있느냐보다, 프랑스 경제가 얼마나 기여할 수 있는지를 보고 미국이나 중국과 비교하는 편이 더 정확함. 규모가 안 나옴. 대신 그 낮은 규모로 무엇을 해내는지 보는 게 좋고, Leanstral, Voxtral 같은 틈새 제품들이 그런 결과임
    • 대체로 맞음
      프랑스와 독일이 EU에서 가장 큰 경제권인데, 프랑스에는 Mistral이 있고, 독일에는 정부 지원 벤처캐피털 성격의 기관이 있음. 그 기관은 유럽 연구자들이 주권 모델에서 새 최첨단을 달성하도록 돕겠다며 무려 1억2500만 유로(<1억5000만 달러)를 내놓는 걸 너무 자랑스러워함[1]
      그 돈도 단일 우승자에게 가는 게 아니라 여러 수령자에게 나뉨. 첫걸음으로는 멋지지만, 정확히는 3~4년 전이었다면 첫걸음이 될 만했음. 참 아쉬움
      [1] (독일어) https://www.sprind.org/worte/magazin/verkuendung-next-fronti...
    • 소프트웨어 전반도, AI도 부익부 빈익빈 시장임. 미국 대기업들은 유럽 인재와 떠오르는 유럽 회사를 쓸어 담을 여력이 있고 실제로 그렇게 함. 사고 싶지 않으면 가격으로 눌러 파산시킬 수도 있음
      우리는 인간 자본을 원자재로 삼는 식민지 경제에 살고 있고, 그 모든 것이 미국으로 흘러감. 피하려면 지금의 게임을 그만두고, 중국처럼 제대로 된 산업정책으로 경쟁력 있는 산업을 키워야 함. 지난 수십 년 동안 그런 의지는 없었지만, Trump가 국가의 귀환을 아주 명확히 보여주고 있고 유럽도 천천히 인정하는 중임
    • Mistral은 40억 달러 이상을 조달했으니 꽤 큰돈이긴 하지만, OpenAI/Anthropic/xAI급은 아님
      어려운 부분은 순수 LLM 개발을 재무적으로 정당화하는 것임. 모델들은 서로 매우 비슷함. OpenAI는 처음에 순수 연구를 위한 “자선단체”라는 명분으로 정당화했고, Anthropic은 OpenAI가 안전을 충분히 신경 쓰지 않는다고 하며 갈라져 나왔음. Elon은 자신이 Grok을 만들지 않으면 AI가 깨어 있는 척하며 진실하지 않을 거라고 했고, Google은 Gemini를 만든 이유가 원래 그들이 시작점이었고 AI 연구가 Larry와 Sergey가 창업 때 부여한 핵심 임무였기 때문임. 다만 재무적 이유로 한동안 묵혀뒀음
      중국 모델들의 동기는 솔직히 불분명함. 훌륭한 설명은 본 적 없고 가설만 봤음. 하지만 무료로 풀거나 지나치게 싸게 내놓는 걸 보면 그 동기도 재무적인 것 같지는 않음
      반면 Mistral은 일반 회사임. 우주적 운명 같은 서사를 믿고 돈을 쏟아붓는 부자 후원자가 없으니, 하는 일을 투자수익률로 정당화해야 함. 그러면 대규모 LLM 학습은 거의 배제됨
      EU 규제도 고려해야 함. 예전에 찾아봤을 때 유럽 기술 산업의 가능성을 없애는 이상한 규칙이 많았음. 영국에는 연구 목적으로만 인터넷을 크롤링할 수 있다는 규정도 있었음
      https://knowledgerights21.org/news-story/the-uks-copyright-l...
      그리고 수정헌법 제1조가 없으면 모델이 한 말 때문에 기소될 위험이 훨씬 큼. 독일이 검색 결과 페이지에 모델이 넣은 내용 때문에 Google을 법정에 세운 사례를 보면 됨
      그래서 이익은 불분명하고 법적 위험은 매우 큼
    • EU에는 제대로 된 공동 시장이 없고, 특히 자본 시장에서 그렇다. 미국보다 인구가 많고 총경제 규모가 커도, 자원을 효율적으로 모을 수 없다면 별 의미가 없음
      유럽에서 새 연구소 하나에 1000억 달러 조달이 가능할까? 아니라면 끝난 것이고 포기해도 됨

  • 우연이네. 오늘 아침에 OpenATP를 막 공개했음. OpenATP는 에이전트형 자동 정리 증명기를 위한 오픈소스 Python 패키지이자 CLI임
    Mistral의 Vibe 하네스를 통한 Leanstral 지원도 포함되어 있음. 이전 프로덕션 Leanstral 모델은 5월 22일에 폐기됐고, 패키지가 Leanstral 1.5를 가리키도록 최대한 빨리 업데이트할 예정임
    GitHub: https://github.com/henryrobbins/open-atp
    Docs: https://open-atp.henryrobbins.com

  • 404인가?
    https://web.archive.org/web/20260630223430/https://docs.mist...

  • 가중치 정책을 잘 이해하지 못하겠음. 이 사이트는 가중치가 Apache 라이선스라고 해서 공개 가중치처럼 보이는데, 다운로드 링크를 찾을 수 없음
    Hugging Face 프로필에는 이전 스냅샷만 제공하는 것 같음[0]. 가중치를 다운로드할 수 있는지, 가능하다면 어디서 받을 수 있는지 아는 사람이 있을까?
    [0] https://huggingface.co/mistralai/Leanstral-2603

  • 나도 “Page not found”가 뜸. 접근에 성공했나? 이게 무슨 내용임?

  • Leanstral 1에 대한 논의: https://news.ycombinator.com/item?id=47404796

  • Lean 4와 Idris 2는 저평가되어 있고, 추가 보장을 제공하므로 LLM이 코딩하기에 아주 좋을 가능성이 큼

  • 지금 404가 뜸

  • 이 소식 때문에 가입했는데, “Code”를 쓰려면 GitHub 연결을 해야 하나? 너무 제한적으로 보임

답변달기