近日，Leanstral团队正式开源发布形式化验证模型Leanstral 1.5。该模型采用Apache-2.0协议，拥有1190亿总参数量与60亿活跃参数，专为Lean 4语言设计，旨在降低形式化方法的实践门槛。训练过程涵盖中期训练、监督微调及CISPO强化学习三阶段，模型通过在多轮定理证明与代码代理环境中交互学习，逐步掌握复杂证明推导与文件系统操作能力。评测数据显示，Leanstral 1.5在多项权威基准测试中取得突破性进展：全面饱和miniF2F数据集，在PutnamBench中成功解题587/672，并在FATE-H与FATE-X基准测试中分别以87%和34%的正确率刷新纪录。相较于同类大型模型，其单题推理成本仅约4美元，且展现出优异的测试时扩展性。除数学证明外，该模型在代码验证领域同样表现卓越，不仅严格证明了AVL树的时间复杂度，还通过自动化流水线在57个开源仓库中定位出5个此前未公开的隐藏漏洞。目前，模型权重已完整托管至Hugging Face平台并开放免费API接口。此次发布标志着形式化验证正从学术理论走向工程实践，为开发者提供高效、低成本的自动化程序正确性保障方案，有力推动可信软件技术的普及与应用。