Re:Form——在基于LLM的可扩展形式化软件验证中减少人类先验：基于Dafny的初步研究
计算与语言
2025-10-14 v3
摘要
现有的基于非形式化语言（如人类语言）并通过强化学习（RL）训练的大语言模型面临一个重大挑战：其提供关键训练信号的验证过程既不可靠也不可扩展。事实上，主流的大型专有模型几乎无法生成可验证的程序。一个有前景但很大程度上未被探索的替代方案是基于形式化语言的推理。将LLM植根于严格的形式化系统中，使生成模型在形式化语言空间（如Dafny）中运行，能够实现对其推理过程和结果的自动且数学上可证明的验证。这一能力对于实现大规模、可靠的形式化软件验证至关重要。采用人工标注的思维链和其他人类先验来诱导LLM的推理和编码能力是一种常见做法。遗憾的是，为监督复杂编程任务提供此类先验变得令人难以接受地耗费资源。在这项工作中，我们系统地探索了减少人类先验的方法，以形式化语言Dafny作为我们初步研究的主要环境。我们的流水线主要依赖于引入自动且可扩展的数据整理流水线，以及结合形式化语言验证器反馈的精心RL设计。我们引入了DafnyComp，一个具有自动形式化规约的组合式形式化程序基准，用于规约推理。我们的监督微调（SFT）阶段使即使是小模型（如0.5B）也能生成语法有效且可验证的Dafny代码，超越了专有模型。带正则化的RL进一步提升了性能，对域外任务实现了更强的泛化，并在具有挑战性的DafnyComp基准上优于所有强基线。
引用
@article{arxiv.2507.16331,
title = {Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny},
author = {Chuanhao Yan and Fengdi Che and Xuhan Huang and Xu Xu and Xin Li and Yizhi Li and Xingwei Qu and Jingzhe Shi and Chenghua Lin and Yaodong Yang and Binhang Yuan and Hang Zhao and Yu Qiao and Bowen Zhou and Jie Fu},
journal= {arXiv preprint arXiv:2507.16331},
year = {2025}
}