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

Mistral AI 于本月 2 日推出面向 Lean 4 的 Leanstral 1.5 模型，拥有 119B 参数、激活 6B 参数，以 Apache-2.0 许可开源。该模型在 miniF2F 验证集和测试集上均实现 100% 完成率，在 PutnamBench 的 672 道问题中解决 587 道，在硕士级 FATE-H 上达 87%、博士级 FATE-X 为 34%，均为最佳表现。成本优势显著：PutnamBench 平均解决开支仅 4 美元，远低于竞品。实际测试 57 个代码库，标记 47 个违规属性，其中 11 个指向真实缺陷，包括 5 个此前未报告的问题。 via AI HOT · https://aihot.virxact.com/items/cmr8xoe5n01f5sllsc3m94j56