Mistral AI 近日开源了 Leanstral 1.5 模型，该模型专为 Lean 4 形式化证明领域设计，总参数量达 1190 亿，激活参数约 65 亿，采用 Apache-2.0 协议，并提供免费 API 访问。作为 Mistral AI 在数学推理方向的最新成果，Leanstral 1.5 旨在通过大规模语言模型提升定理证明和代码验证的效率。
正文解读
官方评测显示，Leanstral 1.5 在 PutnamBench 的 672 道题目中成功解出 587 道；在抽象代数基准 FATE-H 和 FATE-X 上分别达到 87% 和 34%，刷新了同类模型的最佳表现。值得注意的是，该模型在 PutnamBench 上的平均解题成本仅约 4 美元，大幅低于此前部分系统数十至数百美元的成本。随着单题 token 预算的提高，它的解题数量持续增加；在 AVL 树复杂度证明中，模型经过超过 270 万 token 推理和 22 次上下文压缩，最终完成了相关证明。
除了数学证明，Leanstral 1.5 还被用于代码验证任务。团队在 57 个开源 Rust 仓库中发现了 11 个真实 bug，其中 5 个此前未被报告。这一成果展示了形式化模型在软件安全性检测中的潜力，也反映出开源社区对自动化验证工具的需求。Leanstral 1.5 以较低的计算成本在多项基准上取得领先，或将对现有形式化验证工具链形成补充。
Leanstral 1.5 的开源和免费 API 访问将降低用户使用门槛，推动数学定理证明和软件验证领域的进一步探索。不过，形式化证明的实际应用仍面临挑战，例如复杂场景下 token 消耗量极大，以及模型结果的可靠性需要持续验证。开发者和研究者在部署时需结合具体任务进行权衡。
原创文章，作者：admin，如若转载，请注明出处：https://www.23btc.com/197414/
