Mistral 发 Leanstral 1.5：6.5B 激活参数啃下 Lean 4 证明

6 月 30 日，Mistral 悄悄把 Leanstral 更新到了 1.5 版本。发布节奏一如既往地欧洲人风格——没有发布会、没有预热，就一篇博客加一张模型卡，扔进 playground 就算完事。

这是继 3 月首版 Leanstral 之后的第一次大更新。定位没变：一个专门给 Lean 4 写形式化证明的代码代理模型。总参数 119B，激活 6.5B，稀疏 MoE 架构，跑起来比一个 7B 稠密模型还轻，但吃的活儿是数学家和验证工程师的活儿。

先说这次更新到底改了什么

坦白讲，Mistral 这次的信息披露相当克制。模型卡里没有放新的 benchmark 数字，也没说清楚相比 3 月版本的具体提升点。目前能确认的是：

• 架构参数不变——119B 总参数、6.5B 激活；
• 继续针对 Lean 4 的两大核心任务优化：自动定理证明（ATP）和自动形式化（autoformalization）；
• 可以在 Mistral AI playground 免费试用；
• 权重发布政策官方还没正式表态，3 月首版是 Apache 2.0，1.5 版本会不会跟随，得再等等。

所以更准确地说，这次是一次在架构不动的前提下重新训练+微调的迭代，不是一次算力翻倍的大版本。Mistral 自己在博客里用了「Proof Abundance for All」这个标题，翻译过来大概意思是：让形式化证明这件事变得便宜、够用、不再是学术圈的奢侈品。

这个定位其实挺关键，我们后面会聊。

一个专门做「证明」的模型，为什么值得关注

先把背景补齐。Lean 4 是一门用来写形式化数学证明和验证程序正确性的编程语言，由微软研究院和莱布尼茨中心主导开发。跟普通编程语言不一样的是，Lean 4 写出来的每一行不只是「能跑」，而是「被机器逐行验证过、逻辑上无懈可击」。

听起来很酷，但用过的人都知道痛在哪：极难写。一个数学系博士生用 Lean 证明一个本科教材上的引理，可能要花一周。写代码的人如果想用 Lean 证明自己函数的正确性，那更是要把每个不变量、每个边界条件都手动喂给证明器。

这就是为什么 AI 圈这两年一直在往这个方向砸资源。DeepMind 有 AlphaProof，OpenAI 内部有相关探索，国内的 Kimi 和智谱都在做数学证明的模型。逻辑很简单：能自动证明数学定理的 AI，大概率也能自动证明代码没 bug。

这在金融清算、航天嵌入式、密码学库这些「一个 bug 死一片」的场景里，是刚需。

Mistral 3 月份切进来做 Leanstral，用的是这个思路的极致版本——把「形式化证明」当成一个独立的模型能力，而不是通用模型的一个 side task。

稀疏架构 + 专业化，成本上直接把 Claude 拉下水

性能这块，3 月版本的对比数据我们有，1.5 版本 Mistral 没重新跑 benchmark，但架构没变，可以做参考。

在 miniF2F、ProofNet 这类 Lean 4 主流基准上，Leanstral 的 pass@2 是 26.3 分，比 Claude Sonnet 4.6 高 2.6 分。这个差距不算特别夸张，真正吓人的是成本对比：

| 模型 | pass@2 | 跑完基准成本 | |------|--------|-------------| | Leanstral | 26.3 | $36 | | Claude Sonnet 4.6 | 23.7 | $549 | | Claude Opus 4.6 | 更高 | 更贵 |

一次证明任务，Leanstral 是 Sonnet 的 1/15 价格。

为什么能便宜到这个程度？稀疏 MoE 是一半原因，激活参数只有 6.5B，推理时该走的算力路径就是那么点。另一半是专业化——通用模型在 Lean 上要绕一大堆弯路，Leanstral 训练时就是喂 Lean 4 的语料和证明轨迹长大的，没有认知税。

对比的开源阵营也不轻松。Qwen3.5 397B-A17B、Kimi-K2.5 1T-A32B、GLM5 744B-A40B 这几个都是激活参数几十 B 起步的重量级选手，在通用 Lean 任务上被一个 6.5B 激活的模型打，说明专业化模型在垂直领域仍然打得过通用大模型——至少在这个成本区间是这样。

这也是 Mistral 一贯的产品哲学：不追 SOTA，追 Pareto。你要最好的，去用 Opus；你要够用又便宜的，那用 Mistral 家的。

「可自证的代码」不是营销词，是真需求

讲点技术细节。Leanstral 在实际工作流里是怎么用的？

