注目★★★★★Hacker News
Mistral がLeanstral 1.5 公開、6B パラメータで数学証明を自動化・未知のバグ 5 件発見
30秒で把握
- 1Mistral Leanstral 1.5 公開・6B パラメータで数学証明 587/672 問解く・FATE-H 87% 達成
- 2未報告バグ 5 件自動発見・Seed-Prover 1.5 比 75 倍のコスト削減・Rust コード形式検証に対応
- 3Apache-2.0 オープンソース・Hugging Face と無料 API で即利用可能・Lean 4 エコシステムで実装開始
要約
Mistral は形式検証向け言語モデル Leanstral 1.5 を Apache-2.0 ライセンスで公開した。6B アクティブパラメータながら miniF2F を 100% 飽和、PutnamBench で 587/672 問を解き、FATE-H で 87%・FATE-X で 34% の最高性能を達成した。中段階学習・教師あり微調整・CISPO 強化学習の 3 段階で訓練され、実コード検証で 57 リポジトリから未報告のバグ 5 件を自動発見、Seed-Prover 1.5 比約 $300/問から $4/問へ推論コストを削減した。Hugging Face と無料 API で即座に利用可能。
あなたへの影響
形式検証は理論的には強力だが計算コストと実装難度で現場導入が進まなかった。
推奨：Leanstral 1.5 の安価で自動化された証明生成と実際のバグ発見は、Lean 4 やセキュリティ要件が高いチームにおいて継続的な形式検証パイプラインの構築を検討する価値があり、特に Rust-to-Lean 自動変換による既存コードベースの検証は段階的導入の入口になり得る。