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

- 来源：IT之家（RSS）
- 发布时间：2026-07-06 15:54
- AIHOT 分数：41
- AIHOT 链接：https://aihot.virxact.com/items/cmr8xoe5n01f5sllsc3m94j56
- 原文链接：https://www.ithome.com/0/973/135.htm

## AI 摘要

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 个此前未报告的问题。

## 正文

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%，均为最佳表现。

Mistral AI 强调了新模型的成本优势：对于 PutnamBench 数据集中的问题，Leanstral 1.5 的平均解决开支仅有 4 美元，而 Seed-Prover 1.5 需要 300 美元以上，Aleph Prover 也需要 54~68 美元。

而在实际场景应用中，Leanstral 1.5 在测试的 57 个代码库中标记了 47 个违规属性，其中 11 个指向了真实的缺陷，包括 5 个此前未在 GitHub 上被报告过的问题。