Training Smaller LLMs to Generate Verified Code With Less Human Input

Researchers have found a way to cut down on manual labeling when training language models to generate formally verified code, using reinforcement learning and formal languages like Dafny. The approach enables even compact models—with just 500 million parameters—to produce code that exceeds the capabilities of larger proprietary systems.

The Core Challenge#

Training large language models (LLMs) on complex coding tasks typically requires extensive human-created examples and chain-of-thought annotations to guide learning. This labeling workload becomes prohibitive at scale, especially for specialized domains like formal software verification. Traditional LLM approaches rely on informal natural language reasoning, which is difficult to verify automatically and often fails to produce code that actually compiles or runs correctly.

A Formal Language Alternative#

The new framework pivots toward formal languages—specifically Dafny—where code and its correctness properties exist in a mathematically rigorous system. This shift matters because a formal verifier can automatically check whether generated code is correct, providing a scalable, automatic training signal without human annotators. Rather than trusting the model's informal reasoning, the system grounds verification in mathematical proof.

Key Method and Results#

The researchers introduced DafnyComp, a benchmark of compositional formal programs with auto-generated specifications. Their pipeline combines:

• An automatic data curation stage to generate training material with minimal manual input
• Supervised fine-tuning (SFT) to teach models syntactically valid Dafny code
• Reinforcement learning with regularization, using feedback from the formal verifier to improve reasoning and generalization

Results showed that even small 0.5B-parameter models surpassed large closed-source systems at generating valid, verifiable Dafny code. The RL stage boosted performance further and improved transfer to out-of-domain tasks, with the approach outperforming established baselines on the DafnyComp benchmark.

Why It Matters#

This work signals a path toward scalable formal verification without drowning annotation teams in labels. By grounding LLMs in formal systems where correctness is automatically verifiable, the approach opens the door to training reliable, verifiable code generators across multiple domains and model sizes.