2026-07-04 02:53:25
Mistral 发布 Leanstral 1.5 用于形式化证明,成本降至约每问题 $4
据 OneMillionAI 称,Mistral AI 近期发布了 Leanstral 1.5,这是一款针对 Lean 4 的形式化证明模型,总参数量达1190亿,活跃参数量为650亿。该模型采用 Apache-2.0 许可证发布,并提供免费 API 访问。在 PutnamBench 上,Leanstral 1.5 平均每道问题的求解成本约为4美元,远低于此前每道问题成本高达数十至数百美元的系统。 Leanstral 1.5 成功解决了 PutnamBench 672道问题中的587道,在抽象代数基准 FATE-H 上达到87%,在 FATE-X 上达到34%,创下同类模型的新性能纪录。除数学证明外,Leanstral 1.5 还被应用于代码验证,在57个开源 Rust 仓库中发现了11个真实错误,其中5个此前未被报告。