7B开源大模型助力形式化验证

香港科技大学等高校和研究机构联合开源一系列形式化推理与验证大模型。这些模型仅用7B参数量即可达到671B的DeepSeek-R1同等水平。研究团队构建了18000对高质量指令-响应对的数据集，并将形式化验证任务细分为六个子任务。通过微调，小模型性能显著提升，甚至超过大规模模型。此外，微调后的模型在其他任务上也表现出色，平均性能提升1.37%至5.15%，有助于降低形式化验证门槛。
来源：https://mp.weixin.qq.com/s/oyhICTRo2fJL5MZkDrutXg