欧洲人工智能领域迎来重要突破，专注于数学形式化证明的专用模型Leanstral 1.5由Mistral AI公司正式发布。这款模型专为Lean4程序语言设计，总参数规模达1190亿，但在实际推理过程中仅激活60亿参数，通过这种创新方式显著降低了计算开销，同时保持了强大的证明能力。更值得关注的是，该模型采用Apache-2.0许可协议完全开源，为全球数学和人工智能研究者提供了重要工具。
在性能测试方面，Leanstral 1.5展现出卓越表现。在miniF2F形式数学基准测试中，该模型在验证集和测试集上均实现100%完成率；面对PutnamBench数学竞赛中的672道Lean4问题，成功解决587道；针对抽象代数领域的FATE系列基准测试，硕士级FATE-H达成率87%，博士级FATE-X达成率34%，两项指标均刷新现有纪录。这些数据充分证明其在复杂数学证明任务中的领先地位。
成本优势是该模型的另一大亮点。在PutnamBench数据集测试中，Leanstral 1.5平均每题解题成本仅需4美元，而字节跳动的Seed-Prover 1.5需要超过300美元，Aleph Prover的解题成本也在54至68美元之间。这意味着在相同工作量下，Leanstral 1.5的推理成本仅为最强竞品的百分之一左右，这种显著的成本差异为数学形式化证明技术的大规模应用扫清了经济障碍。
实际应用场景中，Leanstral 1.5同样表现出色。在针对57个代码库的测试中，该模型成功标记出47个违规属性，其中11个指向真实存在的代码缺陷，更令人惊讶的是发现5个此前未在GitHub上报告过的新问题。从数学竞赛到软件工程验证，这款模型证明参数规模并非决定AI能力的唯一因素，高效激活参数才是将推理能力转化为实际应用的关键所在。
