Mistral AI、Leanstral 1.5（1190億パラメータ）モデルをApache 2.0でオープンソース公開

Mistral AIは2026年7月前後にLeanstral 1.5モデルを正式リリースした。総パラメータ数は1190億、アクティブパラメータ数は60億で、重みはApache 2.0ライセンスでオープンソース化されるとともに、無料APIエンドポイント「leanstral-1-5」も公開された。同モデルはLean 4形式検証言語向けに最適化されており、数学的証明コードの自動生成および検証が可能である。

事実の整理

Leanstral 1.5はMistral Small 4シリーズに属し、Mixture-of-Experts（MoE）アーキテクチャを採用している。エキスパート数は128個で、1トークンあたり4個がアクティブになる。256kトークンのコンテキストをサポートし、テキストと画像を入力として受け付け、出力はテキストである。本モデルはLeanstral-2603バージョンからの更新版であり、トレーニングは中間トレーニング、教師ありファインチューニング（SFT）、CISPOを用いた強化学習の3段階で構成されている。

仕組みの解説

トレーニングプロセスでは2種類の強化学習環境が構築されている。マルチターン環境では、モデルが定理の記述を受け取り、証明を提出した後にLeanコンパイラからのフィードバックを読み取り、成功するかバジェットを超過するまで反復的に改善を続ける。コードエージェント環境では、モデルがファイルシステムを直接操作し、bashコマンドを実行してLean言語サーバーを呼び出すことで、目標・エラー・型情報をリアルタイムに取得し、部分的な証明の完成、補助補題の構築、コンテキスト圧縮の処理を行う。正確性はMistralのSafeVerifyブランチによって検証される。

Leanstral 1.5はFLTEvalベンチマークにおいて、pass@1が21.9から28.9へ、pass@8が31.9から43.2へと向上した。このベンチマークはFermatの最終定理リポジトリの実際のプルリクエストに基づいている。

産業への影響

開発者にとっては、Apache 2.0によるオープンソースの重みと無料APIにより、形式検証の参入障壁が低下する。開発者は重みを直接ダウンロードしてデプロイするか、APIを通じてleanstral-1-5を呼び出し、ローカルリポジトリで証明タスクを実行することができる。

企業ユーザーにとっては、航空・医療などの安全クリティカル領域において検証可能なコード生成能力を提供する。同モデルはAVL木の挿入・削除操作の時間計算量の証明に成功し、自動テストにおいて従来未報告だった5件の潜在的欠陥を発見しており、実際の開発環境における実用性が示されている。

競合状況については、Leanstral 1.5はminiF2Fの検証セットおよびテストセットの双方で100%を達成し、PutnamBenchでは672問中587問を解決した。また、FATE-Hで87%、FATE-Xで34%という新たな最高スコアを記録した。シングルパスでより大規模な一部オープンソースモデルを凌駕しており、コストはClaude Opus 4.6の7分の1以下である。

戦略的評価

既存のベンチマークおよび実際のリポジトリでのパフォーマンスに基づけば、Leanstral 1.5は高信頼性コード生成のシナリオにおいて迅速に統合される可能性が最も高い。開発者はまず無料APIを通じて特定のLeanリポジトリでの通過率をテストし、その上でオープンソース重みのデプロイを検討するとよい。企業が採用を判断する際には、公開ベンチマークのスコアのみに頼るのではなく、自社の形式仕様における実際の通過率と反復コストを重点的に検証すべきである。

この評価は公開されているFLTEval・PutnamBenchおよび実際の欠陥発見データに基づくものであり、将来の応用経路に関する分析であって確定的事実ではない。