Mistral AI、Leanstral 1.5を無償公開
Judul asli: Leanstral 1.5: Proof abundance for all
Mengapa Ini Penting
6Bアクティブパラメータで形式検証の最先端性能を実現し、実用的な証明工学のアクセシビリティを拡大
Mistral AIは2026年7月2日、Apache-2.0ライセンスのLeanstral 1.5を公開。総パラメータ119B・アクティブ6BでPutnamBench 587/672問を解決、FATE-H 87%を達成。
Mistral AIは形式検証モデル「Leanstral 1.5」をリリースした。総パラメータ数119B、アクティブパラメータ数6Bの構成で、Apache-2.0ライセンスの下で無償提供される。Hugging FaceおよびAPIからアクセス可能。
性能面では、数学的定理証明ベンチマーク「miniF2F」を飽和させ、PutnamBench（672問）のうち587問を解答。形式検証ベンチマーク「FATE-H」で87%、「FATE-X」で34%という最先端の結果を達成した。
トレーニングは3段階で実施。中間訓練、教師あり微調整（SFT）、そして独自手法「CISPO」を用いた強化学習（RL）を組み合わせている。RLは「マルチターン環境」と「シングルターン環境」の2つの環境で実施され、モデルは定理の証明または反証を行う。
実用面では、57のオープンソースリポジトリをテストした結果、これまで知られていなかったバグを5件発見。Lean 4を用いた実世界のコード検証に適用可能であることを示した。