Mistral AI、形式検証モデル「Leanstral 1.5」公開
原題: Leanstral 1.5: Proof abundance for all
なぜ重要か
形式検証の民主化が進み、バグ発見や数学的証明の自動化が実用段階に入りつつあることを示す事例として業界注目度が高い。
Mistral AIは2026年7月2日、形式検証に特化したオープンソースモデル「Leanstral 1.5」をApache-2.0ライセンスで公開した。総パラメータ数119B・アクティブパラメータ数6Bの軽量設計で、数学ベンチマークminiF2Fを飽和させ、PutnamBenchでは672問中587問を解決、FATE-Hで87%・FATE-Xで34%という最高水準の成績を記録した。
Mistral AIのLeanstralチームは、Lean 4向け形式検証モデル「Leanstral 1.5」を正式リリースした。モデルは総パラメータ数119Bながらアクティブパラメータ数は6Bに抑えた混合エキスパート（MoE）アーキテクチャを採用しており、推論コストを低減しつつ高い性能を実現している。
性能面では、数学的定理証明の標準ベンチマークであるminiF2Fを飽和（実質的に完全解決）し、PutnamBenchでは672問中587問を正解。形式検証ベンチマークのFATE-Hで87%、FATE-Xで34%という最先端の結果を達成した。
トレーニングは3段階で実施された。まず中間トレーニング（mid-training）でLean 4関連の知識を強化し、次に教師あり微調整（SFT）を行い、最後に強化学習手法「CISPO」を用いたRLフェーズを経ている。強化学習では2種類の環境を活用した。マルチターン環境ではモデルが定理を証明または反証し、Leanコンパイラからフィードバックを受け取る形式を採用している。
ベンチマーク性能だけでなく、実際のオープンソースコードへの応用でも成果を示している。57のリポジトリを検証した結果、これまで知られていなかったバグを5件発見したと報告されており、実用的な形式検証ツールとしての有効性を実証している。
モデルはHugging Faceで公開されているほか、Mistral AIが提供する無料APIからも利用可能。Apache-2.0ライセンスのため商用・研究目的を問わず自由に利用・改変できる。