Leanstral 1.5：形式検証AIの性能と活用法#
形式検証（Formal Verification）の世界に、新たな無料ツールが登場した。 数学的証明やコードのバグ発見に使えるAIモデルとして、どれほどの実力があるのだろうか？
この記事でわかること：
- Leanstral 1.5の基本スペックとライセンス
- 主要ベンチマークでの具体的なスコア
- 競合モデルとのコスト比較
- 実際の活用事例（AVL木の証明・バグ発見）
- 導入手順の概要
⏱ 約6分で読めます。
このモデルを理解することで、形式検証ツールの選定判断に役立てることができる。
【結論】Leanstral 1.5の重要ポイント5選#
忙しい読者のために、核心情報をまず整理する。
- 完全無料のApache-2.0ライセンス。HuggingFaceと無料APIで入手できる。
- miniF2Fを100%達成。PutnamBenchでは672問中587問を解いた。
- コストが圧倒的に低い。PutnamBench1問あたり約4ドル（競合比較は後述）。
- 実際のバグを発見。57リポジトリをテストし、未報告バグ5件を検出した。
- トークン予算を増やすほど性能が伸びる。4Mトークンで587問解決という結果が出ている。
詳細は各セクションで掘り下げる。
Leanstral 1.5とは？基本概念の解説#
Leanstral 1.5は、Mistral AIが2026年7月2日にリリースした形式検証特化のAIモデルだ。
形式検証（Formal Verification）とは、数学的な証明技法を用いてプログラムや定理の正しさを厳密に確かめる手法のこと。 Leanstral 1.5はその作業を自動化・支援するために設計されている。
動作プラットフォームはLean 4という定理証明支援システム。 Mistral AIは以前からLeanstralシリーズを展開しており、今回の1.5はその性能強化版という位置づけだ。
ライセンスはApache-2.0で、商用・非商用を問わず無料で利用できる。
主な特徴と技術仕様#
このセクションでは、モデルの構造とトレーニング方法を整理する。
モデル構造#
| 項目 | 内容 |
|---|---|
| 総パラメータ数 | 119B |
| アクティブパラメータ数 | 6B |
| ライセンス | Apache-2.0 |
| 提供形態 | HuggingFace（重み）＋無料APIエンドポイント |
| APIモデル名 | leanstral-1-5 |
3段階のトレーニングプロセス#
Leanstral 1.5は以下の3段階で訓練されている。
- ミッドトレーニング
- 教師あり微調整（Supervised Fine-Tuning）
- 強化学習（CISPOを使用）
強化学習では、2つの環境が使われた。
マルチターン環境：
- モデルに定理の命題を与える。
- 証明を提出し、Leanコンパイラのフィードバックを受け取る。
- コンパイルが通れば成功、通らなければ予算が尽きるまでループを繰り返す。
コードエージェント環境：
- モデルが実際のファイルシステム上で動作する。
- ファイル編集・bashコマンド実行・Lean言語サーバーの利用が可能。
- 補助補題の構築や複数ラウンドのコンテキスト圧縮にも対応。
- 最終的な正しさの検証にはSafeVerifyのフォーク版が使われる。
ベンチマーク結果と競合モデルとのコスト比較#
「なぜこのモデルが注目されるのか」を数値で確認しよう。
主要ベンチマークのスコア#
| ベンチマーク | 内容 | Leanstral 1.5のスコア |
|---|---|---|
| miniF2F | 初等〜IMOレベルの形式数学（代数・組合せ・数論など） | 検証・テスト両セット100%（完全達成） |
| PutnamBench | Putnam数学競技会の672問 | 672問中587問 |
| FATE-H | 大学院レベルの抽象代数（群論・環論・加群論など） | 87%（新SOTA） |
| FATE-X | 博士レベルの抽象代数 | 34%（新SOTA） |
| FLTEval | フェルマーの最終定理リポジトリの実プルリクエスト | pass@1: 28.9、pass@8: 43.2 |
FATE-HとFATE-Xでは最先端（SOTA）を更新した。
競合モデルとのコスト比較#
PutnamBench上での比較を整理する。
| モデル | 1問あたりのコスト | 備考 |
|---|---|---|
| Leanstral 1.5 | 約4ドル | |
| Seed-Prover 1.5（高設定） | 300ドル以上 | 10 H20-days/問の予算 |
| Aleph Prover | 54〜68ドル |
Leanstral 1.5はSeed-Prover 1.5より7問多く解き、コストは大幅に低い。
なお、Leanstral 1.5より上位にランクされる一部のモデルは、自然言語による証明ガイダンスを受けている、またはコストが大幅に高いという異なる条件下で動作している点に注意が必要だ。
トークン予算とのスケーリング特性#
Leanstral 1.5はトークン予算を増やすと性能が単調に向上するという特性を持つ。
PutnamBenchのPass@8において：
- 50kトークン → 44問
- 200kトークン → 244問
- 1Mトークン → 493問
- 4Mトークン → 587問
予算が尽きても諦めず、ファイル編集と推論を継続する挙動がこの結果を生んでいる。
実際の活用事例：コード検証への応用#
Leanstral 1.5は数学だけでなく、実際のコード検証にも応用できる。以下の2つの事例がソース記事で紹介されている。
事例1：AVL木の時間計算量の証明#
AVL木（自己平衡二分探索木）の挿入・削除がO(log n)であることを、実際の実装に対して証明した。
この証明には以下が必要だった。
- 木の再帰構造を反映した構造的帰納法
- モナドによる時間追跡の慎重な処理
- 再バランス処理のパスを網羅した場合分け
2.7Mトークン・22回のコンテキスト圧縮を経て、挿入の上界として「高さ単位あたり48ステップ＋定数」という証明を完成させた。 さらに高さとサイズの対数的関係を結びつけ、O(log n)であることを完全に検証した。
事例2：オープンソースリポジトリのバグ発見#
自動化パイプラインを構築し、以下のフローでバグを探索した。
- AeneasツールでRustコードをLeanに変換する。
- Leanstral 1.5がコードからユーザーの意図を推測し、正しさに関する性質を生成する。
- 各性質を4回証明しようとする。
- 4回すべて失敗した場合、否定命題の証明を4回試みる。
57リポジトリをテストした結果：
- 47件の違反性質を検出
- そのうち11件が本物のバグ
- 5件はGitHubに未報告の新規バグ
具体例として、datrs/varintegerライブラリのzigzagデコードにおける符号関数のバグが挙げられている。
Std.U64.MAXを入力した場合に(value + 1)がオーバーフローし、デバッグモードではクラッシュ、リリースモードでは静かなデータ破損が発生する。
このバグはテストやファジングでは見つけにくいエッジケースだったとされている。
導入手順の概要#
実際に使い始めるための手順をソース記事に基づいて紹介する。
詳細なコマンドや設定ファイルの全内容は元記事を参照のこと。
必要な準備#
- Mistral APIキーの取得
mistral-vibeのインストール（uv tool install mistral-vibe）
基本的な起動フロー#
- Mistral Vibeをセットアップする（
vibe --setup）。 - Leanstral 1.5をインストールする（
/leanstallコマンドを使用）。 - エージェントを起動する（
vibe --agent lean）。 - Lean LSP MCP（オプション）を
~/.vibe/config.tomlに追加してインストールする。ツールタイムアウトは600秒に設定する。 - 証明作業を開始する。定理の証明、証明のデバッグ、コード検証などを依頼できる。
なお、既存のMCPサーバー設定がない場合はmcp_servers = []の行を削除する必要があるとされている。
まとめ：Leanstral 1.5が示すもの#
Leanstral 1.5は以下の点で注目に値するモデルだ。
- Apache-2.0ライセンスで完全無料。HuggingFaceと無料APIで入手可能。
- miniF2F 100%達成、FATE-HとFATE-XでSOTA更新という高い性能。
- PutnamBench1問あたり約4ドルという低コスト。
- 実際のオープンソースリポジトリで5件の未報告バグを発見という実用実績。
- トークン予算を増やすほど性能が伸びるスケーリング特性。
形式検証を実際の開発ワークフローに組み込む選択肢として、Leanstral 1.5は具体的なデータに基づいた選択肢の一つとなっている。
出典： Leanstral 1.5: Proof Abundance for All – Mistral AI（2026年7月2日公開）
