ハクソク

世界を動かす技術を、日本語で。

Leanstral 1.5: すべての人のための証明の豊富さ

2026年7月4日原文(mistral.ai)

概要

Leanstral 1.5は、6Bアクティブパラメータを持つ無料のApache-2.0ライセンスモデル。 miniF2FやPutnamBenchで高い性能を発揮し、実世界のコード検証でも成果。 3段階のトレーニングとCISPOによる強化学習を採用。 Hugging Faceと無料APIで完全オープンソース提供。 Lean 4環境で実用的な証明工学を可能にする最新モデル。

Leanstral 1.5の特徴と進化

  • Leanstral 1.5 は、 119B総パラメータ 中 6Bアクティブパラメータ を持つ無料モデル
  • Apache-2.0ライセンス で完全オープンソース、商用利用や改変も自由
  • miniF2F を完全制覇、 PutnamBench では672問中587問を解決
  • FATE-H （87%）、 FATE-X （34%）で新たな最先端性能達成
  • 実世界のコード検証 に強く、57リポジトリで5件の未発見バグを自動発見
  • Hugging Face および 無料API 経由で即利用可能
  • Lean 4 環境での実用的な証明工学を強力に推進

トレーニング手法

  • 3段階学習 （ミッドトレーニング→教師ありファインチューニング→CISPOによる強化学習）を採用
  • マルチターン環境
    • 定理文を与えられ、証明または反証を試みる
    • Leanコンパイラのフィードバックを受けながら繰り返し証明を改善
  • コードエージェント環境
    • 開発者のようにファイル編集、bashコマンド実行、Lean言語サーバでゴールやエラーをリアルタイム確認
    • 長期的な証明課題や補助補題生成、複数回の文脈圧縮を通じて証明ワークフロー全体を習得
  • SafeVerify を用いた最終検証で正確性を保証

ベンチマーク評価

  • miniF2F
    • 初等問題からIMOレベルまで、多様な数学分野で100%達成
  • PutnamBench
    • 672問のうち587問を解決、コストは1問あたり約$4（他モデルは$300以上も）
  • FATE-H/X
    • 抽象代数分野で最先端（87問/34問）を記録
  • FLTEval
    • Fermat’s Last Theoremリポジトリの実際のプルリクエストを用いた実用証明工学評価
    • Pass@1を21.9→28.9、Pass@8を31.9→43.2に向上
    • Opus 4.6を1/7のコストで上回る成績
  • 大規模トークン予算 でのスケーリング性能も顕著
    • 50kトークンで44問→4Mトークンで587問と着実に向上

コード検証の実例

  • AVL木の時間計算量証明
    • 挿入・削除のO(log n)保証を実装コード上で厳密に証明
    • 2.7Mトークン、22回の文脈圧縮を経て完全な証明を構築
  • バグ発見パイプライン
    • RustコードをLeanに変換し、Leanstralが意図推論と正しさ性質生成
    • 57リポジトリ中47件の性質違反を検出、11件が本物のバグ、うち5件は未報告
    • datrs/varintegerのzigzagデコード関数の符号化バグなど、従来のテストやファジングで見逃されがちなエッジケースも自動発見

利用方法

  • Apache-2.0ライセンス で自由に利用可能
  • Hugging Face でモデルウェイト配布、 無料API （leanstral-1-5）も提供
  • Mistral Vibe 環境推奨
    • API Keyの取得
    • Mistral Vibeのセットアップ
      • uv tool install mistral-vibe
      • uv tool update mistral-vibe
      • vibe --setup
    • Leanstral 1.5のインストール
      • /leanstallexit
    • エージェントの起動
      • vibe --agent lean
    • Lean LSP MCPのインストール（推奨）
      • ~/.vibe/config.tomlにMCPサーバ設定を追加
      • MCPサーバがなければmcp_servers = []を削除
  • 証明やデバッグ、リポジトリ貢献 などをLeanstralに依頼するだけで利用開始可能

まとめ

  • Leanstral 1.5 は、 証明工学・形式検証・バグ発見 における新たな実用基準
  • Lean 4 と連携し、 研究・産業問わず幅広い応用 が期待される
  • 無料・オープンソース で今すぐ導入可能

Hackerたちの意見

