Mistral 的 Leanstral 1.5 强化形式数学与找 Bug 能力

关键信息

Mistral 表示，Leanstral 1.5 主要通过中期训练、监督微调和强化学习来训练数学能力。在一次实测中，它扫描了 57 个开源仓库，并据称发现了 5 个此前未知的漏洞，其中包括 Rust 库 varinteger 中的一个溢出问题。

资讯摘要

Mistral AI 发布了 Leanstral 1.5，这是一款用于 Lean 4 形式验证的免费开源模型。Lean 4 主要用于正式验证数学证明和软件正确性，因此这款模型的目标不是生成开放式文本，而是执行需要严格逻辑推理的任务。Mistral 表示，该模型在 miniF2F 基准上达到 100%，这个基准覆盖了从高中水平到数学奥林匹克难度的问题。它还在 PutnamBench 上解出了 672 道题中的 587 道，而 PutnamBench 基于 Putnam 数学竞赛题目。

对于 FATE-H 和 FATE-X 这两个代数基准，Mistral 称 Leanstral 1.5 分别取得了 87% 和 34% 的领先成绩，这些任务涉及群论、环论等研究生到博士级内容。除了数学能力之外，该公司还表示，这个模型也能帮助进行代码验证。在一次实测中，它检查了 57 个开源仓库，并发现了 5 个此前未知的漏洞，其中包括 Rust 库 varinteger 的一个溢出问题。Mistral 还表示，该模型可通过 Hugging Face 和免费 API 使用，其训练流程包含中期训练、监督微调和强化学习。

资讯正文

Mistral 的开源 Leanstral 1.5 在形式化数学基准测试中表现出色，并能在代码中发现真实漏洞

Mistral AI 发布了 Leanstral 1.5，这是一款用于 Lean 4 编程语言形式化验证的免费开源模型（Apache 2.0 许可证）。Lean 4 的设计目标是对数学证明和软件正确性进行形式化验证。

Mistral 表示，这个模型在 miniF2F 上达到了 100%，该形式化数学基准覆盖从高中水平到数学奥林匹克难度的问题。在 PutnamBench 上，它解决了 672 道来自 Putnam 数学竞赛的问题中的 587 道。至于代数基准 FATE-H 和 FATE-X，这两项测试面向群论、环论等领域的硕士和博士级任务，该模型分别取得了 87% 和 34% 的最高结果。

该模型主要针对数学训练，但 Mistral 表示，它在代码验证方面也表现良好。在一次实际测试中，它扫描了 57 个开源仓库，并发现了 5 个此前未知的漏洞，其中包括 Rust 库 varinteger 中一个溢出漏洞。该模型可通过 Hugging Face 和一个免费 API 获取。训练过程包括中期训练、监督微调和强化学习。

来源与参考

1. 原始链接
2. Mistral's open-source Leanstral 1.5 aces formal math benchmarks and catches real bugs in code