Mistral 发布 Leanstral 1.5：6B 激活参数的形式化验证模型

Mistral 发布 Apache-2.0 许可的 Leanstral 1.5，总参数 119B、激活参数 6B，在 miniF2F 上达到 100%，PutnamBench 解出 587/672 题，FATE-H 与 FATE-X 分别取得 87% 和 34% 的 SOTA。该模型经 mid-training、监督微调与 CISPO 强化学习三阶段训练，在 57 个代码仓库中发现 5 个此前未知的 bug，FLTEval 上 pass@1 从 21.9 提升至 28.9。模型已完全开源，可通过 Hugging Face 和免费 API 使用。