Leanstral 1.5(リーンストラルワンポイントファイブ)とは
Leanstral 1.5とは、Mistral AIが公開した、Lean 4の形式証明とコード検証に特化したLeanstralの更新版モデルです。数学の証明やソフトウェア仕様を、AIが文章でそれらしく説明するだけでなく、証明器で確かめられる形へ近づけることを狙っています。
英語表記：Leanstral 1.5
形式証明に寄せた更新版
Mistral Docsでは、Leanstral 1.5は119B総パラメータ、約6.5Bの実際に動くパラメータ、256kのコンテキスト長を持つLabsモデルとして説明されています。実際に動くパラメータは、計算で主に使われる部分の規模を示す目安です。一般的なチャットAIの紹介で出る「賢さ」だけでなく、長い証明作業を続けるための作業机の広さも見ておく必要があります。
公式発表では、中間訓練、教師あり微調整、CISPOを使った強化学習という流れで訓練したと説明されています。専門語が多いですが、要するに、証明を書いてLeanの反応を見て直すという試行錯誤を、AIが長く続けられるように鍛えたモデルです。証明器からのフィードバックを使う点が、通常の文章生成AIとの大きな違いになります。
ビジネスでの意味
Leanstral 1.5は、通常のWebサイト制作や広告運用ですぐ使うAIというより、ミスの許容度が低いソフトウェアの検証に近い領域の技術です。金融システム、暗号、基盤ライブラリ、医療や安全に関わる制御などでは、「動いたように見える」だけでは足りません。正しさを説明ではなく検証へ寄せるためのモデルと見ると理解しやすいでしょう。
2026年7月確認時点で、Mistral DocsはLeanstral 1.5を無償表示のLabsモデルとして示し、公式発表はApache-2.0 licenseやHugging Face上の公開weightにも触れています。ただし、提供条件は変わり得るため、導入判断では必ず最新のMistral Docsを見直すべきです。
Topic未報告バグを見つけたという実務寄りの話
Mistralの発表では、57のリポジトリを対象にした検証で、47件の破られた性質を検出し、そのうち11件が本物のバグ、さらに5件はGitHubで未報告だったと説明されています。形式証明は数学だけの話に見えますが、実コードの見落としを拾う方向にも伸びています。
Leanstral 1.5に関するよくある質問
- なぜ形式証明モデルが企業に関係するのですか？
- ソフトウェアの不具合が大きな損失につながる領域では、テストだけでなく仕様通りかを確かめる考え方が重要になります。Leanstral 1.5は、その検証作業をAIで支援する方向のモデルです。
- Lean LSP MCPはLeanstral 1.5とどう関係しますか？
- Lean LSP MCPは、AIエージェントがLeanの状態やエラーを扱いやすくするための接続口です。Mistralの案内では、Leanstral 1.5をMistral Vibeで使う際の補助として推奨されています。
- Leanstral 1.5は一般的な業務チャットに向きますか？
- 主な用途はLean 4の形式証明やコード検証です。社内検索や文章作成より、正しさを機械的に確かめたい専門領域に向いたモデルと考えてください。
