面向數學形式化證明：Mistral AI 發佈 Leanstral 1.5 低使用成本開源模型

歐洲人工智慧領域的新創公司 Mistral AI 於當地時間本月 2 日正式發布了一款名為 Leanstral 1.5 的全新開源模型。這款模型特別針對數學形式化證明設計，專注於支援 Lean 4 程式語言，目標是降低使用者在進行嚴謹數學推理時所需的運算成本。Mistral AI 強調，Leanstral 1.5 不僅在多項數學基準測試中締造最佳成績，其平均解題成本更遠低於市面上其他同類模型，有望讓形式化證明技術變得更普及。Leanstral 1.

5 採用混合專家（MoE）架構，總參數量達到 119B，但每次推理時僅需激活約 6B 參數，這使得模型在維持強大性能的同時，能大幅減少記憶體與運算資源的消耗。該模型以 Apache-2.0 開源授權釋出，允許學術界與工業界自由使用、修改與部署。Mistral AI 表示，這項設計宗旨是讓更多研究團隊能以更低的門檻投入數學形式化證明領域。所謂數學形式化證明，是指用計算機可嚴格驗證的邏輯語言來表述數學定理及證明過程，確保每個推理步驟都無漏洞。Lean 4 是微軟研究院開發的交互式定理證明器，目前已成為形式化數學社群的主流工具之一。

過去要訓練一個能有效協助 Lean 4 證明的 AI 模型，往往需要極高的運算成本，使得多數研究機構難以負擔。Mistral AI 推出 Leanstral 1.5，正是為了打破這項瓶頸。在標準化的形式數學基準測試 miniF2F 上，Leanstral 1.5 在驗證集與測試集均達到 100% 的完成率，意味著模型能夠百分之百成功生成符合規範的證明。這項成績顯示，模型對常見定理的證明能力已趨近完美。miniF2F 是業界常用來評估神經定理證明器的重要指標，涵蓋高中至大學層級的數學問題。針對更高難度的數學競賽問題集 PutnamBench，Leanstral 1.5 也交出亮眼成績。

PutnamBench 收錄了 672 道 Lean 4 語言編寫的問題，這些題目源自普特南數學競賽，向來以靈活與深度著稱。Leanstral 1.5 能夠成功解決其中 587 道，解題率約 87.3%，大幅領先其他現有模型。這代表模型在處理需要創造性推理的進階問題時，展現出相當穩健的實力。此外，Mistral AI 也使用 FATE 系列抽象代數基準測試來評估模型的表現。FATE 分為碩士級別的 FATE-H 與博士級別的 FATE-X。Leanstral 1.5 在 FATE-H 上達成 87% 的達成率，而在更艱深的 FATE-X 上也有 34% 的達成率。

這兩項成績均被 Mistral AI 稱為「最佳表現」，顯示模型在抽象代數領域的推理深度已能覆蓋高等研究所層級的知識。成本效益是 Leanstral 1.5 最受關注的亮點之一。根據 Mistral AI 提供的數據，對於 PutnamBench 數據集中的問題，Leanstral 1.5 的平均解決開支僅需約 4 美元。相比之下，Seed-Prover 1.5 的平均解決開支超過 300 美元，而 Aleph Prover 也需要 54 至 68 美元。這意味著 Leanstral 1.5 的運算效率至少是其他模型的 10 倍以上，甚至達到 75 倍。在實際場景應用中，這項成本優勢格外重要。

目前許多大學、研究單位以及科技公司都在嘗試將形式化證明整合到軟體驗證、數學研究與 AI 安全領域，但高昂的算力費用往往成為阻礙。Leanstral 1.5 的低使用成本，讓更多專案能夠以合理的預算進行大規模證明嘗試，從而加速數學定理的機器驗證進度。Mistral AI 是一家總部位於法國巴黎的人工智慧企業，自成立以來便以開源高效能模型聞名。先前推出的 Mistral 7B、Mixtral 8x7B 等模型已在自然語言處理與推理任務上獲得廣泛好評。此次進軍數學形式化證明領域，顯示該公司不僅專注於通用語言模型，也積極拓展專業垂直場景的深度應用。Leanstral 1.

5 的發布時間點也相當具有指標意義。隨著 Lean 4 社群持續壯大，越來越多的數學家與電腦科學家投入形式化證明專案，例如菲爾茲獎得主所帶領的「數學形式化」計畫。高效率且低成本的 AI 助手，將有機會大幅縮短證明編寫的人工作業時間，並降低初學者進入此領域的學習曲線。Mistral AI 並未透露 Leanstral 1.5 的具體訓練細節，但強調模型已針對 Lean 4 的語法與邏輯結構進行專門優化。開源社群可透過 Hugging Face 等平台取得模型權重，並依據 Apache-2.0 授權進行二次開發。這使得其他研究團隊能夠基於 Leanstral 1.

5 進一步微調，以適應特定領域的證明需求。整體而言，Leanstral 1.5 的問世代表形式化證明 AI 的成本障礙正在被打破。從 100% 的 miniF2F 完成率到遠低於對手的解題成本，Mistral AI 成功展示了如何透過架構設計與開源策略，讓先進的數學推理技術變得更可親近。未來若能在更多實際專案中驗證其可靠性，Leanstral 1.5 很可能成為數學形式化證明領域的標竿模型。