Leanstral 1.5とは？Mistralの形式検証AIがRustライブラリの未知バグを5件発見した意味
Mistral AIが公開したオープンソースモデル「Leanstral 1.5」は、形式検証言語Lean 4向けに設計され、数学ベンチマークminiF2Fで100%を記録。実地テストでは57のOSSリポジトリを走査し、Rust製ライブラリvarintegerのオーバーフローを含む未知のバグ5件を発見しました。
#形式検証 の記事一覧（2）
形式検証AIとは？Pramaana Labsが27億円調達、法律・税務・創薬で「間違えないLLM」を狙う理由
インドのPramaana Labsが、Khosla Venturesらから27百万ドル（約42億円）のシードを調達。LLMの出力を数学証明用言語LEANで形式検証する仕組みで、法律・税務・創薬といった「間違いが許されない領域」を狙います。