← AI 動態
The Decoder
Mistral AI 推出開源模型 Leanstral 1.5，通過正式數學基準測試並發現代碼漏洞
Mistral AI 的開源模型 Leanstral 1.5 成功通過正式數學基準測試，並在掃描 57 個開源倉庫時發現了五個以前未知的漏洞
Mistral AI
Leanstral 1.5
正式驗證
代碼查錯
Mistral AI 的 Leanstral 1.5 模型是為 Lean 4 編程語言設計的正式驗證工具，能夠驗證數學證明和軟件正確性。這個模型在 miniF2F 和 PutnamBench 等基準測試中取得了優異的成績，展現了其強大的數學推理能力。此外，Leanstral 1.5 還在掃描開源倉庫時發現了多個以前未知的漏洞，展現了其在代碼查錯方面的實用價值。這個模型的開源發布為開發者和研究人員提供了一個強大的工具，能夠幫助他們提高代碼的正確性和可靠性。這項技術的發展對於提高軟件質量和安全性具有重要意義，同時也反映了人工智慧技術在正式驗證和代碼查錯方面的應用前景。