Mistral AI、Lean 4向けオープンソースのコードエージェントLeanstralを公開

Leanstralは証明支援系Lean 4のために設計されたコードエージェントである。既存の証明システムが大規模な汎用モデルのラッパーであったり、単一の数学問題に特化していたりするのに対し、実際の形式化リポジトリでの作業を想定して学習したという。スパース構成でアクティブパラメータは6Bに抑えられ、Leanを検証器として並列推論を行うことで性能とコスト効率を両立するとしている。vibe経由で任意のMCPに対応し、lean-lsp-mcpで最大性能が出るよう学習されている。

評価はFLTプロジェクトの各PRで、すべての形式証明を完成させ新しい数学概念を正しく定義できるかを測る方式で行われた。比較対象にはClaude Opus 4.6、Sonnet 4.6、Haiku 4.5とオープンモデルのQwen3.5 397B-A17B、Kimi-K2.5 1T-A32B、GLM5 744B-A40Bが含まれる。GLM5とKimiはFLTEvalのスコアがそれぞれ約16.6と20.1で頭打ちとなり、Qwen3.5は4パスで25.4に達する。Leanstralは1パスでGLM5とKimiを上回り、pass@2で26.3、pass@4で29.3を記録した。

Claude系との比較では、Leanstralのpass@2が26.3でコストは36ドル、Sonnetは23.7で549ドルである。pass@16では31.9に達しSonnetを8ポイント上回る。品質ではOpus 4.6が39.6で首位だが、コストは1,650ドルでLeanstralの92倍とされる。評価ではMistral Vibeを改変なしでスキャフォールドに使っている。

事例として、学習に含めていないLean 4.29.0-rc6で`rw`タクティクが型エイリアスに一致しなくなった質問に対し、テストコードで環境を再現し、`def`を`abbrev`に替える修正を説明付きで提案した。またRocqで書かれたImpの定義をLeanへ変換し、カスタム記法も実装したうえで、プログラムの性質に関する定理の証明まで行った。

提供形態は三つある。Mistral Vibeでは`/leanstall`で有効化し、Shift+Tabでモデル表示をLeanstralに切り替えるか`vibe --agent lean`で使う。Labs APIのエンドポイントは`labs-leanstral-2603`で、フィードバック収集のため期間限定で無料または低価格に保たれる。重みはApache 2.0で配布される。技術レポートと新しい評価スイートFLTEvalも公開予定とされている。