Leanstral 1.5：人人可用的形式化證明工具

Leanstral 自發布以來，一直為 Lean 4 提供開放、實用的證明工程方法。今天，我們釋出 Leanstral 1.5，這是一款免費、Apache-2.0 許可的模型，擁有 119B 總引數，但僅啟用 6B 引數，其效能提升使形式化驗證比以往更強大、更易用。

Leanstral 1.5 在 miniF2F 上達到飽和（驗證集和測試集均為 100%），解決了 PutnamBench 中 587/672 的問題，並在 FATE-H（87%）和 FATE-X（34%）上創下新紀錄。在基準測試之外，它還能驗證複雜程式碼屬性，並在開源倉庫中發現先前未知的 bug，證明嚴謹的形式化方法在實際應用中同樣有效且實用。

訓練過程 Leanstral 1.5 經過三個階段：中期訓練、監督微調和基於 CISPO 的強化學習。它利用兩個強化學習環境進行廣泛訓練：

• 多輪環境：模型被給予一個定理陳述，需要證明或證偽。模型提交證明，接收 Lean 編譯器反饋，並在每次嘗試中改進方法。如果證明編譯成功，則成功；否則迴圈繼續，直到模型解決問題或耗盡預算。
• 程式碼代理環境：Leanstral 像開發者在原始檔案系統中一樣操作：編輯檔案、執行 bash 命令，並使用 Lean 語言伺服器即時檢查目標、錯誤和型別資訊。這使其能夠處理長期任務，如補全倉庫中的部分證明、構建輔助引理，並在多輪上下文壓縮中持續工作。模型學會導航整個證明工程工作流，並最終透過我們的 SafeVerify 分支驗證正確性。

評估結果 在 miniF2F 上，Leanstral 1.5 完全飽和。在 PutnamBench 和 FATE-H/X 上，與 Goedel-Architect（無自然語言引導）、Seed-Prover 1.5（高設定）和 AxProverBase 相比，Leanstral 1.5 在 FATE-H/X 上達到新紀錄（分別解決 87 和 34 個問題）。在 PutnamBench 上，它以遠低於 Seed-Prover 的成本（每個問題約 4 美元 vs. Seed-Prover 的 300 美元以上）多解決了 7 個問題。排名更高的證明器要麼使用自然語言證明指導，要麼執行成本更高（如 Aleph Prover 每個問題 54-68 美元）。

Leanstral 1.5 展示了我們所見過的形式化推理模型中最強的測試時擴充套件能力。隨著每次嘗試的 token 預算從 25k 增加到 4M，PutnamBench 上的 Pass@8 平滑單調增長：從 50k 時的 44 個問題增加到 200k 時的 244 個、1M 時的 493 個和 4M 時的 587 個。當證明執行時間較長時，Leanstral 不會放棄，而是繼續推理、編輯檔案和修訂，將預算直接轉化為已解決的問題。

此外，我們還完全開源了 FLTEval 基準。Leanstral 1.5 將基準上的 pass@1 從 21.9 提升到 28.9，pass@8 從 31.9 提升到 43.2，以七分之一的成本超過了 Opus 4.6 的 39.6，並擴大了與 3-10 倍大小的開源模型的差距。

程式碼驗證案例研究

• AVL 樹時間複雜度證明：Leanstral 1.5 使用結構歸納法和細緻的單子時間跟蹤，證明了真實實現中 AVL 樹的 O(log n) 時間複雜度。經過 270 萬 token 和 22 次壓縮，它系統性地展開 TimeM 單子的每一層，揭示了與控制流交織的底層計算，建立了近乎嚴格的界限，並連線了高度與樹大小，最終完整驗證了插入和刪除操作的時間複雜度。
• 漏洞發現：透過自動化流水線（Aeneas 將 Rust 程式碼翻譯為 Lean，Leanstral 推斷使用者意圖並生成正確性屬性），在 57 個測試倉庫中標記了 47 個違反屬性，其中 11 個指向真實 bug，5 個先前未在 GitHub 上報告。例如，在 datrs/varinteger 庫的 zigzag 解碼符號函式中，輸入 Std.U64.MAX 時表示式 (value + 1) 溢位，導致除錯模式崩潰和釋出模式靜默損壞——這種邊緣情況通常會被測試和模糊測試遺漏。

如何開始 Leanstral 1.5 採用 Apache-2.0 許可。權重可在 Hugging Face 上獲取，同時也可透過免費 API 端點 leanstral-1-5 使用。推薦在 Mistral Vibe 中使用。獲取 API 金鑰後，按步驟設定：安裝 Mistral Vibe、安裝 Leanstral 1.5、啟動代理，並可選安裝 Lean LSP MPC。即可開始證明定理、除錯證明或貢獻程式碼。