何が発表されたか
Mistral AIは、Lean 4を用いた形式検証に特化したオープンソースモデル「Leanstral 1.5」をApache 2.0ライセンスで公開しました。Hugging Faceおよび無料APIを通じて利用可能で、中間学習・教師ありファインチューニング・強化学習を組み合わせて訓練されています。
ベンチマーク結果
数学分野では、高校から数学オリンピックレベルまでを扱うminiF2Fで100%を達成。パトナム数学競技の672問を含むPutnamBenchでは587問を解き、群論・環論など修士〜博士級の代数課題を扱うFATE-Hで87%、FATE-Xで34%を記録しました。オープンソース勢の中ではPutnamBench、FATE-H、FATE-Xすべてで首位で、PutnamBenchでは非公開モデルAleph Proverのみが上回っています。
なぜコード検証に効くのか
主に数学向けに訓練されたにもかかわらず、コード検証でも高い性能を示した点が重要です。Mistralは57のOSSリポジトリを走査するテストを実施し、これまで報告されていなかったバグ5件を検出。中にはRustのvarintegerライブラリにおけるオーバーフローバグが含まれていました。数学的に「正しさ」を証明するアプローチが、テスト網羅型のQAが取りこぼす境界バグを掘り起こす実力を持つことが実証された形です。
💼 事業会社視点：これは自社にどう効くか
金融・医療・自動運転・決済インフラなど「バグが即座に賠償や事故につながる」領域を持つ日本企業にとって、これは静的解析やユニットテストの延長線上ではなく、品質保証の設計思想を変える号砲です。特にSIer・受託開発企業は、これまで人月と目視レビューで担保してきた「重要ロジックの正しさ」を、形式検証AIによる自動証明で置き換える提案が現実味を帯びます。SaaSプロダクトを持つ企業では、決済計算・権限判定・課金ロジックといった「間違えると全額返金級」のモジュールに絞って導入するのが現実解でしょう。Apache 2.0で無料APIも提供されるため、まずはPoCで自社の中核ライブラリを走査し、既存のCIパイプラインに組み込めるかを技術部門に検証させるべき段階です。役員層は「テストが通っている=安全」という前提を疑い、形式検証を品質KPIに組み込む議論を始める価値があります。