Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny

TL;DR

The paper tackles the challenge of verifying large language models when generating code by grounding reasoning in a formal language, Dafny, and pursuing a minimal-human-prior reinforcement learning pipeline. It introduces a scalable data-curation and benchmarking workflow (DafnyComp) and demonstrates that SFT followed by verifier-driven RL with subset-based rewards substantially improves both syntax- and semantics-level correctness, including strong out-of-domain generalization up to 14B parameter models. Key findings show RL yields novel, semantically meaningful specifications that exceed ground-truth constraints, while careful reward design (subset reward) and regularization (KL+entropy) mitigate reward-hacking and mode collapse. The work argues that reducing human priors, leveraging automated formal verification feedback, and distributing learning across smaller models can outperform large proprietary models on formal-programming tasks, with potential implications for scalable, reliable formal software verification. Overall, the approach advances scalable, verifiable AI programming by combining automatic data generation, formal reasoning, and RL-driven exploration, while acknowledging limitations and avenues for future work in more complex reasoning domains and data integrity.

Abstract

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.

Figures (25)

• Figure 1.1: Model Performance on DafnyComp benchmark. We roughly categorize the cases into four groups in an ascending quality order: Syntax Error, Syntax Correct, Verified and Verified with Superior Specification. The growing proportion of Verified with Superior Specification suggests a rudimentary of exploration capabitliy to generate stronger specifcation than the ground-truth of the models incentivized by reinforcement learning. For further model behavioural analysis, a more refined set of definition of benchmarking metrics is provided in §\ref{['sec:exp_setup']} as standard protocol.
• Figure 1.2: The Illustration of Re:Form Pipeline. Human prior is extensively removed across different components of the pipeline. Heuristic cleansing rules and model-based conversion are introduced in the data construction and benchmark annoation for scaling along with compute investment. The task is formalized as a simple and flexible specification generation, providing the model a vast landscape of self-exploration under the reinforcement learning paradigm.
• Figure 2.1: Statistics of the Dataset.
• Figure 3.1: The figure presents an example of comments generated during RL learning, which is not extended reasoning and is inserted after the complete Dafny code.
• Figure 3.2: The figure shows the comparison between GPT-4o, our Qwen base models, SFT models and RL-trained models scaling over model size on our in-domain evaluation set. The pass@1 improvement of SFT and subsequent RL over our base models is substantial.