标题：7B级形式化验证小模型全面开源，媲美满血版DeepSeek-R1，推动大模型与AI4Math在自然语言处理和深度学习领域的创新与发展

研究团队介绍
香港科技大学、中国科学院软件研究所、西安电子科技大学和重庆大学共同组成了一个跨学科的研究团队。该团队的核心成员包括香港科技大学的研究助理教授曹嘉伦，主要研究领域涵盖AI与软件工程（AI&SE）、人工智能测试及形式化验证等；以及中国科学院软件研究所的副研究员陆垚杰，专注于大语言模型及其应用。

形式化推理与验证的需求增长
随着DeepSeek-R1的流行和AI4Math研究的深入，大模型在辅助形式化证明写作方面的需求日益增长。作为数学推理最直接的应用场景，形式化推理与验证（formal reasoning and verification）也获得了持续关注。然而，当前的形式化推理大模型大多只针对单一形式化语言，缺乏对多形式化语言和任务场景的深度探索。

开源形式化推理大模型
近日，由香港科技大学牵头，联合中科院软件所、西安电子科技大学和重庆大学等单位，开源了一系列形式化推理与验证大模型。这些模型仅用7B参数即可在相关任务上达到671B满血版DeepSeek-R1的水平。论文标题为《从非形式化到形式化——将自然语言要求转化为可验证的形式化证明》，论文链接：[https：//arxiv.org/abs/2501.16207](https：//arxiv.org/abs/2501.16207)，Hugging Face模型链接：[https：//huggingface.co/fm-universe](https：//huggingface.co/fm-universe)。

形式化验证的发展趋势
正如Meta FAIR和斯坦福大学等机构在去年年底的立场论文中指出的，多语言形式化验证模型正成为业界发展的趋势。形式化验证不仅是计算机科学的核心问题，也是形式化数学的重要应用之一。由于其高门槛和高成本，形式化验证的普及一直受到限制。引入大模型技术有望加速验证流程，降低人力成本并提升自动验证效率。

形式化任务拆解
研究团队首先对形式化验证任务进行了分层拆解，从非形式化的自然语言输入到可验证的形式化证明或可检测的模型。在此基础上，团队将传统的端到端形式化验证流程细化为六个子任务，包括验证需求分解、形式化规约片段生成、规约补全、填空，以及代码到形式化规约的自动生成。

数据准备过程
研究团队从GitHub收集了五种形式化语言的数据，并经过一系列数据收集、清洗与整理，最终得到了14k数据用于训练微调（fm-alpaca），4k数据用于测试（fm-bench）。

大模型能力对比
通过对五种形式化语言（Coq, Lean4, Dafny, ACSL, TLA+）在形式化证明写作上的六种细分能力进行对比，研究团队获得了一些有趣的发现。例如，未经微调的通用指令大模型更擅长从代码生成形式化证明，而不擅长从自然语言生成形式化证明。此外，较大规模的模型在某些任务中的表现反而不如小规模模型。

微调带来的能力提升
研究团队在3个7～8B的基础模型上用fm-alpaca（14k数据）进行了微调，结果表明，微调后的模型在各类形式化任务上均有显著提升，性能几乎翻倍。混合微调进一步提升了模型性能，从21.79%（仅用fm-alpaca微调）提升至25.16%（fm-alpaca + tulu）。

能力迁移探究
研究团队还探索了形式化数据微调对大模型数学、推理和编程等任务的「迁移能力」。实验结果显示，微调后模型在这些任务上的平均性能提升了1.37%至5.15%，这为未来探索模型的「元能力」提供了启发。

总结
研究团队构建了包含18000对高质量指令-响应对的微调数据集（fm-alpaca）与评估集（fm-bench），覆盖五种主流形式化语言和六种不同形式化推理与验证任务。通过微调，7～8B的小模型在生成形式化证明的能力上得到显著提升，性能提高了近三倍，在评估任务上媲美671B满血版DeepSeek-R1。完整的执行上下文和自动验证流程也将开源，有助于降低形式化验证的门槛，减少人力消耗及部署成本。

本文来源： 机器之心【阅读原文】