Mistralが2026年7月2日に公開したLeanstral 1.5は、Lean 4向けの形式証明モデルを更新したリリースです。速報の要点は、無料APIで試せること、256k contextを持つこと、そして数学ベンチマークだけでなく実コード検証でも成果を示したことです。形式手法そのものを全社導入する話ではなく、まずは安全性が重要なライブラリやアルゴリズム検証の補助役としてどう使うかを見極めるのが現実的です。
Leanstral 1.5の結論
結論から言うと、Leanstral 1.5は『数学に強い実験モデル』で終わらず、証明作成とコード検証をまたぐ実務寄りの位置に一歩進みました。Mistralの公式ブログでは、miniF2Fで100%、PutnamBenchで587/672問、FATE-Hで87%、FATE-Xで34%を示しています。さらに57個のOSSリポジトリを使った検証で47件の性質違反を拾い、そのうち11件が本物のバグ、5件は未報告だったと説明しています。数字の派手さだけでなく、証明器をソフトウェア品質に接続しようとしている点が今回の本質です。
何が変わったのか
今回の更新で確認できた事実は3つあります。1つ目はモデルカード上で119B total parameters、6.5B active、256k context、価格0ドルと整理されていること。2つ目はApache-2.0で公開され、Hugging Faceの重みと無料APIの両方で触れること。3つ目は学習方法としてmid-training、supervised fine-tuning、CISPOを用いたreinforcement learningの3段階が明示され、マルチターン証明とコードエージェント環境の両方で鍛えたと説明されていることです。つまり『高性能な定理証明器』というより、『Lean 4で長い作業を続けるエージェント』として売り出しているわけです。
どの業務に向くか
企業での使いどころはかなり限定的ですが、だからこそ刺さる領域があります。たとえば暗号、コンパイラ、数値計算、金融ロジック、ミッションクリティカルなインフラ制御のように、仕様逸脱のコストが高いコードです。通常の生成AIは実装速度を上げますが、Leanstral 1.5は『その性質が本当に成り立つか』を詰める側に寄っています。社内でいきなり全案件へ広げるより、既存テストでは抜けやすい境界条件や不変条件の検証補助に絞った方がROIを説明しやすいはずです。
Mistralの事例でも、AVL treeの計算量証明やRustライブラリのzigzag decodingに潜むオーバーフロー検出など、品質保証チームや基盤開発チームが評価しやすい題材が並んでいました。運用現場の言葉に直すなら、『AIに実装させる』より『AIに証明責務を洗い出させる』ツールとして見ると理解しやすいです。
ベンチマークはどう読むべきか
ベンチマークを見ると確かに強力ですが、導入判断では2つ切り分けが必要です。1つは、miniF2FやPutnamBenchの好成績がそのまま業務コードの安心に直結するわけではないこと。もう1つは、Leanstral 1.5が長い推論予算を使うほど伸びる設計であり、短時間の補完用途とは前提が違うことです。公式ブログではPutnamBenchで50k token時44問、200kで244問、1Mで493問、4Mで587問まで伸びたとされます。つまり成果は高い一方、運用時には計算資源、待ち時間、どこまで証明させるかのルール設計が必要です。
導入前に確認したい注意点
注意点も明確です。まずLean 4前提なので、一般的なWeb開発やSaaS運用チームがすぐ使えるモデルではありません。次に、無料APIで触れるとはいえ、証明対象をLeanへ落とし込む準備コストは別です。さらにMistralは機能一覧にfunction callingやagents関連機能を載せていますが、HelloCraftAIの読者が最初に見るべき価値はそこではなく、形式検証ワークフローへどう埋め込むかです。PoCでは『対象コードをどこまでLean化するか』『失敗時のレビューを誰が持つか』『証明結果をCIでどう扱うか』の3点を先に決めておくと空振りしにくくなります。
よくある質問
Q. 普通のAIコード生成ツールの代わりになりますか？ A. 代替というより補完です。コーディング全般を速くするモデルではなく、Lean 4での証明や検証に向いた専門モデルです。Q. 料金はかかりますか？ A. 2026年7月4日時点で、Mistralのモデルカードでは価格は0ドル、ブログでもfree API endpointと案内されています。Q. すぐ全社展開すべきですか？ A. いいえ。まずは安全性要求の高い一部コード、あるいは研究開発チームの検証タスクに絞って評価するのが妥当です。
HelloCraftAIとしての見立て
Leanstral 1.5は、生成AIの導入議論を『書けるか』から『正しいと示せるか』へ少し進める材料です。ただし、汎用的な社内AI活用テーマとは温度差があります。もし社内に安全性クリティカルなロジック、長寿命ライブラリ、監査が重い数式実装があるなら、今のうちに形式検証の試験導入ラインを作る価値があります。逆に一般業務の自動化が先なら、優先度は高くありません。ニュース性で飛びつくより、証明責務が明確なチームで小さく検証するのが筋です。
