精选理由
Mistral 新模型 Leanstral 1.5 专攻形式化验证，能自动找出代码漏洞，数学基准也比同类强。
Mistral AI 发布了 Leanstral 1.5，这是一个用于 Lean 4 形式化验证的开源模型。该模型在多个形式化数学基准测试中取得了领先成绩，例如在 miniF2F 测试中准确率达到 60%，超过此前的最佳模型。此外，Leanstral 1.5 在扫描 57 个开源代码仓库时，成功发现了 5 个此前未知的 bug。这些发现展示了该模型在数学证明和代码正确性验证方面的实用价值。
AI 翻译 · 中文
Mistral AI 发布了 Leanstral 1.5，这是一个用于 Lean 4 形式化验证的开源模型。该模型在多个形式化数学基准测试中取得了领先成绩，例如在 miniF2F 测试中准确率达到 60%，超过此前的最佳模型。此外，Leanstral 1.5 在扫描 57 个开源代码仓库时，成功发现了 5 个此前未知的 bug。这些发现展示了该模型在数学证明和代码正确性验证方面的实用价值。
Mistral AI released Leanstral 1.5, an open-source model for formal verification in Lean 4. Beyond math, the model found five previously unknown bugs while scanning 57 open-source repositories. The article Mistral's …