研究团队由香港科技大学、中国科学院软件研究所、西安电子科技大学和重庆大学组成，开源了一系列形式化推理与验证大模型，仅用7B参数即可在相关任务上达到与671B参数的DeepSeek-R1相当的水平。
该研究通过分层拆解形式化验证任务，将任务细化为六个子任务，并通过大规模数据训练，展示了大模型在形式化证明写作上的显著提升，尤其是在未经微调的情况下，通用指令大模型也能取得较好的效果。
研究还发现，通过微调，大模型在形式化任务上的表现大幅提升，特别是在有限数据集上，微调后的模型能够显著提高准确率，表明大模型具备较强的能力迁移能力。
