Re:Form -- Het verminderen van menselijke aannames in schaalbare formele softwareverificatie met RL in LLMs: Een voorlopige studie over Dafny

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

July 22, 2025

Auteurs: Chuanhao Yan, Fengdi Che, Xuhan Huang, Xu Xu, Xin Li, Yizhi Li, Xingwei Qu, Jingzhe Shi, Zhuangzhuang He, Chenghua Lin, Yaodong Yang, Binhang Yuan, Hang Zhao, Yu Qiao, Bowen Zhou, Jie Fu

cs.AI

Samenvatting

Bestaande informele taalgebaseerde (bijv. menselijke taal) Large Language Models (LLM's) die getraind zijn met Reinforcement Learning (RL) staan voor een aanzienlijke uitdaging: hun verificatieprocessen, die cruciale trainingssignalen leveren, zijn noch betrouwbaar noch schaalbaar. In feite kunnen de heersende grote propriëtaire modellen nauwelijks verifieerbare programma's genereren. Een veelbelovend maar grotendeels onontgonnen alternatief is formeel taalgebaseerd redeneren. Door LLM's te verankeren in rigoureuze formele systemen waar generatieve modellen opereren in formele taalruimtes (bijv. Dafny), wordt het mogelijk om hun redeneerprocessen en uitkomsten automatisch en wiskundig bewijsbaar te verifiëren. Deze mogelijkheid is cruciaal voor het bereiken van grootschalige, betrouwbare formele softwareverificatie. Het is een gangbare praktijk om door mensen geannoteerde chain-of-thought en andere menselijke voorkennis te gebruiken om de redeneer- en codeervaardigheden van LLM's te stimuleren. Helaas wordt het onacceptabel tijdrovend om dergelijke voorkennis te leveren voor het begeleiden van complexe programmeertaken. In dit werk verkennen we systematisch manieren om menselijke voorkennis te verminderen met de formele taal Dafny als de belangrijkste omgeving voor onze pilotstudie. Onze pijplijn bericht voornamelijk op het introduceren van een automatische en schaalbare datacuratiepijplijn, en zorgvuldige RL-ontwerpen geïntegreerd met feedback van de formele taalverifier. We introduceren DafnyComp, een benchmark van compositionele formele programma's met geautomatiseerde formele specificaties voor specificatieredenering. Onze supervised fine-tuning (SFT) fase stelt zelfs kleine modellen (bijv. 0,5B) in staat om syntactisch geldige en verifieerbare Dafny-code te genereren, wat propriëtaire modellen overtreft. RL met regularisatie verbetert de prestaties verder, wat resulteert in een sterkere generalisatie naar taken buiten het domein en alle sterke baselines overtreft op de uitdagende DafnyComp-benchmark.

English

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.