Mistral AI开源数学证明专用模型Leanstral 1.5 算力成本仅为竞品1%

欧洲AI企业Mistral AI于2026年7月推出面向数学形式化证明的专用大模型Leanstral 1.5，该模型适配Lean4程序语言，总参数119B、推理阶段仅激活6B参数，以Apache-2.0许可完全开源，在miniF2F基准测试中验证集、测试集均达100%完成率，算力成本仅为同类型竞品的1%，多项性能指标刷新行业纪录。

数学形式化证明是人工智能进入硬核科研领域的核心关卡：要实现符合学术规范的零误差定理推导，此前行业普遍需要调用参数规模超百亿的大模型，单题推理成本高达数十美元，极高的使用门槛让多数科研团队难以负担。Mistral AI本次推出的Leanstral 1.5，直接从架构层面破解了性能与成本不可兼得的行业难题。

Leanstral 1.5是专门针对Lean4形式化语言优化的专用模型，总参数规模达到119B，但采用了Mistral自研的稀疏激活技术，推理过程中仅需要激活6B参数即可完成全部运算，在保留大规模参数模型的知识储备和推理能力的同时，将推理所需的算力资源压缩到了常规百亿参数模型的二十分之一。

该模型以Apache-2.0许可完全开源，所有机构和个人均可免费商用、修改和二次分发，不存在任何版权限制，这一许可规则也为后续开发者基于模型做领域适配扫清了障碍。