面向数学形式化证明：Mistral推Leanstral 1.5低使用成本模型

IT之家 7 月 6 日消息，面向明欧洲人工智能企业 Mistral AI 于本月 2 日正式发布专为数学形式化证明语言 Lean 4 设计的数学 Leanstral 1.5模型。该模型采用 MoE（混合专家）架构，形式型总参数量达 119B，化证激活参数量为 6B，低使并以 Apache-2.0 许可证开源。用成

在性能表现上，本模Mistral AI 指出 Leanstral 1.5 在 miniF2F 形式数学基准测试的面向明验证集和测试集中均取得了 100%的完成率。在包含 672 道 Lean 4 问题的数学 PutnamBench 数学竞赛数据集中，该模型成功解决了 587 道题。形式型此外，化证在 FATE 系列抽象代数基准测试中，低使其在硕士级 FATE-H 上达成率为 87%，用成博士级 FATE-X 达成率为 34%，本模均刷新了最佳纪录。面向明

Mistral AI 特别强调了新模型在经济成本上的显著优势。以 PutnamBench 数据集为例，Leanstral 1.5 解决单个问题的平均成本仅为 4 美元，相比之下，Seed-Prover 1.5 的成本超过 300 美元，Aleph Prover 的成本也在 54~68 美元之间。

在实际工程应用测试中，Leanstral 1.5 对 57 个代码库进行了扫描，标记出 47 个违规属性，其中 11 个确认为真实缺陷，包括 5 个此前未在 GitHub 上报告过的潜在问题。

本文地址：https://www.dr-wine.com/html/272a13599592.html