Mistral 的 Leanstral 1.5 强化形式数学与漏洞发现
The Decoder··作者 Matthias Bastian
关键信息
Mistral 表示，该模型的训练过程包括中期训练、监督微调和强化学习。在一次实测中，它扫描了 57 个开源仓库，并据称发现了 5 个此前未知的漏洞，其中包括 Rust 库 varinteger 中的一个溢出问题。
资讯摘要
Mistral AI 发布了 Leanstral 1.5，这是一个面向 Lean 4 编程语言的免费开源模型，目标是支持形式化验证。Lean 4 常用于机械化检查数学证明和软件正确性，因此它特别适合那些不能只靠普通测试来保证正确性的场景。根据 Mistral 的说法，该模型在 miniF2F 基准上达到了 100%，这个基准覆盖了从高中数学到奥赛难度的问题。它还在 PutnamBench 上解出了 672 题中的 587 题，而这个基准来自 Putnam 数学竞赛题目。
对于代数类任务，Mistral 表示该模型在 FATE-H 和 FATE-X 上分别取得 87% 和 34% 的成绩，这两个基准被描述为抽象代数和交换代数中的高难度与专家级任务。除了数学能力之外，Mistral 还称该模型在代码验证方面表现良好。在一次实际测试中，Leanstral 1.5 扫描了 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 获取。训练过程包括中期训练、监督微调和强化学习。
来源与参考