Leanstral 1.5公開──形式検証AIは「バグを見つける開発者」になれるか

Mistral AIは、Lean 4向けの形式検証モデル「Leanstral 1.5」を公開した。Apache 2.0ライセンスのモデルとして、数学証明だけでなく実コードの性質検証や未知バグの発見にも踏み込んでいる。

何が新しいのか

Leanstral 1.5は119B total / 6B activeのモデルで、miniF2Fの検証・テストセットを100%解き、PutnamBenchでは672問中587問を解いたとされる。FATE-Hで87%、FATE-Xで34%という結果も示された。

訓練はmid-training、教師ありファインチューニング、CISPOによる強化学習の三段階で進められた。Leanコンパイラのフィードバックを受けながら証明を修正する環境と、ファイルを編集しコマンドを実行するコードエージェント環境が使われている。

開発現場への意味

形式検証は、金融、制御、暗号、インフラ、医療機器など失敗コストの高い領域で重要だが、専門人材と工数がボトルネックだった。AIが補助できれば、重要モジュールだけでも仕様を証明する現実味が増す。

特に注目すべきは、既存リポジトリに対して未知のバグを見つけたという説明だ。テストでは拾いにくい性質を、証明という形で検査できるなら、AIコーディングの品質保証レイヤーとして価値がある。

注意点

形式検証AIは強力だが、何を証明すべきかという仕様設計は人間側に残る。誤った仕様を正しく証明しても安全にはならない。導入するなら、重要な不変条件を定義し、人間のレビューとCIに組み込む形が現実的だ。

参考：Mistral AI公式発表