Mistral AI 发布 Leanstral 1.5：Apache-2.0 许可的 Lean 4 代码代理模型，解决 PutnamBench 672 道问题中的 587 道

Mistral AI 今日发布了 Leanstral 1.5，这是一款专为 Lean 4 打造的代码代理模型，主要面向自动定理证明和证明工程。模型权重以 Apache 2.0 许可开源，同时提供了免费的 API 端点 leanstral-1-5。

Leanstral 1.5 是之前 Leanstral-2603 模型的升级版，属于 Mistral Small 4 系列。Lean 4 是一种证明助手，能够机械地检查每一步逻辑，可表达完美空间等对象以及 Rust 片段的性质。

架构方面，Leanstral 1.5 采用混合专家（MoE）设计，将每个令牌路由至少数专业子网络，从而在保持大容量的同时降低计算量。模型共有 128 个专家，每令牌激活 4 个，总参数量 119B，每令牌激活 6.5B，上下文长度 256k。输入支持文本和图像，输出仅为文本。

训练分为三个阶段：中期训练、监督微调，以及使用 CISPO 的强化学习。两个强化学习环境塑造了模型的代理行为：在多轮环境中，模型需给定定理并尝试证明或反驳，根据 Lean 编译器反馈逐步迭代；在代码代理环境中，模型在原始文件系统中工作，可编辑文件、运行 bash 命令，并使用 Lean 语言服务器实时获取目标、错误和类型信息，从而完成部分证明、构建辅助引理，并通过上下文压缩维持长任务。正确性由 Mistral 的 SafeVerify 分支验证。

性能方面，Leanstral 1.5 在 miniF2F 验证集和测试集上均达到 100%，解决了 PutnamBench 中 672 道问题中的 587 道。在 FATE-H 和 FATE-X 代数基准上达到新 SOTA（87% 和 34%）。在 FLTEval 上，pass@1 从 21.9 提升至 28.9，pass@8 从 31.9 提升至 43.2，且以七分之一成本超越 Opus 4.6。PutnamBench 上，Leanstral 以每问题约 4 美元的成本比 Seed-Prover 1.5 high 设置多解决 7 道问题，而后者每问题成本约 300 美元以上。测试时缩放是模型的核心特性，提高每个尝试的令牌预算可提升性能。

实际应用中，Leanstral 证明了真实 AVL 树的 O(log n) 时间复杂度，并发现了开源代码中的错误：通过 Aeneas 将 Rust 翻译为 Lean，自动推断用户意图并生成正确性属性，在 57 个仓库中标记了 47 个违反属性和 11 个真实错误，其中 5 个先前未报告。开发团队可使用它完成部分证明、自动生成函数正确性属性，或通过证明/反驳推断不变量来压力测试 Rust 代码。

使用方面，最简单的途径是 Mistral Vibe CLI，在免费计划中启用实验模型即可。也支持自托管，需要 vLLM 0.24.0 及以上版本，并提供了详细的部署命令。通过 OpenAI 兼容客户端调用，可设置 reasoning_effort 参数。此外，还支持 OpenAI 风格的函数调用和 lean-lsp-mcp 服务器集成。