Leanstral 1.5：人人可用的形式化证明工具

Leanstral 1.5 是一款免费、Apache-2.0 许可的模型，拥有 119B 总参数和 6B 活跃参数，在形式化验证方面取得重大突破：在 miniF2F 上达到饱和，解决 PutnamBench 中 587/672 的问题，并在 FATE-H (87%) 和 FATE-X (34%) 上实现最优结果。通过中期训练、监督微调和基于 CISPO 的强化学习，它在基于代理的证明工程和真实代码验证中表现出色，在 57 个测试仓库中发现了 5 个先前未知的 bug。该模型完全开源，可通过 Hugging Face 和免费 API 获取。