Leanstral 1.5：为所有人提供丰富的证明

Leanstral 1.5 在多个形式数学基准上取得显著成绩。据 Mistral AI 官方博客，该模型在 miniF2F 上达到 100%（验证集和测试集），在 PutnamBench 上解决 587/672 题，并在 FATE-H 和 FATE-X 上分别获得 87% 和 34% 的新最优结果。这些基准覆盖从高中到博士水平的数学问题。

与现有模型相比，Leanstral 1.5 在 PutnamBench 上比 Seed-Prover 1.5（高设置）多解决 7 题，但成本大幅降低：每个问题约 4 美元，而 Seed-Prover 估计超过 300 美元。闭源模型 Aleph Prover 成本为 54-68 美元/题，但排名更高。

测试时扩展性方面，随着 token 预算从 50k 增至 4M，PutnamBench 解决数从 44 单调升至 587，展示了模型在长推理链中的持续能力。

Leanstral 1.5 采用三阶段训练：中期训练、监督微调和基于 CISPO 的强化学习。训练在两个 RL 环境中进行：多轮环境（模型提交证明并接收 Lean 编译器反馈）和代码代理环境（模型像开发者一样编辑文件、运行 bash 命令，并使用 Lean 语言服务器实时检查目标）。

代码代理环境使模型能够处理长时任务，如完成部分证明、构建辅助引理，并通过多次上下文压缩持续工作。最终通过 SafeVerify 的分支验证正确性。

模型总参数 119B，但活跃参数仅 6B，采用 Apache-2.0 许可，完全开源。

尽管主要针对数学训练，Leanstral 1.5 在代码验证上表现出色。在 57 个开源仓库的测试中，它发现了 5 个此前未知的 bug，包括 Rust 库 varinteger 中的溢出问题。

案例研究展示了 AVL 树时间复杂度证明：模型使用超过 270 万 token 和 22 次压缩，通过结构归纳和单子时间跟踪，证明了真实实现的 O(log n) 高度保证。

在 FLTEval 基准上，pass@1 从 21.9 提升至 28.9，pass@8 从 31.9 提升至 43.2，超过了 Opus 4.6 的 39.6，且成本仅为后者的七分之一。

Leanstral 1.5 通过 Hugging Face 和免费 API 提供，并开源了 FLTEval 基准。这降低了形式验证的门槛，使研究人员和开发者能够免费使用。

Mistral AI 强调，该模型在开放性和实用性之间取得了平衡，使严格的形式方法在现实世界中变得有效且实用。