欧洲人工智能公司mistral ai近日正式发布专用于数学形式化证明的新型模型——leanstral 1.5。该模型深度适配lean4编程语言，整体参数量达1190亿（119b），但在实际推理过程中仅动态激活60亿（6b）参数，以极低的算力消耗展现出卓越的定理证明能力，并依据apache-2.0许可证完全开源。
☞☞☞AI 智能聊天, 问答助手, AI 智能搜索, 多模态理解力帮你轻松跨越从0到1的创作门槛☜☜☜
在关键评测基准中，Leanstral 1.5表现极为亮眼。其在miniF2F形式化数学基准的验证集与测试集上均实现100%的命题完成率；在涵盖672道Lean4编码题目的PutnamBench数学竞赛基准中，成功求解587题。针对抽象代数方向的FATE系列评测，硕士难度的FATE-H任务达成率为87%，博士级FATE-X任务达成率达34%，两项指标均刷新当前公开模型的最佳纪录。
单题推理成本仅为同类产品约1%
尤为突出的是Leanstral 1.5的成本效率优势。在PutnamBench数据集上，其平均每道题目的推理开销仅为4美元，而字节跳动推出的Seed-Prover 1.5需耗费逾300美元，Aleph Prover则介于54至68美元之间。换言之，在同等任务负载下，Leanstral 1.5的推理支出约为最强竞品的1%，显著降低了数学形式化验证落地的经济门槛。
在真实工程环境中，Leanstral 1.5亦展现出强大实用性。模型对57个开源代码库进行扫描后，共识别出47处潜在违规属性，其中11项被确认为真实存在的代码缺陷，更有5个属首次发现、此前从未在GitHub平台被披露的新漏洞。从高难度数学竞赛题目求解，到复杂软件系统的可靠性验证，这一模型持续印证着一个趋势：模型参数量已非决定性能的唯一要素，精准、高效的参数激活机制，正成为推动AI推理走向工业级应用的核心突破口。
