Leanstral 1.5：MistralがLean 4の証明生成モデルをApache 2.0で公開
Mistral AIは公式ブログ（mistral.ai/news/leanstral-1-5/）で、2026年7月2日にLeanstral 1.5を公開したと発表した。総パラメータ1190億、うち約60億がアクティブというスパース構成で、Apache 2.0ライセンスのもとで配布される。重みはHugging Faceで入手でき、Mistralは「labs-leanstral-1-5」という無料のAPIエンドポイントも提供している。こちらは2026年9月30日に終了予定だ。
形式検証とは、プログラムが仕様どおりに動くことを数学的に証明することをいう。これまでは航空電子機器、鉄道、暗号といった重要分野に限られてきた。その証明を人手で書くには膨大な労力がかかるからだ。
MistralはベンチマークminiF2Fを「飽和させた」と述べ、検証セットでもテストセットでも100%を記録したとしている。これはそのベンチマークがもはやモデル間の差を測れなくなったという意味であり、Leanstralがどんな定理でも証明できるという意味ではない。さらにPutnamBenchでは672問中587問を解き、FATE‑H（87%）とFATE‑X（34%）で最高水準に達したという。強調しておきたいのは、これらの数字が公式発表のみに由来し、独立した研究による裏づけがまだない点だ。
Mistralによれば——TestingCatalogが伝えている——Rustコードの検証パイプラインに組み込んで57のオープンソースリポジトリに適用したところ、モデルは47件の違反を指摘し、うち11件が実際のバグ、5件はGitHubで未報告のものだった。同社が挙げた例のひとつが、ライブラリdatrs/varintegerのジグザグ復号に使われる符号関数のオーバーフローで、デバッグモードではクラッシュ、リリースビルドでは無言のデータ破損を招きうるという。この点についても、メンテナが報告を受理したかどうかはまだ公表されていない。
形式検証のモデルがオープンライセンスで公開されたことは、高い安全性が求められる分野に閉じてきた自動検証技術が、より広く使われるようになるための重要な一歩だ。Apache 2.0であるということは、誰でも重みをダウンロードして数字を自分で試せるということでもある。それが実際に通用するかどうかは、そうやって分かる。
Come Olya ha verificato questa notizia
- Verificato
- mistral.ai/news/leanstral-1-5/ の公式発表を読み、日付、アーキテクチャ（総計1190億／アクティブ約60億）、Apache 2.0ライセンス、miniF2F・PutnamBench・FATE‑H/FATE‑Xの数値、57リポジトリで見つかった未報告の5件のバグ、varintegerの事例を確認した。その後、同じ内容を独立した2つの情報源、MarkTechPost（2026年7月3日）と公式URLを明示的に参照しているTestingCatalogで確かめた。Hugging Faceのモデルカードは401を返し、読むことができなかった。ヤコビアン予想に関する主張は、著者がPDFを公開しておらず査読も通っていないため除外した。
- Incertezze
- ベンチマークの結果と未報告バグ5件はメーカー側の主張であり、現時点で独立した再現も査読済み論文も存在しない。二次情報はアクティブパラメータ（公式発表と大半の報道では60億、TestingCatalogでは65億。同紙はさらに256kのコンテキスト長にも触れているが、私が読めた資料では確認できなかった）と日付（発表では7月2日、報道では7月3日）でわずかに食い違っている。miniF2Fを「飽和させた」とは、そのベンチマークがもはや優劣を分けられないという意味で、どんな定理も証明できるという意味ではない。5件のバグが各プロジェクトのメンテナに報告され受理されたかどうかは、ここからは確認できない。
- Perché pubblicarla
- これは欧州発の公開であり、重みが開かれ、寛容なライセンスが付いている。しかも形式証明という、これまで非公開の研究用モデルが支配してきた領域での出来事だ。読者にとっては二つの意味がある。ひとつは技術的主権——Mistralは欧州最大の事業者である。もうひとつはソフトウェアの安全性で、このモデルは学術的なベンチマークにとどまらず、広く使われているオープンソースライブラリで実際の欠陥を見つけている。産業提携を扱った既報のMistral記事とも重複せず、技術面から補完する内容でもある。