いい仕事だけど、バグの例がちょっと変だと思った。>「datrs/varintegerライブラリのジグザグデコーディング用のサイン関数に一つバグがあった。入力Std.U64.MAXのとき、式(value + 1)がオーバーフローして、デバッグモードではクラッシュ、リリースモードではサイレントコラプションを引き起こした—テストやファジングでは通常見逃されるエッジケースだ。」この境界条件が「テストでは通常見逃される」って、どういうことなの？確かに、悪いテストは見逃すかもしれないけど、(a) 注意深い人や(b) MLコーディングシステムは「極端な値をテストしなきゃ」とかすごく得意だと思う。特にユーザー入力を解析するものに関してはね。他にもっと面白いバグを見つけたけど、すぐに説明するのが難しかったのかな？

└

もしかしたら「通常見逃す」ってわけじゃないかもしれないけど、存在証明から言うと、時々見逃すこともあるよね。テストする例が多様である必要がないっていうのは、Leanを使う利点を示してる。

└

そう、基本的なQAだね。もしテストがこういうことを見逃したら、期待されるよりずっと役に立たないものになっちゃう。著者のバックグラウンドについて疑問が生まれるね。

└

特に「ファジング」についてだけど、そうだね。ファジングは一般的に境界値を意図的に探索するから、これに関しては、エンコーディングライブラリのようなものでは、ファジングは良いコードの基本的な期待値だと思うし、ほぼ確実に数秒でこれを見つけられたはずだよ。--- 具体的に言うと、proptestを使ってすごくシンプルなラウンドトリップテストをしたら、数十個の失敗が出て、これが1秒もかからなかった：スレッド 'signed_round_trip' (50528) が tests/test.rs:72:1 でパニックを起こした：テスト失敗：オーバーフローでの掛け算を試みた。最小の失敗入力：値 = 4611686018427387904 成功数：2 ローカル拒否：0 グローバル拒否：0

└

これはゴミみたいなPRだよ。それだけ。すべてのプロパティベースのテストシステム（1980年頃に発明された）は境界値を探索するからね。CやC++のセマンティクス（またはその欠如）は、コンパイラが「テスト通過」と言える入力を許可するから、実際にテストするのが難しいんだ。

最新版のOpenATPでLeanstral 1.5を試してみて！OpenATPはエージェント自動定理証明器のためのオープンソースPythonパッケージとCLIだよ。Dockerでローカルに、またはModalサンドボックスでリモートに証明器を実行することをネイティブでサポートしてる。GitHub: https://github.com/henryrobbins/open-atp ドキュメント: https://open-atp.henryrobbins.com

└

これは広告だね。

Leanは本当に素晴らしい言語だよね。これらのリリースにワクワクしてる。

「datrs/varintegerライブラリのジグザグデコーディング用のサイン関数に一つバグがあった。入力Std.U64.MAXのとき、式(value + 1)がオーバーフローして、デバッグモードではクラッシュ、リリースモードではサイレントコラプションを引き起こした—テストやファジングでは通常見逃されるエッジケースだ。」そのライブラリはここだよ: https://github.com/datrs/varinteger これが正しいっぽいけど、これが公開される一週間前に同じ問題がそのリポジトリに報告されてる: https://github.com/datrs/varinteger/issues/8 （これってLeanstralの社員？情報がほとんどないし、活動もすごく少ない。もしくはLeanstralがこの問題を拾ったのかな？）これは小さくて、意外とテストが不十分で、長い間放置されてる（8年）ライブラリだよ: https://github.com/datrs/varinteger/blob/master/tests/test.r... 1日あたり約1000ダウンロードされてる: https://crates.io/crates/varinteger [1] それはちょっと少ない気がする。正直言って、これを唯一の例として挙げるほどの大成功とは思えないけど。自動検出は確かに役立つけど、これってこのサブフィールドにとって注目すべき成果なのかな？証明を書くLLMを触ったことはないけど、トレーニングデータが少ないから、一般的なコーディングと比べてちょっと荒いかもしれないね。1: https://crates.io/crates/varinteger は https://github.com/mafintosh/varinteger-rs としてリストされてて、そこから https://github.com/datrs/varinteger にリダイレクトされるから、一見違って見えるけど同じライブラリのようだね。

└

証明の問題は、その価値を伝えるのがちょっと難しいことだよね。ポイントはバグを見つけることじゃなくて、特定のクラスのバグがないことを証明することなんだ。でも、これを売り込むのは難しいから、マーケティングは「見て、このバグ見つけたよ」みたいな感じになりがち。

先日話題になった: https://news.ycombinator.com/item?id=48738938

記事の途中で、いくつかのフロンティア系LLMとの比較が出てくるけど、どれも半年前のものだね。「私たちの新しいモデルは、3世代前の中国のモデルよりも優れている」っていうのが、個人的にはすごく面白い。

Hacker Newsで議論の続きを見る