datrs/varinteger のzigzagデコード処理に、符号の扱いを誤るオーバーフローが眠っていた。デバッグビルドではクラッシュし、リリースビルドでは黙って値が壊れる種類のバグだ。GitHubのIssueには誰も上げていなかった。これを見つけたのはセキュリティ研究者でもファジングツールでもなく、Lean 4の証明を書くために訓練されたMistralのモデル、Leanstral 1.5 だった。
コードレビューをするLLMは珍しくない。だが「バグがありそうです」と指摘するのと、「この関数は与えた不変条件を満たさない」とコンパイラに証明させるのは、信頼度がまるで違う。前者はもっともらしい推測で、外すこともある。後者は数学的にチェック済みで、通れば嘘がつけない。Leanstral 1.5が面白いのは、後者をやるために作られたモデルが、実在する57個のOSSリポジトリで47件の性質違反と11件の本物のバグ、うち5件は未報告のものを掘り当てた点にある。
そもそもLean 4とは、なぜ「証明」が効くのか
Lean 4 は定理証明支援系(proof assistant)と呼ばれるツールだ。数学の定理やプログラムの性質を形式言語で書き、その証明を機械が一行ずつ検証する。証明が通ればそれは「正しいことが確認された」を意味し、人間のレビューのような見落としが原理的に入らない。
ここがLLMと相性がいい。ふつうの生成AIは自信満々に間違える(いわゆるハルシネーション)が、Lean 4では証明を書いてもコンパイラが通さなければ即座に「不合格」が返る。つまり出力の正しさを外部の厳格な採点者が保証してくれる。モデルはコンパイラのエラーを読んで書き直し、通るまで詰める。ごまかしが効かない環境で回すからこそ、強化学習の報酬もクリーンに設計できる。Mistralはこの学習を、中間学習・教師ありファインチューニング・CISPOという強化学習の三段階で行ったとしている。
ベンチマークを「卒業」しつつある
証明AIの実力は、これまで数学オリンピック級の問題を集めたminiF2Fや、Putnam(全米大学数学コンペ)由来のPutnamBenchで測られてきた。Leanstral 1.5の数字を見ると、この土俵が終わりつつあるのがわかる。
| ベンチマーク | Leanstral 1.5 | 補足 |
|---|---|---|
| miniF2F (val+test) | 100% | Mistral曰く「飽和」 |
| PutnamBench | 587 / 672 | 1問あたり約$4 |
| FATE-H | 87% | 当時のSOTA |
| FATE-X | 34% | 当時のSOTA |
| FLTEval pass@8 | 43.2 | Opus 4.6の39.6を上回る |
miniF2Fで100%というのは、この検証セットではもう差がつかないということだ。ベンチマークが満点になったら、次は現実のコードに軸足が移る。今回の発表がバグ発見の実績を前面に出しているのは、その移行を象徴している。
コスト面の差も無視できない。PutnamBenchで競合のSeed-Prover 1.5を7問上回りつつ、1問あたり約$4で解く。Mistralはこれを、Seed-Proverの高設定が1問あたり10 H20-day(GPU約10日分)、金額にして$300以上かかるのと対比している。80倍近い効率差だ。証明探索を富豪的に殴るフェーズから、実務に載る価格帯へ降りてきた。
一発生成器ではなく、リポジトリで働くエージェント
前世代のLeanstral-2603(3月公開、Mistral初のLean 4向けオープンソース・コードエージェント)から本質的に変わったのは、「証明を一発で吐く」モデルから「リポジトリの中で作業するエージェント」への性格だ。
Leanstral 1.5は生のファイルシステム上で動く。ファイルを編集し、bashを叩き、Lean language serverが返すゴール(残った証明目標)・型・エラーをリアルタイムに読みながら、部分証明を埋め、補題を自作し、コンテキストが溢れれば要約(compaction)して長い作業を続ける。これは冒頭のバグ発見が単なる採点ではなく、実コードに証明を書き付けて反例を突き止めるワークフローだったことを説明する。59.0%のSWE-Benchを狙う汎用コーディングエージェントとは方向が違い、「正しさを機械証明で押さえる」という一点に特化している。
アーキテクチャはMoE(混合エキスパート)で、総パラメータ119B・トークンあたり6.5Bが有効(128エキスパート中4つが発火)。Mistral Small 4系列で、コンテキスト長は256k。長い証明ファイルと関連コードを一緒に抱えられる。ライセンスはApache 2.0で、重みがそのまま商用利用できる。
触ってみるには
重みとAPIの両方が公開されている。確認できた識別子は次の通り。
# 重み(Apache 2.0)
mistralai/Leanstral-1.5-119B-A6B # Hugging Face
# 無料APIエンドポイントのモデルID
leanstral-1-5 # /v1/chat/completions (OpenAI互換)
# CLIエージェント
Mistral Vibe から lean エージェントを起動
自分の実務にすぐ効くかというと、Lean 4で性質を書き下す前提知識が要るので万人向けではない。ただ、暗号や金融計算、シリアライザのような「壊れたら静かに間違える」コードを持っているなら、そこだけ形式検証で固める選択肢が、Apache 2.0で1問$4のコストに乗ってきた意味は大きい。生成AIの弱点は正しさの保証がないことだったが、コンパイラを採点者に据えたこの系統は、その弱点を正面から潰しにきている。miniF2Fが満点になった今、次に飽和させにくるのは私たちのリポジトリの方だ。