简单说，两种模式：

第一种：自动定理证明（ATP）。 你写好一个数学命题，比如「对任意自然数 n，n 加 0 等于 n」，模型自动生成 Lean 4 的证明脚本。这在数学库（比如 mathlib4）的补全、教育、研究里都有用。

第二种：自动形式化（autoformalization）。 你用自然语言或者 Python/Rust 代码描述一个规范，比如「这个排序函数返回一个有序且元素相同的列表」，模型帮你把它翻译成 Lean 4 的形式化规范，然后再生成证明。

第二种模式是真正有产业价值的。举个具体场景：

-- 一段简化的 IMP 语言语义规则
E_Seq (c1 c2 : com) (st st' st'' : state) 
      (h1 : ceval c1 st st') 
      (h2 : ceval c2 st' st'') :
      ceval (CSeq c1 c2) st st''

这样的规则一个中型编译器可能有几百条，每条都要证明保持某些不变量。人肉写要几个月，Leanstral 这类模型可以把周期压到几天。

把范围放大点看——这几年 vibe coding、AI 全自动写代码的路线，一个死结就是「AI 写的代码你敢不敢上生产」。银行敢不敢让 Claude 直接改核心账务？航天敢不敢让 GPT 生成的 C 代码烧进控制器？答案基本都是不敢。

但如果 AI 写出来的每个函数都带一份 Lean 4 证明，证明它满足预先声明的规范，那画风就变了。Mistral 官方那篇博客里把这套东西叫「trustworthy vibe coding」——可信氛围编程，翻译得有点别扭，但意思到位了。

也有值得吐槽的地方

夸完了说几句实话。

第一，1.5 版本的更新透明度太低。 没新 benchmark，没跟老版本的对比图，没说 weight 什么时候放出来。Mistral 这两年在开放性上其实是在往回收的——你看 Medium 3.5、Voxtral TTS 都不再是完全开源，Leanstral 首版是 Apache 2.0，1.5 版本会不会延续这个政策，官方回避了这个问题。开源社区已经在 HuggingFace 的 discussion 里追问了。

第二，Lean 4 的绝对生态还是太小。 全球会用 Lean 4 熟练写证明的人可能不到一万，模型再便宜，用户基数不涨，商业化天花板就在那儿。Mistral 押这个方向更像是「押未来」，不是「押现在」。

第三，pass@2 才 26.3 分意味着什么。 意思是给模型两次尝试，成功率四分之一多一点。这个成绩比 Sonnet 好，但远没到「可以自动化取代人类」的水平。真要落地到金融系统、核心基础设施，这个通过率至少要翻两倍。Mistral 定位「Proof Abundance」——让证明变多变便宜，但没说「让证明变对」，措辞其实很谨慎。

对开发者意味着什么

如果你在做形式化验证、数学库开发、编译器正确性证明这类事情，Leanstral 1.5 值得试一下 playground，一分钱不花，对着自己手头的 Lean 4 项目跑几个 tactic 生成，看看命中率。

如果你是做通用 AI 编程工具的（比如 IDE 插件、Copilot 类产品），可以留意 Leanstral 后面会不会集成到主流的 Lean 4 工具链里。3 月版本已经有社区做了 vscode 插件的适配，1.5 版本大概率会跟进。

如果你只是普通业务开发者——短期内没什么直接影响，但可以留个印象：AI 生成的代码开始有能力「自证清白」了。这条路径走通之后，行业对 AI 编程可靠性的信任门槛会重新校准。

最后说个观察。这两年模型发布的节奏已经明显分层了：一层是 Opus、GPT、Gemini 那种大而全的旗舰，卷通用能力；另一层是像 Leanstral 这样的专业化小模型，卷成本、卷垂直领域的极致效率。Mistral 明显选了后者作为差异化路线。在通用大模型的「智力过剩」逐渐显现的今天，这个选择未必是防守，反而可能是主动的定位。

跟一个稀疏 MoE 的 119B 模型比智商没意思，比它在你需要的那件小事上便宜多少、准多少，才是真的有用。

参考来源

• Hugging Face - Mistral 官方模型仓库 - Mistral 系列开源模型的权重发布主阵地，Leanstral 系列模型卡也会同步到这里
• GitHub - leanprover/lean4 - Lean 4 语言官方仓库，理解 Leanstral 应用场景的基础
• GitHub - leanprover-community/mathlib4 - Lean 4 的数学库，也是 Leanstral 训练和评测的重要语料来源
• Zhihu - 形式化验证与 AI 相关讨论 - 知乎上关于 Lean 与形式化证明的中文讨论集合