Mistral AIは2026年7月2日(現地時間)、形式検証と定理証明に特化したモデル「Leanstral 1.5」をリリースした。同モデルは6Bのアクティブパラメータを持ち、PutnamBenchの672問中587問を解決。FATE-Hで87%、FATE-Xで34%を達成し、それぞれで新たなSOTAを記録した。Apache-2.0ライセンスでオープンソースとして公開され、無料APIでも提供される。
Leanstral 1.5は総パラメータ119B、アクティブパラメータ6Bのモデルで、形式検証の性能向上を実現した。miniF2Fを完全に飽和させ、FATE-HおよびFATE-Xで新たな最先端（SOTA）の成果を達成している。ベンチマーク結果に加え、複雑なコード特性の検証や、オープンソースリポジトリにおける5つの未発見バグの特定も行ったとされている。
Leanstral 1.5のトレーニングは、mid-training、supervised fine-tuning、CISPOを用いた強化学習の3段階プロセスで実施された。マルチターン環境では定理の証明または反証を試み、Leanコンパイラのフィードバックに基づいてアプローチを洗練させる。コードエージェント環境では、開発者のようにファイル編集やbashコマンドの実行、Lean言語サーバーを用いたリアルタイムな情報検査を行うことで、長期間にわたるタスクに対応する。
評価はminiF2F、PutnamBench、FATE-H、FATE-X、FLTEvalの各ベンチマークで行われた。miniF2Fでは100%の達成率を記録。PutnamBenchではSeed-Prover 1.5 highを7問上回り、問題解決あたりのコストも大幅に低いと報告されている。FLTEvalではpass@1が21.9から28.9へ、pass@8が31.9から43.2へと向上した。
コード検証の事例として、AVLツリーの時間計算量の証明や、57のリポジトリで47の違反プロパティを検出し、そのうち11が実際のバグであったことが示された。特に、datrs/varintegerライブラリのzigzagデコーディングにおける、特定の入力値でオーバーフローを引き起こすバグを自動的に発見したと報告されている。
Leanstral 1.5はApache-2.0ライセンスで提供され、重みはHugging Faceで、また無料APIエンドポイント「leanstral-1-5」を通じて利用可能となっている。
参考: mistral.ai (アーカイブ) — 2026年7月3日 09:00 (JST)