Mistral 开源形式验证 Agent：提升代码可信性

AI agents 在代码生成领域已被证明是高效的工具。然而，当我们将这些模型应用于高风险领域时，从前沿研究数学到关键任务软件，我们遭遇了一个扩展瓶颈：人工审查。手工验证所需的时间和专业知识成为工程效率的主要阻碍。

我们设想着下一代更实用的代码 agent，既能完成任务，又能根据严格的规范形式化证明其实现。与其调试由机器生成的逻辑，不如由人类指定想要的结果。今天，我们朝着这个愿景迈出了第一大步。

Introducing Leanstral

我们发布 Leanstral，这是首个为 Lean 4 设计的开源代码 agent。Lean4 是一个证明助手，能够表达复杂的数学对象（如完美离散空间）和软件规范（如 Rust 代码片段的属性）。与现有的充当大型通用模型包装器或专注于单一数学问题的证明系统不同，Leanstral 的设计高度高效（仅 6B 活跃参数），并经过训练可在现实的形式化仓库中运行。

开放且易获取：我们在 Apache 2.0 许可证下发布 Leanstral 权重，作为 Mistral vibe 中的 agent 模式，以及通过免费 API 端点。我们也会发布详细介绍训练方法的技术报告和新的评估套件 FLTEval，以超越对竞赛数学的聚焦。

高效且强大：我们为 Leanstral 使用高度稀疏的架构，并针对证明工程任务进行了优化。利用与 Lean 作为完美验证器的并行推理，Leanstral 相比现有的闭源竞品既性能优异又成本高效。

通过 MCP 升级：Leanstral 通过 vibe 支持任意 MCP，并经专门训练以在常用的 lean-lsp-mcp 上取得最佳性能。

为了反映现实证明工程场景中的实用性，我们为 Leanstral 进行了基准测试，衡量其完成 FLT 项目每个 PR 中所有形式化证明和正确定义新数学概念的能力，而不是孤立的数学问题。我们将 Leanstral 与业界领先的代码 agent（Claude Opus 4.6、Sonnet 4.6、Haiku 4.5）以及开源模型（Qwen3.5 397B-A17B、Kimi-K2.5 1T-A32B、GLM5 744B-A40B）进行对比。

Leanstral vs. OSS Models

Leanstral-120B-A6B 相比其更大的开源同行展现了显著的效率优势。虽然 GLM5-744B-A40B 和 Kimi-K2.5-1T-32B 这样的模型难以扩展，其 FLTEval 分数分别仅约 16.6 和 20.1，Leanstral 仅用单次通过就超过了它们两者。

即使是表现最强的开源竞品 Qwen3.5-397B-A17B，也需要 4 次通过才能达到 25.4 的分数。相比之下，Leanstral 用其一半的投入（pass@2）就实现了 26.3 的更高分数，并继续线性扩展，在相同成本水平下达到 29.3。

Leanstral vs. Claude Family

Leanstral 是 Claude 系列的高价值替代品，以极低的价格提供有竞争力的性能：Leanstral pass@2 达到 26.3 的分数，超过 Sonnet 2.6 点，而成本仅为 $36，相比 Sonnet 的 $549。在 pass@16 时，Leanstral 达到 31.9 的分数，轻松领先 Sonnet 8 点。虽然 Claude Opus 4.6 仍是质量领导者，但其成本高达 $1,650，比运行 Leanstral 贵 92 倍。

在基准测试中，我们使用了 Mistral Vibe 作为基础架构，评估过程中没有做任何特定的修改。

回答关于最新 Lean 版本变化的 StackExchange 问题

当破坏性变化出现在新的 Lean 发行版中时，迁移代码可能是场噩梦。我们向 Leanstral 提供了一个来自证明助手 Stack Exchange 的真实问题，关于一个脚本在 Lean 4.29.0-rc6 中神秘地停止编译（由于其新近性，我们没有用它训练）。罪魁祸首是一个改写（rw）策术，它突然无法匹配涉及简单类型别名的模式，最初定义为 def T2 := List Bool。

Leanstral 没有盲目猜测，而是付出了努力。它成功构建了测试代码来重现失败的环境，并诊断了潜在的定义相等性问题。模型正确地识别出，因为 def 创建了一个需要显式展开的刚性定义，它实际上阻止了 rw 策术查看它需要匹配的底层结构。

它提议的修复很简单：只需将 def 换成 abbrev。因为 abbrev 创建了一个透明别名，它在定义上立即等于原始类型，rw 策术就能再次完美匹配模式（L2 n）.length 在证明中。Leanstral 完成了工作并完美地向用户解释了其逻辑。

推理程序

我们从 https://www.cs.princeton.edu/courses/archive/fall10/cos441/sf/Imp.html 复制定义到 Rocq，并要求 Leanstral 转换为 Lean。它成功完成了，甚至实现了自定义记号。示例片段：

它也可以转换为 Lean，然后在只给定 Rocq 陈述（不附带证明）的情况下证明关于这种语言中程序的一些属性：

立即需要证明。今天就尝试 Leanstral。

Leanstral 从今天起对所有人可用。

Mistral Vibe 中零配置：我们已将 Leanstral 直接集成到 Mistral Vibe 中，可立即进行零配置的 vibe 编码和证明。使用 /leanstall 激活。然后要使用 Leanstral，按 Shift+Tab 直到模型显示为 Leanstral，或者使用 vibe --agent lean。

Labs API：通过我们的免费/近免费 API 端点 labs-leanstral-2603 访问模型。我们在有限的时间内保持此端点高度可访问，以收集真实反馈和可观测性数据来推动下一代验证代码模型的发展。

自己掌控权重：下载 Apache 2.0 许可的模型并在自己的机器上运行。

Documentation - Sign Up for Mistral Vibe