Mistral AI、Leanstral 1.5 を公開：Apache-2.0ライセンスのLean 4コードエージェントモデル、PutnamBench 672問中587問を解決

Mistral AI は本日、Lean 4 向けのコードエージェントモデル Leanstral 1.5 をリリースしました。このモデルは自動定理証明と証明工学をターゲットとしており、重みは Apache 2.0 ライセンスで公開され、無料の API エンドポイント leanstral-1-5 も利用可能です。

Leanstral 1.5 は以前の Leanstral-2603 モデルのアップデート版で、Mistral Small 4 ファミリーに属します。Lean 4 は証明支援系であり、すべての論理ステップを機械的にチェックします。perfectoid 空間や Rust 断片の性質なども表現可能です。

アーキテクチャは mixture-of-experts (MoE) を採用。各トークンを少数の専門サブネットワークにルーティングし、計算量を抑えつつ大容量を維持します。128 のエキスパートを持ち、トークンあたり 4 つがアクティブ、総パラメータ数 119B、アクティブパラメータ数 6.5B、コンテキスト長 256k トークン。入力はテキストと画像に対応し、出力はテキストのみです。

訓練は 3 段階で行われます：中期訓練、教師ありファインチューニング、そして CISPO を用いた強化学習。2 つの強化学習環境がエージェント的振る舞いを形成します。マルチターン環境では、モデルは定理のステートメントを与えられ、証明または反証を試み、Lean コンパイラのフィードバックを読みながら予算内で成功するまで洗練します。コードエージェント環境では、生のファイルシステム内で動作し、ファイル編集、bash コマンド実行、Lean 言語サーバーの利用（目標、エラー、型情報をリアルタイムで取得）が可能です。これにより、部分証明の完了、補助補題の構築、コンテキスト圧縮による長期タスクの維持が実現します。正しさは Mistral の SafeVerify フォークによって検証されます。

ベンチマーク性能：miniF2F の検証セットとテストセットで 100% を達成。PutnamBench では 672 問中 587 問を解決。FATE-H および FATE-X 代数ベンチマークで新たな SOTA（87% と 34%）。FLTEval では pass@1 が 21.9 から 28.9、pass@8 が 31.9 から 43.2 に向上し、Opus 4.6 の 39.6 を 7 分の 1 のコストで上回りました。PutnamBench では、Seed-Prover 1.5 high 設定よりも 7 問多く解決し、コストは約 4 ドル/問（Seed-Prover は 300 ドル以上/問と推定）。テスト時スケーリングがモデルの特徴であり、トークン予算を増やすと性能が向上します。

実用例として、実際の AVL ツリー実装で O(log n) 時間計算量を証明し、オープンソースコードのバグを発見しました。57 のリポジトリで 47 の違反プロパティと 11 の真のバグをフラグし、うち 5 つは未報告でした。開発チームは、リポジトリ内での部分証明の完了、関数の正しさプロパティの自動生成、推論された不変条件の証明/反証による Rust コードのストレステストなどに利用できます。

利用開始方法：最も簡単なのは Mistral Vibe CLI で、無料プランで利用可能。セルフホスティングには vLLM 0.24.0 以降が必要で、詳細なデプロイコマンドが提供されています。OpenAI 互換クライアントから呼び出し、reasoning_effort パラメータを設定可能。また、OpenAI スタイルの関数呼び出しや lean-lsp-mcp サーバーもサポートされています。