拾雨 (@c519127) 在 面向数学形式化证明：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 模型在 miniF2F 形式数学基准测试的验证集和测试集上均实现了 100% 的完成率；在 PutnamBench 数学竞赛问题集的 672 道 Lean 4 问题中可解决 587 道；对于 FATE 系列抽象代数基准测试，其在硕士级 FATE-H 上实现了 87% 的达成率，博士级 FATE-X 达成率则为 34%，均为最佳表现。 
 [75c4c7d2-abcb-4067-9d73-f23f8005a9ff] 
Mistral AI 强调了新模型的成本优势：对于 Pu...
 
 
Back to Top