Mistral AI 发布了一款名为 Devstral 的大型语言模型，该模型专为应用程序开发（Vibe 编码）而设计，并针对形式化代码验证进行了优化。Devstral 有望用于创建 AI 助手，这些助手不仅可以生成代码，还能确保代码无误。
Devstral 成为首个支持 Lean 4 编程语言及其相关数学证明验证工具包的开源模型。Lean 4 能够以数学方式证明代码的正确性及其与规范的符合性，这在 vibe 编码的背景下，可以确认 AI 模型生成的代码能够准确实现其预期功能。
该模型涵盖 119 亿个参数（每个 token 激活 6.5 亿个参数），考虑 256 个 token 的上下文，并以 Apache 2.0 许可证发布。包含 Leanstral 的可下载压缩包大小为 121 GB，适用于本地系统。vllm、transformers 和 SGLang 库可用于本地执行。
该模型可用于开源的 mistral-vibe 代理的 vibe 开发，并可与 Aeneas 工具包集成以验证 Rust 代码。它接受文本和图像作为输入参数，并仅输出文本。该模型支持图像内容分析。
为了评估人工智能模型的性能，并兼顾形式化代码验证的质量和数学证明的编写，我们开发了一套新的 FLTEval 基准测试套件。在测试中，Leanstral 模型显著优于现有的开源模型 Qwen3.5 397B-A17B、Kimi-K2.5 1T-A32B 和 GLM5 744B-A40B。它与 Anthropic 的 Claude Haiku 4.5 和 Claude Sonnet 4.6 表现相近，但落后于 Claude Opus 4.6 模型。具体而言，Opus 模型得分 39.6 分，而 Leanstral 在单次测试中获得 21.9 分，16 次测试中获得 31.9 分。使用 Opus 的成本为 1650 美元，而 Leanstral 在单次测试中的成本为 18 美元，16 次测试的成本为 290 美元。俳句得了 23 分，价格为 184 美元；十四行诗得了 23.7 分，价格为 549 美元。
来源： opennet.ru
