当形式化验证还在“学术象牙塔”里缓慢爬坡时，一支来自Mistral AI的开源模型突然将关键基准推至天花板。Leanstral 1.5，一个总参数119B但每次仅激活6B参数的MoE架构模型，在miniF2F数学证明基准上实现了100%的饱和——这是该基准自发布以来，首次有模型交出的满分答卷。更令人意外的是，它的训练成本仅为同类模型（如DeepSeek-Prover-V2）的七十五分之一。

Leanstral 1.5的核心技术路径是“组合拳式”训练：先在海量形式化证明语料中执行mid-training（中期预训练），让模型理解Lean语言的语法与推理模式；随后进行监督微调（SFT），用高质量的一步证明（single-step proof）对齐输出；最后引入基于CISPO（Critic-Instructed Self-Play Optimization）的强化学习阶段，让模型在自我对弈中迭代策略。CISPO本质上是将批评模型（critic）的反馈作为指令，指导生成器优化证明搜索空间，相比传统的PPO，它在稀疏奖励下的收敛效率显著提升。

在更难的PutnamBench（普特南数学竞赛题目）上，Leanstral 1.5成功解决了587道题（共672道），FATE-H（人类形式化证明评估）达到87%准确率，FATE-X（跨领域泛化评估）达到34%，均为当前最佳（SOTA）。值得注意的是，34%的FATE-X意味着模型能将学到的证明模式迁移到未见过的数学分支上，这比单纯的“背题”更难。

真正体现“实用化”的是智能体式证明能力。Leanstral 1.5被赋予在开源仓库中自主探索、修改代码并验证正确性的能力。在57个知名Lean仓库（包括mathlib、Lean4、batteries等）的测试中，模型自动发现了5个此前未被报告的真实bug。例如，在一个库的`List.map`实现中，边界条件处理缺失导致空列表时返回错误类型——这种错误对人工审查来说极易漏掉，但形式化验证模型通过类型推导和定理检查精准捕获。这意味着，形式化验证不再只局限于“写出证明”，而是能主动发现软件缺陷。

成本优势同样关键。1/75的推理成本（按总参数与激活参数估算）来源于MoE的稀疏计算：每次推理只有6B参数参与运算，而119B参数作为“知识底座”被选择性激活。Mistral AI通过HuggingFace和免费的API（LeanChat）向开发者开放模型，降低使用门槛。对于追求代码正确性的团队，尤其是金融、航天、自动驾驶等关键领域，Leanstral 1.5提供了一条“用AI自动补全形式化验证”的可行路径。

趋势判断：Leanstral 1.5证明了“小激活参数+大知识储备”在形式化验证领域的有效性。未来，更多团队可以凭借类似思路，用极低成本在专业领域构建专用证明模型。对开发者而言，主动引入形式化验证工具（如Lean）并配合AI辅助，将成为代码质量保障的下一个必选项。