Mistral、Lean 4向け証明AI『Leanstral 1.5』公開——PutnamBench 587/672問、Apache-2.0で無料APIも

結論から言うと、Mistralは数学の証明やコードの正しさ確認をAIに手伝わせる『Leanstral 1.5』を公開しました。公式発表は2026年7月2日で、Lean 4という証明支援言語に特化したモデルです。総パラメータは119B、そのうち動くのは約6BのMoE構成で、Apache-2.0ライセンス、Hugging Faceの重み、無料APIが案内されています。

学習は中間学習、教師あり調整、CISPOによる強化学習の3段階です。Leanコンパイラのフィードバックを読み、証明を修正しながら進めます。具体的には、miniF2Fで検証・テストとも100%、PutnamBench 672問中587問、FATE-Hで87%、FATE-Xで34%を達成したとMistralは説明します。

さらに57のオープンソースリポジトリを調べ、未報告のバグ5件を見つけたともしています。私たちに関係するのは、AIがただコードを書く段階から、数学的に『本当に正しいか』を機械で確かめる方向へ進んでいる点です。重要なライブラリや金融・医療系の処理では特に意味があります。ただし数字はMistral公式評価で、実務導入には自分のコード、費用、検証範囲で再確認が必要です。