Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny
作者: Chuanhao Yan, Fengdi Che, Xuhan Huang, Xu Xu, Xin Li, Yizhi Li, Xingwei Qu, Jingzhe Shi, Chenghua Lin, Yaodong Yang, Binhang Yuan, Hang Zhao, Yu Qiao, Bowen Zhou, Jie Fu
分类: cs.CL
发布日期: 2025-07-22 (更新: 2025-10-11)
💡 一句话要点
Re:Form：通过形式化验证反馈和强化学习，减少LLM软件验证对人工先验的依赖
🎯 匹配领域: 支柱二：RL算法与架构 (RL & Architecture) 支柱九：具身大模型 (Embodied Foundation Models)
关键词: 形式化验证 强化学习 大型语言模型 软件验证 Dafny 自动推理 程序合成
📋 核心要点
- 现有LLM软件验证依赖人工标注数据，成本高昂且难以扩展到复杂任务。
- 提出Re:Form框架，利用Dafny形式化验证器的反馈，通过强化学习减少对人工先验的依赖。
- 实验表明，Re:Form框架能使小型模型超越商业模型，并在DafnyComp基准测试中取得领先。
📝 摘要（中文）
现有基于非形式化语言（如自然语言）的大型语言模型（LLM）在强化学习训练中面临挑战：验证过程既不可靠也不可扩展。事实上，主流的商业模型难以生成可验证的程序。一个有前景但未被充分探索的替代方案是基于形式化语言的推理。将LLM置于严格的形式系统中，使其在形式语言空间（如Dafny）中运行，能够自动且数学上可证明地验证其推理过程和结果。这对于实现大规模、可靠的形式化软件验证至关重要。通常的做法是采用人工标注的思维链和其他人工先验来诱导LLM的推理和编码能力。然而，为复杂的编程任务提供此类先验的监督变得难以接受。本文系统地探索了减少人工先验的方法，以Dafny作为主要环境进行初步研究。我们的流程主要依赖于引入自动且可扩展的数据管理流程，以及与形式语言验证器反馈集成的精心设计的强化学习。我们引入了DafnyComp，这是一个包含自动形式化规范的组合形式程序的基准，用于规范推理。我们的监督微调（SFT）阶段使小型模型（如0.5B）能够生成语法有效且可验证的Dafny代码，超越了商业模型。带有正则化的强化学习进一步提高了性能，实现了对领域外任务的更强泛化，并在具有挑战性的DafnyComp基准上优于所有强大的基线。
🔬 方法详解
问题定义：现有基于LLM的软件验证方法依赖于大量人工标注的思维链数据，以引导模型进行推理和代码生成。这种方法不仅成本高昂，而且难以扩展到更复杂的编程任务中。此外，非形式化语言的验证过程不可靠，难以保证生成代码的正确性。
核心思路：本文的核心思路是利用形式化语言Dafny的验证器作为反馈信号，通过强化学习训练LLM，从而减少对人工先验的依赖。Dafny的验证器可以自动且数学上可证明地验证代码的正确性，为LLM提供可靠的训练信号。通过强化学习，LLM可以学习如何生成满足规范且可验证的Dafny代码。
技术框架：Re:Form框架包含以下主要阶段：1) 数据管理：构建DafnyComp基准测试，包含自动形式化规范的组合形式程序。2) 监督微调（SFT）：使用DafnyComp数据对LLM进行微调，使其能够生成语法有效且可验证的Dafny代码。3) 强化学习（RL）：使用Dafny验证器的反馈信号，通过强化学习进一步优化LLM，提高其泛化能力和性能。
关键创新：最重要的技术创新点在于利用形式化验证器的反馈信号进行强化学习，从而减少对人工先验的依赖。与传统的基于人工标注数据的训练方法相比，Re:Form框架可以自动生成训练数据，并且可以保证训练数据的质量。此外，Re:Form框架还可以利用Dafny的验证器来评估LLM的性能，从而实现更有效的训练。
关键设计：在强化学习阶段，使用了正则化技术来提高模型的泛化能力。具体来说，使用了L1正则化来鼓励模型生成更简洁的代码。此外，还使用了reward shaping技术来加速模型的训练。DafnyComp基准测试包含多种类型的组合形式程序，涵盖了不同的编程范式和算法。
🖼️ 关键图片
📊 实验亮点
实验结果表明，Re:Form框架能够使小型模型（0.5B）生成语法有效且可验证的Dafny代码，超越了商业模型。在DafnyComp基准测试中，Re:Form框架优于所有强大的基线模型，实现了对领域外任务的更强泛化能力。具体性能提升数据未知，但结论是显著优于现有方法。
🎯 应用场景
该研究成果可应用于自动化软件验证、形式化方法教育、以及安全攸关系统的开发。通过减少对人工先验的依赖，可以降低软件验证的成本，提高验证效率，并促进形式化方法在工业界的广泛应用。未来，该方法有望扩展到其他形式化语言和更复杂的软件系统。
📄 摘要（原文）
Existing informal language-based (e.g., human language) Large Language Models (LLMs) trained with Reinforcement Learning (RL) face a significant challenge: their verification processes, which provide crucial training signals, are neither reliable nor scalable. In fact, the prevalent large proprietary models could hardly generate verifiable programs. A promising yet largely uncharted alternative is formal language-based reasoning. Grounding LLMs in rigorous formal systems where generative models operate in formal language spaces (e.g., Dafny) enables the automatic and mathematically provable verification of their reasoning processes and outcomes. This capability is pivotal for achieving large-scale, reliable formal software verification. It is a common practice to employ human-annotated chain-of-thought and other human priors to induce the reasoning and coding capabilities of LLMs. Unfortunately, it becomes unacceptably all-consuming to provide such priors for supervising complex programming tasks. In this work, we systematically explore ways to reduce human priors with the formal language, Dafny, as the main environment for our pilot study. Our pipeline mainly relies on introducing an automatic and scalable data curation pipeline, and careful RL designs integrated with feedback from the formal language verifier. We introduce DafnyComp, a benchmark of compositional formal programs with auto-formalized specifications for specification reasoning. Our supervised fine-tuning (SFT) stage enables even small models (e.g., 0.5B) to generate syntactically valid and verifiable Dafny code, surpassing proprietary models. RL with regularization further improves performance, achieving stronger generalization to out-of-domain tasks and outperforming all strong baselines on the challenging DafnyComp benchmark.