精选理由
Mistral AI 新出的 Leanstral 1.5，专攻数学证明，miniF2F满分，解决成本只要几美元，比竞品便宜几十倍，搞形式化验证的可以试试。
Mistral AI 于7月2日发布 Leanstral 1.5 模型，拥有119B参数（激活6B），采用Apache-2.0开源。该模型在miniF2F形式数学基准测试的验证集和测试集上均达100%完成率。在PutnamBench数学竞赛的672道Lean 4问题中可解决587道，FATE-H硕士级基准达成率87%，FATE-X博士级达成率34%，均为最佳表现。其平均解决成本仅4美元，远低于Seed-Prover 1.5的300美元以上和Aleph Prover的54~68美元。实际测试中在57个代码库标记47个违规属性，发现11个真实缺陷，含5个此前未报告的问题。
AI 翻译 · 中文
Mistral AI 于7月2日发布 Leanstral 1.5 模型，拥有119B参数（激活6B），采用Apache-2.0开源。该模型在miniF2F形式数学基准测试的验证集和测试集上均达100%完成率。在PutnamBench数学竞赛的672道Lean 4问题中可解决587道，FATE-H硕士级基准达成率87%，FATE-X博士级达成率34%，均为最佳表现。其平均解决成本仅4美元，远低于Seed-Prover 1.5的300美元以上和Aleph Prover的54~68美元。实际测试中在57个代码库标记47个违规属性，发现11个真实缺陷，含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…