重塑：借助大语言模型中的强化学习来降低可扩展形式化软件验证中的人为先验——一项关于Dafny的初步研究

现有基于非正式语言（例如，人类语言）并通过强化学习（RL）训练的大型语言模型（LLMs）面临一个重大挑战：它们提供关键训练信号的验证过程既不可靠也无法扩展。事实上，普遍存在的专有大型模型几乎无法生成可验证的程序。一种有前景但仍在很大程度上未经探索的替代方案是基于形式语言的推理。将LLMs置于严格的形式系统中，其中生成模型在形式语言空间（例如Dafny）中运行，能够实现对其推理过程和结果的自动化且数学上可证明的验证。这种能力对于实现大规模、可靠的形式化软件验证至关重要。通常，人们会采用人工标注的思维链和其他人类先验知识来激发LLMs的推理和编码能力。不幸的是，为监督复杂的编程任务提供此类先验知识会变得耗时耗力，令人难以接受。在这项工作中，我们系统地探索了利用形式语言Dafny作为我们初步研究的主要环境来减少人类先验知识的方法。我们的流程主要依赖于引入自动化且可扩展的数据整理流程，以及结合了形式语言验证器反馈的精心设计的强化学习方法。我们引入了DafnyComp，这是一个包含组合式形式程序并带有自动形式化规范的基准，用于规范推理。我们的有监督微调（SFT）阶段使即使是小型模型（例如0.5B）也能生成语法有效且可验证的Dafny代码，超越了专有模型。带正则化的强化学习进一步提高了性能，实现了对域外任务的更强泛化能力，并在具有挑战性的DafnyComp基准上超越了所有强大的基线模型。