Ep.1341 Mistral AI、形式的検証モデル「Leanstral 1.5」を発表──AIがAIのコードを証明する時代の幕開け（2026年7月9日配信）

名古屋ではたらく社長のITニュースポッドキャスト · Jul 8, 2026 · 4m

タイトル

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…