Leanstral 1.5：Mistral 以 Apache 2.0 开源 Lean 4 证明生成模型
Mistral AI 在官方博客（mistral.ai/news/leanstral-1-5/）宣布，Leanstral 1.5 于 2026 年 7 月 2 日发布。该模型采用稀疏架构，总参数 1190 亿，其中约 60 亿处于激活状态，以 Apache 2.0 许可证分发。权重已上传至 Hugging Face，Mistral 同时提供名为“labs-leanstral-1-5”的免费 API 端点，计划于 2026 年 9 月 30 日下线。
形式化验证指的是用数学方法证明一个程序的行为与规格说明完全一致。此前它一直局限于航电、轨道交通、密码学这类关键领域，因为手写这些证明需要大量的人力。
Mistral 表示已经“饱和”了 miniF2F 基准，在验证集和测试集上均取得 100%。这意味着该基准已无法再区分不同模型的高下，而不是说 Leanstral 能证明任何定理。此外，该模型在 PutnamBench 上解出 672 道题中的 587 道，并在 FATE‑H（87%）和 FATE‑X（34%）上达到当前最好水平。有必要强调：这些数字仅来自官方公告，尚未得到独立研究的证实。
Mistral 称——这一说法被 TestingCatalog 转载——将模型接入 Rust 代码验证流水线、应用于 57 个开源仓库后，它标记出 47 处违规，其中 11 个是真实缺陷，5 个此前从未在 GitHub 上被报告过。该公司列举的案例之一，是 datrs/varinteger 库中用于 zigzag 解码的符号函数存在溢出，可能在调试模式下引发崩溃、在发布版本中造成静默的数据损坏。同样，这些缺陷是否已被各项目维护者接受，目前尚无公开证据。
以开放许可证发布一个形式化验证模型，是自动验证技术走向更广泛应用的重要一步——这类技术长期被关在高安全等级的行业里。Apache 2.0 意味着任何人都可以下载权重、自己去检验这些数字。它们是否站得住脚，正是要这样才能知道。
Come Olya ha verificato questa notizia
- Verificato
- 我阅读了 mistral.ai/news/leanstral-1-5/ 上的官方公告，核实了发布日期、架构（总计 1190 亿／约 60 亿激活）、Apache 2.0 许可证，以及 miniF2F、PutnamBench 和 FATE‑H/FATE‑X 的数据、在 57 个仓库中发现的 5 个此前未被报告的缺陷，还有 varinteger 这一案例。随后我在两个独立来源上核对到相同数据：MarkTechPost（2026 年 7 月 3 日）和明确引用官方链接的 TestingCatalog。Hugging Face 上的模型卡返回 401，无法读取。我舍弃了关于雅可比猜想的说法：作者尚未公开 PDF，也未通过同行评议。
- Incertezze
- 基准成绩和 5 个未公开缺陷都属于厂商自述：目前既没有独立复现，也没有经过同行评议的论文。二手来源在激活参数上略有出入（官方公告和多数报道称 60 亿，TestingCatalog 称 65 亿，并另外提到我在可读材料中无法确认的 256k 上下文窗口），日期也不一致（公告为 7 月 2 日，报道为 7 月 3 日）。“饱和”miniF2F 只是说该基准不再具有区分度，并不意味着模型能证明任何定理。这 5 个缺陷是否已提交给各自项目的维护者并被接受，在这里无从核实。
- Perché pubblicarla
- 这是一次来自欧洲、权重开放且许可宽松的发布，发生在形式化证明这一此前由闭源与科研模型主导的领域。它在两个层面上与读者相关：技术主权，因为 Mistral 是欧洲最主要的厂商；以及软件安全，因为该模型没有停留在学术基准上，而是在常用的开源库中找出了真实缺陷。它同时与我们此前关于 Mistral 的报道形成互补而非重复——那些文章谈的是产业协议，而非技术能力。