Mistral 发布 Leanstral 1.5：形式化证明模型开始进入真实代码验证和 Agent 工作流

法国 Mistral AI 在 7 月 2 日发布 Leanstral 1.5。它不是常见的通用聊天模型，而是面向 Lean 4 形式化证明和代码验证的专门模型。Mistral 称它采用 Apache-2.0 许可，119B 总参数、6B 激活参数，并通过 Hugging Face 和免费 API endpoint 提供。

这条前沿值得关注，是因为形式化证明正在从少数学术和高可靠系统场景，慢慢进入 AI Agent 的工程工作流。以前我们让 Agent 写代码，主要靠测试和人工 review；如果证明模型足够可用，未来它可以帮助验证关键性质，甚至在开源仓库里发现测试难以覆盖的 bug。

从数学证明扩展到代码验证

Mistral 的摘要里给出几个关键结果：Leanstral 1.5 在 miniF2F 上达到饱和，在 PutnamBench 中解决 587/672 个问题，在 FATE-H 和 FATE-X 上达到新的领先结果，还能在真实代码验证里发现 bug。

它的训练流程分为三段：mid-training、supervised fine-tuning，以及使用 CISPO 的 reinforcement learning。更重要的是，它有两个强化学习环境：一个面向多轮 theorem proving，另一个让模型像开发者一样在原始文件系统里编辑文件、运行 bash 命令，并使用 Lean language server 查看目标、错误和类型信息。

这说明 Mistral 并不只是训练一个会补全证明的模型，而是在训练一个能在证明工程环境里循环行动的 Agent。

长预算推理让证明任务继续推进

Mistral 的文章展示了 Leanstral 1.5 在 PutnamBench 上的 test-time scaling：随着每次尝试的 token budget 从 25k 提升到 4M，性能继续上升。文章还提到一个 AVL-tree 证明案例，运行超过 270 万 token，经历 22 次 compaction。

这与普通问答模型的体验不同。证明和代码验证经常需要反复尝试、读错误、补引理、改文件，再继续尝试。一个模型如果只能在短上下文里给一次漂亮答案，离真正工程可用还很远；能长时间保持目标、持续修正，才接近 Agent 工作。

自动发现开源仓库中的隐藏缺陷

Leanstral 1.5 的一个案例是 bug discovery。Mistral 构建了一个自动化 pipeline：Aeneas 把 Rust 代码翻译成 Lean，Leanstral 推断用户意图并生成正确性性质，然后尝试证明。如果四次都失败，再尝试证明反面。

在 57 个测试仓库中，这个流程标记了 47 个 violated properties，其中 11 个指向真实 bug，5 个此前没有在 GitHub 上报告。文章举了一个 zigzag decoding 的 sign function 例子：当输入 Std.U64.MAX 时，表达式溢出，debug 模式崩溃，release 模式静默损坏。

这个方向对软件工程很有意义。测试往往只能覆盖样例，而形式化验证尝试证明性质本身；当 AI Agent 能协助生成性质、运行证明、定位失败原因，代码审核会多出一种更硬的工具。

对普通开发者的实际启发

现在 Leanstral 1.5 还不是普通项目的默认工具，但它给出了一个清晰趋势：AI 编程不应该只停留在“写得快”，还要进入“能证明、能验证、能发现隐藏边界”的阶段。

对 HelloAIFlow 的读者来说，可以先把这个能力理解为未来的高阶验收环节。平时用 Codex 或 Claude Code 生成代码后，仍然要跑测试、查权限、审查数据边界；将来某些关键模块也许可以交给形式化证明 Agent 做进一步验证。AI 开发的下一步，不只是生成更多代码，而是生成更可靠的代码。

参考来源

• Leanstral 1.5: Proof Abundance for All
• Lean theorem prover