IT 之家 7 月 6 日消息，欧洲人工智能企业 Mistral AI 当地时间本月 2 日宣布推出面向数学形式化证明程序语言 Lean 4 的 Leanstral 1.5 模型。该模型总共拥有 119B 参数，激活 6B 参数，以 Apache-2.0 许可开源。
而在实际场景应用中，Leanstral 1.5 在测试的 57 个代码库中标记了 47 个违规属性，其中 11 个指向了真实的缺陷，包括 5 个此前未在 GitHub 上被报告过的问题。
IT之家
37分钟前
面向数学形式化证明：Mistral 推 Leanstral 1.5 低使用成本模型
相关标签
