近日，Mistral AI正式推出专为数学形式化证明语言Lean4设计的开源模型Leanstral1.5。该模型以Apache-2.0许可协议开放，拥有119B的总参数量但仅激活6B参数，在保持高性能的同时大幅压低了使用成本。
在权威的miniF2F形式数学基准测试中，Leanstral1.5在验证集和测试集上均拿下100%的完成率；面对极具难度的PutnamBench数学竞赛题库，它从672道Lean4问题中成功解答587道。在抽象代数领域的FATE系列测试中，该模型同样展现出统治力——硕士级别FATE-H达成率高达87%，博士级别FATE-X也达到34%，刷新了该类模型的历史纪录。
成本优势更是令人瞩目：在PutnamBench中，Leanstral1.5求解单题平均仅需4美元，而对比模型Seed-Prover1.5的开销超过300美元，Aleph Prover也在54至68美元之间，极大降低了科研试错门槛。实际代码审查场景中，该模型对57个代码库进行检测，成功识别出47个违规属性，其中11个经核实为真实缺陷，更有5个漏洞此前从未在GitHub上被报告过，充分验证了其在程序验证与安全审查中的实战价值。
随着Leanstral1.5的开源，数学形式化证明的辅助工具正变得前所未有的高效与亲民，科研人员有望从繁重的计算核对中解放出来，将更多精力聚焦于核心科学问题的突破。
原创文章，作者：李森，如若转载，请注明出处：https://www.kejixun.co/article/756902.html
