降低數學科研門檻：Mistral AI 發佈開源模型 Leanstral 1.5

法國人工智慧初創公司 Mistral AI 近日正式發表一款專為數學形式化證明語言 Lean4 設計的開源模型，命名為 Leanstral 1.5。這款模型採用 Apache 2.0 許可協議，以總參數量 119B、激活參數僅 6B 的稀疏架構，在維持高效能的同時大幅降低運算成本，目標是讓更多研究人員能夠以合理的資源投入參與數學定理的機器證明。 作為專注於數學推理的智慧工具，Leanstral 1.5 在權威的形式數學基準測試 miniF2F 中展現了驚人的表現。根據 Mistral AI 公布的數據，該模型在驗證集與測試集上均達到 100% 的完成率，意味著它能正確處理所有標準化的形式化證明問題，成為目前少數在該指標上獲得滿分的開源模型之一。 在更進階的數學競賽題庫 PutnamBench 中，Leanstral 1.5 同樣交出亮眼成績。Putnam 競賽向來以高難度聞名，其 Lean4 版本總計有 672 道題目，而 Leanstral 1.5 成功解答其中 587 道，答題率接近 87.4%。這項結果顯示該模型不僅能處理基礎的形式化證明，也能應對大學層級以上的數學推理挑戰。 除了標準化測試與競賽題庫，Leanstral 1.5 在抽象代數領域的 FATE 系列基準測試中也展現統治級表現。FATE 測試分為碩士等級的 FATE-H 與博士等級的 FATE-X 兩個層級，Leanstral 1.5 在 FATE-H 的達成率高達 87%，而在難度更高的 FATE-X 測試中仍有 34% 的達成率，創下該類模型的新紀錄。這意味著模型已能夠理解並生成較為抽象的代數結構證明，貼近高等數學研究的需求。 成本優勢是此波模型發布的另一核心亮點。Mistral AI 強調，相較於市面上其他以全參數運作的大型語言模型，Leanstral 1.5 利用混合專家（Mixture of Experts, MoE）架構，每次推論僅激活 6B 參數，大幅減少記憶體與計算資源的消耗。這使得學術機構、中小型實驗室甚至個人研究者，都能以較低硬體門檻運行這款模型，從而降低數學形式化研究的進入障礙。 開源策略同樣是 Mistral AI 一貫的立場。Leanstral 1.5 採用 Apache 2.0 許可，允許使用者自由下載、修改與商用部署。這對於推動形式化證明在數學界的普及具有關鍵意義——傳統上，撰寫 Lean4 程式碼需要專業訓練與大量時間，而具有開源授權的專用模型可以作為輔助工具，自動生成或補全證明步驟，讓數學家更專注於核心推理。 Lean4 是由微軟研究院開發的互動式定理證明器，近年來在數學界逐漸獲得重視，許多頂尖數學家開始嘗試用 Lean4 形式化複雜的定理。然而，學習曲線與編寫效率一直是推廣的瓶頸。Mistral AI 推出 Leanstral 1.5，正是看到這項需求，試圖以生成式 AI 輔助 Lean4 開發，讓不熟悉機器語法的數學家也能透過自然語言描述來獲得形式化證明草稿。 此次模型的發布也反映了當前 AI 在科學研究中的角色轉變。過去大型語言模型多用於一般問答或文字生成，現在則開始深入專科領域，例如數學推理、程式碼生成與形式驗證。Leanstral 1.5 的優異成績證明，透過適當的架構設計與訓練資料，開源模型也能在高度專業的數學任務上達到接近前沿的水準。 值得注意的是，Mistral AI 並未在公告中詳細說明 Leanstral 1.5 的訓練資料來源與具體訓練方式，但從模型在數項基準上的表現來看，其訓練集很可能包含了大量的 Lean4 原始碼與形式化證明庫。該公司亦表示將持續迭代模型，未來有望進一步提升對高難度定理的支援能力。 對於數學科研社群而言，Leanstral 1.5 的出現意味著形式化證明不再僅是少數專家才能觸及的技術。搭配開源授權與低推論成本，研究人員可以將這類模型整合到自己的工作流程中，例如自動驗證定理證明的正確性、補齊遺漏的步驟，或從非形式的數學描述直接生成 Lean4 程式碼。這不僅能加速數學研究的進展，也能提升成果的可重現性與機器可讀性。 綜合來看，Mistral AI 透過 Leanstral 1.5 在數學形式化領域打下一記強心針。從 miniF2F 的滿分、PutnamBench 的高解題率，到 FATE 系列測試的破紀錄表現，都顯示該模型已經具備高度的數學推理能力。而其低廉的運算需求與開放的授權方式，更讓全球各地的數學研究者有機會親身體驗 AI 輔助證明的便利。未來若能持續擴大訓練數據與優化架構，Leanstral 系列有望成為數學形式化領域不可或缺的基礎工具。