Re:Form -- Reducing Human Priors in Scalable Formal Software
  Verification with RL in LLMs: A Preliminary Study on Dafny
Authors: name: Chuanhao Yan, name: Fengdi Che, name: Xuhan Huang, name: Xu Xu, name: Xin Li, name: Yizhi Li, name: Xingwei Qu, name: Jingzhe Shi, name: Zhuangzhuang He, name: Chenghua Lin, name: Yaodong Yang, name: Binhang Yuan, name: Hang Zhao, name: Yu Qiao, name: Bowen Zhou, name: Jie Fu

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.