定理证明也开始卷成本：Mistral开源Leanstral 1.5，每题约4美元

据 动察 Beating 监测，Mistral AI 开源 Leanstral 1.5，一款面向 Lean 4 形式化证明的模型。模型总参数量 1190 亿，激活参数约 65 亿，采用 Apache-2.0 协议，并提供免费 API 访问。 官方评测显示，Leanstral 1.5 在 PutnamBench 672 道题中解出 587 道；在抽象代数基准 FATE-H 和 FATE-X 上分别达到 87% 和 34%，刷新同类模型最佳表现。 Leanstral 1.5 在 PutnamBench 上的平均解题成本约为 4 美元，低于此前部分系统数十至数百美元的成本。随着单题 token 预算提高，它的解题数量持续增加；在 AVL 树复杂度证明中，模型经过超过 270 万 token 推理和 22 次上下文压缩，最终完成相关证明。 除数学证明外，Leanstral 1.5 还被用于代码验证。团队在 57 个开源 Rust 仓库中发现 11 个真实 bug，其中 5 个此前未被报告。

「查看原文」