Re:Form——利用大语言模型中的强化学习减少可扩展形式化软件验证中的人工标注：关于Dafny的初步研究
Re:Form -- Reducing Human Annotations in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny
AI总结：
研究利用形式语言Dafny减少人工标注，核心方法是引入自动可扩展数据处理流程及结合形式语言验证器反馈的强化学习设计，主要贡献是提升模型在DafnyComp基准测试表现。
摘要：
现基于非正式语言（如人类语言）经强化学习训练的大语言模型面临挑战，其验证过程不可靠且不可扩展。基于形式语言的推理是有前景的替代方案。本文以Dafny为主要环境探索减少人工标注的方法，介绍DafnyComp基准测试，通过监督微调及带正则化的强化学习提升模型性能。
英文摘要：
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 answers 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 annotations 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
