Mistral AI 发布 Leanstral 1.5：开源形式验证模型实现性能飞跃
原标题：Leanstral 1.5: Proof Abundance for All
AI 摘要
Mistral AI 发布了 Leanstral 1.5，这是一个免费、Apache-2.0 许可的模型，拥有 119B 总参数和 6B 激活参数，在形式验证方面实现了重大性能提升，完全饱和 miniF2F，解决 587/672 个 PutnamBench 问题，并在 FATE-H 和 FATE-X 上达到新的最先进水平。该模型通过三阶段训练（中期训练、监督微调和基于 CISPO 的强化学习）在代理式证明工程和真实代码验证中表现出色，在 57 个仓库中发现了 5 个此前未知的 bug。Leanstral 1.5 已完全开源，可通过 Hugging Face 和免费 API 获取，使 Lean 4 中的实际证明工程更加普及。
正文节选
Thinking Summary Leanstral 1.5, a free Apache-2.0 licensed model with 6B active parameters, delivers a major performance upgrade in formal verification, saturating miniF2F, solving 587/672 PutnamBench problems, and achieving state-of-the-art results on FATE-H (87%) and FATE-X (34%). Trained through mid-training, supervised fine-tuning, and reinforcement learning with CISPO, it excels in agentic proof engineering and real-world code verification, uncovering 5 previously unknown bugs across 57 rep