Mistral「Leanstral 1.5」公開──形式検証AIは数学ベンチマークから実コードのバグ発見へ

2026.07.10

Mistral AIは、Lean 4向けの形式検証モデル「Leanstral 1.5」を公開した。Apache 2.0ライセンスで提供され、総パラメータ119B、アクティブパラメータ6Bの構成を採る。数学証明だけでなく、実際のコード検証にも踏み込んでいる点が特徴だ。

形式検証とは、プログラムや定理が仕様を満たすことを、数学的な証明として確認する手法である。従来は専門家の負担が重く、実務導入の壁が高かった。AIが証明作成を支援できれば、安全性が重要なソフトウェア開発の裾野が広がる。

ベンチマークで何を示したのか

Mistralによると、Leanstral 1.5はminiF2Fで検証・テストセットとも100％に到達し、PutnamBenchでは672問中587問を解いた。FATE-Hでは87％、FATE-Xでは34％を記録し、抽象代数の高難度タスクでも性能向上を示した。

注目すべきは、長い証明タスクでトークン予算を増やすほど性能が伸びた点だ。PutnamBenchでは、試行あたりの予算を増やすにつれて解ける問題数が単調に増え、証明が長くなっても推論、ファイル編集、コンパイラフィードバックの利用を続けられることを示している。

Leanstral 1.5は、定理を一度出力して終わるだけではない。ファイルシステム上でコードを編集し、bashコマンドやLean言語サーバーを使い、エラーを見ながら補題を追加する。これは、AIエージェントが開発環境内で長い作業を進める構図に近い。

Mistralは、57のオープンソースリポジトリを対象に検証し、未発見のバグ5件を見つけたとしている。もしこの方向が進めば、金融、医療、ロボティクス、インフラ制御など、障害コストが高い領域で形式検証の利用が現実的になる。

ただし、形式検証AIは一般的なコード補完とは異なる。仕様をどう書くか、どこまで証明すべきか、証明が保守可能かを人間が判断する必要がある。AIが証明を生成しても、検証環境、依存関係、対象範囲の設計が曖昧では効果は限定的だ。

Leanstral 1.5は、AIが「コードを書く」だけでなく、「コードが正しいことを証明する」方向へ進んでいることを示す。開発組織にとっては、テスト、静的解析、レビューに続く品質保証の新しい選択肢として注目に値する。