Mistral 发布了 Leanstral 1.5，这是一个采用 Apache-2.0 许可证的免费模型，具有 6B 活跃参数，专为形式化验证和自动定理证明而设计。

  • 在 miniF2F 基准测试中达到饱和，并解决了 PutnamBench 中的 672 个问题中的 587 个。
  • 在 FATE-H (87%) 和 FATE-X (34%) 上取得了 state-of-the-art 结果。
  • 通过 mid-training、supervised fine-tuning 以及使用 CISPO 的 reinforcement learning 进行训练。
  • 在 agentic proof engineering 期间，在 57 个测试仓库中发现了 5 个以前未知的 bug。

此发布使开发人员能够通过形式化 proof engineering 验证其软件和代码规范的正确性。