Re:Form -- 在LLMs中使用强化学习减少人类先验知识的可扩展形式化软件验证：关于Dafny的初步研究

现有的基于非正式语言（如人类语言）的大型语言模型（LLMs）在使用强化学习（RL）进行训练时面临一个重大挑战：其验证过程所提供的关键训练信号既不可靠，也不具备可扩展性。事实上，目前主流的大规模专有模型几乎无法生成可验证的程序。一种有前景但尚未被充分探索的替代方法是基于形式语言的推理。将LLMs建立在严格的正式系统之上，使生成模型在形式语言空间中运行（例如Dafny），可以实现对其推理过程和结果的自动验证和数学可证明性。这一能力对于实现大规模、可靠的正式软件验证至关重要。通常的做法是利用人工标注的思维链（chain-of-thought）和其他人类先验知识，以引导LLMs的推理和编程能力。然而，为监督复杂的编程任务提供这些先验知识变得不切实际且耗费大量资源。在本研究中，我们系统地探索了如何通过以形式语言Dafny作为主要实验环境，来减少对人类先验知识的依赖。我们的方法主要依赖于引入一个自动且可扩展的数据整理（data curation）流程，并结合形式语言验证器的反馈进行细致的强化学习设计。我们提出了DafnyComp，这是一个包含自动生成形式化规范的组合式形式程序基准，用于规范推理任务。在监督微调（SFT）阶段，即使是小型模型（例如0.5B参数量）也能生成语法正确且可验证的Dafny代码，其表现超越了现有的专有模型。通过正则化强化学习（RL with regularization）进一步优化性能，模型在跨领域任务中表现出更强的泛化能力，并在具有挑战性的DafnyComp基准测试中优于所有强基线模型。