📰 面向数学形式化证明：Mistral AI 发布 Leanstral 1.5 低使用成本开源模型

IT之家 7 月 6 日消息，欧洲人工智能企业 Mistral AI 当地时间本月 2 日宣布推出面向数学形式化证明程序语言 Lean 4 的 Leanstral 1.5 模型。该模型总共拥有 119B 参数，激活 6B 参数，以 Apache-2.0 许可开源。

Mistral AI 表示，Leanstral 1.5 模型在 miniF2

查看原文 → ^↗