7B级形式化推理与验证小模型，媲美满血版DeepSeek-R1，全面开源！

AIGC动态1天前发布 almosthuman2014

113 0 0

文章摘要

随着大模型在形式化证明写作中的需求日益增长，形式化推理与验证（formal reasoning and verification）逐渐成为研究的焦点。然而，现有的形式化推理大模型大多局限于单一形式化语言，缺乏对多形式化语言和多任务场景的深入探索。近期，由香港科技大学牵头，联合中科院软件所、西安电子科技大学、重庆大学等单位，开源了一系列形式化推理与验证大模型。这些模型仅用7B参数，便在相关任务上达到了与671B满血版DeepSeek-R1相当的水平，标志着多语言形式化验证模型成为业界发展的趋势。

形式化验证不仅是计算机科学的核心问题，也是形式化数学最直接的应用之一。尽管其重要性不言而喻，但由于门槛高、人力消耗大和部署成本高，形式化验证的普及与推广一直受到限制。大模型在语义理解和代码自动生成等方面的优势，为加速验证流程、降低人力成本提供了新的可能性。研究团队首先对形式化验证任务进行了分层拆解，从非形式化的自然语言输入到可验证的形式化证明或可检测的模型。这一过程被细化为六个子任务，包括验证需求分解、形式化规约片段生成、规约补全、填空，以及代码到形式化规约的自动生成。

研究团队从Github收集了五种形式化语言的数据，经过清洗与整理，最终得到了14k数据用于训练微调（fm-alpaca），4k数据用于测试（fm-bench）。通过对五种形式化语言（Coq, Lean4, Dafny, ACSL, TLA+）在形式化证明写作上六种细分能力的对比，研究团队发现，未经微调的通用指令大模型更擅长从代码生成形式化证明（准确率43.57%），而不擅长从自然语言生成形式化证明（8.65%～10.61%）。此外，较大规模的模型在形式化规约填空任务中表现不佳，70B的llama3.1-instruct模型在填空任务上的准确率仅为8B模型的一半，这可能与这些模型的微调策略有关。

从形式化语言的角度看，大模型在ACSL上的效果最好（34.92%），Dafny次之（15.92%）。研究团队认为，ACSL语言的关键词更贴近自然语言，其语法结构类似于C语言，使得生成过程更为顺畅。此外，仅通过增加生成次数（从1次提升至5次），即可在不用微调的情况下，得到10.82%～63.64%的提升。结合上下文学习（in-context learning），可以进一步将准确率翻番（51.33%～532.83%）。

研究团队在3个7～8B的基础模型（LLaMA-3.1，Qwen-2.5，Deepseek-coder-v1.5）上用fm-alpaca（14k数据）进行微调，结果显示，经过形式化数据微调后，大模型在各类形式化任务上均有明显提升，性能几乎翻倍。值得注意的是，这种显著提升仅用了14k条形式化相关的指令数据。当把形式化数据和对话型指令数据混合微调时，能进一步提升模型性能，从21.79%（仅用fm-alpaca微调）提升至23.75%（fm-alpaca + ultrachat）和25.16%（fm-alpaca + tulu）。

研究团队还探索了形式化数据微调对大模型在数学、推理和编程等任务上的「迁移能力」。实验结果表明，利用形式化数据（FM-Alpaca）进行微调后，模型在数学、推理、代码任务上的平均性能提升达到了1.37%至5.15%。这一发现为未来探索模型的「元能力」和「能力迁移」提供了启发。

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