标题：开源模型Leanstral 1.5：119B参数仅6B活跃，成本1/75实现形式化验证实用化
摘要：Mistral AI发布Leanstral 1.5，Apache-2.0许可，119B总参数仅6B活跃。在miniF2F上达到100%饱和，PutnamBench解决587/672题，FATE基准创SOTA。训练采用mid-training、SFT及CISPO强化学习，具备智能体式证明能力，在57个开源仓库中发现5个未知bug。成本仅为同类模型的1/75，已通过HuggingFace和免费API开放使用，标志AI形式验证进入实用阶段。

形式化验证长期以来是软件工程中的“圣杯”——它能数学层面证明代码行为正确，但高昂的人工成本和专业门槛让绝大多数项目望而却步。Mistral AI发布的Leanstral 1.5正在打破这一僵局。这款Apache-2.0许可的开源模型以稀疏激活架构（119B总参数、仅6B活跃）和仅同类模型1/75的成本，在多项定理证明基准上刷新记录，并实际发现5个真实代码漏洞，意味着AI驱动的形式化验证已从学术演示走向工程实用。

模型训练技术本身亦有看点。Leanstral 1.5经历了中期训练（mid-training）、监督微调（SFT）以及基于CISPO的强化学习三个阶段。CISPO（一种Constrained Importance Sampling Policy Optimization的变体）允许模型在证明搜索空间中更高效分配计算资源，这是其能以极低活跃参数（6B）获得强大推理能力的关键。相较于传统稠密模型需要激活全部参数，稀疏架构在保证质量的同时大幅降低了推理成本和延迟，使得免费API开放成为可能。

基准测试成绩几乎“饱和”。在miniF2F（数学竞赛证明库）上，Leanstral 1.5获得了100%的解决率，正式宣告该基准对于当前模型已无挑战。更具说服力的是PutnamBench（普特南数学竞赛题目），它包含672道高难度题目，模型解决了587道，覆盖率达87.4%。在面向工业代码的FATE基准上，Leanstral 1.5在FATE-H（正确性验证）和FATE-X（漏洞检测）两个子项上分别达到87%和34%，均创下公开模型的最佳成绩（SOTA）。这里的差距——34%对87%——恰好揭示了形式化验证的两个维度：验证“代码满足规范”相对容易，而主动发现隐藏bug仍具挑战。

最令人兴奋的是真实世界检测成果。研究团队用Leanstral 1.5以智能体方式主动探索57个开源仓库，自动生成证明并交叉验证，最终在多个成熟项目中发现了5个此前未被报告的错误。这意味着该模型不仅能理解已有证明，还能像人类专家一样“阅读”代码、提出假设、构造证明链。这5个bug的发现流程无需人工介入，完整自动化，标志着AI形式化验证从“辅助工具”向“自主检查”的跨越。

结合极低的成本（仅为同类模型的1/75，比如与Azure、GPT-4等专有证明服务的推理费用对比），Leanstral 1.5给出了一个清晰的实用化路径：开发者可直接通过HuggingFace下载模型权重（Apache-2.0许可无商业限制），或使用Mistral AI提供的免费 API 进行集成。建议关注码安全或要求高可靠性的团队（如金融、航空航天、区块链合约）优先将其嵌入CI/CD流水线，作为代码审查的自动补充。可以预见，形式化验证的普及不再是五年十年后的远景，而是今明两年即可落地的现实。