IT之家7月6日消息，欧洲人工智能企业Mistral AI当地时间本月2日宣布推出面向数学形式化证明程序语言Lean4的Leanstral1.5模型。该模型总共拥有119B参数，激活6B参数，以Apache-2.0许可开源。
Mistral AI表示，Leanstral1.5模型在miniF2F形式数学基准测试的验证集和测试集上均实现了100%的完成率；在PutnamBench数学竞赛问题集的672道Lean4问题中可解决587道；对于FATE系列抽象代数基准测试，其在硕士级FATE-H上实现了87%的达成率，博士级FATE-X达成率则为34%，均为最佳表现。
Mistral AI强调了新模型的成本优势：对于PutnamBench数据集中的问题，Leanstral1.5的平均解决开支仅有4美元，而Seed-Prover1.5需要300美元以上，Aleph Prover也需要54~68美元。
而在实际场景应用中，Leanstral1.5在测试的57个代码库中标记了47个违规属性，其中11个指向了真实的缺陷，包括5个此前未在GitHub上被报告过的问题。
