Episode Details

タイトル

Mistral AI、形式的検証モデル「Leanstral 1.5」を発表──AIがAIのコードを証明する時代の幕開け

このエピソードで登場するキーワードを説明します。

Mistral AI: フランス発の有力AIスタートアップ。効率的なオープンソースモデルの開発で知られ、世界のAI開発競争において独自の地位を確立している。

Leanstral 1.5: 2026年7月2日にMistral AIが発表した形式的検証に特化したAIモデル。総パラメータ数1190億ながら、推論時は約65億のみをアクティブにする高効率なアーキテクチャを採用している。

Lean 4: 数学の定理証明やソフトウェアの正確性を検証するために用いられるプログラミング言語および証明支援システム。

形式的検証 (Formal Verification): ソフトウェアやハードウェアの設計が仕様通りに正しく動作することを、数学的な手法を用いて厳密に証明するプロセス。

それでは解説に入ります。

Mistral AIは2026年7月2日、数学的証明とコードの形式的検証に特化したオープンソースモデル「Leanstral 1.5」を公開しました。近年、生成AIがコードを書く能力は飛躍的に向上していますが、生成されたコードがミッションクリティカルな環境で安全に動作するかを人間がレビューする作業が、現在の開発現場における最大のボトルネックとなっています。Leanstral 1.5は、この課題を根本から解決するために開発されたモデルであり、数学の定理証明やコード検証に用いられる言語「Lean 4」の環境下で、エージェントとして自律的に証明作業を行います。

特筆すべきはその圧倒的な性能とコスト効率です。高校から数学オリンピックレベルの難問を含むベンチマーク「miniF2F」で100%の正答率を叩き出し、難関数学コンペティションの「PutnamBench」でも672問中587問を解決しました。オープンソース領域ではトップの成績であり、同等の性能を持つプロプライエタリな競合モデルであるAleph Proverが1問あたり54ドルから68ドルのコストを要するのに対し、Leanstral 1.5はおよそ4ドルで実行可能です。これは総パラメータ数1190億に対して、推論時に稼働するパラメータを約65億に抑えたMoE（Mixture of Experts）アーキテクチャの採用が大きく貢献しています。

さらに、実際のビジネス環境における有用性も実証されています。Mistral AIが57のオープンソースリポジトリに対してLeanstral 1.5で検証を行った結果、これまで見過ごされていた5つの未知のバグを発見しました。その中には、広く使われているRust言語のライブラリ「varinteger」において、特定の入力時にシステムクラッシュやデータ破損を引き起こす重大なオーバーフローのバグも含まれていました。モデルは数百万トークンに及ぶ長大なコンテキストを維持しながら、ファイルの編集やコンパイラからのフィードバックを通じた試行錯誤を繰り返し、人間のエンジニアが見落とすようなエッジケースの欠陥を数学的なアプローチで特定しています。

今回のリリースは、単なる高性能モデルの発表にとどまらず、ソフトウェア開発のパラダイムシフトを示唆しています。Apache 2.0ライセンスで無償公開され、Hugging FaceやAPIを通じて誰でもアクセス可能なこのモデルは、これまで専門知識と莫大なコストが必要だった形式的検証を広く民主化するものです。AIがコードを生成し、別のAIがその安全性を数学的に証明するという、人間を介さない自己完結型の開発パイプラインの構築が、現実のビジネスにおいて本格的に始まろうとしています。

今回のエピソードは以上で終了です。また次回お会いしましょう。