Leanstral 1.5

 (docs.mistral.ai)
1 ポイント 投稿者 GN⁺ 3 시간 전 | 1件のコメント | WhatsAppで共有
  • Leanstral 1.5は、Lean 4の形式証明エンジニアリングに合わせた更新モデルで、自動定理証明と自動形式化を狙ったもの
  • モデル規模は総計119Bパラメータ、6.5Bアクティブパラメータ構成で、長い証明・文書コンテキストの処理を前提とする
  • 提供識別子はlabs-leanstral-1-5で、ドキュメント上ではLabs v1.5モデルとして表記される
  • コンテキスト長は256k、価格項目は**$0**と表示され、実験・評価向けのアクセスしやすさを強調している
  • Chat Completions、Function Calling、Agents、Structured Outputs、OCR、Document QnA、FIM、Embeddings、Moderations、Audio、Batch Processing APIとあわせて利用できる

Lean 4の形式証明に合わせたモデル

  • Leanstral 1.5は、Lean 4形式証明エンジニアリングモデルの更新版
  • 主な最適化対象は自動定理証明と自動形式化
  • モデル識別子はlabs-leanstral-1-5として提供される

モデル規模と基本属性

  • パラメータ構成は119B total parameters、6.5B activeと表記される
  • コンテキスト長は256k
  • 価格項目は**$0**と表示される
  • リリース区分はLabs v1.5

会話・エージェント・構造化出力API

文書処理・コード補完・埋め込み

安全性・オーディオ・バッチ処理

関連記事

1件のコメント

 
GN⁺ 3 시간 전
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 企業との契約を1件取るのに18か月かかり、今日署名して送り返したら「申し訳ありませんが、7月末まで休暇中です……」という自動返信が来た
      この1年、その担当者とやり取りする中で受け取った休暇の自動返信はこれで4回目だ
    • 奇妙でイライラするが、私は決済手段をまったく紐づけたことがなくても、このモデルを無料で使用できる
    • この人たちはメールに返信しない。qwant も同じだった
      サンプルは2つだけだが、フランス企業は英語で連絡されるのをあまり好まないのだと考えるようになった

  • 少し別の話だが、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 にはまともな単一市場がなく、特に資本市場ではそうだ。米国より人口が多く、経済規模の合計が大きくても、資源を効率的に集められないなら大した意味はない
      欧州で新しい研究所1つに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 連携 が必要なんでしょうか？かなり制限が強いように見えます