Leanstral 1.5: 證明豐饒，全民共享

Mistral AI 已發布 Leanstral 1.5，這是一款專為 Lean 4 證明工程設計的專用模型。該模型總參數達 119B，但僅有 6B 為活躍參數，採用 Apache-2.0 授權，並在形式化驗證與數學推理方面提供了顯著的性能提升。

性能基準測試

Leanstral 1.5 在多項關鍵數學基準測試中取得了尖端（state-of-the-art）的結果，展現了其處理基礎與進階推理的能力。

• miniF2F: 該模型完全飽和了這項用於形式化數學的跨系統基準測試，在驗證集與測試集上均達到 100%。
• PutnamBench: Leanstral 1.5 從 Putnam Mathematical Competition 中解決了 672 題中的 587 題。其表現優於 Seed-Prover 1.5 (high setting)，且成本顯著降低——每題約 4 美元，而後者估計超過 300 美元。
• FATE-H and FATE-X: 該模型在這些針對研究生與博士級問題的抽象代數基準測試中創下了新的尖端紀錄，解決了 87% 的 FATE-H 與 34% 的 FATE-X 問題。
• FLTEval: Leanstral 1.5 將 pass@1 從 21.9 提升至 28.9，並將 pass@8 從 31.9 提升至 43.2，以僅為 Opus 4.6 七分之一的成本超越了其 39.6 的表現。

訓練方法論

Leanstral 1.5 是透過三階段流程開發的：中期訓練（mid-training）、監督式微調（supervised fine-tuning）以及結合 CISPO 的強化學習。該模型在兩種不同的 RL 環境中進行訓練：

1. Multiturn Environment: 該模型被要求證明或反駁一個定理陳述。它會提交證明，接收來自 Lean 編譯器的回饋，並迭代地優化其方法，直到證明通過編譯或預算耗盡。
2. Code Agent Environment: 該模型作為開發者在原始檔案系統中運作，編輯檔案、執行 bash 指令，並利用 Lean language server 來檢查目標、錯誤與型別資訊。這種環境允許模型處理長程任務，例如在儲存庫中完成部分證明並建立輔助引理。

測試時擴展性（Test-Time Scaling）與推理

Leanstral 1.5 展現了強大的測試時擴展性，這意味著隨著每次嘗試的 token 預算增加，其性能會單調提升。在 PutnamBench 上，Pass@8 的性能從使用 50k tokens 時解決的 44 題，提升至使用 4M tokens 時解決的 587 題。這種能力讓模型能夠在數百萬個 tokens 之間進行推理、編輯檔案並進行修正，例如在一個複雜的 AVL-tree 證明中，該過程需要超過 270 萬個 tokens 與 22 次壓縮。

真實世界程式碼驗證案例研究

Leanstral 1.5 在驗證程式碼屬性與在開源儲存庫中發現錯誤（bug）方面展現了實用的價值。

AVL Tree 時間複雜度

該模型成功證明了 AVL trees 的實際實作對於 O(log n) 時間複雜度的保證。這需要結構歸納法、處理單子（monadic）時間追蹤，以及針對重新平衡路徑進行詳盡的案例分析。

開源軟體中的錯誤發現

透過結合 Aeneas（將 Rust 程式碼轉換為 Lean）與 Leanstral 1.5（用以推論意圖並生成正確性屬性）的流程，Mistral AI 在 57 個測試的儲存庫中識別出 11 個真實的錯誤，其中 5 個是先前在 GitHub 上未曾報告過的。一個顯著的例子是 datrs/varinteger 函式庫中 zigzag decoding 的 sign function 發生溢位錯誤，該錯誤在輸入 Std.U64.MAX 時會發生。

社群回饋與分析

雖然模型的性能令人印象深刻，但 Hacker News 的社群成員提出了幾點討論議題：

"I found the bug finding example to be weird... In what way would this boundary condition case be considered something that 'testing [...] would typically miss'?"

部分使用者認為，像 datrs/varinteger 中發現的邊界條件錯誤，通常可以透過 fuzzing 或仔細的測試來捕捉。其他人則指出，該錯誤在公告前一週就已經在 GitHub 上被報告為 issue，質疑了所謂「發現」的有效性。

此外，有些使用者對基準測試的時間點提出了質疑，認為比較對象是較舊的模型，而其他人則質疑選擇 Lean 4 而非其他形式化驗證工具（如 Isabelle/HOL 或 TLA+）的選擇。

開始使用 Leanstral 1.5

Leanstral 1.5 已作為 Apache-2.0 授權的模型在 HuggingFace 上提供，並提供免費的 API 端點 (leanstral-1-5)。使用者可以透過 Mistral Vibe 進行部署，設定如下：

1. 安裝 Mistral Vibe: uv tool install mistral-vibe 接著執行 vibe --setup。
2. 安裝 Leanstral 1.5: /leanstallexit。
3. 啟動 Agent: vibe --agent lean。
4. 選擇性使用 LSP MCP: 透過將 lean-lsp-mcp 加入到 ~/.vibe/config.toml 檔案中來增強功能。