欧洲人工智能企业Mistral AI近日宣布推出一款名为Leanstral 1.5的新型模型，该模型专为数学形式化证明程序语言Lean 4设计。作为一款开源模型，Leanstral 1.5以Apache-2.0许可协议发布，其总参数规模达119B，激活参数为6B，为数学证明领域提供了强大的计算支持。
在性能测试中，Leanstral 1.5展现了卓越的数学推理能力。在miniF2F形式数学基准测试中，该模型在验证集和测试集上均实现了100%的完成率，证明了其在数学证明任务中的高度可靠性。在PutnamBench数学竞赛问题集的672道Lean 4问题中，Leanstral 1.5成功解决了587道，显示出其应对复杂数学问题的强大实力。在FATE系列抽象代数基准测试中，该模型在硕士级FATE-H上达到了87%的达成率，在博士级FATE-X上则取得了34%的达成率，两项成绩均为当前最佳表现。
除了性能优势，Leanstral 1.5还具备显著的成本效益。Mistral AI指出，在处理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上被报告过，凸显了Leanstral 1.5在代码审查和缺陷检测方面的独特价值。这一成果不仅为开发者提供了更高效的代码优化工具，也为数学证明领域的实际应用开辟了新的可能性。
